Re: Layout syntax

Ian Zimmerman <bayard@newsguy.com>
1 Feb 2004 12:35:31 -0500

          From comp.compilers
Related articles
[12 earlier articles]
Re: Layout syntax joachim.durchholz@web.de (Joachim Durchholz) (2004-01-12)
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: Ian Zimmerman <bayard@newsguy.com>
Newsgroups: comp.compilers
Date: 1 Feb 2004 12:35:31 -0500
Organization: Compilers Central
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
Keywords: theory, syntax
Posted-Date: 01 Feb 2004 12:35:31 EST

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.


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


I think if there is a confusion (and I don't feel that way, having
background in both areas) it is because the formula connective
(your => ?) is quite redundant in a sequent style calculus; it is
more natural (even in pratical terms) to think of formulas only
comprising \/ , /\ and ~, and of implication as a relation between
formula sets.


--
Nothing can be explained to a stone.
Or to a stoned person, either.

Post a followup to this message

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