Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeSep 20th 2012
   • (edited Sep 20th 2012)
   • PermaLink
   Author: Urs
   Format: MarkdownItexI felt that we had too many gray links to _[[metalanguage]]_, so I gave it a try. But I don't really have the leisure for it now and not the expertise anyway. Experts please feel invited to take apart what I wrote there and replace with it something better.

   I felt that we had too many gray links to metalanguage, so I gave it a try. But I don’t really have the leisure for it now and not the expertise anyway. Experts please feel invited to take apart what I wrote there and replace with it something better.

2. • CommentRowNumber2.
   • CommentAuthorUrs
   • CommentTimeSep 20th 2012
   • PermaLink
   Author: Urs
   Format: MarkdownItexI had originally wanted to add a remark along the lines: > If the formal language is implemented concretely as a programming language such as Coq or Agda, then the metalanguage _is_ precisely... and then I originally wanted to write > ... precisely that software/that program itself . But then I was getting unsure about how best to say it. It would be nice to add something like this, though.

   I had originally wanted to add a remark along the lines:

   If the formal language is implemented concretely as a programming language such as Coq or Agda, then the metalanguage is precisely…

   and then I originally wanted to write

   … precisely that software/that program itself .

   But then I was getting unsure about how best to say it.

   It would be nice to add something like this, though.

3. • CommentRowNumber3.
   • CommentAuthorUrs
   • CommentTimeJan 26th 2014
   • PermaLink
   Author: Urs
   Format: MarkdownItexI have added to that Idea-section at _[[metalanguage]]_ a sentence combining the two previous thoughts, saying that in the presence of a [[deduction theorem]] a [[sequent]]/[[entailment]] in the [[metalanguage]] may be turned into an [[implication]] in the object language. I think I know what I am doing, but logic professionals please check.

   I have added to that Idea-section at metalanguage a sentence combining the two previous thoughts, saying that in the presence of a deduction theorem a sequent/entailment in the metalanguage may be turned into an implication in the object language.

   I think I know what I am doing, but logic professionals please check.

4. • CommentRowNumber4.
   • CommentAuthorTobyBartels
   • CommentTimeJan 26th 2014
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexThat looks good. I remarked that modus ponens is the converse, and then made a pedantic parenthetical comment that could maybe be taken out again.

   That looks good. I remarked that modus ponens is the converse, and then made a pedantic parenthetical comment that could maybe be taken out again.

5. • CommentRowNumber5.
   • CommentAuthorDavid_Corfield
   • CommentTimeJan 26th 2014
   • PermaLink
   Author: David_Corfield
   Format: MarkdownItexShouldn't $$ \vdash (\psi \to \phi) $$ have 'true' after it?

   Shouldn’t

   $$\vdash (\psi \to \phi)$$

   have ’true’ after it?

6. • CommentRowNumber6.
   • CommentAuthorUrs
   • CommentTimeJan 26th 2014
   • PermaLink
   Author: Urs
   Format: MarkdownItexDavid, you are right, I have added the "true" but also added further above a parenthetical > (in [[type theory]] one might also omit the "$true$", see at [[propositions-as-types]] for details on this).

   David, you are right, I have added the “true” but also added further above a parenthetical

   (in type theory one might also omit the “$true$”, see at propositions-as-types for details on this).

7. • CommentRowNumber7.
   • CommentAuthorUrs
   • CommentTimeJan 26th 2014
   • PermaLink
   Author: Urs
   Format: MarkdownItexToby, thanks! That made me start _[[modus ponens]]_.

   Toby, thanks! That made me start modus ponens.

8. • CommentRowNumber8.
   • CommentAuthorTobyBartels
   • CommentTimeJan 27th 2014
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexOne might well omit the ‘true’ in non-type theory as well. Since $\phi$, $\psi$, $\psi \rightarrow \phi$, etc are not judgements, the sequent is meaningless as stated (without ‘true’), but in that case it\'s a fairly well-understood convention that the ‘true’ is simply being elided. In fact, it\'s probably most common to leave it out in pure propositional calculus (more so than in type theory or anything else), since in that case the *only* judgements that ever appear are judgements of truth.

   One might well omit the ‘true’ in non-type theory as well. Since $\phi$, $\psi$, $\psi \rightarrow \phi$, etc are not judgements, the sequent is meaningless as stated (without ‘true’), but in that case it's a fairly well-understood convention that the ‘true’ is simply being elided. In fact, it's probably most common to leave it out in pure propositional calculus (more so than in type theory or anything else), since in that case the only judgements that ever appear are judgements of truth.