Dramatic Foundational Revelations

[Harvey Friedman]

>From Tim Chow, May 24 15:50:10 EDT 2022.
https://cs.nyu.edu/pipermail/fom/2022-May/023350.html

Harvey Friedman wrote:

>* Furthermore, at least so far, category theory hasn't even been useful
*>* for ANY of our dramatic foundational revelations, of which we have a
*>* few. The really useful tool for uncovering the dramatic foundational
*>* revelations has always been through the usual standard classical set
*>* theoretic foundations.
*
Chow wrote:

While it might not count as "dramatic," the fact that a certain segment of
homotopy theory ("synthetic" homotopy theory), which at first glance seems
to require rather strong set-theoretic axioms to formalize (universes),
actually requires much less proof-theoretic strength (some kind of
Martin-Lof type theory or Kripke-Platek set theory) was discovered by
thinking hard about foundations from the point of view of higher category
theory and type theory.

******************

I like my phrase "dramatic foundational revelations", and that purposefully
puts the standard of what I am talking about rather high in the realm of
foundational advances.

This has suggested to me to start a series called DRAMATIC FOUNDATIONAL
ADVANCES. When I support items as dramatic foundational advances, it forces
me to present a vision of what f.o.m. is really after and what has been
accomplished. And when I reject items as dramatic foundational davances, it
also is very revealing as to what I see as the main goals and achievements.

Here is a short list of dramatic foundational advances that I compile here,
without thinking too deeply for thoroughness. This will give readers an
idea of what league we are talking about.

I am sure I have probably left out stuff that maybe even more deserving
than what I wrote.

In no particular order. Ordering these requires much more work and may not
work well. I don't know at this stage.

1. Delineation of purely logical proof, via predicate logic.
2. Formulation of the gold standard f.o.m. via ZFC.
3. Semantics and completeness of predicate logic.
4. Incompleteness of ZF(C) for fundamental set theoretic problems.
5. Formulation of fundamental extensions of ZFC via large cardinal
hypotheses.
6. Use of large cardinal hypotheses and their correspondence with
fundamental descriptive set theoretic problems.
7. Use of large cardinal hypotheses and their correspondence with
essentially finitistic statements in the core mathematics tradition.
Embedded Maximality. Nearing completion.
8. Development of models of computation and their equivalences, via Turing
et al and String Replacement..
9. Reverse Mathematics and Strict Reverse Mathematics.
10. The standard hierarchy of logical strengths and observed linearity.
11. The essential role of impredicativity for celebrated discrete
combinatorial mathematics, via tree embeddings and graph minors.
12. Interpretations, Relative Consistency, and their equivalence.
13. Formulations of intuitionistic logic and the disjunction and existence
properties.
14. Formulations of intuitionistic systems and their disjunction and
existence properties.
15. Completeness of axioms for real and complex algebra.
16. o-minimality and real algebra with exponentiation.
17. Embeddings of fundamental mathematical structures corresponding with
lage cardinal hypotheses.

These developments 1-17 have a certain kind of universal
mathematical resonance that is apparent. The developments surrounding type
theory and synthetic homotopy theory alluded to by Chow above, as well as
related matters, is not close to being included in such a list. Even any
kind of type theory is a specialized subject whose fundamental value is
still in question, without real universal resonance. E.g., see
http://aitp-conference.org/2018/slides/JH.pdf  for a reconsideration of its
value even for a particularly highly developed and highly touted purpose.

Harvey Friedman
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20220531/d027456d/attachment-0001.html>