<ul>
<li><p>Coq without Prop is not strong enough, because it's basically Martin-Löf type theory with universes.</p></li>
<li><p>Coq with Prop is strong enough, because you can encode sets of normalizing terms via predicates $S : \mathrm{Term} \to \mathrm{Prop}$, and impredicative universal quantification lets you express arbitrary intersections.</p></li>
</ul>

CC BY-SA 4.0
2018-06-08T16:37:29.163Z
Is there an existing Coq formalization?
Łukasz Lew
CC BY-SA 4.0
2018-06-08T19:12:25.437Z
@ŁukaszLew I couldn't find anything compelling online, but there is a Lego formalization by Altenkirch (1993!) described here: http://www.cs.nott.ac.uk/~psztxa/publ/tlca93.pdf
cody
CC BY-SA 4.0
2018-06-09T00:49:21.037Z
Found two more: 

 [Strong normalization for System F by HOAS on top of FOAS](https://www.ideals.illinois.edu/bitstream/handle/2142/15451/HOASonTopOfFOAS.pdf?sequence=2) 
 and  [Girard Normalization Proof in LEGO, page 67](https://www.researchgate.net/profile/Lincoln_Wallen/publication/220806453_Investigations_into_Proof-Search_in_a_System_of_First-Order_Dependent_Function_Types/links/54b694830cf2e68eb27ea1a6.pdf#page=70)
Łukasz Lew
CC BY-SA 4.0
2022-06-09T18:46:13.900Z
Here's one in Coq! https://github.com/coq-community/autosubst/blob/master/examples/ssr/SystemF_CBV.v
cody
CC BY-SA 4.0
2018-06-08T11:01:45.407Z
2018-06-08T11:01:45.407Z
Neel Krishnaswami
<p>In particular Agda <a href="https://cstheory.stackexchange.com/questions/32859/logical-reations-for-an-impredicative-system-in-a-predicative-metatheory">seems not strong enough</a> to prove that.</p>

<p>Is the predicative Calculus of Inductive Constructions universes (Coq without Prop) sufficient?</p>

<p>How about with the impredicative Prop?</p>

CC BY-SA 4.0
2018-06-14T08:59:42.333Z
There's one here: https://www.ps.uni-saarland.de/autosubst/doc/Ssr.SystemF_SN.html (see 
https://www.ps.uni-saarland.de/autosubst/ for context — it's an exercise done with a new library for formalization).
Blaisorblade
<lo.logic><type-systems><coq><normalization><agda>
Is there a formalization of normalization of impredicative system F?
Łukasz Lew
# Is there a formalization of normalization of impredicative system F?

(Asked by: username_0 on 2018-06-08)

In particular Agda [seems not strong enough](https://cstheory.stackexchange.com/questions/32859/logical-reations-for-an-impredicative-system-in-a-predicative-metatheory) to prove that.

Is the predicative Calculus of Inductive Constructions universes (Coq without Prop) sufficient?

How about with the impredicative Prop?

**Tags:** lo.logic, type-systems, coq, normalization, agda

> **Comments:**
> **username_1**: There's one here: https://www.ps.uni-saarland.de/autosubst/doc/Ssr.SystemF_SN.html (see  https://www.ps.uni-saarland.de/autosubst/ for context — it's an exercise done with a new library for formalization).  

---

## 1 answers

### Answer by username_2 on 2018-06-08. Score: 8 | Accepted answer

* Coq without Prop is not strong enough, because it's basically Martin-Löf type theory with universes.
* Coq with Prop is strong enough, because you can encode sets of normalizing terms via predicates $S : \mathrm{Term} \to \mathrm{Prop}$, and impredicative universal quantification lets you express arbitrary intersections.

> **Comments:**
> **username_0**: Is there an existing Coq formalization?  
> **username_3**: @ŁukaszLew I couldn't find anything compelling online, but there is a Lego formalization by Altenkirch (1993!) described here: http://www.cs.nott.ac.uk/~psztxa/publ/tlca93.pdf  
> **username_0**: Found two more:    [Strong normalization for System F by HOAS on top of FOAS](https://www.ideals.illinois.edu/bitstream/handle/2142/15451/HOASonTopOfFOAS.pdf?sequence=2)   and  [Girard Normalization Proof in LEGO, page 67](https://www.researchgate.net/profile/Lincoln_Wallen/publication/220806453_Investigations_into_Proof-Search_in_a_System_of_First-Order_Dependent_Function_Types/links/54b694830cf2e68eb27ea1a6.pdf#page=70)  
> **username_3**: Here's one in Coq! https://github.com/coq-community/autosubst/blob/master/examples/ssr/SystemF_CBV.v  

---

