[FOM] Foundational Issues: Friedman/Carneiro

[Mario Carneiro]

On Thu, Apr 7, 2016 at 9:32 AM, Alan Weir <Alan.Weir at glasgow.ac.uk> wrote:

> I like Marco [sic] Carneiro's line (Vol 160, Issue 11):
>
>
>
> '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.'
>
>
>
> though I wouldn't want to identify the (non-existent) abstract objects
> with concrete strings, but rather identify the latter with what makes
> assertions about abstract existence true.
>
>
>
> But on the face of it such a position, if adopted in support of
> thoroughgoing anti-platonism,  smacks of inconsistency or hypocrisy: both
> asserting the existence of integers, indeed infinite sets of integers,
>  infinite sets of expressions or proofs and so on, and (moving up the
> corridor or across a few blocks from the Maths room to the Metaphysics
> room) rejecting such existence claims.
>

I think we have a difference of understanding of the word "exists" here.
When I say "the natural numbers exist", I mean no more or less than "∃ N,
(0 in N /\ ∀ n in N, n+1 in N) is a theorem in the theory of interest".
That's a finite statement about a finite string, with a finite proof
(assuming I am not making a false claim). It's all well and good if you
want to think there is some world out there where you can meet the actual
natural numbers, but it literally has no bearing on the statement. I
suppose you could call this "anti-platonism", although that makes it sound
as if I assert the *non*existence of platonic objects, when instead my
position is closer to "who cares".

In our imaginations, we might maintain a mapping from expressions like "∃
N, (0 in N /\ ∀ n in N, n+1 in N)" to "the natural numbers exist", and
maybe picture a line of numbers going off to the distance, but these are
intuitive tools to help us with the proofs, not actual evidence of a
Platonic realm. The symbol ∃ has a certain syntactical behavior in proofs,
and we assign this the semantic meaning and English wording "exists", with
all its loaded connotations, because it is convenient for our intuition.


> I (here follows some shameless tooting of own trumpet) try to address
> those worries about the inconsistency of this anti-platonist position in
> 'Truth through Proof: a formalist foundation for mathematics', Oxford
> University Press, 2010. The short introductory chapter gives an overview of
> the strategy. Chapter Seven on Idealisation addresses most directly the
> issues raised particularly what I see as the crucial point made by Harvey
> Friedman (and supported by theorems such as Godel's speed-up theorems) FOM
> Digest, Vol 160, Issue 10:
>
>
>
> '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.'
>
>
>
> A relevant observation here is Marco Carneiro's
>
>
>
> 'It is true that there are "proofs of proof existence".'.
>
>
>
> Trumpet a-tooting again: I look at this sort of issue- indirect versus
> direct concrete proof- in 'Informal Proof, Formal Proof, Formalism', Review
> of Symbolic Logic (early online 2015, print version Vo. 9, March 2016)
> especially section 7. The problem is that Harvey Friedman's point shows
> that no amount of moving to indirect proofs of the existence of proofs of
> proofs ... will alter the fact that some statements, even of very basic
> mathematics, will have neither concrete proofs nor disproofs, however
> indirect.
>
>
>
> I do not conclude that the formalist should abandon excluded middle in
> such cases.
>

This sounds less like excluded middle and more like incompleteness. It is
no surprise that some statements are neither provable nor disprovable, and
going down a meta level won't change this. Then again, it is possible that
pushing up proofs of proof existence can accidentally introduce
inconsistency, if for example the proof existence is actually of
nonstandard length, and so pushing it up to a real proof is actually
strengthening the system.

Mario Carneiro
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160407/079dbd57/attachment.html>