Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
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.
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.
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.
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.
Shouldn’t
$(\mathcal{X}_i, \mathcal{O}_{\mathcal{X_ \vdash (\psi \to \phi)$have ’true’ after it?
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).
Toby, thanks! That made me start modus ponens.
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.
1 to 8 of 8