Resent-From: alti@dcs.ed.ac.uk Resent-Message-Id: <199611291506.QAA24261@lionsden.informatik.uni-muenchen.de> Resent-Date: Fri, 29 Nov 1996 14:58:01 +0000 Resent-To: alti@informatik.uni-muenchen.de From: Healfdene Goguen To: types@cs.indiana.edu Subject: Hilbert systems vs. Gentzen systems Date: Thu, 28 Nov 1996 17:55:31 +0000 [------- 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 --------------------------------------------------------------------------- From: Thorsten Altenkirch To: Healfdene Goguen Cc: types@cs.indiana.edu Subject: Hilbert systems vs. Gentzen systems Date: Mon, 2 Dec 1996 13:35:58 +0100 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 --------------------------------------------------------------------------- Resent-From: alti@dcs.ed.ac.uk Resent-Message-Id: <199612030722.IAA14729@lionsden.informatik.uni-muenchen.de> Resent-Date: Tue, 3 Dec 1996 07:21:41 +0000 Resent-To: alti@informatik.uni-muenchen.de From: selinger@math.upenn.edu (Peter Selinger) To: types@cs.indiana.edu Subject: Re: Hilbert systems vs. Gentzen systems Date: Mon, 2 Dec 1996 20:08:26 -0500 (EST) [------- The Types Forum ------ http://www.cs.indiana.edu/types -------] > From Healfdene Goguen: > * 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. > From Thorsten Altenkirch: > > 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. There is a point to be considered here that is often overlooked. In a certain, strong, sense, the lambda calculus actually *is* algebraic. The failure of the above properties (Curry's abstraction does not satisfy the xi-rule; lambda calculus models are not closed under submodels) comes from the notion of model considered, and not from the lambda calculus itself. It is my impression that this has been known to a few people for a long time, but since this point is missing from some standard texts (including Hindley and Seldin's book and also Barendregt's book), it is still relatively obscure. What I mean is the following: Let A be a lambda algebra (i.e. a combinatorial algebra satisfying the additional 4 or 5 Curry axioms). There are two different styles of defining what it means for M=N to hold in A, where M,N are open (lambda or combinatory) terms: M=N holds 'locally' iff it holds for all substitutions of elements of A for the free variables, and it holds 'absolutely' iff it holds in A[x_1...x_n], i.e. in the lambda algebra obtained from A by freely adjoining indeterminates x_1...x_n (assuming the free variables of M and N are contained in this set). It should not be surprising that these interpretations are strictly different. All the rules of the lambda calculus, including the xi rule, are sound for the 'absolute' interpretation. (But not for the 'local' interpretation: here the non-equational class of "lambda models" is needed). As a consequence, the class of lambda algebras is not only sound and complete *for arbitrary lambda theories*, but the theories of lambda algebras and the lambda calculus become the same, in the sense that the categories of their respective theories are equivalent. This interpretation (for the beta-eta case) can be found in Lambek's paper "From lambda calculus to cartesian closed categories". In the typed case, this is also implicit in Lambek and Scott's book. I wrote an expository paper on these issues, called "The Lambda Calculus is Algebraic", which is available from my www page http://www.cis.upenn.edu/~selinger/papers.html -- Peter Selinger