Logic in Computer Science (LICS 2000)

Invited Talk: The Curry-Howard Correspondence in Set Theory (at LICS 2000)

Authors: Jean-Louis Krivine

Abstract

This talk presents a system of typed lambda-calculus for the Zermelo-Fränkel set theory, in the framework of classical logic [10]. The Curry-Howard correspondence between proofs and programs was originally discovered with the system of simple types, which uses the intuitionistic propositional calculus, with the only connective. It was extended to second order intuitionistic logic, in 1970, by J.-Y. Girard [4], under the name of system F for which he proved the normalization property .The relation with programming languages was made by Reynolds [13].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 [12]. We use 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 order to extend the Curry -Howard correspondence to classical Zermelo-Fränkel set theory, we give realizability models, which are built recursively like in the well-known construction of forcing. We show that each axiom of ZF is then realized; we obtain in this way a type s stem in which set-theoretic proofs are formalizable and give rise to programs, which are ë -terms with control instructions. In this system, the normalization property is “essentially true” in the sense that we get correct computations on data types. Of course, not every typable term is normalizable since, for example, Y has the type of the foundation axiom. These realizability models differ deeply from forcing models and pose several interesting problems. In particular, they do not seem to be end extensions of the original model of ZFC. In addition, it is likely that the negation of the axiom of choice is realized in them.

BibTeX

  @InProceedings{Krivine-TheCurryHowardCorre,
    author = 	 {Jean-Louis Krivine},
    title = 	 {The Curry-Howard Correspondence in Set Theory},
    booktitle =  {Proceedings of the Fifteenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 2000},
    year =	 2000,
    editor =	 {Martin Abadi},
    month =	 {June}, 
    pages =      {307--308},
    location =   {Santa Barbara, CA, USA}, 
    note =       {Invited Talk},
    publisher =	 {IEEE Computer Society Press}
  }