Proof-theoretic Semantics for Classical Mathematics

Synthese 148 (3):603-622 (2006)
  Copy   BIBTEX


We discuss the semantical categories of base and object implicit in the Curry-Howard theory of types and we derive derive logic and, in particular, the comprehension principle in the classical version of the theory. Two results that apply to both the classical and the constructive theory are discussed. First, compositional semantics for the theory does not demand ‘incomplete objects’ in the sense of Frege: bound variables are in principle eliminable. Secondly, the relation of extensional equality for each type is definable in the Curry-Howard theory.



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

External links

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

Through your library

Similar books and articles

Some problems for proof-theoretic semantics.William R. Stirton - 2008 - Philosophical Quarterly 58 (231):278–298.
Harmony in Multiple-Conclusion Natural-Deduction.Nissim Francez - 2014 - Logica Universalis 8 (2):215-259.
Bilateralism in Proof-Theoretic Semantics.Nissim Francez - 2013 - Journal of Philosophical Logic (2-3):1-21.


Added to PP

109 (#162,173)

6 months
15 (#167,403)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

William W. Tait
University of Chicago

References found in this work

Mathematical logic.Willard Van Orman Quine - 1951 - Cambridge,: Harvard University Press.
Combinatory logic.Haskell Brooks Curry - 1958 - Amsterdam,: North-Holland Pub. Co..
Variables Explained Away.Willard V. Quine - 1960 - Journal of Symbolic Logic 32 (1):112-112.
The formulæ-as-types notion of construction.W. A. Howard - 1995 - In Philippe De Groote (ed.), The Curry-Howard isomorphism. Louvain-la-Neuve: Academia.
Combinatory Logic Vol. 1.Haskell Brooks Curry & Robert M. Feys - 1958 - Amsterdam, Netherlands: North-Holland Publishing Company.

View all 10 references / Add more references