[FOM] Are Proofs in mathematics based on sufficient evidence?

[Vaughan Pratt]

First let me thank everyone who responded to my request for perspective. 
  Most of you I imagine will have noticed that common sense has 
prevailed in the Wikipedia article on Proof (truth), which is now pretty 
much as it should be.  (At one point one editor removed everything to do 
with both mathematical and logical proof on the ground that for neither 
kind of proof could premises be considered evidence. To satisfy those of 
that opinion, "evidence" was broadened to "evidence or argument.")

Hopefully I'll be able to respond to at least some of the responses.  I 
very much appreciated Martin Davis's defense of the past century of 
development of intuition into the nature of mathematical proof.  I also 
like Jim Hardy's confirmation just now of what seems to be a reasonably 
broadly shared intuition on this group about the nature of proof outside 
the distinction between mathematics and law, and Catarina Dutilh's 
pointer to Netz's book, which I will definitely look into.  And that 
just scratches the surface.

Immediately on the heels of Jim's post was that of Irving Anellis 
concerning the distinction between formal deductive systems and 
axiomatic systems.  I would like to add a third category to this, 
computer programs, and respond to Irving's post as follows.

Aristotle's syllogisms and Euclid's postulates are both of a formal 
logical character to one degree or another, though the deductive nature 
of syllogistic reasoning seems clearer if only because it is both 
simpler and domain independent.  The Oxford mathematician Lewis Carroll 
published a weekly series of syllogisms (the basis for my master's 
thesis), so one might imagine he would look to elementary mathematical 
arguments as his source of material, but instead he reasoned about 
crocodiles and babies.  (But not tables, chairs, and beer mugs as 
suggested by Hilbert for an alternative interpretation of points, lines, 
and planes.)  So I would like to imagine that Aristotle and Carroll 
would both approve of Proof (truth).  Whether Euclid saw a hard line 
between mathematical proof and Aristotle's syllogisms is a very 
interesting question that I have no intuition for.

But where does one draw the line between axiomatic systems, formal 
deduction, and computation?  I have no idea.  Is the following an 
axiomatic system, a formal deductive system, both, or neither?  The 
variables range over positive integers and the "formulas" as such can be 
either triples of integers or simply integers.

AXIOM. (x, y, 1).

INFERENCE RULES.

R1: (p, x, a), q  |-  (p, x, qa)  provided q divides p-1 and x^((p- 
1)/q) is not congruent to 1 (mod p).

R2: (p, x, p-1)  |-   p  provided  x^(p-1) is congruent to 1 (mod p).

This is taken straight from "Every prime has a succinct certificate," 
SIAM J. Comp. 4:3, 214-220 (Sept. 1975).  The paper can be found at

   www.cc.gatech.edu/~subruk/4510/primes_pratt.pdf

for example, or just google succinct certificate.

Those theorems that are just integers are all and only the primes.  The 
interest in this system, which is based on what had up until then been 
considered the Lucas-Lehmer *heuristic* for testing primality, was that 
there was a sense in which it was more than a mere heuristic that worked 
only some of the time, but could be used to assign a polynomial-length 
proof to *every* prime (the point of the "every" in the title, which 
also witnessed the first appearance of "succinct certificate" as a 
technical term---it was not my idea to identify "succinct" with "Pratt" 
as I do not consider myself at all succinct).

I wrote this nondeterministic program with the idea that it was a hybrid 
between a conventional computer program with if-statements and 
assignments of numbers to variables, and a formal deduction system with 
mere data where one would expect to see propositions.  To me 
propositions were merely one of various kinds of data, and I saw no 
reason why nondeterministic programs had to manipulate propositions in 
order to be deemed either axiomatic systems or formal deductive systems. 
  What's wrong with deducing data of all kinds, not just propositions? 
Why must the value of every deduction be a truth value?

One could argue that this is easily fixed by enclosing the two types of 
"theorem" here in two corresponding uninterpreted predicate symbols 
phi(x,y,z) and psi(x).  (So the crucial property of this system is that 
in the standard model psi(p) can only be the predicate prime(p), and 
moreover it is.)  But the same can be done for any computer program: 
just associate a distinct uninterpreted predicate symbol with each 
n-tuple of variables and the program counter or location, for each n, 
and then every program becomes a formal deductive system, as a triviality.

Clearly what I wrote is an axiomatic system because it has an axiom and 
two inference rules.  But is there really a coherent notion of "formal 
deductive system," or is the concept just a mirage?

Vaughan Pratt

On 7/13/2010 11:26 AM, Irving wrote:
>
>>
> I should like to address specifically the issue of Euclid's Elements as
> an example of a deductive system.
>