Adequacy Conditions on a Foundation
I'm interested in the recent claims about Homotopy Type Theory, HoTT, being a foundation of mathematics. For example, Frege, Cantor, Russell and Zermelo did provide foundations for (parts of) mathematics. But what did they do? What is a foundation?
First, here's a proposed list of five adequacy conditions for a claimed foundation $F$ for mathematics:
Usually, mathematicians have taken $ZFC$ (or something similar, perhaps weaker, or perhaps stronger, like $MK$) as their favourite foundation and teach it to first-year maths students throughout the world (Boolean operations, pairs, relations, functions, the natural numbers, ordinals, sequences, etc., etc). Here are the reasons for this:
However, $ZFC$ violates the Structural Invariance criterion: One can certainly reduce, e.g., arithmetic, analysis, etc., to $ZFC$ successfully (to $Z$ in fact). But these reductions are "implementation-dependent". If one is inclined towards structuralism, then this implementation-dependence is an unhappy state of affairs. (However, having said that, I think that one can remedy this defect by adding abstraction principles for particular kinds of mathematical object, as sui generis entities.)
Does HoTT satisfy these criteria? First, it aims to satisfy Structural Invariance: this is the point of the Univalence Axiom. And it seems to me that it also satisfies Interpretability Strength, as the new book shows in detail. But it also seem to me that it fails the criteria of Austerity, Non-Circularity and Justification.
First, here's a proposed list of five adequacy conditions for a claimed foundation $F$ for mathematics:
(Austerity) $F$ is conceptually austere.This is a rough proposal, and these may not be necessary and/or jointly sufficient. And there are matters of degree here too.
(Non-Circularity) $F$ is conceptually non-circular.
(Justification) $F$ has an intuitive epistemic justification.
(Interpretability Strength) $F$ has high interpretability strength.
(Structural Invariance) $F$ should characterize certain structures only "up to isomorphism".
Usually, mathematicians have taken $ZFC$ (or something similar, perhaps weaker, or perhaps stronger, like $MK$) as their favourite foundation and teach it to first-year maths students throughout the world (Boolean operations, pairs, relations, functions, the natural numbers, ordinals, sequences, etc., etc). Here are the reasons for this:
- $ZFC$ is conceptually austere: its sole primitive concepts are $\in$ and $=$.
- $ZFC$ is conceptually non-circular: one does not assume the axioms of arithmetic, analysis, etc. One proves the axioms of arithmetic, analysis, etc.
- $ZFC$ has some kind of intuitive epistemic justification: one can have an intuitive picture of the cumulative hierarchy $V = \bigcup_{\alpha \in ON} V_{\alpha}$.
- $ZFC$ has high interpretability strength: $ZFC$ interprets pretty much everything. If you want more, move to $MK$ or add large cardinals.
However, $ZFC$ violates the Structural Invariance criterion: One can certainly reduce, e.g., arithmetic, analysis, etc., to $ZFC$ successfully (to $Z$ in fact). But these reductions are "implementation-dependent". If one is inclined towards structuralism, then this implementation-dependence is an unhappy state of affairs. (However, having said that, I think that one can remedy this defect by adding abstraction principles for particular kinds of mathematical object, as sui generis entities.)
Does HoTT satisfy these criteria? First, it aims to satisfy Structural Invariance: this is the point of the Univalence Axiom. And it seems to me that it also satisfies Interpretability Strength, as the new book shows in detail. But it also seem to me that it fails the criteria of Austerity, Non-Circularity and Justification.
Thanks for bringing up these questions!
ReplyDeleteHere are my thoughts...
Austerity of HoTT is debatable but this is an acceptable loss for HoTT. In fact, it takes a moderately strict sense of austerity to claim that HoTT is not austere.
HoTT is indeed conceptually non-circular. (I wish this were more obvious since the topological inspiration is still very present in a lot of HoTT literature.)
I haven't seen a good epistemic justification of HoTT but I'm willing to believe there will be one in the near future... That will take much more work than the cumulative picture of ZFC.
Interpretability strength is the major issue. Prima facie, univalence seems to clash with strong set-theoretic hypotheses. Is HoTT consistent with the existence of a countably complete ultrafilter on a set? Elementary embeddings are pretty scary beasts in the presence of univalence.
Of course, HoTT does great with structural invariance, that's the major strength of HoTT! The question is whether the price to pay is too high. Some loss of austerity is acceptable loss but any loss of interpretability strength is not acceptable. We will have to wait for some of these answers...
Thanks for your thoughts. It's good to have comparisons/alternatives to make sense of what one already has!
ReplyDeleteBeyond "core mathematics", inside $V_{\omega + 3}$, say, Interpretability may be an issue for HoTT for the reasons you say. Another concern I have is that HoTT might be argued to violate Non-Circularity in its treatment of arithmetic, which is added "by hand". In contrast, within Fregean logicism, one proves the axioms of arithmetic from the cardinality principle: and with axiomatic set theory, one proves the axioms of arithmetic (under some convenient interpretation, like von Neumann's).
But this is all up in the air, I guess, at the moment!
Cheers,
Jeff
Indeed, the treatment of arithmetic in the book is synthetic since $\mathbb{N}$ is posited to satisfy the axioms. However, there is an alternate presentation via Church numerals (as is done in the $\lambda$-calculus). Then the axioms can be proved from basic concepts and the mapping of $\mathbb{N}$ to Church numerals provides a non-circular justification for $\mathbb{N}$.
ReplyDeleteIt is an interesting feature of univalence that constructions are ultimately irrelevant. This leads to the idea that objects can be "synthesized" just by stating the final goal (provided these goals are suitable). This is not necessarily a bad thing. For example, I think I would have preferred the treatment of real numbers in Chapter 11 to be fully synthetic rather than formalizing the Dedekind and Cauchy constructions.
Best,
François
François, yes, right - I'd forgotten the details of Church's type theory, which I haven't looked at for years, so checked up again earlier and was going to add a question about why Church numerals weren't used instead for arithmetic. But I assume the approach in the HoTT book is used because it follows Martin-Löf's approach more closely.
ReplyDeleteSo, I guess, for the real numbers, instead of Dedekind sections, etc., the synthetic approach would start with the complete ordered field axioms, and these would be stated axiomatically in some way? But the construction plays an epistemic role, in convincing us that there is at least one system with the desired properties.
Cheers,
Jeff
When you say that ZFC has an epistemic justification, are you saying that inductive definitions (inductive types?) are intuitively clear?
ReplyDeleteIn the book we construct a model of set theory in homotopy type theory using higher inductive types. We observe the resemblance with Conway's permissible constructions (from On numbers and games):
* Objects may be created from earlier objects in any reasonably constructive fashion.
* Equality among the created objects can be any desired equivalence relation.
Conway's constructions seem easier in type theory than in ZFC.