We now want to show that proofs are notations for evidence. They are expressions which denote objects and thus have direct mathematical meaning. The explanation of proofs comes in three parts. We define first their simple algebraic structure. Then we discuss the conditions needed to guarantee that they are meaningful expressions and to determine what they prove. The statement of these conditions corresponds most closely to what we think of as ``proof rules.'' The format suggests also rules for determining type correctness of expressions. Finally we give the meaning of proof expressions with respect to a model. The method here is similar to that for giving meaning to algebraic expressions or to programs. We can in fact use rewrite rules to define most of the constructors.
The Syntax of Proof Expressions
Let a,b,c,d,e,f,g,p,l range over proof expressions and let m,v,w,x,y denote variables (we will use x,y to denote ordinary variables over D and m,v,w,z to denote variables over proof expressions). Let A,B,C,G,L,R denote formulas. Then the following are proof expressions: variables z,w and
¯¯
In 
the variables u,v are binding occurrences
whose scope is 
so that all occurrences of 
in G or g are bound. In
x,v are binding occurrences whose scope is 
so
an occurrence of x in G is bound by 
. In 
and 
, z and x are binding occurrences whose scope is 
. In 
and 
, x,u are binding
occurrences whose scope is 
. In 
u is a binding
occurrence whose scope is 
and v is one whose scope is 
. In 
is a binding occurrence whose scope is 
.
To preserve the pattern of the notation we introduce a name for the domain of discourse D. For simplicity we take D to be the name of itself; this should cause no confusion since we could take a name like ``domain'' for D in the proof expressions and agree that the meaning of ``domain'' is D.
Correctness Restrictions
We impose certain restrictions on the parts of these expressions when we say what it
means for a proof expression a to prove a formula A. For example in 
the expression F must be an implication, say 
, and f must denote
a proof F and a proof of A. The result is a proof expression for G. The
constructor name, impel, is mnemonic for implication elimination, which is
a rule usually written in logic books as shown below (and sometimes called modus
ponens in the special case when G is B.
In the implication introduction form, 
, it must be that z denotes an
assumption of a formula A and b a proof expression for B, and the 
is
a proof expression for 
. The expression b may use assumption z. One might
think of z as a label for the assumption. In an informal proof we might see these
elements in this relationship:
show
assume
show B
¯
B
qed
The proof of B from assumption z actually shows how to build a proof expression b
which may refer to the label z. For example here is an informal proof 
.
show
assume
A by assumption z
qed.
The proof expression built by this derivation is 
.
It is interesting to note that the part of a derivation that is sometimes called the justification [BC85,CO78] corresponds closely to the proof expression. For example, suppose we look at this fragment of a proof
by and introduction from a,b.
The rule name, and introduction, is used in conjunction with labels (or expressions themselves) to justify this line of the proof.
Generally in a proof expression, the operator names, such as andin, andel etc., correspond
to the names of inference rules. Subexpressions of the form 
correspond to labeled assumptions, and subexpressions of the form 
correspond to
subproofs of B by b. Thus we can read the following informal proof as the
counterpart of the proof
expression 
showby
assumption z that A holds
show
by
assumption u that B holds
show A by assumption
In short, variables occur to the left of the colon and indicate an assumption of the formula while proof expressions appear to the right of the colon and indicate why the formula is true in the context of all of the assumptions in whose scope the formula lies.
The correctness conditions on proof expressions are given by rules that are thought of as proof rules. Thus the rule for and introduction is written
The formulas above the line are the hypotheses, those below the line are conclusions. If we include the proof expressions as justifications, we would get a rule of the form
This last rule shows the pattern that we will adopt. But one additional feature is needed to
keep track of the variables. A proof expression such as 
has a free variable
y in it. This represents some undischarged assumption. There are no such variables in a
completed proof. But at some points in building a proof expression, there will be free
variables and we must keep track of them. We must know what formula or what type the variable
refers to so that the type conditions and correctness conditions can be checked. Thus it is
usual in presenting a proof to have a mechanism for indicating the assumptions and variable
bindings known at any point. This is done by keeping an environment with every rule and showing
how the rules change the environment.
Environments will be represented as lists of variable bindings 
. The 
are either the domain D or formulas. The type bindings arise from
all introduction while the formula bindings arise from implication introductions.
The use of environments may be familiar from certain logic texts. For example, they appear explicitly in Gentzen's sequent calculus [Kle52]. They are carefully defined in refinement logics [BC85]. In programming logics like PL/CV [CO78] they appear as they do in block structured programming languages. Some textbooks on natural deduction introduce the analogue of a block at least for propositional arguments.
The format we adopt for rules is to take as basic units the triple consisting of: a proof expression, the formula it proves and the environment for the variables, written together as
from H infer A by a
where a is a proof expression, A is a formula and H is a list of bindings, 
. We sometimes isolate a specific binding by writing the
environment as 
where 
are the surrounding context. We call these basic
units sequents, following Gentzen. Let 
denote them.
A rule has the form of a production as is customary in logic:
The 
are the hypothesis; S is the conclusion. Here are the rules. These define
the relationship a is a proof expression for A inductively.
{ Rules
A proof expression is built inductively using the constructors starting from the axiom and observing the correctness restrictions. These restrictions can be thought of as type restrictions on the formation of proof expressions. We give an example.
¯
¯
¯
¯
¯
¯
¯
¯
¯
¯
¯
¯
¯
the proof expression without the subformulas displayed is:
¯
¯
¯
¯
¯
¯
¯
¯
¯
¯
Semantics of Proof Expressions
We now assign meaning to proof expressions with respect to some model. The definition is given inductively on the structure of the expression and is only given for proof expressions which are correct, i.e. only for expresisons a for which we know that there is a formula A such that a proves A. We will not know that the definition makes sense until Theorem 2 is proved.
In the course of the definition we must apply the meaning function over a model m to
a function body. To explain this we extend the definition of a state to account for
variables ranging over formulas. We want to say that 
. But now A may depend on other variables over D whose meaning is given by a state, say 
.
We observe that the variables occurring in a proof expression a and in a formula A which
it proves can be listed in order of dependency. For simplicity, assume that all variables,
both free and bound, are uniquely and uniformliy named, say 
.
Let 
be the type or formula over which 
ranges. Then these can be listed in
order, for simplicity 
such that there are no free variables in
, only 
is free in 
, only 
are free in 
, etc. Let
us call this a cascade of variables and write it as 
. Now a state s will map 
into
and the appearence of s in the definition of
will be sensible. For the remainder of this section we assume that we are dealing
with such a state. Now give the meaning of a proof expression with respect to a model and
a state.
= any 
when any maps the empty set into any set
an element of 
The operations inl, inr are injections of a set into its disjunct in a disjoint union, i.e.
We know by correctness that orinl applies only if l is a proof expression for L and
is one for L|R. Similarly for orinr. So the mappings make sense in clauses 9 and 10.
In 
we know that d must be a proof expression for a
disjunction, so 
is A|B. Thus 
will be a member of 
as we show. Thus 
is either 
or 
for a in 
and b in 
.
The analysis of 
is just as for andel. We know that 
is a pair consisting of an element of D and evidence that the element is a witness
for an existential quantifier. In case of 
, we must use the axiom of choice to pick out an element of the
inhabited type. We conclude this section with a theorem that shows that the
meaning of a proof expression
is well-defined when the proof expression proves a formula.
proof
The proof is by induction on the structure of the proof expression a. In the base case, a
is some variable 
or 
for a formula C. If a is a variable, then by
hypotheses 
. If a is 
, then A is 
and 
.
Now consider the induction case. We assume that the result holds for any subexpression b of a, in any state 
assigning proper values to all free variables of b as
required by the antecedent of the induction hypothesis.
where B is the formula proved by b for b a subexpression of a.
We proceed by cases on the outer structure of a (see the syntax of proof expressions).
because otherwise a would not be a proof
expression for A. By the induction hypothesis the subexpressions of a satisfy the theorem,
so 
and 
. But
then the result holds by the definition that 
, 
must be formulas, p must be a proof expression for 
, and
g is a proof expression for G in which variables u,v can occur. We also know by the
typing rules that 
are hypotheses in typing g. Now consider any state 
which extends s and assigns 
to 
and 
to 
.
For this state and for g, the induction hypothesis holds, so that 
. By definition, 
, and 
is a state satisfying the condition on 
since 
is true by the induction hypothesis.
, w must be a term and b is a
proof expression for 
. By the induction hypothesis, 
, so by definition the meaning of a belongs
to the right set.
and
g is a proof expression for G using x a variable over D and y a variable
over B. By the induction hypothesis, the meaning of p is a pair, say 
with 
in D and b in 
. Just as in
2 we conclude 
.
and b is a proof expression for B which can use the variable
z assumed to range over 
. This means that by the induction hypothesis,
is in 
for all l in 
. Thus 
is a function from 
into 
as required to prove this case.
is a proof expression for it,
and the induction hypothesis, 
. Also, 
and for all states 
extending s and assigning u a
value in 
. Let b denote
, since b belongs to 
, then 
; so the result holds.
and l is a proof expression for L. So by the induction
hypothesis 
. Thus 
belongs
to 
as required.
, and by the induction hypothesis 
. Thus t is either 
or 
. Also by the typing
rules we know that 
and 
are proof expressions for G under variable
bindings for u and v so by induction hypothesis we know that 
and 
. This is what is needed to show
.
. That is, A is proved
under the assumption that there is something in the empty set, 
. But
there is a trivial map from the empty set to any set, call it any, so 
belongs
to any set, in particular to 
.
and by definition 
which is 
.
and 
for any 
where 
, thus 
since 
satisfies the condition for 
.
* qed.
Computational Semantics and Constructive Logic
With the exception of 
, all proof expressions are given meaning in terms of
recursively defined equations. For example, 
.
If the law of excluded middle, 
, is removed from the predicate logic, then we know
that in some sense the underlying theory of evidence is computable. If we add
expressions and rules which can be explained in terms of computable evidence, then the
entire theory can be explained this way.
Predicate logics without the law of excluded middle or its equivalents are in some sense constructive, sometimes they are called Intuitionistic logics after Brouwer [Bro23]. Arithmetic based on this logic and the Peano axioms is called Heyting arithmetic after the Intuitionist A. Heyting [Hey66]. These topics are treated thoroughly in Kleene [Kle52], Dummett [Dum77] and Troelstra [Tro73]. Analysis built on such a logic extended to higher order is sometimes called constructive analysis see Bishop [Bis67]. These topics are discussed in Troelstra [Tro73] and Bridges [BB85].
Programming
The PRL programming systems built at Cornell in the early 1980's [BC85,ML82] are based on the idea that formal constructive logic, because of its conputational semantics, provides a new kind of very high level programming language. This idea was first explored in Constable [Con71] and Bishop [Bis70]. It was later developed by Bates and put into practice by Bates and Constable [BC85]. The semantics of evidence discussed here is quite close to the actual implementation ideas in Nuprl [ML82].
Acknowledgements
I want to thank Ryan Stansifer and Todd Knoblock for helpful comments and Elizabeth Maxwell for preparing the manuscript.