[FOM] Foundational Issues: Friedman/Carneiro

[tchow]

On 2016-04-12 16:47, Mario Carneiro wrote:
> In the case of "formal proof" (as well as of "string"), when the
> length is not too long, we are physically capable of realizing it as
> bits in a computer or words on a page. In this case I don't believe
> its "reality" can meaningfully be questioned. This is also true for
> small numbers like 1 or 3. These might be seen as a physical
> realization of a more abstract notion of "1" or "string" or "formal
> proof", which does not have the unpleasant properties of being limited
> by size, and it is this latter thing, existing in a platonic realm,
> whose existence I question.
[...]
> Insofar as it is a
> convenient abstraction for reasoning about mathematics, I like to keep
> my platonic realm unfettered by the constraints of reality, and allow
> large finite objects and infinite objects inside it.

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.

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

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.

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.

Tim Chow