Documentation

Logic.Propositional.Superintuitionistic.Kripke.LEM

Counterexample to the Law of Excluded Middle in Intuitionistic Logic #

Theorems #

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

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

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

    Intuitionistic logic is proper weaker than classical logic.

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