Are there known type theories in the literature, which have strong normalization proofs and their proof-theoretical strength goes beyond strength of type theories with induction-recursion?
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
15
Yes. System F is probably the simplest example. As far as I know, you can’t prove normalisation for it in a dependent type theory with induction-recursion — you need at least impredicative prop to do so.
answered Mar 11, 2021 at 14:02
-
2$\begingroup$ @Nift The "system-f-in-agda" repo does not use induction-recursion, and does not formalize strong normalization either. $\endgroup$ Mar 11, 2021 at 16:00
-
1$\begingroup$ @cody It's more than a hunch, but I don't have a reference for it. Full 2nd order arithmetic is known to be stronger than MLTT with universes (see Griffor and Rathjen). and Swedes (both actual and honorary) have told me the situation doesn't change much with induction-recursion. But I don't know the proof, don't have references, and can neither find nor construct a counterexample. Possibly Cody Roux knows more! $\endgroup$ Mar 12, 2021 at 11:57
-
2$\begingroup$ another thing to add is that adding Prop breaks strong normalization by arxiv.org/abs/1911.08174 @AndrásKovács thanks for clarification $\endgroup$– NiftMar 12, 2021 at 21:15
-
3$\begingroup$ @Nift Notice that it does so if you have proof-irrelevant propositional equality. It's not the case in Coq, for instance, but Coq has impredicative Prop. $\endgroup$ Mar 12, 2021 at 21:18
-
2$\begingroup$ I haven’t tried to encode IR in MLTT with impredicative prop, but it is encodable in any topos using Pataraia’s fixed point theorem. I expect that if you assume function extensionality then you could redo the proof in Coq and get IR there as well. $\endgroup$ Mar 13, 2021 at 8:32