[Prev][Next][Index][Thread]
Hilbert systems vs. Gentzen systems
[------- The Types Forum ------ http://www.cs.indiana.edu/types -------]
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 am aware of several tradeoffs (thanks to Randy Pollack for his
helpful comments, any misunderstandings are mine):
* The size of derivations or proof objects explodes using
the deduction theorem in Hilbert systems.
* Meta-properties, such as the deduction theorem, are commonly
brought into the object language. This is more serious since Curry's
abstraction doesn't satisfy the xi rule which allows equality
underneath abstraction.
* Models of Hilbert systems don't have to model the
meta-properties as rules of inference, leading to a more permissive
notion of model.
* The introduction / elimination duality in Gentzen systems
doesn't appear in Hilbert 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.
Yours,
Healf GOGUEN
Follow-Ups: