system of simple types
, which uses the intuitionistic propositional calculus, with the only connective →. It is very important, because the well known Curry-Howard correspondence between proofs and programs was originally discovered with it, and because it enjoys the normalization property: every typed term is strongly normalizable. It was extended to second order intuitionistic logic, in 1970, by J.-Y. Girard [4], under the name of system F, still with the normalization property.
More recently, in 1990, the Curry-Howard correspondence was extended to classical logic, following Felleisen and Griffin [6] who discovered that the law of Peirce corresponds to control instructions in functional programming languages. It is interesting to notice that, as early as 1972, Clint and Hoare [1] had made an analogous remark for the law of excluded middle and controlled jump instructions in imperative languages.
There are now many type systems which are based on classical logic; among the best known are the system LC of J.-Y. Girard [5] and the λμ-calculus of M. Parigot [11]. We shall use below a system closely related to the latter, called the λ c -calculus [8, 9]. Both systems use classical second order logic and have the normalization property.
In the sequel, we shall extend the λ c -calculus to the Zermelo-Frænkel set theory. The main problem is due to the axiom of extensionality. To overcome this difficulty, we first give the axioms of ZF in a suitable (equivalent) form, which we call ZF ɛ .
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
Author information
Authors and Affiliations
Additional information
Received: 6 September 1999 / Published online: 25 January 2001
Rights and permissions
About this article
Cite this article
Krivine, JL. Typed lambda-calculus in classical Zermelo-Frænkel set theory. Arch. Math. Logic 40, 189–205 (2001). https://doi.org/10.1007/s001530000057
Issue Date:
DOI: https://doi.org/10.1007/s001530000057