[FOM] foundations meeting/FOMUS/discussion

[Bruno Bentzen]

Harvey Friedman:
> A FOUNDATION FOR MATHEMATICS
> There is a standard classical meaning for this. Namely, to provide a
> precise "workable" rule book for mathematical "activity", that
> provides suitable criteria for "correctness" or "legitimacy".

If I am interpreting you correctly, a key aspect of a foundational theory's "philosophical coherence" would be the question - perhaps motivated by Wittgenstein's famous slogan "meaning is use" - of whether or not it is compatible with the way mathematics is done in practice. In this sense, I think that the set-theoretical approach has some drawbacks.

It turns out that in practice mathematicians often identify two structures whenever they are isomorphic. This is clearly in conflict with set-theoretic foundational theories such as ZFC, since, for example, if A \cong B and \empty \in A then in general \empty \notin A.

Harvey Friedman:
> I favor the approach of carefully adding a lot of sugar to ZFC, rather
> than bringing in foreign elements or replacing aspects of ZFC.

I believe this issue is not a matter of adding more "sugar" to ZFC or other set theory, it is a limitation of the very set-theoretical framework, since equality, as given by the axiom of extensionality, is a much stronger requirement than isomorphism.

In contrast, this idea can be embodied within type theory. It is (roughly) the univalence axiom: two structures are equal if they are isomorphic.This is made possible by the fact that type theory, like category theory, has the nice property that every definable predicate of in the system is isomorphic-invariant. Therefore, HoTT admits a structuralist (and constuctivist) foundations of mathematics.

Harvey Friedman:
>>> Among the obvious merits of ZFC as a foundation for mathematics, there
>>> is one that I often see not sufficiently emphasized. That is, its
>>> PHILOSOPHICAL COHERENCE.
>>>
>>> ../..
>>>
>>> But my impression is that the more radical proposals, particularly
>>> HOTT, philosophical coherence is proudly thrown away.
>
> That is my understanding, which may or may not be correct. (However,
> see below for a pointer to an internet manuscript ).This certainly
> prima facie precludes HOTT as any kind of reasonable "foundation for
> mathematics" in any standard sense.

In this respect, I cannot easily understand why HoTT would lack of "philosophical coherence" while ZFC would not.

I am learning a lot with this great discussion, however, I think we cannot objectively move forward with it since a better clarification of the word "philosophical coherence" is obviously required.

Bruno Bentzen
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160325/32d568a9/attachment-0001.html>