[FOM] "Salvaging" Voevodsky's talk

[Daniel Mehkeri]

Neelakantan Krishnaswami writes:
 > Voevodsky is coming to type theory from the point of view of a
 > homotopy theorist. The traditional set-theoretic formulations of that
 > subject make use of Grothendieck universes, and so go beyond
 > ZFC. However, the big discovery of his univalent foundations project
 > is that homotopy theory has a natural formalization in Martin-Lof type
 > theory, which has the proof-theoretic strength of Kripke-Platek set
 > theory (ie, vastly less than ZF). (IIRC, Anton Setzer has written a
 > survey paper on this, "Proof Theory of Martin-Lof Type Theory: an
 > Overview".)

 > Generally, it's no surprise when a theorem can be encoded in a weaker
 > foundations, but the real shocker behind homotopy type theory is that
 > a suitable type-theoretic view seemingly requires *fewer* encoding
 > tricks than the traditional view. The apparent need for large
 > constructions vanishes because the type structure of type theory
 > prevents you from performing constructions which are okay on points
 > but which fail to respect geometrical invariants like continuity.  As
 > a result, you can now talk about plain old functions instead of
 > natural transformations on sheaf categories or whatever.

 > So even if the worst fears of the predicativists are true and ZFC is
 > inconsistent, the homotopy type theory crowd can make the argument
 > that homotopy theory is still a coherent subject.

The homotopy interpretation is quite elegant.

Had Voevodsky said instead "what if ZFC is inconsitent" then no doubt 
this would have been a different conversation on FOM. But none of the 
above seems to be of any help if Peano/Heyting arithmetic is 
inconsistent. (Mind you, ex falso quodlibet. If PA is inconsistent, then 
Voevodsky's programme is the best hope for mathematics, moreover I am 
the walrus.)

Also, I counterclaim that the coherence of constructive type theory 
comes more from the constructive bit, and not so much from the type 
theory bit.

In this regard I would point out that CZF is a system of constructive 
set theory that is also equiconsistent with Kripke-Platek set theory 
(and ID_1; their proof-theoretic ordinal is the Bachmann-Howard ordinal).

CZF plus the Law of the Excluded Middle (LEM) has the same theorems as 
ZF. Indeed its axioms are close to those of ZF. I could spin this as: ZF 
(therefore ZFC) is inconsistent if and only if CZF refutes LEM. So in 
the event ZFC falls, the set theory crowd can also claim theirs is still 
a coherent subject, just that LEM has been refuted.

Moreover in CZF we also talk about plain old sets and functions just as 
we do classically. And Grothendieck universes, for that matter - adding 
a proper class of those to CZF still remains in the (generalised) 
predicative realm.

Conversely, if you add LEM to even simple constructive type theory (such 
as HA^omega, and Voevodsky is using more than that), then it already 
interprets fully impredicative n'th order arithmetic.

So discarding LEM seems to be necessary as well as sufficient, and the 
type-theoretic versus set-theoretic question not so important.

Daniel Mehkeri