Re: Layout syntax

Ian Zimmerman <bayard@newsguy.com> wrote:


>Hans> Computer scientists can get around this, it seems, by making
>Hans> use of Gentzen sequents. But these cannot capture the full
>Hans> generality of the Hilbert metamathematics.
>
>I'll bite - wth do you mean by this? Natural deduction (with Excluded
>Middle in, of course) is a completely equivalent, if radically
>different, formulation of the predicate calculus; I don't know of any
>reason why all of standard metamathematics, e.g. Goedel's
>Incompleteness proof, could not be formulated in it.


The Gentzen logic system G1 (or G2) is more special than the Hilbert logic
system H. The theorem is (see S.C. Kleene, "Introduction to
Metamathematics", Ch. XV, paragraph 77, p. 445, Theorem 46):
    Theorem. If Gamma |-_H E with the variables held constant in the proof, then
    |-_G1 Gamma -> E.
where "->" is the Gentzen sequent. A free variable of Gamma is said to be
varied (p.95, loc. cit.) if a formula in the deduction a formula that
depends on it binds it; otherwise, it is said to be held constant.


Thus, the Gentzen system using "->" automatically ensures that in the
proofs, variables are held constant. One thus do not get all proofs
possible in the Hilbert system.


When I look into the usage in the computer world, it indeed looks
confusing, because one treats "->" as though it was the same as "=>",
which also can be hard to distinguish from the provability "|-".


I am not sure exactly what this means in terms of working math; I just
found it surer to stick to the Hilbert system for generality. With
unification branching in place, it seems that I do not need the Gentzen
sequents.


>Are we talking about the same things? I cannot be sure because of the
>somewhat vague style of your posts.


I hope this clarifies. You can give it another go and ask again, if
you so want.


    Hans Aberg

Return to the comp.compilers page.
Search the comp.compilers archives again.