<p>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.</p>

CC BY-SA 4.0
2021-03-11T14:12:29.173Z
Are there any references/explanations for this?
Ilk
CC BY-SA 4.0
2021-03-11T15:36:22.523Z
Digging around, I am confused, how does this interact with the results in https://github.com/input-output-hk/plutus/tree/master/papers/system-f-in-agda, which seems to use induction-recursion to formalize System F's strong normalization?
On the other hand I keep finding this dead link: http://fplab.bitbucket.org/posts/2012-12-06-induction-recursion.html as a supposed reference for this.
Ilk
CC BY-SA 4.0
2021-03-11T16:00:33.310Z
@Nift The "system-f-in-agda" repo does not use induction-recursion, and does not formalize strong normalization either.
András Kovács
CC BY-SA 4.0
2021-03-11T22:47:03.923Z
Is there a reference for this claim, or is it more of a hunch?
Andrej Bauer
CC BY-SA 4.0
2021-03-12T11:57:40.307Z
@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!
Neel Krishnaswami
CC BY-SA 4.0
2021-03-12T18:19:16.843Z
i managed to find a working bitbucket link, but i have yet to make sense of the broken typesetting,
https://fplab.bitbucket.io/posts/2012-12-06-induction-recursion.html
Ilk
CC BY-SA 4.0
2021-03-12T18:32:37.870Z
archiving it seems to have (mostly) fixed type setting so for future reference: https://archive.is/6MB4t
Ilk
CC BY-SA 4.0
2021-03-12T20:06:47.697Z
Is this the trick? https://gist.github.com/jcmckeown/07d844a9724745cedd61
cody
CC BY-SA 4.0
2021-03-12T20:39:40.470Z
@cody not really. The gist only uses large W-types, which is well below the strength of IR. We can try to emulate IR with large induction, using family-fibration equivalences, but we get a universe level bump in doing so. The power of IR comes from squeezing into one universe, so internal universe operators can be arbitrarily iterated. I don't know of any modeling of IR in Coq although Coq should be much stronger proof-theoretically.
András Kovács
CC BY-SA 4.0
2021-03-12T21:03:31.403Z
ok, from what i gather we have that 1. impredicative prop can simulate IR, but bumps universe levels 2. System F is stronger than MLTT without IR by Griffor and Rathjen 3. a hunch that SN for System F can be proven using impredicative Prop and can't be proven using IR by some extension of GR's results
Ilk
CC BY-SA 4.0
2021-03-12T21:10:48.077Z
@Nift: I don't know how to simulate IR with impredicative Prop. What I mentioned doesn't use impredicative Prop and does not get us IR, even with the universe bump. A single universe with IR is stronger than any transfinite hierarchy of vanilla predicative universes, up to an extremely large ordinal.
András Kovács
CC BY-SA 4.0
2021-03-12T21:15:37.390Z
another thing to add is that adding Prop breaks strong normalization by https://arxiv.org/abs/1911.08174
@AndrásKovács thanks for clarification
Ilk
CC BY-SA 4.0
2021-03-12T21:18:11.653Z
@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.
Anton Trunov
CC BY-SA 4.0
2021-03-13T08:24:21.633Z
@Nift You can definitely prove SN for system F in Coq; impredicative prop is more than enough.
Neel Krishnaswami
CC BY-SA 4.0
2021-03-13T08:32:04.533Z
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.
Neel Krishnaswami
CC BY-SA 4.0
2021-03-11T14:02:54.637Z
2021-03-11T14:02:54.637Z
Neel Krishnaswami
<p>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?</p>

<reference-request><type-theory>
Strongly normalizing type theory beyond induction-recursion
Ilk
# Strongly normalizing type theory beyond induction-recursion

(Asked by: username_0 on 2021-03-11)

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?

**Tags:** reference-request, type-theory

---

## 1 answers

### Answer by username_1 on 2021-03-11. Score: 8 | Accepted answer

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.

> **Comments:**
> **username_0**: Are there any references/explanations for this?  
> **username_0**: Digging around, I am confused, how does this interact with the results in https://github.com/input-output-hk/plutus/tree/master/papers/system-f-in-agda, which seems to use induction-recursion to formalize System F's strong normalization? On the other hand I keep finding this dead link: http://fplab.bitbucket.org/posts/2012-12-06-induction-recursion.html as a supposed reference for this.  
> **username_2**: @Nift The "system-f-in-agda" repo does not use induction-recursion, and does not formalize strong normalization either.  
> **username_3**: Is there a reference for this claim, or is it more of a hunch?  
> **username_1**: @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!  
> **username_0**: i managed to find a working bitbucket link, but i have yet to make sense of the broken typesetting, https://fplab.bitbucket.io/posts/2012-12-06-induction-recursion.html  
> **username_0**: archiving it seems to have (mostly) fixed type setting so for future reference: https://archive.is/6MB4t  
> **username_4**: Is this the trick? https://gist.github.com/jcmckeown/07d844a9724745cedd61  
> **username_2**: @cody not really. The gist only uses large W-types, which is well below the strength of IR. We can try to emulate IR with large induction, using family-fibration equivalences, but we get a universe level bump in doing so. The power of IR comes from squeezing into one universe, so internal universe operators can be arbitrarily iterated. I don't know of any modeling of IR in Coq although Coq should be much stronger proof-theoretically.  
> **username_0**: ok, from what i gather we have that 1. impredicative prop can simulate IR, but bumps universe levels 2. System F is stronger than MLTT without IR by Griffor and Rathjen 3. a hunch that SN for System F can be proven using impredicative Prop and can't be proven using IR by some extension of GR's results  
> **username_2**: @Nift: I don't know how to simulate IR with impredicative Prop. What I mentioned doesn't use impredicative Prop and does not get us IR, even with the universe bump. A single universe with IR is stronger than any transfinite hierarchy of vanilla predicative universes, up to an extremely large ordinal.  
> **username_0**: another thing to add is that adding Prop breaks strong normalization by https://arxiv.org/abs/1911.08174 @AndrásKovács thanks for clarification  
> **username_5**: @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.  
> **username_1**: @Nift You can definitely prove SN for system F in Coq; impredicative prop is more than enough.  
> **username_1**: 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.  

---

