Propositional extentionality in the lean theorem prover is stated as the following axiom:

axiom proptext {a b : Prop} : (a $\iff$ b) \to a = b

My confusion about this is as follows: Previously I’ve read (in “introduction to type theory” by Herman Geuvers) that one key property of type theory is that we don’t say that two types are equal just because the set of its instances is equal (unlike in set theory).

He stated that this is on of the sources of type theory’s power because it allows one to syntactically check whether something is of a certain type, whereas with set theory, we can’t. He stated that this can be understood as, $:$ is a decidable operator, whereas $\in$ is not.

I’m confused about how the axiom of propositional extentionality fits into Geuvers’ characterization of what type theory is about.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.