Formal knowledge
Propositional extensionality
The principle that logically equivalent propositions are equal as propositions.
Definition
Propositional extensionality
Propositional extensionality turns a proof of P if and only if Q into an equality between the propositions P and Q.
Logical equivalence is available constructively, but equality of proposition objects is a stronger principle in Lean's foundation. Some mathlib declarations depend on this axiom through their proof chain.
Notation (P ↔ Q) → P = Q
01
Example
A proof of P ∧ True ↔ P can become the equality (P ∧ True) = P when propositional extensionality is available.
02
Important distinction
Propositional extensionality is not the same as function extensionality or ordinary rewriting by an equivalence.
After reading this article, you should be able to
- Define Propositional extensionality in the sense used on this site.
- Distinguish logical equivalence from equality of propositions.