Variable-free formalization of the Curry-Howard theory


The reduction of the lambda calculus to the theory of combinators in [Sch¨ onfinkel, 1924] applies to positive implicational logic, i.e. to the typed lambda calculus, where the types are built up from atomic types by means of the operation A −→ B, to show that the lambda operator can be eliminated in favor of combinators K and S of each type A −→ (B −→ A) and (A −→ (B −→ C)) −→ ((A −→ B) −→ (A −→ C)), respectively.1 I will extend that result to the case in which the types are built up by means of the general function type ∀x : A.B(x) as well as the disjoint union type ∃x : A.B(x)– essentially to the theory of [Howard, 1980]. To extend the treatment of −→ to ∀ we shall need a generalized form of the combinators K and S, and to deal with ∃ we will need to introduce a new form of the combinator S..



    Upload a copy of this work     Papers currently archived: 92,150

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

  • Only published works are available at libraries.

Similar books and articles

The Curry-Howard isomorphism.Philippe De Groote (ed.) - 1995 - Louvain-la-Neuve: Academia.
The completeness of Heyting first-order logic.W. W. Tait - 2003 - Journal of Symbolic Logic 68 (3):751-763.
Syntactic calculus with dependent types.Aarne Ranta - 1998 - Journal of Logic, Language and Information 7 (4):413-431.
Lectures on the Curry-Howard isomorphism.Morten Heine Sørensen - 2007 - Boston: Elsevier. Edited by Paweł Urzyczyn.


Added to PP

38 (#421,143)

6 months
7 (#436,298)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

William W. Tait
University of Chicago

Citations of this work

Necessity of Thought.Cesare Cozzo - 2015 - In Heinrich Wansing (ed.), Dag Prawitz on Proofs and Meaning. Springer. pp. 101-20.
Godel's interpretation of intuitionism.William Tait - 2006 - Philosophia Mathematica 14 (2):208-228.
Dag Prawitz on Proofs and Meaning.Heinrich Wansing (ed.) - 2014 - Cham, Switzerland: Springer.

Add more citations

References found in this work

No references found.

Add more references