[FOM] 461: Reflections on Vienna Meeting

[Harvey Friedman]

> Dear Harvey,
>
> thank you so much indeed for this very interesting and very rich  
> report about the past meeting in Vienna - and also for posting the  
> link to slides of your talk! I comment here only on some of your  
> most general points.
>
>>
>> As you can see, I began by emphasizing that there are distinct  
>> forms of intellectual lives, where I briefly discuss
>>
>> The Mathematical Life
>> The Philosophical Life
>> The Foundational Life
>>
>> These have very different value systems and aims. The overlapping  
>> concerns between the Mathematical Life and the Foundational Life,  
>> and between the Philosophical Life and the Foundational Life, dwarf  
>> the overlapping concerns between the Mathematical Life and the  
>> Philosophical Life, at least at the present time and for  
>> considerable time past.
>>
>
> I'm not convinced that what you call the Foundational Life is indeed  
> on equal footing with what you call Mathematical and Philosophical  
> Lives.

And in my opinion, the top of the Foundational Life is vastly superior  
than the top of the Mathematical Life and the top of the Philosophical  
Life.

For example, a top of Foundational Life should include what I  
understand of Einstein's thought experiments.

The Foundational Life uses heavily mathematical and heavily  
philosophical methods.

The foundational life is far far broader than f.o.m. (FOM). I have  
been using FOM as an abbreviation for this email list, and f.o.m. for  
foundations of mathematics.

On the other hand, the Foundational Life is incomparable smaller than  
the Mathematical Life or the Philosophical Life. By far its most  
highly developed part is f.o.m., where some of top items reside.

> FOM in your sense is one among a number of other research programs  
> that use the same title. I doubt, in particular, that Voevodsky's  
> recent proposal in (what he calls) FOM  http://video.ias.edu/univalent/voevodsky 
>   qualifies as FOM in your sense  (please correct if needed).  
> Lawvere's categorical foundations definitely don't (as Lawvere  
> himself makes it clear).   My own research in (what I call) FOM  
> doesn't qualify as FOM in your sense either, in particular, because  
> it essentially involves historical considerations, in a way which is  
> incompatible with your notion of FOM if I understand it correctly.  
> This notwithstanding I can see no reason to give up the title.

Titles are always difficult. But I believe that Foundational Life and  
f.o.m. are the best titles available, and I am content with having to  
explain the crucial differences between f.o.m. and imposters, to the  
extent that I am able to do. In fact, I would like to understand more  
of what people like to put forward as foundational than I do.  
Generally speaking, I don't find it hard to pinpoint the difference.

>  Your claim that FOM *begins* only in the 19th century is  
> understandable given the narrow sense of FOM that you make explicit  
> - but anyway it strikes me as historically erroneous (I provide a  
> relevant argument below).

I didn't say it that way, but I took the 1800 situation as a good  
starting point, following what is at least implied by, say, Morris  
Kline's book Mathematics from Ancient to Modern Times.

On the other hand, I am perfectly open to going back earlier, but I  
don't think it would have made any difference for that talk. E.g., I  
am willing to contemplate the foundational meaning of investigating  
solutions to the equation x^2 = 2. There is quite an early  
impossibility theorem (independence result) here! Much earlier than  
the 19th century!

> Thus delimiting the area of FOM in the way you suggest seems me a  
> bad idea because it prevents your research program from any external  
> critique. Actually the attention you pay to arguments of Angus and  
> other people who think differently (including myself) fully  
> convinces me that to protect your research from an external critique  
> is not your real intention. So my critique here concerns the  
> terminological choice rather than the substance. However this  
> particular terminological choice seems me an important issue because  
> among other things it has a bearing on the power game between  
> different group of researchers.

My conception of f.o.m. does not originate with me. On the contrary,  
it follows people quite senior to me, and I felt any impulse to change  
terminology. It was widely in use when I went to graduate school by  
people such as Solomon Feferman, Georg Kreisel, Patrick Suppes, Kurt  
Goedel, Quine, Russell, etcetera. So the idea of changing terminology  
never entered my imagination.

> Now briefly about the substance.  I agree that the set concept at  
> the time of its emergence appeared to be a powerful unifying concept  
> in mathematics. I also agree that this fact makes set theory  
> relevant to FOM (so our different notions of FOM coincide at this  
> point). But I also observe that in the history of maths there were a  
> number of other concepts that played a similar role in different  
> times. In particular, in 17th century maths such a role was played  
> by the general concept of magnitude (that generalized on more  
> traditional concepts of geometrical magnitude and number). This is  
> why (leaving more general philosophical reasons aside) I think that  
> FOM has its history dating back at least to Euclid's time. Looking  
> back in time one can observe that the history of FOM involved  
> drastic changes of fundamental concepts and that these changes were  
> essential for the mathematical progress. One consequence of these  
> historical consideration concerns the future but not the past. There  
> are strong evidences - and some leading mathematicians including  
> Manin claim this explicitly - that the set concept no longer affords  
> to play the unifying role in today's maths and is gradually replaced  
> by the category concept. This is still a relatively new development,  
> so nobody knows yet how things are going to be settled. What is  
> obvious though is that there are rapid developments going on here.  
> And the history of the subject suggests that the ongoing  
> transformation of FOM is not something exceptional but something  
> that happens in maths all the time. Claims about the irrelevance of  
> set theory (and hence of FOM in your sense) made by working  
> mathematicians (I refer now to you posting) are further evidences  
> that confirm my guess about the role of set theory in today's maths.  
> This suggest that a sound theory of FOM must take such  
> transformations of FOM into consideration. I cannot see that the FOM  
> in your sense does it.

1. The set foundations, as I wrote, is more than sufficient to draw  
incredibly deep conclusions. That is because many of these incredibly  
deep conclusions are simply not sensitive to a shift from sets to,  
say, categories.

2. Part of the f.o.m. technology is that of the notion of  
INTERPRETATION. Rigorous results abound by people doing f.o.m.  
establishing that various theories of categories are mutually  
interpretable with various theories of sets. These interpretations  
preserve many properties. Much of the incredibly deep conclusions are  
automatically preserved under these interpretations, and therefore  
remain under any change from sets to categories.

3. Item 2 is perfectly compatible with working mathematicians talking  
about irrelevance of set theory.

4. There certainly can be a point where a shift from sets to  
categories really matters. Only here the issue arises as to whether  
one wants to use categories as fundamental, or rather as only as  
organizationally fundamental. These are quite different.

5. Any systematic organization of mathematics - with emphasis on  
systematic - is within the purview of f.o.m. as I view it. What is not  
within the purview of f.o.m. is any pretension that categories are  
fundamental in the sense that sets are, which is not backed up  
philosophically coherent argumentation.

6. In fact, philosophical clarity is the clear weak point in  
alternative foundational schemes.

7. In summary, for a vast variety of even yet to be mined purposes,  
alternative foundational schemes aren't going to facilitate or clarify  
anything, and they demonstrably don't make any difference.

8. But when it might make a difference, it is either organizational  
(an entirely different matter), or incoherent philosophically. Or at  
least incoherent thus far.

9. For example, consider

is there a concrete mathematically natural sentence independent of the  
usual axioms and rules for mathematics?

This question appears totally impervious to alternative foundational  
schemes. And I have never seen any advance on this spectacularly  
relevant question from anyone other than the usual suspects in f.o.m.
>
> Another critical point, that I would like to make, concerns the  
> axiomatic method used in ZFC and more generally in FOM in your  
> sense. This method relies onto a strong epistemic assumption  
> according to which Logic is an ultimate foundation of any  
> mathematical theory. Historically speaking this is an old idea  
> dating back to Aristotle and then pushed forward by Schoolmen in  
> their attempts to make science, in particular make physics. The  
> relative in-success of the scholastic science and the great success  
> of the modern science and the modern maths that gave up the old  
> aristotelian approach is a strong historical evidence  that there is  
> something fundamentally wrong in the aristotelian approach. I don't  
> believe that the replacement of the traditional aristotelian by the  
> modern FOL solves the problem. There are understandable historical  
> reasons why this rather old-fashioned epistemic approach has been  
> retaken in maths of the beginning of the 20 century but in my  
> understanding today it becomes more and more clear that it was a  
> wrong strategic decision. The relative in-success to extend FOM to  
> science seems me to be an evidence for it. This issue, of course,  
> requires a more systematic philosophical argument, which cannot be  
> given here.

I am completely committed to the supreme robustness of first order  
predicate calculus with equality. This is on a par with, say, the  
ordered field of rational numbers. Granted, the latter is more  
essential in the Mathematical Life, but the former drives the  
Foundational Life.

I do not believe that this has anything to do with the lack of  
appropriate development of foundations of physical science. Major new  
elements need to be injected into logic, but this does not reflect  
negatively on the first order predicate calculus with equality.

> My final remark concerns the idea formalization. In my understanding  
> a formal mathematical theory is a mathematical model of a  
> mathematical theory rather than mathematical theory proper. The  
> impressive development in logic and in particularly in FOM in your  
> sense is due mainly to the idea to apply maths to logic rather than  
> to the idea to apply logic (let alone Logic) to maths. In particular  
> it allowed to give precise mathematical answers to questions about  
> (in)completeness that you stress in your slides. However these  
> mathematical answers are all given by means of the "usual" maths  
> (please correct if I'm wrong); what is unusual in such a  
> mathematical study is rather its object (a formal theory) rather  
> than its method. This leaves the following questions wholly open:  
> what is the evidence that formal theories are adequate models of  
> informal theories; what are criteria of such an adequacy?

I am interested in the above paragraph, but I don't think I understand  
what you are saying well enough to comment. It would if you could give  
multiple examples of what you are talking about. I think you clearly  
have multiple examples in mind, so this should be easy for you.
>
> It is surprising that in spite of so many fundamental disagreements  
> with your approach to FOM I readily agree with more specific things  
> that you say in your slides, in particular about the usefulness of  
> proof assistants.

And maybe here you would take my side against Angus.
>
> Thanks so much again for your arguments that make me react so  
> extensively! Unfortunately I didn't manage so far to get access to  
> Angus's slides, otherwise I could comment more precisely on your  
> exchange.

It's too bad that they are apparently not yet available. I also want  
to take a good look at them.

Harvey