Timeline for Consistency strength of HoTT
Current License: CC BY-SA 4.0
13 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Aug 23 at 16:32 | history | edited | Christopher King |
edited tags
|
|
| Aug 22 at 14:36 | history | became hot network question | |||
| Aug 22 at 12:37 | answer | added | aws | timeline score: 19 | |
| Aug 22 at 2:15 | comment | added | Alec Rhea | I asked a similar question a few weeks back and got some interesting comments and an answer that may be relevant. | |
| Aug 22 at 1:58 | comment | added | Jesse Elliott | Related post to my previous question/comment: mathoverflow.net/questions/425419/… | |
| Aug 22 at 1:38 | comment | added | Jesse Elliott | Is Book HoTT perhaps "re-interpretable" by some class theory like MK (Morse-Kelly) or ACT (Ackermann class theory) or ARC that is more expressive of classes and yet of lower consistency strength? Some class theories are very expressive of classes and, for example, allow for having $P(V)$, $P(P(V))$, etc., where $V$ is the class of all sets, and $P(V)$ is the class of all subclasses of $V$, etc. The blog post linked by @AndrejBauer is very informative. | |
| Aug 22 at 1:24 | comment | added | Andrej Bauer | François G. Dorais wrote a blog post about “ZFC + inaccessibles” a while ago, it might contain relevant information. And I think the discussion therein confirms that having universe $U_n$ indexed by external natural numbers amounts to having (at least) $n$ inaccessibles for every (external) $n$, and not internally having $\mathbb{N}$-many inaccessibles. | |
| Aug 22 at 0:47 | comment | added | James E Hanson | @MikeShulman Do you mean ZFC + 'There are countably many inaccessible cardinals' or do you mean ZFC + $\{\text{‘There are at least}~n~\text{inaccessible cardinals’} : n \in \mathbb{N}\}$? I don't see how you would be able to get the first one in a typical MLTT setup without having a universe above a countable sequence of universes (specifically because of issues with unbounded quantification). | |
| Aug 22 at 0:32 | comment | added | Mike Shulman | However, chapter 10 of the book constructs a model of (intuitionistic) ZF from a type-theoretic universe, which implies that it proves the consistency of ZF and is thus stronger than it. By doing the same construction in higher universes, it should prove the consistency of ZF + n inaccessibles for any finite n. Probably a fancier version of the interpretation, not lying inside any universe, shows that it is mutually interpretable with ZFC + countably many inaccessibles. | |
| Aug 22 at 0:30 | comment | added | Mike Shulman | "Homotopy type theory" is not a specific well-defined formal system, but the name of an entire subject, like "ring theory". The specific formal system used in the HoTT Book is sometimes known as "Book HoTT", but even that is not fully precisely specified since the book doesn't give any general characterization of the class of higher inductive types that are allowed. | |
| Aug 22 at 0:07 | comment | added | Jesse Elliott | Thank you @NaïmFavier. If HoTT can be interpreted in T = ZFC+countably many inaccessibles, that doesn't mean that it can't be interpreted in some theory with sets and classes that is equiconsistent with ZFC. Is there a proof that HoTT is equiiconsistent with T? | |
| Aug 22 at 0:02 | comment | added | Naïm Favier | See math.stackexchange.com/questions/1588578/…. HoTT interprets ZFC; see HoTT book 10.5.11. | |
| Aug 21 at 23:55 | history | asked | Jesse Elliott | CC BY-SA 4.0 |