** Next:** Introduction

# Assigning Meaning to Proofs: a semantic basis for problem solving environments

**Robert L. Constable**

Cornell University

Ithaca, NY 14853

### 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 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.

*
*

*nuprl project *

Tue Nov 21 10:57:11 EST 1995