10
$\begingroup$

I understand that we can use W-types to encode natural numbers and a wide variety of other inductive types in intensional MLTT. Can we encode W-types using only natural numbers within type theory, potentially giving up some of the judgmental equalities, but keeping the propositional equality the same? I always thought it was the case based on this quote from nLab W-type page:

"In a topos with a natural numbers object (NNO), W-types for any polynomial endofunctor can be constructed as certain sets of well-founded trees; thus every topos with a NNO is a ΠW-pretopos. This applies in particular in the topos Set (unless one is a predicativist, in which case Set is not a topos and W-types in it must be postulated explicitly)."

But I am unsure if this is a correct interpretation of the categorical concepts involved. I think the culprit here is the requirement of a topos with NNO, not just a locally cartesian closed category. Is this the case? Can we construct W-types from natural numbers?

Edit: I have found a construction of W-types from natural numbers in presence of propositional resizing in Strictly Positive Types in Homotopy Type Theory, so I think I should specify that I want to keep the theory as predicative as possible and hopefully free of uses of K or univalence.

Edit 2: To specify what I mean by intensional MLTT, it is the rules for $\Pi$, $\Sigma$, $\mathbb{N}$, Id, 0, 1, 2, plus an infinite predicative hierarchy of universes. $U_0 : U_1$, $U_1 : U_2$ etc.

$\endgroup$
7
  • 2
    $\begingroup$ How much structure are you assuming, something like MLTT ($\Pi$, $\Sigma$, $\mathrm{Id}$, $\mathbb{N}$, $0$, $1$, $2$), possibly with universes? $\endgroup$ Commented Aug 23, 2022 at 6:22
  • $\begingroup$ proofassistants.stackexchange.com/a/1377/153 apparently a generic construction is possible within simple type theory. However, I don't really understand the construction myself. $\endgroup$ Commented Aug 23, 2022 at 17:18
  • 2
    $\begingroup$ @MolossusSpondee That answer there only seems to address HOL-like settings, but HOL importantly lacks dependency and universes, note the signature of W (A : Set) (B : A -> Set) : Set, in HOL type families like B cannot be defined (we could still quantify over small A). $\endgroup$
    – Ilk
    Commented Aug 23, 2022 at 17:50
  • 1
    $\begingroup$ yes, that's what I am trying to say is that intensional MLTT + N should be an internal language of locally closed cartesian categories with NNO, not topos with an NNO, so the quote would only apply to stronger type theories/internal languages and won't tell us much about the W-types in internal language of LCCC+NNO. $\endgroup$
    – Ilk
    Commented Aug 25, 2022 at 4:44
  • 3
    $\begingroup$ Wikipedia's page on ordinal analysis says that the proof theoretic ordinal for MLTT without W-types (but with universes) is smaller than that for MLTT with W-types (even without universes). So, that suggests that you cannot build W-types with just ℕ and (predicative) universes. It's not very clear where all the information on that page comes from, though. $\endgroup$
    – Dan Doel
    Commented Aug 28, 2022 at 23:19

1 Answer 1

14
$\begingroup$

The answer is no. According to Anton Setzer's PhD thesis: Proof theoretical strength of Martin-Löf Type Theory with W-type and one universe:

Aczel has shown in [Acz77] that Martin-Löf’s type theory with one universe but no W-type has strength $| \widehat{ID}_1 | = \phi_{\epsilon_0}0$.

However:

The strength we prove, is in fact far bigger [than that shown by Palmgren], it is slightly bigger than the strength of $| KP_i|$. Until recently (work of Rathjen, [Rat90], [Rat91a], [Rat92], see also [Buc93], [Sch91a], [Sch91b], [Sch92b]), $KP_i$ has been essentially the strongest theory, for which proof theoretical analysis could be carried out. For the author, $|KP_i|$ is an ordinal which seems to be an ordinal of significance similar to that of $\Gamma_0$

Furthermore:

Precisely we calculate the proof theoretical strength of intensional Russel, extensional, Tarski, and extensional Russel-version of Martin-Löf’s type theory with one Universe and the W-type, $ML^i_1W_R$ , $ML^e_1W_T$ and $ML^e_1 W_R$, namely $$|ML^i_1W_R| =|ML^e_1W_T|=|ML^e_1 W_R|= |\bigcup_{n\in{\mathbb N}}KPi_n^+| = \psi_{\Omega_1}\Omega_{I+\omega}.$$

This sorts out the proof theoretical strength for MLTT with a single universe.

Now, according to Michael Rathjen's paper The strength of Martin-Löf type theory with a superuniverse (which is at least stronger than MLTT with an infinite hierarchy of universes):

the proof-theoretic ordinal of $MLS$ is $\Phi_{\Gamma_0}0$

But according to the wikipedia page on ordinal analysis, as pointed out by Dan Doel, $$\phi_{\epsilon_0}0 < \Gamma_0 < \Phi_{\Gamma_0}0 < \psi_{\Omega_1}\Omega_{I+\omega}$$

And therefore $|ML_\omega| < |ML_1W|$ thus it cannot be possible to encode W-types in $ML_\omega$.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.