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

Tue Apr 5 13:58:03 EDT 2016

> On Apr 1, 2016, at 02:02, Harvey Friedman <hmflogic at gmail.com> wrote:
> 
> c. FOL= should be for free on the following grounds. It is utterly
> fundamental to the whole of deductive thought, whether in mathematics
> or not in mathematics.
> 
> d. This raises the crucial question of whether there is some analog of
> FOL= living in seriously alternative foundations, that is also utterly
> fundamental to the whole of deductive thought, whether in mathematics
> or not, and whether if we also charge nothing for it, then the
> alternative foundations will be as simple as ZFC.

I think this is a fundamental question for HoTT/UF. I don’t think it’s necessarily a problem for HoTT/UF, but it is an interesting challenge, and it will be interesting to see if it can be met. It is also a good way of making more precise the demand for “philosophical coherence”. Allow me to rephrase the “challenge” hopefully in order to discuss it:

CHALLENGE: What are the “core” principles of reasoning on which HoTT/UF is based? Are they distinct from FOL=? Are they as “fundamental to the whole of deductive thought” as FOL=?

Some thoughts:

1. One possible answer is that it is the kind of reasoning employed in laying out Martin-Lof’s meaning explanation [1]. Specifically, the kind of reasoning that is employed in pp.33-50 of [1]. But this is not very satisfactory. Firstly, Martin-Lof’s meaning explanation cannot in any straightforward sense be extended to HoTT. Secondly, the reasoning in pp. 33-50 of [1] looks very much like standard FOL=. Thirdly, it is unclear whether it would ever be satisfactory to have the “core” principles of reasoning of any type theory be untyped.

2. A common response to the CHALLENGE is to point out that in MLTT-style systems there is no rigid separation between the language and the axioms (equivalently, between logical and non-logical symbols). As such, there are no “core” and “non-core” principles of reasoning. There are are rather deductive rules handling judgments, and that’s it. 

But I think this misses the point. Exactly *what* a well-formed judgment is and exactly *how* to form them does not come for free (or it comes for free only insofar as FOL= comes for free). There is a certain non-trivial logic that handles the formation of judgments. Indeed this logic also includes an equality (judgmental equality). And if this “logic” cannot be anything other than FOL=, then Friedman’s point seems to me a very powerful one. It would seem to indicate that (up to interpretation) HoTTs will always live in some standard foundation.

In these terms, the CHALLENGE would be to give a non-FOL= logic for forming judgments which are then handled by the rules of the deductive system. This would give a fully geometric HoTT. (I believe this is possible, and also a worthwhile goal.) But then one would also need to argue that this “logic” is “fundamental to the whole of deductive thought”.

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? 

(4. It also doesn’t really help with the CHALLENGE to note that FOL= can be recovered inside HoTT because what one recovers uses only the internal identity.)

And if all this has become too philosophical and vague, then there is a very concrete related formal aspect to this problem, namely:

FORMAL CHALLENGE: Define what it is for a type U to be a model of HoTT in HoTT

There are many ways to make the FORMAL CHALLENGE precise, e.g. Mike Shulman in [2]. 

In my opinion this is not a permanent defect of HoTTs. But it shows that the “correct” HoTT has yet to be defined. The “correct” HoTT would be one in which the metatheory of HoTT can be carried out just as naturally as the metatheory of ZF(C) can be carried out in ZF(C). And to define such a correct HoTT it seems to me crucial to have in hand some good answer to the first CHALLENGE.

Relatedly, on Google+ Friedman wrote:

Of course, cardinality plays a significant role in standard f.o.m., and CH (continuum hypothesis) is an extremely natural question from the general set theoretic point of view. I was wondering whether it or something like it arises as an extremely natural question in seriously alternative f.o.m. environments?

The FORMAL CHALLENGE is very much related to the so-called “definability of (semi-)simplicial types” and I have often thought the latter to bear some resemblance, as a problem, to CH in standard foundations. Firstly, it is a very natural question that has proven very difficult to settle. Secondly, there are straightforward ways to “settle” it by adding new features (extra identity types) but there is not (yet) a proof that in certain systems it is impossible. 

Dimitris

[1] http://www.pps.univ-paris-diderot.fr/~saurin/Enseignement/LMFI/articles/Martin-Lof83.pdf <http://www.pps.univ-paris-diderot.fr/~saurin/Enseignement/LMFI/articles/Martin-Lof83.pdf>
[2] http://homotopytypetheory.org/2014/03/03/hott-should-eat-itself/ <http://homotopytypetheory.org/2014/03/03/hott-should-eat-itself/>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20160405/3997780a/attachment-0001.html>