Documentation

Logic.IntProp.Kripke.LEM

Counterexample to the Law of Excluded Middle in Intuitionistic Logic #

Theorems #

source
@[reducible, inline]
abbrev LO.IntProp.Kripke.NoLEMFrame :
LO.Kripke.Frame
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem LO.IntProp.Kripke.NoLEMFrame.transitive :
    Transitive LO.IntProp.Kripke.NoLEMFrame.Rel
    source
    theorem LO.IntProp.Kripke.NoLEMFrame.reflexive :
    Reflexive LO.IntProp.Kripke.NoLEMFrame.Rel
    source
    theorem LO.IntProp.Kripke.NoLEMFrame.confluent :
    Confluent LO.IntProp.Kripke.NoLEMFrame.Rel
    source
    theorem LO.IntProp.Kripke.NoLEMFrame.connected :
    Connected LO.IntProp.Kripke.NoLEMFrame.Rel
    source
    theorem LO.IntProp.Kripke.noLEM_on_frameclass {α : Type u} [Inhabited α] :
    ∃ (p : LO.IntProp.Formula α), ¬𝔽(𝐈𝐧𝐭) ⊧ p ⋎ ∼p
    source
    theorem LO.IntProp.Kripke.noLEM {α : Type u} [Inhabited α] :
    ∃ (p : LO.IntProp.Formula α), 𝐈𝐧𝐭 ⊬ p ⋎ ∼p

    Law of Excluded Middle is not always provable in intuitionistic logic.

    source
    theorem LO.IntProp.Kripke.Int_strictly_weaker_than_Cl {α : Type u} [Inhabited α] :
    𝐈𝐧𝐭 <ₛ 𝐂𝐥

    Intuitionistic logic is proper weaker than classical logic.

    source
    theorem LO.IntProp.Kripke.noLEM_on_frameclass_KC {α : Type u} [Inhabited α] :
    ∃ (p : LO.IntProp.Formula α), ¬𝔽(𝐊𝐂) ⊧ p ⋎ ∼p
    source
    theorem LO.IntProp.Kripke.noLEM_KC {α : Type u} [Inhabited α] :
    ∃ (p : LO.IntProp.Formula α), 𝐊𝐂 ⊬ p ⋎ ∼p
    source
    theorem LO.IntProp.Kripke.KC_strictly_weaker_than_Cl {α : Type u} [Inhabited α] :
    𝐊𝐂 <ₛ 𝐂𝐥
    source
    theorem LO.IntProp.Kripke.noLEM_on_frameclass_LC {α : Type u} [Inhabited α] :
    ∃ (p : LO.IntProp.Formula α), ¬𝔽(𝐋𝐂) ⊧ p ⋎ ∼p
    source
    theorem LO.IntProp.Kripke.noLEM_LC {α : Type u} [Inhabited α] :
    ∃ (p : LO.IntProp.Formula α), 𝐋𝐂 ⊬ p ⋎ ∼p
    source
    theorem LO.IntProp.Kripke.LC_strictly_weaker_than_Cl {α : Type u} [DecidableEq α] [Inhabited α] :
    𝐋𝐂 <ₛ 𝐂𝐥