[Prev][Next][Index][Thread]
Hilbert systems vs. Gentzen systems
[------- The Types Forum ------ http://www.cs.indiana.edu/types -------]
Healfdene Goguen writes:
> I am interested in opinions on the tradeoffs between two styles of
> presenting logic:
> * systems where the deduction theorem is a theorem, hereafter
> Hilbert systems, and
> * systems where the deduction theorem is internalized as a
> rule of inference, hereafter Gentzen systems.
>
> This distinction is lifted to type theory, with first class proof
> objects, through Curry's abstraction algorithm in the Hilbert systems
> and through Church's typed lambda calculus in the Gentzen systems.
...
> I would be interested in any opinions on these tradeoffs, further
> differences between the systems, or recent or historical references
> that discuss this question.
One important difference between combinatory logic (i.e. Hilbert
systems) and lambda calculus (here Gentzen systems) is that the first
is "algebraic", whereas the second is not. In particular the models of
combinatory logic are closed under submodels which is not the case for
lambda calculus. E.g. the closed terms of combinatory logic (the
"interior") form a combinatory algebra which is not the case for
lambda calculus (the closed terms are just a combinatory algebra).
This is discussed in Hindley's & Seldin's "Introduction to Combinators
and lambda calculus", pp. 107 for the untyped case but it is easy to
see that it applies to typed calculi as well.
--
Thorsten Altenkirch phone : (+49 89) 2178-2209
Theoretical Computer Science fax : (+49 89) 2178-2238
LMU, Munich, Germany Oettingenstr 67, D105
http://www.tcs.informatik.uni-muenchen.de/~alti
Follow-Ups:
References: