Models of predicative type theory are well-studied and have been mechanized, ranging from proofs of consistency for a minimal type theory with a predicative hierarchy in 1000 lines of Rocq to proofs all the way up to decidability of conversion in 10 000 lines of Agda.
In contrast, the story for impredicative type theory is not so clear. Incorporating different features alongside an impredicative Prop may require substantially different proof methods. This post catalogues these various models, what type theories they model, and what proof technique is used. Most proofs fall into one of three techniques: proof-irrelevant set-theoretic models, reducibility methods, and realizabililty semantics.
Overview
| Work | Theory | Proof method | Universes | Inductives | Equality |
|---|---|---|---|---|---|
| Coquand (1985) | CC | ? | Prop, Type | none | untyped |
| Pottinger (1987) | CC | ? | Prop, Type | none | untyped |
| Ehrhard (1988) | CC | ω-Set | Prop, Type | none | none |
| Coquand and Gallier (1990) | CC | reducibility | Prop, Type | none | untyped |
| Luo (1990) | ECC | reducibility; ω-Set | Prop ⊆ Type{i} | dependent pairs | untyped |
| Terlouw (1993) | CC | reducibility | Prop, Type | none | untyped |
| Altenkirch (1993) | CC | Λ-Set | Prop, (Type) | impredicative | typed |
| Goguen (1994) | UTT | set-theoretic | Prop, Type | predicative | typed |
| Geuvers (1995) | CC | reducibility | Prop, Type | none | untyped |
| Melliès and Werner (1998) | PTS | Λ-Set | Prop ⊈ Type{i} | none | untyped |
| Miquel (2001) | CCω | set-theoretic; ω-Set | Prop ⊆ Type{i} | none | untyped |
| Miquel (2001) | ICC | ? | Prop ⊆ Type{i} | none | untyped |
| Miquel and Werner (2003) | CC | set-theoretic | Prop, Type | none | untyped |
| Lee and Werner (2011) | pCIC | set-theoretic | Prop ⊆ Type{i} | predicative | typed |
| Sacchini (2011) | CIC^- | Λ-Set | Prop, Type{i} | predicative, sized | untyped |
| Barras (2012) | CCω | set-theoretic | Prop ⊆ Type{i} | naturals | untyped |
| Barras (2012) | CC | Λ-Set | Prop, Type | naturals | untyped |
| Timany and Sozeau (2018) | pCuIC | set-theoretic | Prop ⊆ Type{i} | predicative | typed |
Glossary
- CC: the Calculus of Constructions
- CCω: CC with universes
- ECC: the Extended CC
- UTT: a Unified Type Theory
- ICC: the Implicit CC
- pCIC: the Predicative Calculus of Inductive Constructions
- pCuIC: the Predicative Calculus of Cumulative Inductive Constructions
- Prop, Type: an impredicative universe Prop and its type universe Type, with no subtyping
- Prop ⊆ Type{i}: a fully cumulative universe hierarchy Prop : Type₀ : Type₁ : … where Prop ⊆ Type₀ ⊆ Type₁ ⊆ …
- Prop ⊈ Type{i}: a partially cumulative universe hierarchy where instead Prop ⊈ Type₀ ⊆ Type₁ ⊆ …
Set-theoretic models
An early set-theoretic model for an impredicative type theory is given by Goguen (1994) for UTT, a type theory with an impredicative Prop type and a predicative Type universe, typed equality, and predicative inductives with large elimination. It must be emphasized that Prop is merely a type and not a universe: predicates (that is, impredicative quantifications into Prop) have introduction and elimination forms that are distinct from ordinary functions and applications, and there’s an explicit inclusion from Prop into Type. The model is proof-irrelevant, meaning that Prop is interpreted as a two-element set, and its inhabitants (propositions) are interpreted as one of these two elements (true or false). It appears that the syntactic distinction between predicates and functions is what makes the proof-irrelevant model unproblematic.
Miquel (2001) describes a proof-irrelevant set-theoretic model for the Calculus of Constructions (CC) with untyped equality, an impredicative Prop, and a predicative hierarchy of type universes, known as CCω. The hierarchy is fully cumulative, so there is an inclusion of Prop in Type₀ and of each type universe in the next one up. Predicates are ordinary dependent functions, so to accommodate both functions into Prop and Type, he appeals to a trace encoding by Peter Aczel. This thesis, however, doesn’t go into the details of proving soundness of typing with respect to this model.
Miquel and Werner (2003) then go into the details of the proof for the original CC, which only has an impredicative Prop universe, a predicative Type universe, and no inclusion. They find that they require variables to be syntactically annotated with the sort of their type. Interestingly, they settle for a simpler encoding of functions rather than the trace encoding.
The primary issue with Miquel and Werner’s system is the lack of an inclusion of Prop in Type₀, featured in Rocq. Lee and Werner (2011) resolve this exactly by using the trace encoding together with a typed equality judgement rather than an untyped one to eliminate the need for sort-annotated variables. The system they model includes a fully cumulative predicative universe hierarchy atop an impredicative Prop, predicative inductives, guarded fixpoints, and large elimination, and is referred to in the literature as pCIC.
Timany and Sozeau (2018) then augment this system to pCuIC with cumulative predicative inductives, which are featured in Rocq, and adapt the same proof-irrelevant set-theoretic model with trace encodings, albeit using eliminators rather than fixpoints.
Barras (2012) in his habilitation thesis mechanizes in Rocq a proof-irrelevant set-theoretic model, with the same trace encoding, of a system with untyped equality, impredicative Prop and a fully cumulative predicative universe hierarchy, and naturals with an induction principle and large elimination. Inductive types are also discussed in a later chapter.
One key feature all of these type theories are missing that’s common in proof assistants with an impredicative Prop is inductive propositions and predicates: inductive definitions that live in Prop.
Reducibility methods
The methods in this section all use some notion of Girard’s reducibility candidates, which are sets of strongly normalizing terms. Types are interpreted as reducibility candidates, and well-typed terms shown to be elements of the interpretation of the type, concluding that well-typed terms are strongly normalizing.
Coquand and Gallier (1990) use a Kripke logical relation to define their notion of reducibility as sets of terms to prove strong normalization for the Calculus of Constructions. In Section 7, they list other proofs of SN for CC, notably the PhD thesis of Coquand (1985) which apparently contains an error, and a private manuscript circulated by Coquand in 1987 correcting this error. They also cite Pottinger (1987) for a published proof of strong normalization for the Calculus of Constructions, and Seldin (1987) for a proof of SN for a variant of CC.
Geuvers (1995) again proves strong normalization for the Calculus of Constructions by a reducibility method, but instead using saturated sets of terms, which is claimed to be a more flexible and extensible method. In the introduction, many other proofs of SN for CC are cited, including one by Terlouw (1993) which also uses saturated sets and is inspired from Coquand’s proof:
The specific proof presented [by Coquand] is also in some sense of a model theoretical nature (it refers to Kripke-like interpretations), but as to its elaboration it differs considerably from the proof hereafter: it does not assign a key role to a formal theory T (of the kind as explained in the general introduction) and in the present situation the notion of “interpretation” is simpler and the explicit role of contexts has been strongly reduced.
The Extended Calculus of Constructions (ECC) by Luo (1990) extends CC with dependent pairs and a fully cumulative universe hierarchy, and strong normalization is proven by reducibility via quasi-normalization to define a complexity measure for types. However, it’s unclear to me whether any sort of large elimination would be compatible. It certainly seems that going through quasi-normalization isn’t very popular, as I haven’t seen any subsequent work follow this technique.
Realizability semantics
The models in this section are all D-Set models, where types are interpreted as D-Sets, which consist at least of some set X and a relation ⊧ between D and X, where if d ⊧ x holds then d is said to be a realizer of x. In ω-Sets, the realizers are the naturals, and in Λ-Sets, the realizers are terms.
Ehrhard (1988) gives an ω-Set model of the Calculus of Constructions, and Luo (1990) in the same thesis sketches out an ω-Set model for ECC, but notes that:
We shall not give a model semantics in full detail. There is a known problem about defining a model semantics of rich type theories like the calculus of constructions; that is, since there may be more than one derivation of a derivable judgement, a direct inductive definition by induction on derivations is questionable.
Altenkirch (1993) modifies the ω-Set model and introduces a Λ-Set model for proving strong normalization. A proof is worked out for a Calculus of Constructions with typed equality and impredicative inductives with large elimination. The system is presented à la Tarski rather than à la Russell.
Melliès and Werner (1998) then generalize this technique to all PTSes whose sorts satisfy a certain property. To demonstrate, they apply the method to prove strong normalization of ECC (without dependent pairs). However, it appears that it does not cover inclusion of Prop in Type. Sacchini (2011), who uses a Λ-Set model based on Melliès and Werner’s to show strong normalization for a variant of CIC with sized types (CIC^-), notes in Section 4.3.1 that:
It is important to separate proofs from computation. Therefore, it is not trivial to extend this model in the presence of a subtyping rule of the form Prop ≤ Type₀. This is the reason we do not consider this rule in our proof (cf. Sect. 5.1).
and in Section 5.1 notes that:
We cannot easily adapt our Λ-set model to handle rule [Prop ≤ Type₀]. In the presence of this rule, the separation property of proofs and computations is no longer valid.
Miquel (2001) sketches out an ω-Set model for CCω, but doesn’t go into proving soundness of typing with respect to the model. The proof method that he does use for the Implicit Calculus of Constructions (ICC) is a simplified version of the Λ-set model using coherent 𝒦-spaces. ICC has the distinction of being the only language cited here that is Curry-style (unannotated lambdas) rather than Church-style (domain-annotated lambdas). It’s unclear to me how he handles a cumulative impredicative Prop.
Barras (2012) mechanizes in Rocq a Λ-set model for a Calculus of Constructions with naturals and large elimination. It appears there are no larger universes, nor cumulativity.
Other proofs and papers
- Geuvers and Nederhof (1991) show strong normalization of the Calculus of Constructions by reducing it down to System Fω and using its strong normalization property.
- Casinghino (2010) gives a comparative survey of three different proof methods for the Calculus of Constructions: a reducibility proof, a realizability proof, and Geuvers and Nederhof’s reduction to System Fω.
[Altenkirch 1993] Thorsten Altenkirch. Constructions, Inductive Types, and Strong Normalization. (PhD thesis). ᴜʀʟ: https://www.cs.nott.ac.uk/~psztxa/publ/phd93.pdf.
[Barras (2012)] Bruno Barras. Semantical Investigations in Intuitionistic Set Theory and Type Theories with Inductive Families. (Habilitation thesis). ᴜʀʟ: http://www.lsv.fr/~barras/habilitation/barras-habilitation.pdf.
[Casinghino (2010)] Chris Casinghino. Strong Normalization for the Calculus of Constructions. ᴅᴏɪ: 10.48550/arXiv.2210.11240.
[Coquand (1985)] Thierry Coquand. Une Théorie Des Constructions. (PhD thesis).
[Coquand and Gallier (1990)] Thierry Coquand, Jean Gallier. A Proof Of Strong Normalization For The Theory Of Constructions Using A Kripke-Like Interpretation. (1990). ᴜʀʟ: https://repository.upenn.edu/handle/20.500.14332/7509.
[Ehrhard (1988)] Thomas Ehrhard. A categorical semantics of constructions. (LICS 1988). ᴅᴏɪ: 10.1109/LICS.1988.5125.
[Geuvers and Nederhof (1991)] Herman Geuvers, Mark-Jan Nederhof. Modular proof of strong normalization for the calculus of constructions. (JFP 1991). ᴅᴏɪ: 10.1017/S0956796800020037.
[Geuvers (1995)] Herman Geuvers. A short and flexible proof of strong normalization for the calculus of constructions. (TYPES 1994). ᴅᴏɪ: 10.1007/3-540-60579-7_2.
[Goguen (1994)] Healfdene Goguen. A Typed Operational Semantics for Type Theory. (PhD thesis). ᴜʀʟ: http://hdl.handle.net/1842/405.
[Lee and Werner (2011)] Gyesik Lee, Benjamin Werner. Proof-Irrelevant Model of CC with Predicative Induction and Judgemental Equality. (LMCS 7(4)). ᴅᴏɪ: 10.2168/LMCS-7(4:5)2011.
[Luo (1990)] Zhaohui Luo. An Extended Calculus of Constructions. (PhD thesis). ᴜʀʟ: https://www.lfcs.inf.ed.ac.uk/reports/90/ECS-LFCS-90-118/.
[Melliès and Werner (1998)] Paul-André Melliès, Benjamin Werner. A Generic Normalisation Proof for Pure Type Systems. (RR-3548, INRIA). ᴜʀʟ: https://inria.hal.science/inria-00073135.
[Miquel (2001)] Alexandre Miquel. Le calcul des constructions implicite: syntaxe et sémantique. (PhD thesis). ᴜʀʟ: https://www.fing.edu.uy/~amiquel/publis/these.pdf.
[Miquel and Werner (2003)] Alexandre Miquel, Benjamin Werner. The Not So Simple Proof-Irrelevant Model of CC. (TYPES 2002). ᴅᴏɪ: 10.1007/3-540-39185-1_14.
[Pottinger (1987)] Garrel Pottinger. Strong Normalization for Terms of the Theory of Constructions. (TR 11-7, Odyssey Research Associates). ᴅᴏɪ: 10.5281/zenodo.11455038.
[Sacchini (2011)] Jorge Luis Sacchini. On Type-Based Termination and Dependent Pattern Matching in the Calculus of Inductive Constructions. (PhD thesis). ᴜʀʟ: https://pastel.hal.science/pastel-00622429.
[Seldin (1987)] Jonathan P. Seldin. MATHESIS: the mathematical foundation for ULYSSES. (RADC-TR-87-223, Odyssey Research Associates). ᴜʀʟ: https://apps.dtic.mil/sti/tr/pdf/ADA195379.pdf.
[Terlouw (1993)] Jan Terlouw. Strong normalization in type systems: A model theoretical approach. (Annals of Pure and Applied Logic 73(1)). ᴅᴏɪ: 10.1016/0168-0072(94)00040-A.
[Timany and Sozeau (2018)] Amin Timany, Mattieu Sozeau. Consistency of the Predicative Calculus of Cumulative Constructions. (FSCD 2018). ᴅᴏɪ: 10.4230/LIPIcs.FSCD.2018.29.