ax8_tiers_exclu

Énoncé

∀ (p : Prop), p ∨ ¬p

Toute proposition est vraie ou fausse, même sans savoir laquelle.

Axiomes consommés

C’est un axiome : il est admis, pas démontré. Tout ce qui s’appuie dessus en hérite, et c’est précisément ce que cette bibliothèque rend visible.

• ax8_tiers_exclu

Code

/-- **Axiome 8.** Toute proposition est vraie ou fausse.
C'est ce qui débloque le raisonnement par l'absurde général `¬¬P → P`, indispensable dès qu'on
démontre une égalité réelle par double inégalité à partir de `ax7_completude`. -/
axiom ax8_tiers_exclu (p : Prop) : p ∨ ¬p