Skip to main content
PRL Project

Assigning Meaning to Proofs: A Semantic Basis for Problem Solving Environments

by Robert L. Constable

Constructive Methods of Computing Science (NATO ASI Series)

  • unofficial copies PDF, PS

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.

bibTex ref: Con89

cite link