22 Jan 2004 23:10:28 -0500

Related articles |
---|

[10 earlier articles] |

Re: Layout syntax joachim.durchholz@web.de (Joachim Durchholz) (2004-01-07) |

Re: Layout syntax haberg@matematik.su.se (2004-01-09) |

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) |

From: | haberg@matematik.su.se (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 <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

Post a followup to this message

Return to the
comp.compilers page.

Search the
comp.compilers archives again.