Proof-theoretic semantics for classical mathematics (Q2500813)

This article originated from the 1999 conference on `proof-theoretic semantics', and in it the author extends Curry-Howard's `formulae-as-types' notion from constructive mathematics to classical, thus showing, according to the author, that it ``does not need to be founded on an inchoate picture of truth-functional semantics in the big-model-in-the-sky, a picture that can in any case never be coherently realized.'' In this paper, the author discusses only the elementary theory of types and objects, and does not touch upon numbers or arithmetic. After setting up formalism, including type-base and object-forming operations, the author shows how to get rid of variables from \(\lambda\)-abstraction and quantification by means of combinators. He defines extensional equality for each type. Also, the principle of the excluded middle is shown to be not about truth values but about the introduction of ideal elements, and its connection to the comprehension principle is exhibited.