[FOM] Foundational Issues: Friedman/Carneiro

[Alan Weir]

I like Marco 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 (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. Rather an adequate notion of idealisation is needed to save the day: very roughly, all the formalist needs (with respect to a given mathematical system) is a concrete 'very finite' proof of the equivalence of provability and truth to validate excluded middle for that framework or across that branch of maths. Nor, once we have abandoned belief in the mind-independent existence of abstract objects, finite or infinite, is there any rational requirement that only assertions of the existence of finite proof objects are legitimate, there are after all concrete very finite proofs of the existence of infinitary formal systems (albeit the concrete proofs are always, or almost always, informal: the relationship between informal and formal proof being, of course, a crucial, and very thorny, problem here).

Alan Weir
Roinn na Feallsanachd/Philosophy
Sgoil nan Daonnachdan/School of Humanities
Oilthigh Ghlaschu/University of Glasgow
GLASCHU G12 8QQ /GLASGOW G12 8QQ

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160407/7b6c04fd/attachment-0001.html>