next up previous
Next: Proofs Up: Assigning Meaning to Proofs: Previous: Introduction

The Logic

Syntax

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:

(i) false is a formula (it is a propositional constant)

(ii) if is a propositional function of arity n, and are terms, then is a formula

(iii) if are formulas, then so are



(iv) if B is a formula, then so are
and .

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 .

Truth Conditions


  1. for P a propositional function constant of arity n.

  2. with a in D

  3. for a in D

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


  1. empty otherwisefor P a propositional function constant.



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.

proof

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

  1. If B is atomic, then the result is immediate.

    (1)
    B is
    Then so b is a pair, say, and and . By induction then, and so .

    (2)

    Given , it must be in one disjunct or the other. That disjunct will be true by the induction hypothesis, so the whole disjunction is true.

    (3)
    B is
    Given , we consider two cases. Either is empty or there is some . In the later case so is true and so is . If is empty, then by the hypothesis is false. So is true.

    (4)
    B is
    Given
     ¯
    

    ¯

    then for any . So is true for all elements of D. Thus is true.

    (5)
    B is
    Given c in we have that is true on a. So B is true.

  2. Now we must show that if B is true in model and state s, then there is evidence for . Again we proceed by induction on the structure of B. Clearly B cannot be false, and the result is immediate for other atomic B.

(1)
B is
Both and must be true if B is. So by the induction hypothesis there are
. By definition .

(2)
B is
Either or is true. In either case, by induction there is an element of or of .

(3)
B is
is either true or false. If it is true, then by the induction hypothesis there is . So the constant function returning this value is evidence for . If is false, then must also be false. This means by the induction hypothesis that is empty. But then the identity function is evidence for .

(4)
B is
Since this is true, we know that for every element a of D,

By the axiom of choice there is a function f such that .

(5)
B is
For B to be true, there must be some a in D on which is true. By the induction hypothesis, there is . Then is evidence for .


* qed.



next up previous
Next: Proofs Up: Assigning Meaning to Proofs: Previous: Introduction



nuprl project
Tue Nov 21 10:57:11 EST 1995