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.

Toby, thanks! That made me start *modus ponens*.

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

Shouldn’t

$\vdash (\psi \to \phi)$have ’true’ after it?

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

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

]]>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

isprecisely…

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