Not signed in (Sign In)

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.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • 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 “truetrue”, 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.