[FOM] Foundational issues:Friedman/Baez

[Mario Carneiro]

(Duplicated from G+)

On Wed, Apr 6, 2016 at 1:51 AM, Harvey Friedman <hmflogic at gmail.com> wrote:

> Here I assume that you are talking about strictly finitary rules, with
> derivations immediately subject to computer check? What if the sizes
> are far beyond computers?? We actually have theorems to the effect
> that there are situations like that where something bit sized is
> derivable from bit sized rules, but the derivation is incredibly long,
> and cannot be proved to exist by computer. In fact, the only proofs of
> the mere existence of the finite derivations use massively infinite
> reasoning - or if they don't use massively infinite reasoning, then
> they must be far too long - at least 2^2^2^2^2^2^2^2^2^2^2^2 bytes.
>

After some introspection (like any good philosophy discussion will induce),
I think I would actually classify myself as a meta-ultrafinitist. I am not
an ultrafinitist insofar as I am perfectly comfortable "asserting the
existence" of infinite objects like the integers. But at the meta level,
these are (very) finite strings, and the theorems we prove about them are
also (very) finite.

It is true that there are "proofs of proof existence". I have no qualms
whatsoever about rejecting these as proofs in the same way that an
ultrafinitist might reject that Skewes' number exists. These are actually
proofs that T proves "T proves A" for some statement A (where T is your
theory of interest, strong enough for Goedel's incompleteness theorem).

Correct me if I am wrong, but I think T proves "T proves "T proves A""
implies "T proves A"", so working one meta-level down is sufficient to talk
about these sorts of statements with ludicrously long "proofs". It is up to
you whether you want to infer T proves A from T proves "T proves A", but if
you do this it should be treated as an axiomatic extension, because that's
what it is. If you really want to prove A, you should do so directly.

Practically all of "concrete" mathematics (the sort we've been talking
about) doesn't need these sort of contortions. You pick your theory, and
then (very) finitely deduce your theorems. Even large proofs like Wiles'
proof of FLT easily fit here.

The only real contenders for going past "very finite" into merely "finite"
are modern computer proofs such as the four color theorem or Hales' proof
of the Kepler Conjecture. These often require large enumerations, which are
not performed directly by the computer proof, but are performed by writing
a program to efficiently verify the cases, then verifying the program. This
is a special case of the "computational reflection principle", and again,
it's up to you if you want to use it. I find it vaguely discomforting.


> In my response, I moved to a difficulty for the finitist/formalist
> positions, which is the choice of "good rules". One very important
> criteria that (almost everybody thinks) has to be met is consistency
> (this usually can be formulated without using jargon from math logic).
> But how do you tell whether a given set of even very interesting and
> be sized rules are in fact consistent? That's a Pi-0-1 sentence, not
> capable of Baez-witnessing like Sigma-0-1 sentences.
>

This is absolutely true. With my meta-ultrafinitist approach, Pi-0-1
statements are utterly pointless to consider. Our only recourse is to
blindly work away with our possibly-inconsistent system, and hope that we
don't find an inconsistency (and if we do, scramble to backtrack and cordon
off the bad axiom). Then again, people have done this for years with ZFC
and it seems to work out alright.

If ZFC is inconsistent, but the inconsistency is not very finite, then it
doesn't matter, because we will never discover it. If instead ZFC proves
"there is a proof of inconsistency of ZFC of length less than 10^4000" then
I'm not sure what I'd make of it.

Mario
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160406/9c1e0b23/attachment-0001.html>