[FOM] Solution (?) to Mathematical Certainty Problem
robblin at thetip.org
Thu Jun 26 08:05:47 EDT 2003
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
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.
More information about the FOM