Counterexample to the Law of Excluded Middle in Intuitionistic Logic #
Theorems #
noLEM: LEM is not always valid in intuitionistic Foundation.
@[reducible, inline]
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
LO.IntProp.Kripke.noLEM
{α : Type u}
[Inhabited α]
:
∃ (p : LO.IntProp.Formula α), 𝐈𝐧𝐭 ⊬ p ⋎ ∼p
Law of Excluded Middle is not always provable in intuitionistic Foundation.
theorem
LO.IntProp.Kripke.noLEM_KC
{α : Type u}
[Inhabited α]
:
∃ (p : LO.IntProp.Formula α), 𝐊𝐂 ⊬ p ⋎ ∼p
theorem
LO.IntProp.Kripke.noLEM_LC
{α : Type u}
[Inhabited α]
:
∃ (p : LO.IntProp.Formula α), 𝐋𝐂 ⊬ p ⋎ ∼p