[FOM] Solution (?) to Mathematical Certainty Problem

[Robbie Lindauer]

On Wednesday, June 25, 2003, at 01:33 AM, Harvey Friedman wrote:

> I am only talking about a given human declaring that they have proved 
> something. I then tell him to go interact with the INTERACTIVE PROOF 
> CREATOR and ship the export to the CORE PROOF CHECKER. The export is 
> not going to be very large, since the human directed its creation. The 
> CORE PROOF CHECKER runs a transparent, and transparently humanly 
> verified multitape Turing machine program.

You seem to be restricting your notion of "certainty" to the same kind 
of thing that a person might have "aided with a computer" as one he 
might have "aided by a few smart friends", in which case, the practical 
suggestion is useful since we have "faith" that computers are more 
accurate than people.  What it doesn't get you is "Certainty" in the 
philosopher's sense, for arbitrary proofs, only proofs for which we 
already think we have proofs.

> Unless we can agree on these fundamental aspects of the setup, there 
> does not seem to be any point in continuing the discussion.

Probably. I find the epistemological "foundation of mathematics" to be 
among the most interesting of all subjects - does mathematics DESERVE 
the epistemologically privileged position it IN FACT holds in our 
communal reasoning?  To what extent?  Why?   I find these questions 
interesting philosophically, maybe not so much mathematically (although 
I think it bears on questions about infinite and transfinite cardinal 
numbers).  I take it it was among the goals of Principia Mathematica to 
give an epistemological justification of mathematics in terms of the 
basic logic of bivalence/alternation.

Inasmuch as there is a "mathematical certainty" problem it is this - is 
there an epistemological privilege for mathematical claims to truth?  
If so, in what does it consist?

A transcendentalist might say that mathematical reasoning is a 
prerequisite for communication of any kind (numerical distinctness 
being a prerequisite for meaningful exchanges of information, etc.)

You appear to be attempting to offer another kind of solution to the 
problem - an engineering solution.  If we could build a smart computer, 
we could refer to it for our certainty.  But with the restriction that 
the only proofs we're interested in checking are ones that we already 
"think" we understand, it abandons the classical notions of 
mathematical truth and mathematical certainty that were the foundations 
of the question.  The underlying assumption here is that if we can 
present an argument we can potentially understand it.

Presumably, there is a unique answer to simple arithmetic questions 
about very large numbers, but humans can't genuinely form them, so they 
won't ever be tested by your machine and so the question of whether or 
not they are "in principle" solvable by them in some way is not 
supposed to come up.

But the question then becomes one about Turing machines akin to 
Kripke's quus sign - what if after some very large number, the machine 
starts counting by threes instead of by ones?  Or perhaps your machine 
is just an extraordinary finitist, with Wittgenstein thinking that 
there really is a highest number or something.  Perhaps you'd just 
build it into the specification of the machine, that it need not deal 
with numbers with more than 100,000,000 digits.

 >  There are very interesting remaining issues if we can get past this 
point.

I guess one interesting one would be whether or not your proposed 
machine could prove/validate the proof for things like:

"This machine cannot validate the proof for the statement that this 
machine cannot validate the proof of this statement."

You may have already dealt with this, I'm relatively new to FOM.

Best,

Robbie Lindauer