Documentation

Foundation.IntProp.Kripke.Basic

source
structure LO.IntProp.Kripke.Frame :
Type 1
Instances For
source
instance LO.IntProp.Kripke.instCoeSortFrameType :
CoeSort Frame Type
Equations
source
instance LO.IntProp.Kripke.instCoeFunFrameForallWorldForallProp :
CoeFun Frame fun (F : Frame) => F.World → F.World → Prop
Equations
source
instance LO.IntProp.Kripke.instNonemptyWorld {F : Frame} :
Nonempty F.World
source
instance LO.IntProp.Kripke.instIsPartialOrderWorldRel {F : Frame} :
IsPartialOrder F.World F.Rel
source
@[reducible, inline]
abbrev LO.IntProp.Kripke.Frame.Rel' {F : Frame} (x y : F.World) :
Prop
Equations
  • (x ≺ y) = F.Rel x y
source
def LO.IntProp.Kripke.«term_≺_» :
Lean.TrailingParserDescr
Equations
source
theorem LO.IntProp.Kripke.Frame.rel_trans {F : Frame} {x y z : F.World} :
x ≺ y → y ≺ z → x ≺ z
source
theorem LO.IntProp.Kripke.Frame.rel_trans' {F : Frame} :
Transitive F.Rel
source
@[simp]
theorem LO.IntProp.Kripke.Frame.rel_refl {F : Frame} {x : F.World} :
x ≺ x
source
theorem LO.IntProp.Kripke.Frame.rel_refl' {F : Frame} :
Reflexive F.Rel
source
@[simp]
theorem LO.IntProp.Kripke.Frame.rel_antisymm {F : Frame} {x y : F.World} :
x ≺ y → y ≺ x → x = y
source
theorem LO.IntProp.Kripke.Frame.rel_antisymm' {F : Frame} :
AntiSymmetric F.Rel
source
@[reducible, inline]
abbrev LO.IntProp.Kripke.pointFrame :
Frame
Equations
source
@[reducible, inline]
abbrev LO.IntProp.Kripke.FrameClass :
Type 1
Equations
Instances For
source
@[reducible, inline]
abbrev LO.IntProp.Kripke.AllFrameClass :
FrameClass
Equations
Instances For
source
@[reducible, inline]
abbrev LO.IntProp.Kripke.SymmetricFrameClass :
FrameClass
Equations
source
@[reducible, inline]
abbrev LO.IntProp.Kripke.ConfluentFrameClass :
FrameClass
Equations
Instances For
source
@[reducible, inline]
abbrev LO.IntProp.Kripke.ConnectedFrameClass :
FrameClass
Equations
Instances For
source
@[reducible, inline]
abbrev LO.IntProp.Kripke.EuclideanFrameClass :
FrameClass
Equations
Instances For
source
structure LO.IntProp.Kripke.Valuation (F : Frame) :
Type
  • Val : F.World → ℕ → Prop
  • hereditary {w₁ w₂ : F.World} : w₁ ≺ w₂ → ∀ {a : ℕ}, self.Val w₁ a → self.Val w₂ a
Instances For
source
instance LO.IntProp.Kripke.instCoeFunValuationForallWorldForallNatProp {F : Frame} :
CoeFun (Valuation F) fun (x : Valuation F) => F.World → ℕ → Prop
Equations
source
structure LO.IntProp.Kripke.Modelextends LO.IntProp.Kripke.Frame :
Type 1
Instances For
source
instance LO.IntProp.Kripke.instCoeFunModelForallWorldForallNatProp :
CoeFun Model fun (M : Model) => M.World → ℕ → Prop
Equations
source
def LO.IntProp.Formula.Kripke.Satisfies (M : Kripke.Model) (w : M.World) :
Formula ℕ → Prop
Equations
source
instance LO.IntProp.Formula.Kripke.Satisfies.semantics (M : Kripke.Model) :
Semantics (Formula ℕ) M.World
Equations
source
@[simp]
theorem LO.IntProp.Formula.Kripke.Satisfies.iff_models {M : Kripke.Model} {w : M.World} {φ : Formula ℕ} :
w ⊧ φ ↔ Satisfies M w φ
source
@[simp]
theorem LO.IntProp.Formula.Kripke.Satisfies.atom_def {M : Kripke.Model} {w : M.World} {a : ℕ} :
w ⊧ atom a ↔ M.Val.Val w a
source
@[simp]
theorem LO.IntProp.Formula.Kripke.Satisfies.top_def {M : Kripke.Model} {w : M.World} :
w ⊧ ⊤ ↔ True
source
@[simp]
theorem LO.IntProp.Formula.Kripke.Satisfies.bot_def {M : Kripke.Model} {w : M.World} :
w ⊧ ⊥ ↔ False
source
@[simp]
theorem LO.IntProp.Formula.Kripke.Satisfies.and_def {M : Kripke.Model} {w : M.World} {φ ψ : Formula ℕ} :
w ⊧ φ ⋏ ψ ↔ w ⊧ φ ∧ w ⊧ ψ
source
@[simp]
theorem LO.IntProp.Formula.Kripke.Satisfies.or_def {M : Kripke.Model} {w : M.World} {φ ψ : Formula ℕ} :
w ⊧ φ ⋎ ψ ↔ w ⊧ φ ∨ w ⊧ ψ
source
@[simp]
theorem LO.IntProp.Formula.Kripke.Satisfies.imp_def {M : Kripke.Model} {w : M.World} {φ ψ : Formula ℕ} :
w ⊧ φ ➝ ψ ↔ ∀ {w' : M.World}, w ≺ w' → w' ⊧ φ → w' ⊧ ψ
source
@[simp]
theorem LO.IntProp.Formula.Kripke.Satisfies.neg_def {M : Kripke.Model} {w : M.World} {φ : Formula ℕ} :
w ⊧ ∼φ ↔ ∀ {w' : M.World}, w ≺ w' → ¬w' ⊧ φ
source
instance LO.IntProp.Formula.Kripke.Satisfies.instTopWorldNat {M : Kripke.Model} :
Semantics.Top M.World
source
instance LO.IntProp.Formula.Kripke.Satisfies.instBotWorldNat {M : Kripke.Model} :
Semantics.Bot M.World
source
instance LO.IntProp.Formula.Kripke.Satisfies.instAndWorldNat {M : Kripke.Model} :
Semantics.And M.World
source
instance LO.IntProp.Formula.Kripke.Satisfies.instOrWorldNat {M : Kripke.Model} :
Semantics.Or M.World
source
theorem LO.IntProp.Formula.Kripke.Satisfies.formula_hereditary {M : Kripke.Model} {w w' : M.World} {φ : Formula ℕ} (hw : w ≺ w') :
w ⊧ φ → w' ⊧ φ
source
theorem LO.IntProp.Formula.Kripke.Satisfies.neg_equiv {M : Kripke.Model} {w : M.World} {φ : Formula ℕ} :
w ⊧ ∼φ ↔ w ⊧ φ ➝ ⊥
source
def LO.IntProp.Formula.Kripke.ValidOnModel (M : Kripke.Model) (φ : Formula ℕ) :
Prop
Equations
source
instance LO.IntProp.Formula.Kripke.ValidOnModel.semantics :
Semantics (Formula ℕ) Kripke.Model
Equations
source
@[simp]
theorem LO.IntProp.Formula.Kripke.ValidOnModel.iff_models {M : Kripke.Model} {φ : Formula ℕ} :
M ⊧ φ ↔ ValidOnModel M φ
source
theorem LO.IntProp.Formula.Kripke.ValidOnModel.verum {M : Kripke.Model} :
M ⊧ ⊤
source
theorem LO.IntProp.Formula.Kripke.ValidOnModel.andElim₁ {M : Kripke.Model} {φ ψ : Formula ℕ} :
M ⊧ φ ⋏ ψ ➝ φ
source
theorem LO.IntProp.Formula.Kripke.ValidOnModel.andElim₂ {M : Kripke.Model} {φ ψ : Formula ℕ} :
M ⊧ φ ⋏ ψ ➝ ψ
source
theorem LO.IntProp.Formula.Kripke.ValidOnModel.andInst₃ {M : Kripke.Model} {φ ψ : Formula ℕ} :
M ⊧ φ ➝ ψ ➝ φ ⋏ ψ
source
theorem LO.IntProp.Formula.Kripke.ValidOnModel.orInst₁ {M : Kripke.Model} {φ ψ : Formula ℕ} :
M ⊧ φ ➝ φ ⋎ ψ
source
theorem LO.IntProp.Formula.Kripke.ValidOnModel.orInst₂ {M : Kripke.Model} {φ ψ : Formula ℕ} :
M ⊧ ψ ➝ φ ⋎ ψ
source
theorem LO.IntProp.Formula.Kripke.ValidOnModel.orElim {M : Kripke.Model} {φ ψ χ : Formula ℕ} :
M ⊧ (φ ➝ χ) ➝ (ψ ➝ χ) ➝ φ ⋎ ψ ➝ χ
source
theorem LO.IntProp.Formula.Kripke.ValidOnModel.imply₁ {M : Kripke.Model} {φ ψ : Formula ℕ} :
M ⊧ φ ➝ ψ ➝ φ
source
theorem LO.IntProp.Formula.Kripke.ValidOnModel.imply₂ {M : Kripke.Model} {φ ψ χ : Formula ℕ} :
M ⊧ (φ ➝ ψ ➝ χ) ➝ (φ ➝ ψ) ➝ φ ➝ χ
source
theorem LO.IntProp.Formula.Kripke.ValidOnModel.mdp {M : Kripke.Model} {φ ψ : Formula ℕ} (hpq : M ⊧ φ ➝ ψ) (hp : M ⊧ φ) :
M ⊧ ψ
source
theorem LO.IntProp.Formula.Kripke.ValidOnModel.bot {M : Kripke.Model} :
¬M ⊧ ⊥
source
instance LO.IntProp.Formula.Kripke.ValidOnModel.instBotModelNat :
Semantics.Bot Kripke.Model
source
theorem LO.IntProp.Formula.Kripke.ValidOnModel.efq {M : Kripke.Model} {φ : Formula ℕ} :
M ⊧ Axioms.EFQ φ
source
theorem LO.IntProp.Formula.Kripke.ValidOnModel.neg_equiv {M : Kripke.Model} {φ : Formula ℕ} :
M ⊧ Axioms.NegEquiv φ
source
theorem LO.IntProp.Formula.Kripke.ValidOnModel.lem {M : Kripke.Model} {φ : Formula ℕ} :
Symmetric M.Rel → M ⊧ Axioms.LEM φ
source
theorem LO.IntProp.Formula.Kripke.ValidOnModel.dum {M : Kripke.Model} {φ ψ : Formula ℕ} :
Connected M.Rel → M ⊧ Axioms.Dummett φ ψ
source
theorem LO.IntProp.Formula.Kripke.ValidOnModel.wlem {M : Kripke.Model} {φ : Formula ℕ} :
Confluent M.Rel → M ⊧ Axioms.WeakLEM φ
source
def LO.IntProp.Formula.Kripke.ValidOnFrame (F : Kripke.Frame) (φ : Formula ℕ) :
Prop
Equations
source
instance LO.IntProp.Formula.Kripke.ValidOnFrame.semantics :
Semantics (Formula ℕ) Kripke.Frame
Equations
source
@[simp]
theorem LO.IntProp.Formula.Kripke.ValidOnFrame.models_iff {F : Kripke.Frame} {φ : Formula ℕ} :
F ⊧ φ ↔ ValidOnFrame F φ
source
theorem LO.IntProp.Formula.Kripke.ValidOnFrame.verum {F : Kripke.Frame} :
F ⊧ ⊤
source
theorem LO.IntProp.Formula.Kripke.ValidOnFrame.andElim₁ {F : Kripke.Frame} {φ ψ : Formula ℕ} :
F ⊧ φ ⋏ ψ ➝ φ
source
theorem LO.IntProp.Formula.Kripke.ValidOnFrame.andElim₂ {F : Kripke.Frame} {φ ψ : Formula ℕ} :
F ⊧ φ ⋏ ψ ➝ ψ
source
theorem LO.IntProp.Formula.Kripke.ValidOnFrame.andInst₃ {F : Kripke.Frame} {φ ψ : Formula ℕ} :
F ⊧ φ ➝ ψ ➝ φ ⋏ ψ
source
theorem LO.IntProp.Formula.Kripke.ValidOnFrame.orInst₁ {F : Kripke.Frame} {φ ψ : Formula ℕ} :
F ⊧ φ ➝ φ ⋎ ψ
source
theorem LO.IntProp.Formula.Kripke.ValidOnFrame.orInst₂ {F : Kripke.Frame} {φ ψ : Formula ℕ} :
F ⊧ ψ ➝ φ ⋎ ψ
source
theorem LO.IntProp.Formula.Kripke.ValidOnFrame.orElim {F : Kripke.Frame} {φ ψ χ : Formula ℕ} :
F ⊧ (φ ➝ χ) ➝ (ψ ➝ χ) ➝ φ ⋎ ψ ➝ χ
source
theorem LO.IntProp.Formula.Kripke.ValidOnFrame.imply₁ {F : Kripke.Frame} {φ ψ : Formula ℕ} :
F ⊧ φ ➝ ψ ➝ φ
source
theorem LO.IntProp.Formula.Kripke.ValidOnFrame.imply₂ {F : Kripke.Frame} {φ ψ χ : Formula ℕ} :
F ⊧ (φ ➝ ψ ➝ χ) ➝ (φ ➝ ψ) ➝ φ ➝ χ
source
theorem LO.IntProp.Formula.Kripke.ValidOnFrame.mdp {F : Kripke.Frame} {φ ψ : Formula ℕ} (hpq : F ⊧ φ ➝ ψ) (hp : F ⊧ φ) :
F ⊧ ψ
source
theorem LO.IntProp.Formula.Kripke.ValidOnFrame.efq {F : Kripke.Frame} {φ : Formula ℕ} :
F ⊧ Axioms.EFQ φ
source
theorem LO.IntProp.Formula.Kripke.ValidOnFrame.neg_equiv {F : Kripke.Frame} {φ : Formula ℕ} :
F ⊧ Axioms.NegEquiv φ
source
theorem LO.IntProp.Formula.Kripke.ValidOnFrame.lem {F : Kripke.Frame} {φ : Formula ℕ} (F_symm : Symmetric F.Rel) :
F ⊧ Axioms.LEM φ
source
theorem LO.IntProp.Formula.Kripke.ValidOnFrame.dum {F : Kripke.Frame} {φ ψ : Formula ℕ} (F_conn : Connected F.Rel) :
F ⊧ Axioms.Dummett φ ψ
source
theorem LO.IntProp.Formula.Kripke.ValidOnFrame.wlem {F : Kripke.Frame} {φ : Formula ℕ} (F_conf : Confluent F.Rel) :
F ⊧ Axioms.WeakLEM φ
source
theorem LO.IntProp.Formula.Kripke.ValidOnFrame.top {F : Kripke.Frame} :
F ⊧ ⊤
source
instance LO.IntProp.Formula.Kripke.ValidOnFrame.instTopFrameNat :
Semantics.Top Kripke.Frame
source
theorem LO.IntProp.Formula.Kripke.ValidOnFrame.bot {F : Kripke.Frame} :
¬F ⊧ ⊥
source
instance LO.IntProp.Formula.Kripke.ValidOnFrame.instBotFrameNat :
Semantics.Bot Kripke.Frame
source
def LO.IntProp.Formula.Kripke.ValidOnFrameClass (C : Kripke.FrameClass) (φ : Formula ℕ) :
Prop
Equations
source
instance LO.IntProp.Formula.Kripke.ValidOnFrameClass.semantics :
Semantics (Formula ℕ) Kripke.FrameClass
Equations
source
@[simp]
theorem LO.IntProp.Formula.Kripke.ValidOnFrameClass.models_iff {C : Kripke.FrameClass} {φ : Formula ℕ} :
C ⊧ φ ↔ ValidOnFrameClass C φ
source
theorem LO.IntProp.Formula.Kripke.ValidOnFrameClass.bot {C : Kripke.FrameClass} (h_nonempty : Set.Nonempty C) :
¬C ⊧ ⊥
source
def LO.IntProp.Kripke.Frame.theorems (F : Frame) :
Set (Formula ℕ)

A set of formula that valid on frame F.

Equations
source
def LO.IntProp.Kripke.FrameClass.DefinedBy (C : FrameClass) (T : Set (Formula ℕ)) :
Prop
Equations
source
theorem LO.IntProp.Hilbert.Kripke.sound_hilbert_of_frameclass {φ : Formula ℕ} {C : Kripke.FrameClass} {T : Set (Formula ℕ)} (definedBy : C.DefinedBy T) :
{ axioms := 𝗘𝗙𝗤 ∪ T } ⊢! φ → C ⊧ φ
source
theorem LO.IntProp.Hilbert.Kripke.sound_of_equiv_frameclass_hilbert {H : Hilbert ℕ} {φ : Formula ℕ} {C : Kripke.FrameClass} {T : Set (Formula ℕ)} (definedBy : C.DefinedBy T) (heq : { axioms := 𝗘𝗙𝗤 ∪ T } =ₛ H) :
H ⊢! φ → C ⊧ φ
source
instance LO.IntProp.Hilbert.Kripke.instSound {H : Hilbert ℕ} {C : Kripke.FrameClass} {T : Set (Formula ℕ)} (definedBy : C.DefinedBy T) (heq : { axioms := 𝗘𝗙𝗤 ∪ T } =ₛ H) :
Sound H C
source
theorem LO.IntProp.Hilbert.Kripke.unprovable_bot {H : Hilbert ℕ} {C : Kripke.FrameClass} [sound : Sound H C] (hNonempty : Set.Nonempty C) :
H ⊬ ⊥
source
theorem LO.IntProp.Hilbert.Kripke.consistent {H : Hilbert ℕ} {C : Kripke.FrameClass} [Sound H C] (h_nonempty : Set.Nonempty C) :
H.Consistent
source
instance LO.IntProp.Hilbert.Int.Kripke.sound :
Sound (Hilbert.Int ℕ) Kripke.AllFrameClass
source
instance LO.IntProp.Hilbert.Int.instConsistentNat :
(Hilbert.Int ℕ).Consistent
source
instance LO.IntProp.Hilbert.KC.Kripke.sound :
Sound (Hilbert.KC ℕ) Kripke.ConfluentFrameClass
source
instance LO.IntProp.Hilbert.KC.instConsistentNat :
(Hilbert.KC ℕ).Consistent
source
instance LO.IntProp.Hilbert.LC.Kripke.sound :
Sound (Hilbert.LC ℕ) Kripke.ConnectedFrameClass
source
instance LO.IntProp.Hilbert.LC.instConsistentNat :
(Hilbert.LC ℕ).Consistent
source
instance LO.IntProp.Hilbert.Cl.Kripke.sound :
Sound (Hilbert.Cl ℕ) Kripke.EuclideanFrameClass
source
instance LO.IntProp.Hilbert.Cl.instConsistentNat :
(Hilbert.Cl ℕ).Consistent