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.
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:
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 .
A by assumption z
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
assumption z that A holds
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.
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.
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.
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).
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].
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].
I want to thank Ryan Stansifer and Todd Knoblock for helpful comments and Elizabeth Maxwell for preparing the manuscript.