[FOM] Are Proofs in mathematics based on sufficient evidence?
Vaughan Pratt
pratt at cs.stanford.edu
Wed Jul 14 00:16:55 EDT 2010
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.
>
More information about the FOM
mailing list