[FOM] Are proofs in mathematics based on sufficient evidence?
pratt at cs.stanford.edu
Sat Jul 17 01:06:46 EDT 2010
On 7/8/2010 4:18 AM, Arnold Neumaier wrote:
> I wonder why you put mathematical proof and logical proof into the same
> category, as opposed to legal or other kinds of proofs.
> There are worlds between these two notions of proof, in spite of the
> common ground these notions have.
(A belated response to Arnold's early response to my original question.)
The Wikipedia article Proof (truth) actually does distinguish these, as
it has done since I first wrote it. Part of the confusion arose when a
zealous editor deleted all the material on both mathematical and logical
proof on the ground that only informal proof took evidence for premises.
This editor did not see enough difference between the two to treat
them differently in that regard.
While there are plenty of nuanced distinctions, I see two somewhat
independent binary distinctions in the concept "sufficient evidence for
truth." (Not everyone will see the same ones, and I may change my own
mind about these later on.)
1. The evidence may be drawn either from experience or hypothesis.
2. Sufficiency may be either soft or hard.
1. Experiential evidence comes from nature, namely the real or
sensorially apprehended world, augmented with inferences from that
evidence about nature. This includes the actual state of a computer
gate, register, or memory.
Hypothetical evidence comes either directly from what-if counterfactuals
or axioms or indirectly as consequences of direct hypotheticals
(reasoning). This includes the activity of program verification.
One might call these respectively fact (real truth) and fiction
There is a phenomenon whereby fiction appears as fact: just as a
pot-boiler that can't be put down conjures up images hard to distinguish
from facts gleaned from newspapers, so can mathematical axioms seem real
to the mathematician accustomed to intensively visualizing abstract
2. The soft-hard dichotomy in sufficiency is to me the same as the
informal-formal dichotomy (I could be talked out of this but first read
the next paragraph). Hard is when there are precise criteria that
evidence must meet to constitute a complete proof, soft is everything else.
The term "precise" offers a loop-hole here. Precision can only be
measured up to some standard of equality, isomorphism, equivalence, or
whatever. Each such standard may have a mathematically or
scientifically rigorous definition, but there may be more than one, and
they may induce a partial order on the standards. We see this in proof
theory, with Girard's notion of proof net as an abstraction of
sequential proof ("bureaucracy" to use Girard's term), and with the even
more abstract notion of proof contemplated in Dosen and Petric in their
2004 book Proof-Theoretical Coherence, where a proof is simply a
morphism interpreted as a proof in a category with suitable structure
supporting that interpretation.
These two distinctions combine in the following four ways, with the
Experience/soft Scientific investigation, arguments in court, work,
bars, home, etc.
Hypothesis/soft Mathematical reasoning, counterfactual reasoning
Experience/hard Formal deduction applied to the real world, whether
it be Aristotle's syllogisms as popularized by Lewis Carroll, Boolean
logic applied to database search, etc.
Hypothesis/hard Formal deduction applied to mathematics (the core
focus of FOM perhaps?), but also to counterfactual reasoning about
One distinction this analysis does not make is between counterfactuals
about real-world situations and mathematical theories. There may well
be such a distinction in most people's minds; in that respect I may be
out of step with everyone else. To me every mathematical theory *could*
be about some real-world situation suitably abstracted. One cannot
reason about counterfactuals with every detail filled in, how would you?
Unlike experiential evidence, counterfactual evidence can't be poked
around in because there is no real world backing it up. It is therefore
necessarily abstract. One might quibble as to whether that abstraction
is like mathematical abstraction, but I have great difficulty in drawing
that line and therefore no basis for joining such a quibble.
More information about the FOM