Non-foundationalist foundational thinking

Wed Jun 8 08:00:28 EDT 2022

Harvey Friedman wrote:

"One question I have been asking is whether type theory or category theory
can provide any satisfactory form of Goedel's Second Theorem. With Goedel's
First Theorem, there has been no problem. But several of the leaders in
Category theory and Type Theory today say they have no insight as to how to
look at Goedel's Second Theorem categorically or type theoretically."

André Joyal has given a completely satisfactory proof of both Goedel's
first and second theorem categorically using arithmetic universes, where
he's able to mimic the construction of Goedel's sentence and of Con(T) by
internalizing and show that they are not provable if T is consistent. The
same categorical construction for Goedel's first theorem can be used for
Goedel's second theorem. The proof has recently been made available on
Arxiv, and it conclusively shows that the arithmetization of
metamathematics corresponds to internal reasoning in certain categories.

Christian Espindola
Associate Professor
University of la Réunion
Réunion, France

<https://www.avast.com/sig-email?utm_medium=email&utm_source=link&utm_campaign=sig-email&utm_content=webmail&utm_term=icon>
Virus-free.
www.avast.com
<https://www.avast.com/sig-email?utm_medium=email&utm_source=link&utm_campaign=sig-email&utm_content=webmail&utm_term=link>
<#DAB4FAD8-2DD7-40BB-A1B8-4E2AA1F9FDF2>

On Wed, Jun 8, 2022 at 3:46 AM Harvey Friedman <hmflogic at gmail.com> wrote:

> Tim Chow wrote a lengthy FOM posting "Non-foundationalist foundational
> thinking". The posting comes in three parts.
> https://mail.google.com/mail/u/0/#search/tchow%40alum.mit.edu/WhctKKXXJxWwpDfGTWlvBndlqCmSmVnHWFrjDScmGgXzbcpqhCvcvXfKVzlDKbkgFqbgJcG
>
> PART 1/Chow
>
> Tim's notion of "foundational thinking" is "the type of thinking that
> mathematicians engage in when they work on the "foundations of X" where X
> is some specific subfield of mathematics". This is *NOT* a good example of
> what I have in mind when I refer to "foundational thinking". This is
> because a large component of that Tim is referring to involves issues of
> exposition and simplification and effectiveness in presenting proofs, and
> various in house issues mathematicians deal with when they are involved in
> the practical presentation of mathematics to make the exposition clearer
> and more readily understandable.
>
> Tim puts that aside, and focus on his
>
> (*) What is really needed to prove Theorem T?
>
> This is more or less what I wanted to address when I founded RM and SRM
> going way back to the late 1960's and culminating with the founding RM
> papers in ICM and JSL abstracts. RM was not really quite what I was aiming
> for - it really was SRM which at that time was entirely unwieldy and in
> retrospect highly premature. I tamed SRM into RM with those founding
> papers. An in depth account of the history of RM and SRM can be seen at
> https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
>  #117
>
> At that time and actually all the time up thru now, I am a working
> foundational thinker who is most interested in creating illuminating, rich,
> and productive areas of research that advance our knowledge and
> understanding of fundamental ideas and issues of general intellectual
> interest.
>
> Tim's (*) is, or is close to, an example of what I was and still am
> looking for. Of course, it was obvious at the time that nothing even
> remotely like SRM or RM is going to fully deal with (*). For example, what
> is really needed to prove T includes mathematical insights of various
> kinds, some of which are non foundational in any sense of the word. E.g.,
> see Polya's How to Solve It.
>
> It was obvious back then, even to me, that it was much more promising to
> deal with a limited notion of "need" here in order to inspire the creation
> or discovery of SRM and RM. The alternative is to simply stare at (*) and
> not found a remarkable new subfield of mathematics with a seemingly
> compound growth rate of interest and rich discoveries.
>
> So I was and even still am (despite my age) fully aware of such obvious
> points as
>
> "But there is more to the story than
> reverse mathematics, at least as the subject is usually thought of.  When
> I say "what is really needed" I mean to refer to what practitioners
> intuitively feel is essential, and not just to strict logical implication."
>
> Now I challenge Tim to create a significant new subfield of mathematics
> out of his obvious point. If Tim can set up a new subfield dealing with
> this obvious point across mathematics, then I might be the first to want to
> Simpsonize this by jumping on it with abandon.
>
> "reverse mathematics is not the entire story"
>
> I wouldn't exactly call this a revelation. RM is far from the entire story
> even with regard to its focus on strict logical structure that Tim is
> thinking of as "limiting". It uses logically structured base theories which
> SRM seeks to eliminate. I am gauging that the most productive effort in
> this rough area surrounding Tim's (*) above is the proper development and
> launching of SRM. On a related point, RM is far from the entire story in
> that it isn't really dealing with many mathematical objects lying outside
> the scope of the language of Z2, in a fully satisfactory way. I wrote a
> number of FOM postings concerning this.
>
> PART 2/Chow
>
> Tim writes
>
> "I'm going to assume that if you want to reduce all
> of mathematics systematically to indecomposable concepts, and analyze
> questions of consistency and logical strength, then set theory is the best
> way to go.  I make this assumption because I'm about to say some things
> that might superficially sound anti-set-theoretical, and I want to make it
> clear that what I'm about to say is consistent with a belief that set
> theory is the best choice for carrying out a foundationalist project."
>
> Tim emphasizes that the above does NOT imply any of the following:
>
> -All mathematical objects - manifolds, finite simple groups, differential
> equations, categories, etc. --- are "really" sets.
>
> -The foundations of X, where X is a specific subject, are always best
> formulated in set-theoretical terms.
>
> --Set theory is always the best tool for foundational thinking.
>
> Again these are basically obvious. And once again, if Tim can do anything
> with such banalities, in terms of creating new subjects, then I would be
> greatly interested.
>
> In particular, I have never seen an account of what mathematical objects
> "really are" that is even remotely convincing. The claim of set theory here
> is that it is a remarkably philosophically coherent account of a certain
> kind of mathematical object (sets) that can *simulate* the whole range of
> mathematical objects. Furthermore, that this simulation is rather powerful
> smooth and uniform.
>
> This situation is reasonably similar to the situation in theoretical
> computer science. The rough analogy goes like this: Turing machine model of
> computation presents algorithms in a coherent irreducible fashion. We can
> simulate all algorithms in terms of Turing machines - allowing step by step
> building up with TMs calling previous TMs in an hierarchical development.
> And of course, any serious computer scientist is going to say that their
> algorithms are not expressed that way, and not thought of that way at all.
>
> So trying to pull something productive out of Chow's posting, we have the
> projects
>
> a) Formally Expressing Mathematics as It is Thought of by Mathematicians
>
> b) Formally Expressing algorithms as They are thought of my Programmers
>
> The closest subject I know to the first of these is SRM = strict reverse
> mathematics.
>
> As for the second, there are various high level languages, but I think
> that the prevailing view is that there is no really good way of uniformly
> treating all important algorithmic ideas in one subject.
>
> Incidentally, I think that SRM will succeed with a) and something new will
> succeed with b).
>
> At the moment, the only technical tools relevant to the Dramatic
> Foundational Revelations that we have have arisen from the usual f.o.m.
> Because set theoretic foundations is such a popular setup with incredibly
> strong simulation power, it has spurred the development of powerful tools
> to support various Dramatic Incompleteness and non Computability, as well
> as the discovery of candidates for new mathematical axioms of Revelatory
> effectiveness.
>
> One question I have been asking is whether type theory or category theory
> can provide any satisfactory form of Goedel's Second Theorem. With Goedel's
> First Theorem, there has been no problem. But several of the leaders in
> Category theory and Type Theory today say they have no insight as to how to
> look at Goedel's Second Theorem categorically or type theoretically. I
> thought they could do something with my new form of Goedel's Second Theorem
> in
> https://u.osu.edu/friedman.8/foundational-adventures/downloadable-lecture-notes-2/
> #78 The no interpretation form of G2.
>
> PART 3/Chow
>
> True I am a serious advocate of gii = general intellectual interest, and
> in fact I won't invest serious time on any mathematics - or any inellectual
> activity for that matter - without knowing in advance what the gii will be
> if I succeed.
>
> Foundational thinking has an overwhelming gii anywhere, including way
> outside mathematics. Foundational thinking is needed and is very effective
> when it is mastered in diverse areas.
>
> However, foundational thinking has been most highly developed and
> effective in mathematics and computer science. This is a relative
> statement.
>
> For example, foundational thinking in the physical sciences is
> comparatively impoverished. But I maintain that that is not because it
> has to be ineffective. It is because it seems to be much harder to make it
> effective.
>
> Foundational thinking in the physical sciences is, for example, far far
> less developed than was foundational thinking in mathematics before Frege
> with his (admittedly too messy) predicate logic.
>
> Look, I have been involved to some extent with science writers for decades
> writing about my work and others. Almost every one of them has told me that
> the Dramatic Revelations I emphasize with them are of singular general
> intellectual interest compared to the usual things that they write about in
> mathematics.
>
> Now, respecting Tim's distinction between foundational and
> foundationalist, still the foundationalist way of going about foundational
> thinking is, in my view, when properly implemented (very difficult!),
> singularly effective everywhere.
>
> In fact, I would like to think that the foundationalist method was the
> method I used to go from an unnoticeable high school piano player nobody
> would even recommend go to Music School, to an obviously professional level
> classical and popular player who can hold my own now (significantly
> improved from my YouTube recordings a few years back) on a very good day
> with the world's leading players. I am considered self taught (by
> professional standards) and this seems to not be known to have been done in
> classical piano. So I seems like I did this by some special method - a
> method that I think is foundationalist at its core.
>
> Harvey Friedman
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20220608/a0efdf46/attachment-0001.html>