[FOM] Friedman's challenge on HoTT-analogs of FOL=

[Harvey Friedman]

On Tue, Apr 5, 2016 at 1:58 PM, Dimitris Tsementzis <dtsement at princeton.edu>
wrote:

>> 3. Another, equivalent, way to put the CHALLENGE is this: it seems the
>> only way we have of formalizing the syntax and deductive systems of HoTTs
>> themselves is as first-order theories, namely as strings of symbols defined
>> and manipulated using first-order axioms. Which leads to the question: Can
>> there be a non-FOL=-based method for manipulating strings of symbols?

On Wed, Apr 6, 2016 at 2:18 AM, Mario Carneiro <di.gama at gmail.com> wrote:
>
> It's a little beside the point for the main thrust of this post, but this
> sentence struck me, because this is exactly what Metamath is: a
> non-FOL=-based method for manipulating strings of symbols.
>
> To summarize, in Metamath there are expressions, which are strings of
> constants and variables, and the only primitive is the direct substitution
> of an expression for the variables in another expression, subject to
> disjoint variable conditions (which say that the substitution may not
> contain an "x" in the string anywhere). That's it. There are no bound
> variables or proper substitution, so it is much closer to a string rewriting
> system than FOL. Nevertheless, one can add axioms within this system
> defining the meaning of implies, not, forall and out pops FOL. Or you can
> add axioms for definitional equality and type judgement, applications and pi
> types and lambdas, and the inductive types and univalence, and out pops
> HoTT.
>
> While I don't know whether it would be wise to point the full brunt of
> cross-examination from FOM at Metamath, it is clear to me that in a
> practical sense Metamath is a candidate for foundations of mathematics, that
> is not FOL-based. (I don't know much about Isabelle/Pure, but I think it
> could also stand in here.)
>
I am skeptical that various people are really using the phrase
"foundations for mathematics" or "general purpose foundations for
mathematics" in the same way that I am using it.

I don't think that there has been much (convincing) effort to
abstractly define what we mean by a "general purpose foundation for
mathematics".

There are a couple of good reasons why this is the case. One is that
this is rather challenging to do well. Another is that, at least until
recently, there have been no claims of any seriously alternative
foundations for mathematics.

Now that there are starting to be various claims by various people of
seriously alternative foundations for mathematics, it may be timely to
get much more clarity as to what general purpose foundations for
mathematics is, at least in much greater depth than the usual standard
phrases.

In standard foundations for mathematics, there is a deep complex web
of reinforcing ideas that reflect an amazing amount of philosophical
coherence and robustness from first principles. And the major moves
are fully reflected in the way one normally conceives of and casts
even the Princeton University Undergraduate Mathematics Curriculum.

Now the typical readers of the FOM know pretty well how I would, or
they would, present a fairly brief philosophically coherent account of
the standard f.o.m,, together with some absolutely remarkable
reinforcing results of great clarity and obvious significance,
etcetera. A very clear and convincing account that is readily
digestible even by intellectually astute people of limited
mathematical experience can be given even in one or two reasonable
length FOM postings. I am of course referring to the top top top stuff
of all time in standard f.o.m. A more detailed picture would of course
take many FOM sized posts.

I don't think FOM readers are particularly interested in me giving an
appropriately serious account of standard f.o.m. in one or two FOM
postings. However, I think FOM readers would be much more interested
in seeing appropriately serious accounts of seriously alternative
foundations for mathematics in one or two FOM postings.

Then, after this is fleshed out some, it would make sense for me to
give one for standard f.o.m. so that we can compare them.

Harvey Friedman