[FOM] HoTT unresponsiveness

[Joseph Shipman]

This is helpful.

It does appear that HoTT can be described as "categorial foundations done right".

However, I think I perceive the same kinds of "category errors" (in the sense of analytic philosophy not category theory) that the categorial foundationists were making.

There are emotional and aesthetic objection to the ZFC foundation as commonly presented which are quite forceful and which I do not disparage. Specifically, its replacement of the earlier strong notion of "type" with the  weaker notion of "rank" and its promiscuously incestuous fraternization of elements of different ranks in the same sets in order to develop basic definitions offends an innate sense of order and propriety for some mathematicians, which explains why they joshingly refer to the set-theoretic membership relation as "evil".

The errors here are confusing mathematics with metamathematics, confusing pedagogy with practice, and confusing scaffolding with structure.

I have repeatedly made the point that mathematics as commonly practiced is more naturally formalized in a  version of set theory which contains the integers as urelements and a primitive ordered pair relation and builds functions and relations of all arities into the language.

It is possible to go further, taking the rationals or real numbers as urelements and having even more of the standard set-theoretic relations be primitive rather than defined, but what I have described already eliminates almost all the "offensive" features of ZFC, while being easy both to formalize in the predicate calculus and first-order logic (the "true foundation" of mathematical reasoning in my opinion), and to prove equivalent in a strong sense to the traditional ZFC axiomatization.

The usual ZFC presentation with its finite ordinals and Kuratowski ordered pairs is valuable for its METAmathematical properties, but after you establish the basic development once and for all in half a semester, you (if you are an "ordinary mathematician") work from then on in an informal system like I described above, confident that your proofs are capable of complete formalization in pure ZFC in principle. 

I do not find the traditional ZFC development to be pedagogically unsound because I actually LIKE seeing everything develop from the most primitive notions and find the mingling of ranks to be exciting rather than perverse, but I respect that many have a different reaction and should have access to an alternative development which doesn't attempt to start from pure membership and the empty set, so that their pedagogy can be closer to their practice.

However, they in turn should recognize that the machinery of ZFC is primarily a scaffolding to allow the absolutely rigorous development of results like "the real numbers are an ordered field with the least upper bound property", from which the rest of mathematical analysis can then proceed  without ever going back to Kuratowski ordered pairs and finite ordinals. Mathematicians informally use a "type theory" involving finitely iterated powersets of the real numbers, and really there should be no religious dispute about foundations if this is as far as they needed to go. 

(By the way, "high school foundations" where reals are defined in terms of infinite decimal expansions, 0.9999... is identified with 1, and the least upper bound property is proved very easily by constructing the bound one decimal place at a time, are both intuitive for almost everyone and perfectly adequate to build rigorous analysis on, the stakes in this dispute are not as high as people here like to make out.)

The dispute becomes relevant when you need to go beyond finitely iterated powersets of the real numbers. I'm willing to listen to the HoTT theorists here, but they ought to explain how they intend HoTT to replace ZFC if the objective is to develop standard mathematics in a completely formalizable and rigorous way.

As I ask again, is HoTT superior to ZFC in enabling one to reach the Prime Number Theorem? What about the fundamental theorem of calculus? What about the graph minor theorem? What about Perelman's results?

I want to lower the temperature of the discussion and reduce the stakes here. All the results I named are proven without any need to go beyond finitely iterated powersets of the reals. How do we replace ZFC with HoTT and then get to them?

One final question: in an HoTT framework, is the computability of homotopy groups of finite simplicial complexes easy to establish? That strikes me as the perfect test case, because the only proof I know of this result involves lots of technical machinery in manifold theory such as Postnikov towers and so on.

-- JS

Sent from my iPhone

> On Oct 28, 2014, at 7:27 AM, Paul Levy <P.B.Levy at cs.bham.ac.uk> wrote:
> 
> 
>> Date: Sun, 26 Oct 2014 22:41:04 -0400
>> From: Joseph Shipman <JoeShipman at aol.com>
>> To: Foundations of Mathematics <fom at cs.nyu.edu>
>> Subject: [FOM] HoTT unresponsiveness
>> Message-ID: <22A397EE-B833-47C8-9933-F7C413EC9CD5 at aol.com>
>> Content-Type: text/plain;    charset=us-ascii
> 
>> 4a) is there any theorem in HoTT, no reasonable equivalent of which can be STATED in ZFC?
> 
> "Every endofunction on the universe of sets extends to an endofunctor on the groupoid of sets and bijections."
> 
> This statement is PROVABLE in HoTT and some other systems.
> 
> It is REFUTABLE in ZF with universes, NBG and some other systems.
> 
> Take your pick.  Personally I prefer it not to be a theorem, but I can understand why some people would take a different view.  It's a tricky philosophical question about the very nature of sets.
> 
> Paul
> 
> 
> --
> Paul Blain Levy
> School of Computer Science, University of Birmingham
> +44 121 414 4792
> http://www.cs.bham.ac.uk/~pbl
> 
> 
> 
> 
> 
> 
> 
> 
> 
>