[FOM] 461: Reflections on Vienna Meeting

[Andre.Rodin at ens.fr]

Harvey:

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

 Everyone who has a project  tends to describe it as "vastly superior" w.r.t.
projects of concurrents and may also argue that since the number of people
involved in this particular project is "incomparable smaller" than the number
of people involved in concurrent projects one's project makes a better job for
less money. This makes such arguments uninformative.

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

The first association that came in my mind when I first read this title was
German Lebensphilosophie of the 19th century. Next came computer games and
Aristotle's expression "bios thewretikos", the Theoretical Life. Perhaps my
background is not statistically typical (I assume that nobody on this list is
typical in this sense) but in any case external people will read the title in
their own weird manners. Such things happen with all titles, this is how the
natural language works and as I have already argued in an earlier message this
feature may help a rational discussion if it is used properly.

Distinguishing between true fom and fake fom and, more generally, between true X
and fake X is the most archaic dialectical scheme widely used by Plato and
brilliantly criticized by Popper (in the "Open society"). I don't now argue
that what you qualify as fake fom is true fom but reject this dialectical
scheme that gives to names and titles more power than they should have in a
rational discussion.


>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.
>I understand that. I speak about "your" fom only for brevity here. And I don't
want to use for it the title of fom without specification.




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



That's interesting and important point. Category theory may be helpful to make
the notion of interpretation more precise. Here is a very simple example.
Suppose that A is interpretable as B. In eyes of many this implies some sort of
equivalence of A and B. But think about this interpretation as a morphism m.
There is a natural notion of equivalence in this case only when m is
invertable. But generally it is not. Now consider a stronger condition: A is
interpretable as B and B is interpretable as A. The existence of these
reciprocal interpretations strongly suggests that A and B are equivalent. But
what you need for m be inversible is something much stronger: that the two
interpretations exist AND cancel each other on BOTH sides.
The moral is that the interpretability of one theory in another is a rather weak
relation. Category theory is interpretable in Set theory and Set theory is
interpretable in Category theory. However important are those facts they are
not sufficiently informative for deciding whether categories or sets are good
foundations.

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

yes, but item 2 is also compatible with the claim that set theory doesn't
qualify as a foundations of contemporary maths.


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

I agree that the issue depends on what qualifies as foundations. Clearly we have
different views about it.


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

I agree that the existing philosophical argumentation supporting this claim
needs an improvement . However the previous item seems me both more difficult
and more important in this debate. I agree that categories cannot play the same
foundational role as sets, so I don't think that categories may simply
"replace" sets. But I believe that the notion of foundation coming with the
claim that sets are foundational is not an appropriate notion of foundation -
or at least not the "principle" notion of foundation. The same strategy of
distinguishing between foundations proper and organizational foundations or
foundations qualified in some other special way may be used both pro and contra
set-theoretic foundations. The question is which foundations are *proper*
foundations. Once again I don't think that distinguishing between "X proper"
and "such-and-such X" is a good conceptual framework for discussing
foundations.


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

Clarity is a rather unclear concept. It may deceive easily. It may be
psychological. Descartes noticed that most clear ideas are not, generally, the
most "distinct" and vice versa.


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

A historically important example of clarification of a theory by using
categories was Eilenberg&Steenrod book on foundations of homological algebra. I
realize that you don't take this as an evidence of the foundational
significance of categories.


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

Right. This is because in order to take this question and meaningful and
moreover as important one needs to assume basics of what you call "traditional
f.o.m." (which is again a strange title but let's leave titles aside). Namely,
one needs to assume that there is something like "usual axioms and rules for
maths". I don't think that maths as it actually practiced can be presented as
an axiomatic theory with certain axioms and rules. I think that there is a deep
problem about the relevance of the "usual" axiomatic method.



>I am completely committed to the supreme robustness of first order predicate
>calculus with equality.

This strikes me as an adherence to an Aristotelian approach to maths that, as
the history of maths (in my understanding) demonstrates, was never successful
neither in maths nor in natural science. This concerns the commitment to a
certain fixed system of logic, be it the first order predicate calculus with
equality or any other.


>>My final remark concerns the idea formalization. ...

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

I have in mind Cohen's forcing among other things. Cohen works with axioms and
models of ZF as with objects of his theory and construct new objects (most
importantly new models of ZF) with desired properties out of them. He does this
with a clever mathematical trick, which is similar to some other tricks used by
mathematicians in other areas of maths: as Cohen notices himself forcing is
similar to a field extension through adjunction of a radical - like the
extension of rational numbers with sqrt(2). All of this is a part of "usual"
maths that doesn't develop itself by making inferences from a given set of
axioms. What is specific in this mathematical study is what this study studies:
a formal theory and its models. Cohen's paper contains a mathematical theory
(or at least a fragment of a mathematical theory). Formal theories are to
Cohen's theory what circles and triangles are to Euclid's geometry and what
rational numbers and sqrt(2) are for early modern algebraists. Next comes the
idea that formal theories in some sense may represent or model mathematical
theories. Cohen's work and other similar studies (including all recent studies
in Set theory about which I'm aware - which is admittedly is only a very small
part of the current literature) don't provide any support to this next idea.
Cohen's own way of doing maths looks very unlike making inferences from a set
of axioms. So I'm asking for a justification of this idea. I suspect that this
idea is fundamentally wrong. The fact that Cohen's theory in its turn may be
*interpreted* or *represented* as a (fragment of) formal theory doesn't seem me
to be a strong argument. My guess is compatible with all technical results in
fom about which I know (which again is a small part). Moreover I can hardly
imagine how *any* technical result of this sort (I mean achieved within a
mathematical study like Cohen's) can have a bearing on this question (albeit I
don't rule out the possibility that it can). My guess is NOT compatible with
some bold philosophical claims about fom but I don't take such claims to be
justificatory.


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


Perhaps. He doesn't like proof assistances, does he? Why?

Andrei