Proof-theoretic Semantics for Classical Mathematics |
| |
Authors: | William W Tait |
| |
Institution: | (1) Department of Philosophy, University of Chicago, 5522 S. Everett Ave., Chicago, IL, 60637, U.S.A. |
| |
Abstract: | 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. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|