Not signed in (Sign In)

# Start a new discussion

## Not signed in

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

• Sign in using OpenID

## Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

• CommentRowNumber1.
• CommentAuthorUrs
• CommentTimeSep 20th 2012
• (edited Sep 20th 2012)

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.

• CommentRowNumber2.
• CommentAuthorUrs
• CommentTimeSep 20th 2012

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.

• CommentRowNumber3.
• CommentAuthorUrs
• CommentTimeJan 26th 2014

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.

• CommentRowNumber4.
• CommentAuthorTobyBartels
• CommentTimeJan 26th 2014

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.

• CommentRowNumber5.
• CommentAuthorDavid_Corfield
• CommentTimeJan 26th 2014

Shouldn’t

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

have ’true’ after it?

• CommentRowNumber6.
• CommentAuthorUrs
• CommentTimeJan 26th 2014

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).

• CommentRowNumber7.
• CommentAuthorUrs
• CommentTimeJan 26th 2014

Toby, thanks! That made me start modus ponens.

• CommentRowNumber8.
• CommentAuthorTobyBartels
• CommentTimeJan 27th 2014

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.

Add your comments
• Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
• To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

• (Help)