Documentation

Logic.Propositional.Superintuitionistic.Kripke.Semantics

def LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies {α : Type u} (M : LO.Kripke.Model α) (w : M.World) :

LO.Propositional.Superintuitionistic.Formula α → Prop

Equations

One or more equations did not get rendered due to their size.
LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies M w (LO.Propositional.Superintuitionistic.Formula.atom a) = M.Valuation w a
LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies M w LO.Propositional.Superintuitionistic.Formula.verum = True
LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies M w LO.Propositional.Superintuitionistic.Formula.falsum = False
LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies M w p.neg = ∀ {w' : M.World}, LO.Kripke.Frame.Rel' w w' → ¬LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies M w' p

Instances For

instance LO.Propositional.Superintuitionistic.Formula.Kripke.instSatisfiesSemantics {α : Type u} (M : LO.Kripke.Model α) :

LO.Semantics (LO.Propositional.Superintuitionistic.Formula α) M.World

Equations

LO.Propositional.Superintuitionistic.Formula.Kripke.instSatisfiesSemantics M = { Realize := fun (w : M.World) => LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies M w }

@[simp]

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.iff_models {α : Type u} {M : LO.Kripke.Model α} {w : M.World} {p : LO.Propositional.Superintuitionistic.Formula α} :

w ⊧ p ↔ LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies M w p

@[simp]

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.atom_def {α : Type u} {M : LO.Kripke.Model α} {w : M.World} {a : α} :

w ⊧ LO.Propositional.Superintuitionistic.Formula.atom a ↔ M.Valuation w a

@[simp]

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.top_def {α : Type u} {M : LO.Kripke.Model α} {w : M.World} :

w ⊧ ⊤ ↔ True

@[simp]

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.bot_def {α : Type u} {M : LO.Kripke.Model α} {w : M.World} :

w ⊧ ⊥ ↔ False

@[simp]

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.and_def {α : Type u} {M : LO.Kripke.Model α} {w : M.World} {p : LO.Propositional.Superintuitionistic.Formula α} {q : LO.Propositional.Superintuitionistic.Formula α} :

w ⊧ p ⋏ q ↔ w ⊧ p ∧ w ⊧ q

@[simp]

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.or_def {α : Type u} {M : LO.Kripke.Model α} {w : M.World} {p : LO.Propositional.Superintuitionistic.Formula α} {q : LO.Propositional.Superintuitionistic.Formula α} :

w ⊧ p ⋎ q ↔ w ⊧ p ∨ w ⊧ q

@[simp]

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.imp_def {α : Type u} {M : LO.Kripke.Model α} {w : M.World} {p : LO.Propositional.Superintuitionistic.Formula α} {q : LO.Propositional.Superintuitionistic.Formula α} :

w ⊧ p ⟶ q ↔ ∀ {w' : M.World}, LO.Kripke.Frame.Rel' w w' → w' ⊧ p → w' ⊧ q

@[simp]

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.neg_def {α : Type u} {M : LO.Kripke.Model α} {w : M.World} {p : LO.Propositional.Superintuitionistic.Formula α} :

w ⊧ ~p ↔ ∀ {w' : M.World}, LO.Kripke.Frame.Rel' w w' → ¬w' ⊧ p

instance LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.instTopWorld {α : Type u} {M : LO.Kripke.Model α} :

LO.Semantics.Top M.World

Equations

LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.instTopWorld = { realize_top := ⋯ }

instance LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.instBotWorld {α : Type u} {M : LO.Kripke.Model α} :

LO.Semantics.Bot M.World

Equations

LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.instBotWorld = { realize_bot := ⋯ }

instance LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.instAndWorld {α : Type u} {M : LO.Kripke.Model α} :

LO.Semantics.And M.World

Equations

LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.instAndWorld = { realize_and := ⋯ }

instance LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.instOrWorld {α : Type u} {M : LO.Kripke.Model α} :

LO.Semantics.Or M.World

Equations

LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.instOrWorld = { realize_or := ⋯ }

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.formula_hereditary {α : Type u} {M : LO.Kripke.Model α} {w : M.World} {p : LO.Propositional.Superintuitionistic.Formula α} {w' : M.Frame.World} (herditary : M.Valuation.atomic_hereditary) (F_trans : Transitive M.Frame.Rel) (hw : LO.Kripke.Frame.Rel' w w') :

w ⊧ p → w' ⊧ p

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies.neg_equiv {α : Type u} {M : LO.Kripke.Model α} {w : M.World} {p : LO.Propositional.Superintuitionistic.Formula α} :

w ⊧ ~p ↔ w ⊧ p ⟶ ⊥

def LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel {α : Type u} (M : LO.Kripke.Model α) (p : LO.Propositional.Superintuitionistic.Formula α) :

Equations

LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel M p = ∀ (w : M.World), w ⊧ p

Instances For

instance LO.Propositional.Superintuitionistic.Formula.Kripke.instSemanticsModel {α : Type u} :

LO.Semantics (LO.Propositional.Superintuitionistic.Formula α) (LO.Kripke.Model α)

Equations

LO.Propositional.Superintuitionistic.Formula.Kripke.instSemanticsModel = { Realize := fun (M : LO.Kripke.Model α) => LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel M }

@[simp]

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.iff_models {α : Type u} {M : LO.Kripke.Model α} {p : LO.Propositional.Superintuitionistic.Formula α} :

M ⊧ p ↔ LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel M p

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.verum {α : Type u} {M : LO.Kripke.Model α} :

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.and₁ {α : Type u} {M : LO.Kripke.Model α} {p : LO.Propositional.Superintuitionistic.Formula α} {q : LO.Propositional.Superintuitionistic.Formula α} :

M ⊧ p ⋏ q ⟶ p

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.and₂ {α : Type u} {M : LO.Kripke.Model α} {p : LO.Propositional.Superintuitionistic.Formula α} {q : LO.Propositional.Superintuitionistic.Formula α} :

M ⊧ p ⋏ q ⟶ q

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.and₃ {α : Type u} {M : LO.Kripke.Model α} {p : LO.Propositional.Superintuitionistic.Formula α} {q : LO.Propositional.Superintuitionistic.Formula α} (atom_hereditary : ∀ {w₁ w₂ : M.World}, LO.Kripke.Frame.Rel' w₁ w₂ → ∀ {a : α}, M.Valuation w₁ a → M.Valuation w₂ a) (F_trans : autoParam (Transitive M.Frame.Rel) _auto✝) :

M ⊧ p ⟶ q ⟶ p ⋏ q

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.or₁ {α : Type u} {M : LO.Kripke.Model α} {p : LO.Propositional.Superintuitionistic.Formula α} {q : LO.Propositional.Superintuitionistic.Formula α} :

M ⊧ p ⟶ p ⋎ q

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.or₂ {α : Type u} {M : LO.Kripke.Model α} {p : LO.Propositional.Superintuitionistic.Formula α} {q : LO.Propositional.Superintuitionistic.Formula α} :

M ⊧ q ⟶ p ⋎ q

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.or₃ {α : Type u} {M : LO.Kripke.Model α} {p : LO.Propositional.Superintuitionistic.Formula α} {q : LO.Propositional.Superintuitionistic.Formula α} {r : LO.Propositional.Superintuitionistic.Formula α} (F_trans : autoParam (Transitive M.Frame.Rel) _auto✝) :

M ⊧ (p ⟶ r) ⟶ (q ⟶ r) ⟶ p ⋎ q ⟶ r

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.imply₁ {α : Type u} {M : LO.Kripke.Model α} {p : LO.Propositional.Superintuitionistic.Formula α} {q : LO.Propositional.Superintuitionistic.Formula α} (atom_hereditary : ∀ {w₁ w₂ : M.World}, LO.Kripke.Frame.Rel' w₁ w₂ → ∀ {a : α}, M.Valuation w₁ a → M.Valuation w₂ a) (F_trans : autoParam (Transitive M.Frame.Rel) _auto✝) :

M ⊧ p ⟶ q ⟶ p

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.imply₂ {α : Type u} {M : LO.Kripke.Model α} {p : LO.Propositional.Superintuitionistic.Formula α} {q : LO.Propositional.Superintuitionistic.Formula α} {r : LO.Propositional.Superintuitionistic.Formula α} (F_trans : autoParam (Transitive M.Frame.Rel) _auto✝) (F_refl : autoParam (Reflexive M.Frame.Rel) _auto✝) :

M ⊧ (p ⟶ q ⟶ r) ⟶ (p ⟶ q) ⟶ p ⟶ r

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.mdp {α : Type u} {M : LO.Kripke.Model α} {p : LO.Propositional.Superintuitionistic.Formula α} {q : LO.Propositional.Superintuitionistic.Formula α} (F_refl : autoParam (Reflexive M.Frame.Rel) _auto✝) (hpq : M ⊧ p ⟶ q) (hp : M ⊧ p) :

M ⊧ q

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.efq {α : Type u} {M : LO.Kripke.Model α} {p : LO.Propositional.Superintuitionistic.Formula α} :

M ⊧ LO.Axioms.EFQ p

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.neg_equiv {α : Type u} {M : LO.Kripke.Model α} {p : LO.Propositional.Superintuitionistic.Formula α} :

M ⊧ LO.Axioms.NegEquiv p

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.lem {α : Type u} {M : LO.Kripke.Model α} {p : LO.Propositional.Superintuitionistic.Formula α} (atom_hereditary : ∀ {w₁ w₂ : M.World}, LO.Kripke.Frame.Rel' w₁ w₂ → ∀ {a : α}, M.Valuation w₁ a → M.Valuation w₂ a) (F_trans : autoParam (Transitive M.Frame.Rel) _auto✝) :

Symmetric M.Frame.Rel → M ⊧ LO.Axioms.LEM p

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.dum {α : Type u} {M : LO.Kripke.Model α} {p : LO.Propositional.Superintuitionistic.Formula α} {q : LO.Propositional.Superintuitionistic.Formula α} (atom_hereditary : ∀ {w₁ w₂ : M.World}, LO.Kripke.Frame.Rel' w₁ w₂ → ∀ {a : α}, M.Valuation w₁ a → M.Valuation w₂ a) (F_trans : autoParam (Transitive M.Frame.Rel) _auto✝) :

Connected M.Frame.Rel → M ⊧ LO.Axioms.GD p q

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnModel.wlem {α : Type u} {M : LO.Kripke.Model α} {p : LO.Propositional.Superintuitionistic.Formula α} (atom_hereditary : ∀ {w₁ w₂ : M.World}, LO.Kripke.Frame.Rel' w₁ w₂ → ∀ {a : α}, M.Valuation w₁ a → M.Valuation w₂ a) (F_trans : autoParam (Transitive M.Frame.Rel) _auto✝) :

Confluent M.Frame.Rel → M ⊧ LO.Axioms.WeakLEM p

def LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame {α : Type u} (F : LO.Kripke.Frame) (p : LO.Propositional.Superintuitionistic.Formula α) :

Equations

LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame F p = ∀ {V : LO.Kripke.Valuation F α}, V.atomic_hereditary → { Frame := F, Valuation := V } ⊧ p

Instances For

instance LO.Propositional.Superintuitionistic.Formula.Kripke.instSemanticsDep {α : Type u} :

LO.Semantics (LO.Propositional.Superintuitionistic.Formula α) (LO.Kripke.Frame.Dep α)

Equations

LO.Propositional.Superintuitionistic.Formula.Kripke.instSemanticsDep = { Realize := fun (F : LO.Kripke.Frame.Dep α) => LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame F }

@[simp]

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.models_iff {α : Type u} {F : LO.Kripke.Frame.Dep α} {f : LO.Propositional.Superintuitionistic.Formula α} :

F ⊧ f ↔ LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame F f

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.verum {α : Type u} {F : LO.Kripke.Frame.Dep α} :

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.and₁ {α : Type u} {F : LO.Kripke.Frame.Dep α} {p : LO.Propositional.Superintuitionistic.Formula α} {q : LO.Propositional.Superintuitionistic.Formula α} :

F ⊧ p ⋏ q ⟶ p

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.and₂ {α : Type u} {F : LO.Kripke.Frame.Dep α} {p : LO.Propositional.Superintuitionistic.Formula α} {q : LO.Propositional.Superintuitionistic.Formula α} :

F ⊧ p ⋏ q ⟶ q

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.and₃ {α : Type u} {F : LO.Kripke.Frame.Dep α} {p : LO.Propositional.Superintuitionistic.Formula α} {q : LO.Propositional.Superintuitionistic.Formula α} (F_trans : Transitive F.Rel) :

F ⊧ p ⟶ q ⟶ p ⋏ q

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.or₁ {α : Type u} {F : LO.Kripke.Frame.Dep α} {p : LO.Propositional.Superintuitionistic.Formula α} {q : LO.Propositional.Superintuitionistic.Formula α} :

F ⊧ p ⟶ p ⋎ q

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.or₂ {α : Type u} {F : LO.Kripke.Frame.Dep α} {p : LO.Propositional.Superintuitionistic.Formula α} {q : LO.Propositional.Superintuitionistic.Formula α} :

F ⊧ q ⟶ p ⋎ q

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.or₃ {α : Type u} {F : LO.Kripke.Frame.Dep α} {p : LO.Propositional.Superintuitionistic.Formula α} {q : LO.Propositional.Superintuitionistic.Formula α} {r : LO.Propositional.Superintuitionistic.Formula α} (F_trans : Transitive F.Rel) :

F ⊧ (p ⟶ r) ⟶ (q ⟶ r) ⟶ p ⋎ q ⟶ r

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.imply₁ {α : Type u} {F : LO.Kripke.Frame.Dep α} {p : LO.Propositional.Superintuitionistic.Formula α} {q : LO.Propositional.Superintuitionistic.Formula α} (F_trans : Transitive F.Rel) :

F ⊧ p ⟶ q ⟶ p

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.imply₂ {α : Type u} {F : LO.Kripke.Frame.Dep α} {p : LO.Propositional.Superintuitionistic.Formula α} {q : LO.Propositional.Superintuitionistic.Formula α} {r : LO.Propositional.Superintuitionistic.Formula α} (F_trans : Transitive F.Rel) (F_refl : Reflexive F.Rel) :

F ⊧ (p ⟶ q ⟶ r) ⟶ (p ⟶ q) ⟶ p ⟶ r

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.mdp {α : Type u} {F : LO.Kripke.Frame.Dep α} {p : LO.Propositional.Superintuitionistic.Formula α} {q : LO.Propositional.Superintuitionistic.Formula α} (F_refl : Reflexive F.Rel) (hpq : F ⊧ p ⟶ q) (hp : F ⊧ p) :

F ⊧ q

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.efq {α : Type u} {F : LO.Kripke.Frame.Dep α} {p : LO.Propositional.Superintuitionistic.Formula α} :

F ⊧ LO.Axioms.EFQ p

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.neg_equiv {α : Type u} {F : LO.Kripke.Frame.Dep α} {p : LO.Propositional.Superintuitionistic.Formula α} :

F ⊧ LO.Axioms.NegEquiv p

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.lem {α : Type u} {F : LO.Kripke.Frame.Dep α} {p : LO.Propositional.Superintuitionistic.Formula α} (F_trans : Transitive F.Rel) (F_symm : Symmetric F.Rel) :

F ⊧ LO.Axioms.LEM p

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.dum {α : Type u} {F : LO.Kripke.Frame.Dep α} {p : LO.Propositional.Superintuitionistic.Formula α} {q : LO.Propositional.Superintuitionistic.Formula α} (F_trans : Transitive F.Rel) (F_conn : Connected F.Rel) :

F ⊧ LO.Axioms.GD p q

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.wlem {α : Type u} {F : LO.Kripke.Frame.Dep α} {p : LO.Propositional.Superintuitionistic.Formula α} (F_trans : Transitive F.Rel) (F_conf : Confluent F.Rel) :

F ⊧ LO.Axioms.WeakLEM p

instance LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.instBotDep {α : Type u} :

LO.Semantics.Bot (LO.Kripke.Frame.Dep α)

Equations

LO.Propositional.Superintuitionistic.Formula.Kripke.ValidOnFrame.instBotDep = { realize_bot := ⋯ }

instance LO.Propositional.Superintuitionistic.Formula.Kripke.instSemanticsDep_1 {α : Type u} :

LO.Semantics (LO.Propositional.Superintuitionistic.Formula α) (LO.Kripke.FrameClass.Dep α)

Equations

LO.Propositional.Superintuitionistic.Formula.Kripke.instSemanticsDep_1 = LO.Semantics.instSet (LO.Kripke.Frame.Dep α)

@[reducible, inline]

abbrev LO.Propositional.Superintuitionistic.Kripke.FrameClassOfSystem (α : Type u) {S : Type u} [LO.System (LO.Propositional.Superintuitionistic.Formula α) S] (𝓢 : S) :

LO.Kripke.FrameClass.Dep α

Equations

𝔽(𝓢 of α) = {F : LO.Kripke.Frame | F ⊧* LO.System.theory 𝓢}

Instances For

def LO.Propositional.Superintuitionistic.Kripke.«term𝔽(_Of_)» :

Lean.ParserDescr

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem LO.Propositional.Superintuitionistic.Kripke.sound {S : Type u} {α : Type u} [LO.System (LO.Propositional.Superintuitionistic.Formula α) S] {𝓢 : S} {p : LO.Propositional.Superintuitionistic.Formula α} :

𝓢 ⊢! p → 𝔽(𝓢 of α) ⊧ p

instance LO.Propositional.Superintuitionistic.Kripke.instSoundFormulaDepFrameClassOfSystem {S : Type u} {α : Type u} [LO.System (LO.Propositional.Superintuitionistic.Formula α) S] {𝓢 : S} :

LO.Sound 𝓢 𝔽(𝓢 of α)

Equations

⋯ = ⋯

theorem LO.Propositional.Superintuitionistic.Kripke.unprovable_bot {S : Type u} {α : Type u} [LO.System (LO.Propositional.Superintuitionistic.Formula α) S] {𝓢 : S} (hc : Set.Nonempty 𝔽(𝓢 of α)) :

instance LO.Propositional.Superintuitionistic.Kripke.instConsistentFormulaOfNonemptyFrameFrameClassOfSystem {S : Type u} {α : Type u} [LO.System (LO.Propositional.Superintuitionistic.Formula α) S] {𝓢 : S} (hc : Set.Nonempty 𝔽(𝓢 of α)) :

LO.System.Consistent 𝓢

Equations

⋯ = ⋯

theorem LO.Propositional.Superintuitionistic.Kripke.sound_of_characterizability {S : Type u} {α : Type u} [LO.System (LO.Propositional.Superintuitionistic.Formula α) S] {𝓢 : S} {p : LO.Propositional.Superintuitionistic.Formula α} {𝔽₂ : LO.Kripke.FrameClass} [characterizability : LO.Kripke.FrameClass.Characteraizable 𝔽(𝓢 of α) 𝔽₂] :

𝓢 ⊢! p → 𝔽₂#α ⊧ p

instance LO.Propositional.Superintuitionistic.Kripke.instSoundOfCharacterizability {S : Type u} {α : Type u} [LO.System (LO.Propositional.Superintuitionistic.Formula α) S] {𝓢 : S} {𝔽₂ : LO.Kripke.FrameClass} [LO.Kripke.FrameClass.Characteraizable 𝔽(𝓢 of α) 𝔽₂] :

LO.Sound 𝓢 (𝔽₂#α)

Equations

⋯ = ⋯

theorem LO.Propositional.Superintuitionistic.Kripke.unprovable_bot_of_characterizability {S : Type u} {α : Type u} [LO.System (LO.Propositional.Superintuitionistic.Formula α) S] {𝓢 : S} {𝔽₂ : LO.Kripke.FrameClass} [characterizability : LO.Kripke.FrameClass.Characteraizable 𝔽(𝓢 of α) 𝔽₂] :

instance LO.Propositional.Superintuitionistic.Kripke.instConsistentOfCharacterizability {S : Type u} {α : Type u} [LO.System (LO.Propositional.Superintuitionistic.Formula α) S] {𝓢 : S} {𝔽₂ : LO.Kripke.FrameClass} [LO.Kripke.FrameClass.Characteraizable 𝔽(𝓢 of α) 𝔽₂] :

LO.System.Consistent 𝓢

Equations

⋯ = ⋯

instance LO.Propositional.Superintuitionistic.Kripke.Int_Characteraizable {α : Type u} :

LO.Kripke.FrameClass.Characteraizable 𝔽(𝐈𝐧𝐭 of α) LO.Kripke.ReflexiveTransitiveFrameClass

Equations

LO.Propositional.Superintuitionistic.Kripke.Int_Characteraizable = { characterize := ⋯, nonempty := LO.Propositional.Superintuitionistic.Kripke.Int_Characteraizable.proof_2 }

instance LO.Propositional.Superintuitionistic.Kripke.Int_sound {α : Type u} :

LO.Sound 𝐈𝐧𝐭 (LO.Kripke.ReflexiveTransitiveFrameClass #α)

Equations

⋯ = ⋯

instance LO.Propositional.Superintuitionistic.Kripke.instConsistentFormulaDeductionParameterIntuitionistic {α : Type u} :

LO.System.Consistent 𝐈𝐧𝐭

Equations

⋯ = ⋯

instance LO.Propositional.Superintuitionistic.Kripke.Cl_Characteraizable {α : Type u} :

LO.Kripke.FrameClass.Characteraizable 𝔽(𝐂𝐥 of α) fun (F : LO.Kripke.Frame) => Reflexive F.Rel ∧ Transitive F.Rel ∧ Symmetric F.Rel

Equations

LO.Propositional.Superintuitionistic.Kripke.Cl_Characteraizable = { characterize := ⋯, nonempty := LO.Propositional.Superintuitionistic.Kripke.Cl_Characteraizable.proof_2 }

instance LO.Propositional.Superintuitionistic.Kripke.instSoundDeductionParameterFormulaDepClassicalAltReflexiveTransitiveSymmetricFrameClass {α : Type u} :

LO.Sound 𝐂𝐥 (LO.Kripke.ReflexiveTransitiveSymmetricFrameClass #α)

Equations

⋯ = ⋯

instance LO.Propositional.Superintuitionistic.Kripke.instConsistentFormulaDeductionParameterClassical {α : Type u} :

LO.System.Consistent 𝐂𝐥

Equations

⋯ = ⋯

instance LO.Propositional.Superintuitionistic.Kripke.KC_Characteraizable {α : Type u} :

LO.Kripke.FrameClass.Characteraizable 𝔽(𝐊𝐂 of α) LO.Kripke.ReflexiveTransitiveConfluentFrameClass

Equations

LO.Propositional.Superintuitionistic.Kripke.KC_Characteraizable = { characterize := ⋯, nonempty := LO.Propositional.Superintuitionistic.Kripke.KC_Characteraizable.proof_2 }

instance LO.Propositional.Superintuitionistic.Kripke.instSoundDeductionParameterFormulaDepKCAltReflexiveTransitiveConfluentFrameClass {α : Type u} :

LO.Sound 𝐊𝐂 (LO.Kripke.ReflexiveTransitiveConfluentFrameClass #α)

Equations

⋯ = ⋯

instance LO.Propositional.Superintuitionistic.Kripke.instConsistentFormulaDeductionParameterKC {α : Type u} :

LO.System.Consistent 𝐊𝐂

Equations

⋯ = ⋯

instance LO.Propositional.Superintuitionistic.Kripke.LC_Characteraizable {α : Type u} :

LO.Kripke.FrameClass.Characteraizable 𝔽(𝐋𝐂 of α) LO.Kripke.ReflexiveTransitiveConnectedFrameClass

Equations

LO.Propositional.Superintuitionistic.Kripke.LC_Characteraizable = { characterize := ⋯, nonempty := LO.Propositional.Superintuitionistic.Kripke.LC_Characteraizable.proof_2 }

instance LO.Propositional.Superintuitionistic.Kripke.instSoundDeductionParameterFormulaDepLCAltReflexiveTransitiveConnectedFrameClass {α : Type u} :

LO.Sound 𝐋𝐂 (LO.Kripke.ReflexiveTransitiveConnectedFrameClass #α)

Equations

⋯ = ⋯

instance LO.Propositional.Superintuitionistic.Kripke.instConsistentFormulaDeductionParameterLC {α : Type u} :

LO.System.Consistent 𝐋𝐂

Equations

⋯ = ⋯

@[reducible, inline]

abbrev LO.Propositional.Superintuitionistic.Formula.Kripke.ClassicalSatisfies {α : Type u} (V : LO.Kripke.ClassicalValuation α) (p : LO.Propositional.Superintuitionistic.Formula α) :

Equations

LO.Propositional.Superintuitionistic.Formula.Kripke.ClassicalSatisfies V p = LO.Propositional.Superintuitionistic.Formula.Kripke.Satisfies (LO.Kripke.ClassicalModel V) () p

Instances For

instance LO.Propositional.Superintuitionistic.Formula.Kripke.instSemanticsClassicalValuation {α : Type u} :

LO.Semantics (LO.Propositional.Superintuitionistic.Formula α) (LO.Kripke.ClassicalValuation α)

Equations

LO.Propositional.Superintuitionistic.Formula.Kripke.instSemanticsClassicalValuation = { Realize := LO.Propositional.Superintuitionistic.Formula.Kripke.ClassicalSatisfies }

@[simp]

theorem LO.Propositional.Superintuitionistic.Formula.Kripke.ClassicalSatisfies.atom_def {α : Type u} {V : LO.Kripke.ClassicalValuation α} {a : α} :

V ⊧ LO.Propositional.Superintuitionistic.Formula.atom a ↔ V a

instance LO.Propositional.Superintuitionistic.Formula.Kripke.ClassicalSatisfies.instTarskiClassicalValuation {α : Type u} :

LO.Semantics.Tarski (LO.Kripke.ClassicalValuation α)

Equations

LO.Propositional.Superintuitionistic.Formula.Kripke.ClassicalSatisfies.instTarskiClassicalValuation = LO.Semantics.Tarski.mk

theorem LO.Propositional.Superintuitionistic.Kripke.ValidOnClassicalFrame_iff {α : Type u} {p : LO.Propositional.Superintuitionistic.Formula α} :

𝔽(𝐂𝐥 of α) ⊧ p → ∀ (V : LO.Kripke.ClassicalValuation α), V ⊧ p

theorem LO.Propositional.Superintuitionistic.Kripke.notClassicalValid_of_exists_ClassicalValuation {α : Type u} {p : LO.Propositional.Superintuitionistic.Formula α} :

(∃ (V : LO.Kripke.ClassicalValuation α), ¬V ⊧ p) → ¬𝔽(𝐂𝐥 of α) ⊧ p

theorem LO.Propositional.Superintuitionistic.Kripke.unprovable_classical_of_exists_ClassicalValuation {α : Type u} {p : LO.Propositional.Superintuitionistic.Formula α} (h : ∃ (V : LO.Kripke.ClassicalValuation α), ¬V ⊧ p) :

𝐂𝐥 ⊬! p