We present a standard kind of predicate calculus. The formulas of our logic are built using the binary propositional connectives (and, or, not, implies) and the quantifiers where x ranges over the class of objects called individual variables. There must be at least one propositional function constant, there may be several but only a finite number of them (for simplicity), say . There may also be ordinary function constants, say . With each propositional or ordinary function constant we specify the number of arguments it takes; this is called its arity. The arity can be zero. The language will have terms, these include (individual) variables written . If there are ordinary function constants, then the terms include expressions of the form where the are terms and the has arity n. If the arity of is zero, then is also an individual constant.
A formula of the logic is defined as follows:
A particular instance of this language that is quite familiar arises by taking 0 and 1 as individual constants (arity zero ordinary functions), taking + and as ordinary function constants, (writing for and = and < as propositional functions of arity 2 so that and stand for x=y and . In the remaining examples we will write these familiar functions in their usual infix manner taking them as abbreviations for the ``official'' form. Formulas in (i) and (ii) are atomic. Those in (iii) are compound with principle operator or (in that order). Those in (iv) are quantified formulas, and their principle operators, are or .
The quantifiers are called binding operators because they bind occurrences of the variable x in the formulas to which they are applied. In and in , the formula part B is called the scope of the quantifier. Any occurrence of x in B is bound. It is bound by the quantifier of smallest scope that causes it to be bound.
A variable occurrence in a formula F which is not bound is said to be free. If x is a free variable of F, and t is a term, we write to denote the formula that results by substituting t for all free occurrences of x and renaming bound variables of F as necessary to prevent capture of free variables of t. Thus if t contains a free variable y and x occurs in the scope of a subformula whose quantifier binds y, say , then the quantifier is rewritten with a new variable, say because otherwise y would be captured by . For example, in the formula the variable x is free. If we substitute the term for x we do not obtain but instead . See [Kle52,ML82] for a thorough discussion of these points.
A formula with no free variables is called closed. A closed formula is called a sentence.
If for convenience we want to avoid writing all of the parentheses, then we adopt the convention that all the binary operators are right associative with the precedence &, and then quantifiers. Thus abbreviates .
Semantics of Truth
The meaning of a formula is given with respect to a model which consists of a set D, called the domain of discourse, and a function m called interpretation which maps each ordinary function constant f of arity n to a function from into D denoted m and maps each propositional function constant P of arity n to a function from into denoted m.
To give the meaning of formulas with free variables we need the idea of a state which is a mapping of variables to values, that is belongs to D. When we want to alter a state at a variable we write which denotes if and denotes a if . We define the relation that formula F is true in model and state s, written
Preliminary to this concept we need to define the meaning of a term in state s, written . The meaning of constants is given by , so . The meaning of variables is given s, so . The meaning of is .
Semantics of Evidence
The following set constructors are needed in the semantics of evidence. Given sets A and B, let denote their cartesian product, let A + B denote their disjoint union, and let denote all the functions from A to B. Given a family of sets indexed by A, let
denote the set of functions f from A into,
such that belongs to . We also take
to be the disjoint union of the family of sets. It can be defined as .
Now we define , the evidence for formula A in model and state s
So we have defined inductively on the structure of a formula A a collection of objects that constitute the evidence for A in a particular model . In the base case, 1, the definition relies on the semantics of truth. Here is an example of evidence: <6,T> belongs to . We need to know that 5 < 6 is true so that T belongs to . Truth and evidence are related in this simple way.
The proof is accomplished by induction on the structure of B showing both directions of the biconditional at each step. The easiest direction at each step is showing that if , then . We do these steps first, but the induction assumption at each step is the statement of the theorem for subformulas of B. To determine the subterms we proceed by case analysis on the outer operator of B. (We drop the state when it is not needed.)
then for any . So is true for all elements of D. Thus is true.
By the axiom of choice there is a function f such that .