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:
is a propositional function of arity n, and 
are
terms, then 
is a formula
are formulas, 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
with a in D
for a in DSemantics 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.
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.)
so b is a pair, say, 
and 
and 
. By induction then, 
and 
so 
.
, it must be in one disjunct or
the other. That disjunct will be true by the induction hypothesis, so the whole disjunction is true.
, 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.
¯
¯
then for any 
. So 
is true for all elements
of D. Thus 
is true.
we have that 
is true on a. So B is true.
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.
and 
must be true if B is. So by the induction hypothesis there are
. By definition 
.
or 
is true. In either case, by induction there is an element of 
or of 
.
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 
.
By the axiom of choice there is a function f such that 
.
is true. By the induction
hypothesis, there is 
. Then 
is evidence
for 
.
* qed.