Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: type theory

Topic: implications of type theory on foundations/finitism/etc.

Verity Scheel (Apr 08 2021 at 22:23):

Feel free to move if this belongs in a different stream!

My understanding is that dependent type theories have been proved to be equiconsistent with set theories like ZF(C), up to some large cardinal axioms / universe assumptions on either side, and inclusion of AC/LEM.

My question is how has this influenced the debate over foundations of maths?

I know some people attack the concept of sets as dubious, of questionable signification, not having meaning “in the real world”. And of course there are debates about infinite sets vs (ultra)finitism. And predicativism (which I do not understand).

But does the existence of computable type theories which are equiconsistent with set theory lend credibility to the claim that these are indeed solid foundations?

In my mind, it does. Constructive type theories give computable descriptions of inductive types and functions between them. The distinction between Prop and Bool seems helpful in addressing some arguments of the describability of sets. With AC, the type theory is no longer fully constructive, but still consistent, and it seems like we can describe most of the types that mathematicians use in some type theory, be it Martin-Löf or HoTT or some other.

So it seems to me that even if sets are not precisely the right objects for describing math, maybe types are a little closer, and sets can’t be too bad because of this close relationship between these formal systems. Still, I have not seen skeptics of set theoretic foundations directly address type theories. So I was wondering if it has shifted the debate at all, or been mostly ignored.

(Note that I want to focus on the logical strength and consistency of these systems, not the issues of how closely they resemble the practice of mathematics or what the right formulation of equality is.)

Cody Roux (Apr 09 2021 at 00:59):

Proving equi-consistency of classical theories with constructive ones does indeed lead credence to the solidity of classical foundations, this was one of the original motivations for Gödel's double-negation translation.

However, this is only part of the story: First of all, just because a classical theory is consistent, doesn't mean that the objects they describe exist in a meaningful sense. This is why one might still subscribe to construcivism, even though most classical theories are equi-consistent with a constructive one. E.g. classical mathematics might prove that one of $\pi+e$ and $\pi e$ is transcendental, without specifying which one. A constructivist might argue that this is not a meaningful proof of disjunction (though they would likely agree to the double negation of such a statement).

The other part of the story indeed concerns finitism/predicativism: most finitists will agree that $$\matrm{PRA}$$ is a reasonable theory, while taking umbrage to 2nd order $\mathrm{HA}$ (Heyting Arithmetic) despite the former being classical and the latter being constructive. The reason for this is that 2nd order Heyting Arithmetic allows full comprehension and quantification over sets of naturals, which allow it to prove, e.g. the termination of system T, while $\mathrm{PRA}$ does not. It really commits to the existence of every subset of the naturals, whether it can be explicitly described or not.

Intuitively, one might decry 2nd order Heyting Arithmetic non-constructive in the following sense: while all the functions it can prove total are technically computable, it is very easy to prove termination of programs which, for all intents and purposes, do not actually terminate from a human perspective. $\mathrm{PRA}$ is much more modest in that regard (though it can still write some pretty crazy functions).

Incidentally, adding LEM and AC to Martin-Löf type theory is very much not conservative. The bool vs Prop distinction is strange that way. MLTT is roughly as strong as $\mathrm{PA}$, whereas MLTT + AC + LEM is roughly as strong as Church's simple type theory, or Zermelo set theory. Eesh!

Mike Shulman (Apr 09 2021 at 01:36):

Cody Roux said:

Incidentally, adding LEM and AC to Martin-Löf type theory is very much not conservative. The bool vs Prop distinction is strange that way. MLTT is roughly as strong as $\mathrm{PA}$, whereas MLTT + AC + LEM is roughly as strong as Church's simple type theory, or Zermelo set theory. Eesh!

My understanding is that this jump in consistency strength has nothing to do with AC and little to do with LEM specifically, but is more about impredicativity, in the guise of propositional resizing, which is a consequence of LEM. Adding propositional resizing, which is a "constructive" axiom in that it's topos-valid, should also jump the consistency strength. Is that right?

Cody Roux (Apr 09 2021 at 02:12):

That sounds right, but I'm not sure what propositional resizing is, TBH. Just that there is a retraction of Prop into an element of Set?

Mike Shulman (Apr 09 2021 at 03:08):

Propositional resizing, as stated in the HoTT Book, says that every proposition (= subsingleton) in one universe is equivalent to a proposition in the smallest universe.

Verity Scheel (Apr 09 2021 at 03:30):

Thanks for your thoughts! Could you clarify “MLTT is roughly as strong as PA” – is that Peano Arithmetic? I seem to recall it's sometimes used for something else, but I don't remember …

Verity Scheel (Apr 09 2021 at 03:33):

What would type theory be like with LEM only for the smallest universe?

Ulrik Buchholtz (Apr 09 2021 at 07:22):

Nick Scheel said:

Thanks for your thoughts! Could you clarify “MLTT is roughly as strong as PA” – is that Peano Arithmetic? I seem to recall it's sometimes used for something else, but I don't remember …

Yes, PA refers to 1st order Peano Arithmetic. In terms of proof-theoretic ordinals, PA has strength $\varepsilon_0$, while MLTT (with no infinitary inductive types) has strength $\Gamma_0$, which is a little bit higher, but in the same ballpark of predicative mathematics.

Nick Scheel said:

What would type theory be like with LEM only for the smallest universe?

That would already be very strong, since you get characteristic functions for lots and lots of predicates, and hence the corresponding comprehensions. (Specifically, if you interpret the set sort in 2nd order arithmetic as $\mathbb{N} \to 2$, then you can interpret full 2nd order arithmetic.)
I don't know of a good work-around for this, except to work with a logic-enriched type theory.

Ulrik Buchholtz (Apr 09 2021 at 08:30):

Well, there's always the option of changing the interpretation of the logical connectives to build in a negative translation: $P \vee^c Q :\equiv \lnot(\lnot P \wedge \lnot Q)$ and $\exists^c_{x:A} P(x) :\equiv \lnot(\prod_{x:A}\lnot P(x))$. This way we interpret all of $\mathrm{PA}^\omega$ but with hardly any choice/comprehension.

Mike Shulman (Apr 09 2021 at 14:59):

Is there a nice readable exposition that explains the proof-theoretic strength of MLTT?

Cody Roux (Apr 09 2021 at 15:23):

Is there a nice readable exposition that explain the proof-theoretic strength of X?

Not really.

Cody Roux (Apr 09 2021 at 15:25):

I tend to understand things better in terms of bi-interpretability, or termination arguments. I think the set-theoretic interpretation of MLTT was first explored in depth by Peter Aczel, though I'd be happy to be corrected.

John Baez (Apr 09 2021 at 15:26):

A nice readable article that the masses of people who understand proof-theoretic strength and Martin-Löf type theory can easily understand? :upside_down:

Cody Roux (Apr 09 2021 at 15:26):

Then Rathjen basically wrote the book on the proof-theoretic strength of type theories, without actually writing any books, sadly.

Cody Roux (Apr 09 2021 at 15:28):

This is the first thing that comes up: https://www1.maths.leeds.ac.uk/~rathjen/typeOHIO.pdf. @Ulrik Buchholtz spent years in a monastery getting attuned to the ways of proof theorists, so he probably has much more insight into this question.

John Baez (Apr 09 2021 at 15:31):

Yes, it does seem a particularly monastic branch of math. Why is that, I wonder?

Cody Roux (Apr 09 2021 at 15:33):

I have no clear answer, though I do note that the tradition of ordinal analysis seems to be centered around a rather small community, so there may be social reasons. It seems that there are not a lot of interactions with more mainstream branches of logic, and Martin Hoffman once confided that there's a certain tradition in Germany of carefully hiding the "construction lines" of proofs.

Of course the technical aspects are extremely gnarly, so it's not entirely social.

Ulrik Buchholtz (Apr 09 2021 at 15:41):

Well, I learnt this as a grad student at Stanford, which isn't exactly a monastery :smile:
John Baez said:

A nice readable article that the masses of people who understand proof-theoretic strength and Martin-Löf type theory can easily understand? :upside_down:

Not only that: you also need some background in the systems used as yardsticks, typically subsystems of 2nd order arithmetic or extensions of Kripke–Platek set theory.
It isn't easy going, but you could have a look at Anton Setzer's thesis — following the motto that it's better to learn from someone's thesis.

Cody Roux (Apr 09 2021 at 15:49):

While we're on the subject, I remember reading somewhere a proof of normalization of system T using the intuitive encoding of an infinitary term with an eliminator of the form $\phi(n, t_1,\ldots) \rightarrow t_n$. It was Tait or Martin-Löf, I think.

For the life of me, I can't find it. Would you happen to know what I'm referring to?

Sorry to use you as a "math google".

Ulrik Buchholtz (Apr 09 2021 at 15:54):

Anyway the basic idea is that you can interpret universes (in basic MLTT) using fixed points of arithmetic operators. So that reduces the problem to figuring out how strong those are, which is what Feferman did in this article. The more modern way is to go directly to Kripke–Platek set theory, and then use the known results about the strengths of KP with various extensions. This is all explained reasonably well in Pohlers' book.

Ulrik Buchholtz (Apr 09 2021 at 15:58):

Tait 1965 and Martin-Löf 1972?

Ulrik Buchholtz (Apr 09 2021 at 16:02):

Cody Roux said:

For the life of me, I can't find it. Would you happen to know what I'm referring to?

See above :up: . Tait went straight to transfinite types, apparently, and Martin-Löf then simplified things a bit

Ulrik Buchholtz (Apr 09 2021 at 16:05):

BTW, the Buchholz–Pohlers style infinitary proof theory for meta-predicative systems was in some sense superseded by Girard's $\Pi^1_2$-methods using dilators, but Girard's interests shifted to linear logic, and he never published the second part of his proof theory book that was intended to cover this. Recently, he has put a draft version online.

Cody Roux (Apr 09 2021 at 16:45):

It would be nice to understand the "simple" cases in a nice pedagogical way before moving on to those crazy $\Pi^1_2$ comprehensions at any rate.

Cody Roux (Apr 09 2021 at 16:45):

Thanks a buch Ulrik! (btw your link to "this article" is broken/non-existent)

Ulrik Buchholtz (Apr 09 2021 at 17:38):

np – I've fixed the link

Ulrik Buchholtz (Apr 09 2021 at 17:46):

Re: infinite terms: there's also Schwichtenberg's 1973 Habilschrift

Cody Roux (Apr 09 2021 at 18:01):

just need to brush up on my German

Cody Roux (Apr 09 2021 at 18:07):

BTW I wrote something slightly more extensive with the same message a while back here: https://cstheory.stackexchange.com/a/30904/3984

Mike Shulman (Apr 09 2021 at 22:33):

Thanks!

Verity Scheel (Apr 10 2021 at 16:41):

Thanks for the discussion! I find this stuff really fascinating, maybe I will have time to learn it properly one day. It looks to me like type theories are certainly studied in the context of these results of proof strength and such, but still haven’t entered into the abstract philosophical discussions as much.

Cody Roux (Apr 10 2021 at 17:31):

Not sure what you mean by "abstract philosophical discussions", but the origins of type theory are rife with philosophical concerns.

See e.g. this classic: https://raw.githubusercontent.com/michaelt/martin-lof/master/pdfs/Meanings-of-the-Logical-Constants-1983.pdf