unofficial copies [PDF], [PS]

by Robert L. Constable

Constructive Methods of Computing Science (NATO ASI Series), M. Broy (ed.), vol. F55, pp. 63-91, 1989.

**Abstract**

According to Tarski's semantics, the denotation of a sentence in the classical predicate calculus with respect to a model is its truth value in that model. In this paper we associate with every sentence a set of comprising evidence for it and show that a statement is true in a model exactly when there is evidence for it. According to this semantics, the denotation of a sentence is this set of evidence.

Proofs are regarded as expressions which denote evidence. Assigning this meaning to proofs gives them the same status as other algebraic expressions, such as polynomials. There are laws governing equality and simplification of proofs which can be used to explain the notion of constructive validity. A proof is called *constructive* when the evidence it denotes can be *computed* from it. A sentence is constructively valid when it has a constructive proof. These proofs turn out to be practical ways to present algorithms as has been demonstrated by an implementation of them in the Nuprl proof development system.