Extra property of Prop (Sort 0)

Stream: general

[Kevin Cheung]

In Chapter 3 of Theorem proving in Lean is found the following

the type Prop is syntactic sugar for Sort 0, the very bottom of the type hierarchy described in the last chapter. [...] Prop has some special features, but like the other type universes, it is closed under the arrow constructor

Where can one find out about these "some special features" of Prop?

[Jason Rute]

I’ve found this helpful: https://lean-forward.github.io/logical-verification/2018/41_notes.html (The syntax is Lean 3, but I think all or most of the ideas still apply.)

[Jason Rute]

Also some of this is talked about in TPIL, especially in the chapter about axioms.

[Niels Voss]

One special feature of Prop is that if P : Prop and p : P and q : P, then p = q (this is a definitional equality). In other words, any two proofs of the same statement are equal. As a consequence, proofs don't actually contain data.

[Niels Voss]

Another special feature is that terms like forall n : Nat, P n have type Prop. If Prop didn't have special handling, then this would instead have type Type

[Jason Rute]

Note, this first property mentioned by @Niels Voss is called "proof irrelevance" in TPiL, and is discussed in the chapter 3 you are reading. It indeed makes Prop behave very different from Type. (And to be clear, the property is not called "definitional equality", but I think Neils is saying in Lean it is implemented via a definitional equality rule.)

[Eric Rodriguez]

The second one is called impredicativity, as far as I remember

[Kevin Cheung]

Thanks for the explanations and pointers. I'll need some time to digest. If one wants to go down the rabbit hole and learn more, what are some good resources?

[Niels Voss]

Theorem Proving in Lean is a pretty good resource to learn about these types of things. In particular, you should look at the chapter on axioms and computation.

In general, both of these are very important, but it takes a while to understand why. I would also try to understand the difference between Inhabited and Nonempty, since both types look the same but one lies in Type (or at least the same level as the type you provide as input) and the other is in Prop.

[Kevin Cheung]

Lucky me, it looks like the 2023 version of The Hitchhiker’s Guide to Logical Verification covers these things in Chapter 12! This will keep me busy for a while.