Introduction

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 0, the evidence could be 2, 3 and given 2 it could be 5, 7, etc. But what is evidence for the universal statement? It should include in some way these instances, so it could be a function f which given a number n produces as evidence for the assertion, e.g. could be a pair p,p+2 and proof that p is greater than n.

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