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

[Vaughan Pratt]

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 
(imagined truth).

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

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 
associated applications.

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 
real-world situations.


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.

Vaughan Pratt