Deutsche Gesellschaft
für phänomenologische Forschung

Zeitschrift | Band | Artikel

236915

Proof-theoretic semantics for classical mathematics

William W. Tait

pp. 603-622

Abstrakt

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.

Publication details

Published in:

(2006) Proof-theoretic semantics. Synthese 148 (3).

Seiten: 603-622

DOI: 10.1007/s11229-004-6271-x

Referenz:

Tait William W. (2006) „Proof-theoretic semantics for classical mathematics“. Synthese 148 (3), 603–622.