If I correctly stated the winning lottery number before it has been publicly announced, many
people will be more interested in my evidence for the assertation than in its truth. Even
for routine utterances we are interested in the evidence. ``How do you know?'' we ask. In
formal logic the ``truth'' of a sentence can be defined following Tarski [Tar44] who put
the matter this way for the case of a universal statement: is true in a model
** m** if the model assigns to **B** some propositional function ** m** which has value
true for every element of the * universe of discourse* **D** of the model. That
definition ignores evidence. We want to give a precise definition of evidence and relate it
to truth as defined by Tarski.

In mathematics there is a persistent interest in evidence even though the official definition
of truth does not refer to it. So if I claim that there is a regular 17-gon, then you may
wish to see one. The ancient Greeks would require that I * construct* one or in
some way actually exhibit it. As another interesting example, suppose that I claim that there
are two irrational numbers, say **x** and **y**, such that is rational. I might prove that
they exist this way. Consider , it is either rational or irrational.
If it is rational, take . If it is irrational, take and . Then . So in either
case there are the desired **x,y**. But notice that the evidence for existence here is
* indirect*. I have not actually exhibited **x** by this method, even though you might be
convinced
that the statement is * true* in Tarski's sense. A constructive proof of this statement
would actually exhibit **x** and **y**, say for example and are
irrational plus the computation .

We begin to understand how the concept of evidence is defined if we examine its use in
ordinary discourse. Existence statements like those above are especially significant. Evidence for ** there is an x such that B holds**, symbolized , consists of an element **a** and
evidence for **B** holding on **a**. Consider now evidence for a universal statement
such as * for every natural number x there is a pair of prime numbers, p, p+2 greater than x*. Given

Consider next evidence for a conjunction such as ** n is odd and n is perfect**. We would expect
to have evidence for both statements, say a pair containing (or comprising) a factorization of
**n** as **2m+1** and a summation of all of the factors in n. Evidence for a disjuntion such as **A** or
**B** will be either evidence for **A** or evidence for **B**. We also imagine that we could tell which case the evidence applied to.

Consider this implication: if there is a polynomial time algorithm to decide
whether an arbitrary boolean expression is
satisfiable, then there is an algorithm to determine whether a finite graph has a clique of any
given size. This is a typical statement in modern computational complexity theory. The truth
value of the antecedent is not known, yet the
implication is true. It is true because we have a method to transform any
(hypothetical)
algorithm for satisfiability into one for clique. It is this method which bears witness for the
implication. A more mundane example is this. When I say ``if there is a 6 in the
array A, then there is a 6 in the array B obtained from A by replacing each odd value and
only odd values by 5;'' you
can recognize this as a true implication because you know a method of taking evidence for ``6 is in
A'', say an index i and the value , to evidence that ``**6** is in **B**,'' the same index **i**
and will suffice for instance.

What is evidence for a negation such as ``**4** is not prime.'' First, notice that I mean ``it is not the case
that **4** is prime'' rather than taking ``not prime'' as a separate predicate meaning **4** is
composite. So in general we are looking at a uniform negation, . This is sometimes
equivalent to some positive statement, such as ``**4** is composite.'' But if we do not know anything
about **A** other than that it is a proposition, then we cannot hope to reformulate it positively; so
we ask whether we can say anything about negation uniformly in **A**. Intuitively it seems sensible to
say that evidence for is evidence that there is no evidence for **A**. So the question then
is ``how do we show that sets are empty?'' We cannot do this by producing an element.

One way to show that a set, say described by term **A**, is empty is to show it as a subset of the
canonical empty set, say , i.e. . This amounts to showing an implication
, if then . One formula whose evidence set is clearly empty is
* false*; that is the definition of the formula * false*, one with no proofs. So one way
of proving uniformly is to prove . This is not the only way, but it is
sufficient. We might for example prove that **F=G** and holds. But also, if we know ,
then we know that the evidence set for **F** is empty, so it is a subset of and so . Thus we can take as the * definition* of a general
negation; we adopt this definiton.

These explanations may not be definitive, but they provide a good starting point. In the next section we define a particular specimen of formal logic and give a precise definition of both truth and evidence. Then in section 3 we examine proofs and show how they encode evidence.

This interpretaion of evidence is not new, its origins go back at least to L.E.J. Brouwer who
discovered in the early 1900's that to treat mathematics in a constructive or computational way, one
must also treat logic in such a manner. He showed that this could be done by basing logic on the
judgement that a sentence is * known to be true from evidence* rather than on the judgement that it is
true. At this point in the discussion, we are not concerned with computable evidence exclusively,
but with an abstract notion of evidence. In some sense we are extending Brouwer's ideas to classical
logics as well. Later we will make connection to constructive logic via the so-called
* propositions-as-types* principle due to Curry, Howard, and de Bruijn (for references see
[CAB86,deB80]). This principle can be seen as formalizing the notion of evidence in * type
theory*, see also [ML82], [CAB86].

Tue Nov 21 10:57:11 EST 1995