[FOM] Foundational Issues: Friedman/Carneiro

[Mario Carneiro]

On Thu, Apr 14, 2016 at 10:20 AM, tchow <tchow at alum.mit.edu> wrote:

> So if I understand you correctly, you "like" to allow large finite
> objects inside a "platonic realm" because it is "unpleasant" to have
> limited size.  What you don't want to do is to attach the word "exists"
> to a large finite object inside a platonic realm.  It doesn't "exist";
> it is just "allowed to be inside a platonic realm".  The only abstract
> objects that you allow to "exist" are small finite ones, for which you
> can point to something you consider to be its "physical realization".
> (One thing I don't quite understand, though, is what you mean by "a
> more abstract notion of '1' that is not limited by size".  I understand
> how a string or a formal proof can be unlimited in size.  How are you
> imagining '1' to be unlimited in size?  In what follows I'll assume
> that this was an oversight on your part.)
>
> At the same time, you *do* allow the use of phrases such as "the natural
> numbers exist" but only in the sense of operator overloading: If we
> assert that a small finite number exists then that means that there is
> (or can be?) a physical realization of it; if we assert that a large finite
> number exists, or that an infinite object exists, it doesn't mean that
> there is, or can be, a physical instantiation.  Rather, such a statement
> must be regarded as a convenient abbreviation for an assertion that some
> formal string is a theorem of some formal system.
>

This is a fair characterization. The first "exists" is the concern of a
philosopher, the second "exists" is the concern of a mathematician. As
such, they don't overlap very much and it's generally clear which is which.


> The overloading of the word "exists" is confusing, but I think I can get
> used to it.  However, let me return to your claim that statements of the
> form "is P a proof of A in the theory T" are objectively true or false.
> Do you mean to assert this only for P for which we have a physical
> instantiation, and T a finite list of axioms for which we also have a
> physical instantiation?


Not a finite list of axioms, but a finite list of axiom schema, or more
generally, we can assume that T is equipped with an algorithm for deciding
axiomhood that always terminates in a reasonable time given reasonable
input, and (someone mentioned to me that proofs in some formal systems can
involve long checking times) the entire verification can occur within a
reasonable time period. When all these are satisfied we are able to judge
its "objective correctness" without issue, when it is not we may have to
defer the answer. (For example, is Mochizuki's proof of the abc conjecture
valid?)


>   For example, if T is Th(PA) then T is an infinite
> object, and even if T is the set of axioms of PA then T is also an
> infinite object, and so then it would seem we're not allowed to parse
> the word "is" directly, but have to unabbreviate into an assertion that
>
>   "P is a proof of A in the theory T" is a theorem in a certain system.
>

This is definitely not allowed. By passing to the meta level here, you are
able to introduce artifacts of your meta level formal system into the proof
verification, so for example if the meta level formal system is
inconsistent you will be able to deduce the incorrect answer.

I suppose your point is that in formal logic, "P is a proof of A in the
theory T" is defined simply by comparing each step of P to an axiom or
inference rule in T, which would seem to suggest that it requires T to have
finitely many axioms in order to feasibly implement. But this is an
artifact of the chosen implementation, and there are a great more varieties
of theories for which proof verification is feasible, using more
complicated algorithms that can be shown equivalent to the naive one by a
meta level argument.

If, as I think you want to do, we eliminate the need to unabbreviate "is"
> by restricting T to the (physically realizable) subset of axioms of T
> that are actually needed to carry out P, then I return to something that
> I alluded to previously: This sounds like a claim that statements of the
> form "P is *known to be* a proof of A in T" are objectively true or false,
> and not that statements of the form "P is a proof of A in T" are
> objectively true or false.
>

Now I think I understand what you mean by this. The reason it is not always
necessary to evaluate the proof is because sometimes we can put upper
bounds on the verification time, to determine that yes, we will know within
our lifetime (say) that this proof is correct or not. However, it is
definitely true that this only barely extends the net beyond "P is *known
to be* a proof of A in T" (although this definition does give a satisfying
interpretation to known proofs beyond simply "the mathematical community
agrees that it is valid").

In any case, I find it difficult to distinguish your view from what you
> call a "true ultrafinitist" position.  True ultrafinitists typically
> "allow" infinite objects "inside a platonic realm" provided that we are
> clear that the platonic realm, and the objects therein, don't exist,
> and that any assertion about their existence can be affirmed only if
> recast as a suitable statement about feasibly small proofs.
>

Maybe I'm mischaracterizing, but all ultrafinitists I have heard attempt in
some way for this philosophy (and that's what this is) to back-channel into
mathematical statements, formalizing some kind of system in which the
mathematical "exists" is more like the ultrafinitist "exists". (And most
ultrafinitist formalization efforts have been unsuccessful.) I have
absolutely no plans on doing this, and very much like the expressivity and
power of infinite reasoning through formal systems that allow "infinite
objects" such as ZFC. Quite frankly, I almost never use the above
ultrafinite "exists" in mathematical conversation, and try to stick to the
mathematical "exists" whenever possible.

Are there infinitely many twin primes? I don't know. Does this question
have an objective answer? Again, I don't know, and probably won't know
until we know the answer to the question itself. Is <gigantic number> a
prime? Don't know. Objectively true or false? Won't know until we have the
answer. On the other hand, the statement "<gigantic number> is either prime
or not prime" is true. (This is the difference between "T |- P or T |- ~P"
vs. "T |- P \/ ~P".)

Finally, I should also be clear that I am not asserting that the platonic
realm does not exist in reality, only that we have zero evidence that it
does exist. (And I don't think this is controversial.)

Mario
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160414/10699bb5/attachment-0001.html>