Re: Layout syntax

haberg@matematik.su.se (Hans Aberg)
4 Feb 2004 21:42:12 -0500

          From comp.compilers
Related articles
[13 earlier articles]
Re: Layout syntax haberg@matematik.su.se (2004-01-16)
Re: Layout syntax joachim.durchholz@web.de (Joachim Durchholz) (2004-01-18)
Re: Layout syntax bayard@newsguy.com (Ian Zimmerman) (2004-01-18)
Re: Layout syntax haberg@matematik.su.se (2004-01-22)
Re: Layout syntax haberg@matematik.su.se (2004-01-22)
Re: Layout syntax bayard@newsguy.com (Ian Zimmerman) (2004-02-01)
Re: Layout syntax haberg@matematik.su.se (2004-02-04)
| List of all articles for this month |
From: haberg@matematik.su.se (Hans Aberg)
Newsgroups: comp.compilers
Date: 4 Feb 2004 21:42:12 -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 04-01-126 04-02-011
Keywords: theory
Posted-Date: 04 Feb 2004 21:42:12 EST

Ian Zimmerman <bayard@newsguy.com> wrote:


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


>But the same theorems.


Why? (If you can prove your statement, then you can also prove the
Deduction Theorem without the condition that the variables are held
constant in the proof.)


    Hans Aberg

Post a followup to this message

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