sanity check on Lean's type theory

Stream: new members

[Chris M]

I've been lightly reading through some things, such as Mario Carneiro's thesis and the SEP entry on intuitionistic type theory. I just want to do a sanity check. Are the following correct?

1. We use the term predicative vs impredicative to refer to whether a definition is allowed to reference itself. For Lean, terms are predicative, all types are predicative, except Prop which is impredicative: terms are predicative in the sense that, (without the meta keyword) I can't write a definition of a function f whose body calls f itself. On the other hand Prop is impredicative, in the sense that I can have a type \Pi P:Prop, P : Prop where a term of type Prop itself contains the type Prop. Other types are predicative, in the sense that if \Pi T: Type u, T will have type Type u+1.

2. We need that terms are predicative in order to ensure that the type theory is consistent, but Prop being impredicative only means that the type theory becomes undecidable in general, it doesn't result in inconsistency (as far as we know). I'm unsure about this.

[Mario Carneiro]

We use the term predicative vs impredicative to refer to whether a definition is allowed to reference itself.

Not quite. A definition that references itself is called "recursive", and this is well known since antiquity to lead to contradictions without constraint, c.f. the liar paradox. Impredicativity refers to a definition that is allowed to quantify over a type or collection that contains the object being defined. This leads more subtly to contradiction via Russell's paradox, and different constraints are required to eliminate the contradictions

[Mario Carneiro]

Using impredicativity in lean you can create russell-like properties like:

def russell : Prop := ∃ p : Prop → Prop, ¬ p (∃ x, p x)

[Chris M]

Mario Carneiro said:

Using impredicativity in lean you can create russell-like properties like:

def russell : Prop := ∃ p : Prop → Prop, ¬ p (∃ x, p x)

So this property doesn't introduce an inconsistency, it just is a property for which we can neither prove it nor disprove it. i.e. we can neither have an inhabitant of russel nor of ¬ russel?

[Chris Wong]

Note that "impredicative" in this context has nothing to do with "impredicative types" in Haskell, which is about type inference on nested foralls.

[Mario Carneiro]

@Chris M No, that russell can certainly be proven or disproven. It's not really possible to faithfully represent russell's class inside prop because Prop -> Prop doesn't inject into Prop; Exists , playing the role of subtype inside Prop, is not an injective function (and if it was, Russell's class would yield a contradiction)

[Mario Carneiro]

def russell : Prop := ∃ p : Prop → Prop, ¬ p (∃ x, p x)
theorem russell_true : russell := ⟨λ _, false, id⟩

[Mario Carneiro]

@Chris Wong Actually I think the usage is related. Haskell is based on System F, in which there is one universe called * which is impredicative (you can quantify over types and get another type). However type inference works with only a subset of these types, where all type quantifiers appear at the top level. These are called "rank 1" types, and if you use haskell without ImpredicativeTypes, the universe is not fully impredicative, because types with quantifiers don't act like true types since they can't be used on the left of an arrow. The universe is basically first order at that point and so you don't get impredicative quantification.