Documentation

Logic.IntProp.Kripke.Semantics

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

LO.IntProp.Formula α → Prop

Equations

LO.IntProp.Formula.Kripke.Satisfies M w (LO.IntProp.Formula.atom a) = M.Valuation w a
LO.IntProp.Formula.Kripke.Satisfies M w LO.IntProp.Formula.verum = True
LO.IntProp.Formula.Kripke.Satisfies M w LO.IntProp.Formula.falsum = False
LO.IntProp.Formula.Kripke.Satisfies M w (p.and q) = (LO.IntProp.Formula.Kripke.Satisfies M w p ∧ LO.IntProp.Formula.Kripke.Satisfies M w q)
LO.IntProp.Formula.Kripke.Satisfies M w (p.or q) = (LO.IntProp.Formula.Kripke.Satisfies M w p ∨ LO.IntProp.Formula.Kripke.Satisfies M w q)
LO.IntProp.Formula.Kripke.Satisfies M w p.neg = ∀ {w' : M.World}, w ≺ w' → ¬LO.IntProp.Formula.Kripke.Satisfies M w' p
LO.IntProp.Formula.Kripke.Satisfies M w (p.imp q) = ∀ {w' : M.World}, w ≺ w' → LO.IntProp.Formula.Kripke.Satisfies M w' p → LO.IntProp.Formula.Kripke.Satisfies M w' q

Instances For

instance LO.IntProp.Formula.Kripke.Satisfies.semantics {α : Type u} (M : LO.Kripke.Model α) :

LO.Semantics (LO.IntProp.Formula α) M.World

Equations

LO.IntProp.Formula.Kripke.Satisfies.semantics M = { Realize := fun (w : M.World) => LO.IntProp.Formula.Kripke.Satisfies M w }

@[simp]

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

w ⊧ p ↔ LO.IntProp.Formula.Kripke.Satisfies M w p

@[simp]

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

w ⊧ LO.IntProp.Formula.atom a ↔ M.Valuation w a

@[simp]

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

w ⊧ ⊤ ↔ True

@[simp]

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

w ⊧ ⊥ ↔ False

@[simp]

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

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

@[simp]

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

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

@[simp]

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

w ⊧ p ➝ q ↔ ∀ {w' : M.World}, w ≺ w' → w' ⊧ p → w' ⊧ q

@[simp]

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

w ⊧ ∼p ↔ ∀ {w' : M.World}, w ≺ w' → ¬w' ⊧ p

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

LO.Semantics.Top M.World

Equations

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

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

LO.Semantics.Bot M.World

Equations

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

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

LO.Semantics.And M.World

Equations

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

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

LO.Semantics.Or M.World

Equations

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

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

w ⊧ p → w' ⊧ p

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

w ⊧ ∼p ↔ w ⊧ p ➝ ⊥

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

Equations

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

Instances For

instance LO.IntProp.Formula.Kripke.ValidOnModel.semantics {α : Type u} :

LO.Semantics (LO.IntProp.Formula α) (LO.Kripke.Model α)

Equations

LO.IntProp.Formula.Kripke.ValidOnModel.semantics = { Realize := fun (M : LO.Kripke.Model α) => LO.IntProp.Formula.Kripke.ValidOnModel M }

@[simp]

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

M ⊧ p ↔ LO.IntProp.Formula.Kripke.ValidOnModel M p

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

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

M ⊧ p ⋏ q ➝ p

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

M ⊧ p ⋏ q ➝ q

theorem LO.IntProp.Formula.Kripke.ValidOnModel.and₃ {α : Type u} {M : LO.Kripke.Model α} {p : LO.IntProp.Formula α} {q : LO.IntProp.Formula α} (atom_hereditary : ∀ {w₁ w₂ : M.World}, 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.IntProp.Formula.Kripke.ValidOnModel.or₁ {α : Type u} {M : LO.Kripke.Model α} {p : LO.IntProp.Formula α} {q : LO.IntProp.Formula α} :

M ⊧ p ➝ p ⋎ q

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

M ⊧ q ➝ p ⋎ q

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

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

theorem LO.IntProp.Formula.Kripke.ValidOnModel.imply₁ {α : Type u} {M : LO.Kripke.Model α} {p : LO.IntProp.Formula α} {q : LO.IntProp.Formula α} (atom_hereditary : ∀ {w₁ w₂ : M.World}, 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.IntProp.Formula.Kripke.ValidOnModel.imply₂ {α : Type u} {M : LO.Kripke.Model α} {p : LO.IntProp.Formula α} {q : LO.IntProp.Formula α} {r : LO.IntProp.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.IntProp.Formula.Kripke.ValidOnModel.mdp {α : Type u} {M : LO.Kripke.Model α} {p : LO.IntProp.Formula α} {q : LO.IntProp.Formula α} (F_refl : autoParam (Reflexive M.Frame.Rel) _auto✝) (hpq : M ⊧ p ➝ q) (hp : M ⊧ p) :

M ⊧ q

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

M ⊧ LO.Axioms.EFQ p

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

M ⊧ LO.Axioms.NegEquiv p

theorem LO.IntProp.Formula.Kripke.ValidOnModel.lem {α : Type u} {M : LO.Kripke.Model α} {p : LO.IntProp.Formula α} (atom_hereditary : ∀ {w₁ w₂ : M.World}, 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.IntProp.Formula.Kripke.ValidOnModel.dum {α : Type u} {M : LO.Kripke.Model α} {p : LO.IntProp.Formula α} {q : LO.IntProp.Formula α} (atom_hereditary : ∀ {w₁ w₂ : M.World}, 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.IntProp.Formula.Kripke.ValidOnModel.wlem {α : Type u} {M : LO.Kripke.Model α} {p : LO.IntProp.Formula α} (atom_hereditary : ∀ {w₁ w₂ : M.World}, 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.IntProp.Formula.Kripke.ValidOnFrame {α : Type u} (F : LO.Kripke.Frame) (p : LO.IntProp.Formula α) :

Equations

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

Instances For

instance LO.IntProp.Formula.Kripke.ValidOnFrame.semantics {α : Type u} :

LO.Semantics (LO.IntProp.Formula α) (LO.Kripke.Frame.Dep α)

Equations

LO.IntProp.Formula.Kripke.ValidOnFrame.semantics = { Realize := fun (F : LO.Kripke.Frame.Dep α) => LO.IntProp.Formula.Kripke.ValidOnFrame F }

@[simp]

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

F ⊧ f ↔ LO.IntProp.Formula.Kripke.ValidOnFrame F f

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

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

F ⊧ p ⋏ q ➝ p

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

F ⊧ p ⋏ q ➝ q

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

F ⊧ p ➝ q ➝ p ⋏ q

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

F ⊧ p ➝ p ⋎ q

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

F ⊧ q ➝ p ⋎ q

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

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

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

F ⊧ p ➝ q ➝ p

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

F ⊧ (p ➝ q ➝ r) ➝ (p ➝ q) ➝ p ➝ r

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

F ⊧ q

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

F ⊧ LO.Axioms.EFQ p

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

F ⊧ LO.Axioms.NegEquiv p

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

F ⊧ LO.Axioms.LEM p

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

F ⊧ LO.Axioms.GD p q

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

F ⊧ LO.Axioms.WeakLEM p

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

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

Equations

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

def LO.IntProp.Formula.Kripke.ValidOnFrameClass {α : Type u} (𝔽 : LO.Kripke.FrameClass) (p : LO.IntProp.Formula α) :

Equations

LO.IntProp.Formula.Kripke.ValidOnFrameClass 𝔽 p = ∀ {F : LO.Kripke.Frame}, F ∈ 𝔽 → F#α ⊧ p

Instances For

instance LO.IntProp.Formula.Kripke.ValidOnFrameClass.semantics {α : Type u} :

LO.Semantics (LO.IntProp.Formula α) (LO.Kripke.FrameClass.Dep α)

Equations

LO.IntProp.Formula.Kripke.ValidOnFrameClass.semantics = { Realize := fun (𝔽 : LO.Kripke.FrameClass.Dep α) => LO.IntProp.Formula.Kripke.ValidOnFrameClass 𝔽 }

@[simp]

theorem LO.IntProp.Formula.Kripke.ValidOnFrameClass.models_iff {α : Type u} {𝔽 : LO.Kripke.FrameClass.Dep α} {p : LO.IntProp.Formula α} :

𝔽 ⊧ p ↔ LO.IntProp.Formula.Kripke.ValidOnFrameClass 𝔽 p

@[reducible, inline]

abbrev LO.IntProp.Kripke.FrameClassOfTheory {α : Type u} (T : LO.IntProp.Theory α) :

LO.Kripke.FrameClass.Dep α

Equations

𝔽(T) = {F : LO.Kripke.Frame | F#α ⊧* T}

Instances For

def LO.IntProp.Kripke.«term𝔽(_)» :

Lean.ParserDescr

Equations

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

Instances For

@[reducible, inline]

abbrev LO.IntProp.Kripke.FrameClassOfHilbert {α : Type u} (Λ : LO.IntProp.Hilbert α) :

LO.Kripke.FrameClass.Dep α

Equations

𝔽(Λ) = 𝔽(LO.System.theory Λ)

Instances For

def LO.IntProp.Kripke.«term𝔽(_)_1» :

Lean.ParserDescr

Equations

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

Instances For

theorem LO.IntProp.Kripke.sound {α : Type u} {Λ : LO.IntProp.Hilbert α} {p : LO.IntProp.Formula α} :

Λ ⊢! p → 𝔽(Λ) ⊧ p

instance LO.IntProp.Kripke.instSoundHilbertFormulaDepFrameClassOfHilbert {α : Type u} {Λ : LO.IntProp.Hilbert α} :

LO.Sound Λ 𝔽(Λ)

Equations

⋯ = ⋯

theorem LO.IntProp.Kripke.unprovable_bot {α : Type u} {Λ : LO.IntProp.Hilbert α} (hc : Set.Nonempty 𝔽(Λ)) :

instance LO.IntProp.Kripke.instConsistentFormulaHilbertOfNonemptyFrameFrameClassOfHilbert {α : Type u} {Λ : LO.IntProp.Hilbert α} (hc : Set.Nonempty 𝔽(Λ)) :

LO.System.Consistent Λ

Equations

⋯ = ⋯

theorem LO.IntProp.Kripke.sound_of_characterizability {α : Type u} {Λ : LO.IntProp.Hilbert α} {p : LO.IntProp.Formula α} {𝔽₂ : LO.Kripke.FrameClass} [characterizability : LO.Kripke.FrameClass.Characteraizable 𝔽(Λ) 𝔽₂] :

Λ ⊢! p → 𝔽₂#α ⊧ p

instance LO.IntProp.Kripke.instSoundOfCharacterizability {α : Type u} {Λ : LO.IntProp.Hilbert α} {𝔽₂ : LO.Kripke.FrameClass} [LO.Kripke.FrameClass.Characteraizable 𝔽(Λ) 𝔽₂] :

LO.Sound Λ 𝔽₂#α

Equations

⋯ = ⋯

theorem LO.IntProp.Kripke.unprovable_bot_of_characterizability {α : Type u} {Λ : LO.IntProp.Hilbert α} {𝔽₂ : LO.Kripke.FrameClass} [characterizability : LO.Kripke.FrameClass.Characteraizable 𝔽(Λ) 𝔽₂] :

instance LO.IntProp.Kripke.instConsistentOfCharacterizability {α : Type u} {Λ : LO.IntProp.Hilbert α} {𝔽₂ : LO.Kripke.FrameClass} [LO.Kripke.FrameClass.Characteraizable 𝔽(Λ) 𝔽₂] :

LO.System.Consistent Λ

Equations

⋯ = ⋯

instance LO.IntProp.Kripke.Int_Characteraizable {α : Type u} :

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

Equations

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

instance LO.IntProp.Kripke.Int_sound {α : Type u} :

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

Equations

⋯ = ⋯

instance LO.IntProp.Kripke.instConsistentFormulaHilbertIntuitionistic {α : Type u} :

LO.System.Consistent 𝐈𝐧𝐭

Equations

⋯ = ⋯

instance LO.IntProp.Kripke.Cl_Characteraizable {α : Type u} :

LO.Kripke.FrameClass.Characteraizable 𝔽(𝐂𝐥 ) LO.Kripke.ReflexiveTransitiveSymmetricFrameClass #α

Equations

LO.IntProp.Kripke.Cl_Characteraizable = { characterize := ⋯, nonempty := ⋯ }

instance LO.IntProp.Kripke.instSoundHilbertFormulaDepClassicalAltReflexiveTransitiveSymmetricFrameClass {α : Type u} :

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

Equations

⋯ = ⋯

instance LO.IntProp.Kripke.instConsistentFormulaHilbertClassical {α : Type u} :

LO.System.Consistent 𝐂𝐥

Equations

⋯ = ⋯

instance LO.IntProp.Kripke.KC_Characteraizable {α : Type u} :

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

Equations

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

instance LO.IntProp.Kripke.instSoundHilbertFormulaDepKCAltReflexiveTransitiveConfluentFrameClass {α : Type u} :

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

Equations

⋯ = ⋯

instance LO.IntProp.Kripke.instConsistentFormulaHilbertKC {α : Type u} :

LO.System.Consistent 𝐊𝐂

Equations

⋯ = ⋯

instance LO.IntProp.Kripke.LC_Characteraizable {α : Type u} :

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

Equations

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

instance LO.IntProp.Kripke.instSoundHilbertFormulaDepLCAltReflexiveTransitiveConnectedFrameClass {α : Type u} :

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

Equations

⋯ = ⋯

instance LO.IntProp.Kripke.instConsistentFormulaHilbertLC {α : Type u} :

LO.System.Consistent 𝐋𝐂

Equations

⋯ = ⋯

@[reducible, inline]

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

Equations

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

Instances For

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

LO.Semantics (LO.IntProp.Formula α) (LO.Kripke.ClassicalValuation α)

Equations

LO.IntProp.Formula.Kripke.instSemanticsClassicalValuation = { Realize := LO.IntProp.Formula.Kripke.ClassicalSatisfies }

@[simp]

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

V ⊧ LO.IntProp.Formula.atom a ↔ V a

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

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

Equations

LO.IntProp.Formula.Kripke.ClassicalSatisfies.instTarskiClassicalValuation = LO.Semantics.Tarski.mk

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

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

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

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

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