Re: Layout syntax (Hans Aberg)
22 Jan 2004 23:10:28 -0500

          From comp.compilers

Related articles
[10 earlier articles]
Re: Layout syntax (Joachim Durchholz) (2004-01-07)
Re: Layout syntax (2004-01-09)
Re: Layout syntax (Joachim Durchholz) (2004-01-12)
Re: Layout syntax (2004-01-16)
Re: Layout syntax (Joachim Durchholz) (2004-01-18)
Re: Layout syntax (Ian Zimmerman) (2004-01-18)
Re: Layout syntax (2004-01-22)
Re: Layout syntax (2004-01-22)
Re: Layout syntax (Ian Zimmerman) (2004-02-01)
Re: Layout syntax (2004-02-04)
| List of all articles for this month |

From: (Hans Aberg)
Newsgroups: comp.compilers
Date: 22 Jan 2004 23:10:28 -0500
Organization: Mathematics
References: 03-12-016 03-12-136 04-01-014 04-01-021 04-01-034 04-01-056 04-01-083 04-01-120
Keywords: theory
Posted-Date: 22 Jan 2004 23:10:28 EST

Ian Zimmerman <> 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

>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

Post a followup to this message

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