Foundation.Modal.Kripke.Geach

source

@[reducible, inline]

abbrev LO.Kripke.GeachConfluentFrameClass (t : GeachTaple) :

LO.Kripke.FrameClass

Equations

LO.Kripke.GeachConfluentFrameClass t = {F : LO.Kripke.Frame | GeachConfluent t F.Rel}

Instances For

source

@[reducible, inline]

abbrev LO.Kripke.MultiGeachConfluentFrameClass (ts : List GeachTaple) :

LO.Kripke.FrameClass

Equations

LO.Kripke.MultiGeachConfluentFrameClass ts = {F : LO.Kripke.Frame | MultiGeachConfluent ts F.Rel}

Instances For

source

@[simp]

theorem LO.Kripke.MultiGeachConfluentFrameClass.def_nil :

LO.Kripke.MultiGeachConfluentFrameClass [] = LO.Kripke.AllFrameClass

source

@[simp]

theorem LO.Kripke.MultiGeachConfluentFrameClass.def_one (t : GeachTaple) :

LO.Kripke.MultiGeachConfluentFrameClass [t] = LO.Kripke.GeachConfluentFrameClass t

source

theorem LO.Kripke.MultiGeachConfluentFrameClass.def_cons {t : GeachTaple} {ts : List GeachTaple} (ts_nil : ts ≠ []) :

LO.Kripke.MultiGeachConfluentFrameClass (t :: ts) = LO.Kripke.GeachConfluentFrameClass t ∩ LO.Kripke.MultiGeachConfluentFrameClass ts

source

@[reducible, inline]

abbrev LO.Kripke.FrameClass.IsGeach (𝔽 : LO.Kripke.FrameClass) (ts : List GeachTaple) :

Type

Equations

𝔽.IsGeach ts = 𝔽.DefinedBy (LO.Kripke.MultiGeachConfluentFrameClass ts)

Instances For

source

theorem LO.Kripke.FrameClass.IsGeach.equality {ts : List GeachTaple} {𝔽 : LO.Kripke.FrameClass} [geach : 𝔽.IsGeach ts] :

𝔽 = LO.Kripke.MultiGeachConfluentFrameClass ts

source

instance LO.Kripke.ReflexiveFrameClass.isGeach :

LO.Kripke.ReflexiveFrameClass.IsGeach [{ i := 0, j := 0, m := 1, n := 0 }]

Equations

LO.Kripke.ReflexiveFrameClass.isGeach = { define := @LO.Kripke.ReflexiveFrameClass.isGeach.proof_1, nonempty := LO.Kripke.ReflexiveFrameClass.isGeach.proof_2 }

source

instance LO.Kripke.instIsGeachSerialFrameClassConsGeachTapleMkOfNatNatNil :

LO.Kripke.SerialFrameClass.IsGeach [{ i := 0, j := 0, m := 1, n := 1 }]

Equations

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

source

instance LO.Kripke.TransitiveFrameClass.isGeach :

LO.Kripke.TransitiveFrameClass.IsGeach [{ i := 0, j := 2, m := 1, n := 0 }]

Equations

LO.Kripke.TransitiveFrameClass.isGeach = { define := @LO.Kripke.TransitiveFrameClass.isGeach.proof_1, nonempty := LO.Kripke.TransitiveFrameClass.isGeach.proof_2 }

source

instance LO.Kripke.instIsGeachReflexiveEuclideanFrameClassConsGeachTapleMkOfNatNatNil :

LO.Kripke.ReflexiveEuclideanFrameClass.IsGeach [{ i := 0, j := 0, m := 1, n := 0 }, { i := 1, j := 1, m := 0, n := 1 }]

Equations

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

source

instance LO.Kripke.instIsGeachReflexiveSymmetricFrameClassConsGeachTapleMkOfNatNatNil :

LO.Kripke.ReflexiveSymmetricFrameClass.IsGeach [{ i := 0, j := 0, m := 1, n := 0 }, { i := 0, j := 1, m := 0, n := 1 }]

Equations

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

source

instance LO.Kripke.instIsGeachPreorderFrameClassConsGeachTapleMkOfNatNatNil :

LO.Kripke.PreorderFrameClass.IsGeach [{ i := 0, j := 0, m := 1, n := 0 }, { i := 0, j := 2, m := 1, n := 0 }]

Equations

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

source

instance LO.Kripke.instIsGeachEquivalenceFrameClassConsGeachTapleMkOfNatNatNil :

LO.Kripke.EquivalenceFrameClass.IsGeach [{ i := 0, j := 0, m := 1, n := 0 }, { i := 0, j := 2, m := 1, n := 0 }, { i := 0, j := 1, m := 0, n := 1 }]

Equations

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

source

theorem LO.Modal.Kripke.axiomGeach_defines {α : Type u} [Inhabited α] {t : GeachTaple} {F : LO.Kripke.Frame} :

F#α ⊧* 𝗴𝗲(t) ↔ F ∈ LO.Kripke.GeachConfluentFrameClass t

source

instance LO.Modal.Kripke.axiomGeach_definability {α : Type u} [Inhabited α] {t : GeachTaple} :

𝔽(𝗴𝗲(t)).DefinedBy (LO.Kripke.GeachConfluentFrameClass t)

Equations

LO.Modal.Kripke.axiomGeach_definability = { define := ⋯, nonempty := ⋯ }

source

instance LO.Modal.Kripke.axiomT_defines {α : Type u} [Inhabited α] :

𝔽(𝗧 ).DefinedBy LO.Kripke.ReflexiveFrameClass

Equations

LO.Modal.Kripke.axiomT_defines = ⋯.mpr LO.Modal.Kripke.axiomGeach_definability

source

instance LO.Modal.Kripke.axiomFour_defines {α : Type u} [Inhabited α] :

𝔽(𝟰 ).DefinedBy LO.Kripke.TransitiveFrameClass

Equations

LO.Modal.Kripke.axiomFour_defines = ⋯.mpr LO.Modal.Kripke.axiomGeach_definability

source

theorem LO.Modal.Kripke.axiomMultiGeach_defines {α : Type u} [Inhabited α] {ts : List GeachTaple} {F : LO.Kripke.Frame} :

F#α ⊧* 𝗚𝗲(ts) ↔ F ∈ LO.Kripke.MultiGeachConfluentFrameClass ts

source

instance LO.Modal.Kripke.axiomMultiGeach_definability {α : Type u} [Inhabited α] {ts : List GeachTaple} :

𝔽(𝗚𝗲(ts)).DefinedBy (LO.Kripke.MultiGeachConfluentFrameClass ts)

Equations

LO.Modal.Kripke.axiomMultiGeach_definability = { define := ⋯, nonempty := ⋯ }

source

instance LO.Modal.Kripke.Geach_definability {α : Type u} [Inhabited α] {ts : List GeachTaple} :

LO.Kripke.FrameClass.DefinedBy 𝔽(𝐆𝐞(ts)) (LO.Kripke.MultiGeachConfluentFrameClass ts)

Equations

LO.Modal.Kripke.Geach_definability = inferInstance

source

instance LO.Modal.Kripke.sound_Geach {α : Type u} [Inhabited α] {ts : List GeachTaple} :

LO.Sound 𝐆𝐞(ts) (LO.Kripke.MultiGeachConfluentFrameClass ts)#α

Equations

⋯ = ⋯

source

instance LO.Modal.Kripke.instConsistentFormulaHilbertGeach {α : Type u} [Inhabited α] {ts : List GeachTaple} :

LO.System.Consistent 𝐆𝐞(ts)

Equations

⋯ = ⋯

source

instance LO.Modal.Kripke.instGeachLogicSound {α : Type u} [Inhabited α] {ts : List GeachTaple} {Λ : LO.Modal.Hilbert α} {𝔽 : LO.Kripke.FrameClass} [logic_geach : Λ.IsGeach ts] [class_geach : 𝔽.IsGeach ts] :

LO.Sound Λ 𝔽#α

Equations

⋯ = ⋯

source

instance LO.Modal.Kripke.KD_sound {α : Type u} [Inhabited α] :

LO.Sound 𝐊𝐃 LO.Kripke.SerialFrameClass #α

Equations

⋯ = ⋯

source

instance LO.Modal.Kripke.KT_sound {α : Type u} [Inhabited α] :

LO.Sound 𝐊𝐓 LO.Kripke.ReflexiveFrameClass #α

Equations

⋯ = ⋯

source

instance LO.Modal.Kripke.KTB_sound {α : Type u} [Inhabited α] :

LO.Sound 𝐊𝐓𝐁 LO.Kripke.ReflexiveSymmetricFrameClass #α

Equations

⋯ = ⋯

source

instance LO.Modal.Kripke.K4_sound {α : Type u} [Inhabited α] :

LO.Sound 𝐊𝟒 LO.Kripke.TransitiveFrameClass #α

Equations

⋯ = ⋯

source

instance LO.Modal.Kripke.S4_sound {α : Type u} [Inhabited α] :

LO.Sound 𝐒𝟒 LO.Kripke.PreorderFrameClass #α

Equations

⋯ = ⋯

source

@[deprecated]

theorem LO.Modal.Kripke.S4_sound_aux {α : Type u} [Inhabited α] {p : LO.Modal.Formula α} :

𝐒𝟒 ⊢! p → LO.Kripke.PreorderFrameClass #α ⊧ p

source

instance LO.Modal.Kripke.S5_sound {α : Type u} [Inhabited α] :

LO.Sound 𝐒𝟓 LO.Kripke.ReflexiveEuclideanFrameClass #α

Equations

⋯ = ⋯

source

instance LO.Modal.Kripke.KT4B_sound {α : Type u} [Inhabited α] :

LO.Sound 𝐊𝐓𝟒𝐁 LO.Kripke.EquivalenceFrameClass #α

Equations

⋯ = ⋯

source

theorem LO.Modal.Kripke.geachConfluent_CanonicalFrame {α : Type u} [DecidableEq α] {Ax : LO.Modal.Theory α} [LO.System.Consistent 𝜿Ax] {t : GeachTaple} (h : 𝗴𝗲(t) ⊆ Ax) :

GeachConfluent t (LO.Modal.Kripke.CanonicalFrame 𝜿Ax).Rel

source

theorem LO.Modal.Kripke.multiGeachConfluent_CanonicalFrame {α : Type u} [DecidableEq α] {Ax : LO.Modal.Theory α} [LO.System.Consistent 𝜿Ax] {ts : List GeachTaple} (h : 𝗚𝗲(ts) ⊆ Ax) :

MultiGeachConfluent ts (LO.Modal.Kripke.CanonicalFrame 𝜿Ax).Rel

source

instance LO.Modal.Kripke.instMultiGeachComplete {α : Type u} [Inhabited α] [DecidableEq α] {ts : List GeachTaple} :

LO.Complete (𝜿𝗚𝗲(ts)) (LO.Kripke.MultiGeachConfluentFrameClass ts)#α

Equations

⋯ = ⋯

source

instance LO.Modal.Kripke.instCompleteHilbertFormulaDepAltOfIsGeachOfIsGeach {α : Type u} [Inhabited α] [DecidableEq α] {ts : List GeachTaple} {Λ : LO.Modal.Hilbert α} {𝔽 : LO.Kripke.FrameClass} [logic_geach : Λ.IsGeach ts] [class_geach : 𝔽.IsGeach ts] :

LO.Complete Λ 𝔽#α

Equations

⋯ = ⋯

source

instance LO.Modal.Kripke.KT_complete {α : Type u} [Inhabited α] [DecidableEq α] :

LO.Complete 𝐊𝐓 LO.Kripke.ReflexiveFrameClass #α

Equations

⋯ = ⋯

source

instance LO.Modal.Kripke.KTB_complete {α : Type u} [Inhabited α] [DecidableEq α] :

LO.Complete 𝐊𝐓𝐁 LO.Kripke.ReflexiveSymmetricFrameClass #α

Equations

⋯ = ⋯

source

instance LO.Modal.Kripke.S4_complete {α : Type u} [Inhabited α] [DecidableEq α] :

LO.Complete 𝐒𝟒 LO.Kripke.PreorderFrameClass #α

Equations

⋯ = ⋯

source

instance LO.Modal.Kripke.K4_complete {α : Type u} [Inhabited α] [DecidableEq α] :

LO.Complete 𝐊𝟒 LO.Kripke.TransitiveFrameClass #α

Equations

⋯ = ⋯

source

instance LO.Modal.Kripke.KT4B_complete {α : Type u} [Inhabited α] [DecidableEq α] :

LO.Complete 𝐊𝐓𝟒𝐁 LO.Kripke.EquivalenceFrameClass #α

Equations

⋯ = ⋯

source

instance LO.Modal.Kripke.S5_complete {α : Type u} [Inhabited α] [DecidableEq α] :

LO.Complete 𝐒𝟓 LO.Kripke.ReflexiveEuclideanFrameClass #α

Equations

⋯ = ⋯

source

theorem LO.Modal.KD_weakerThan_KT {α : Type u_1} [Inhabited α] [DecidableEq α] :

𝐊𝐃 ≤ₛ 𝐊𝐓

source

theorem LO.Modal.KD_strictlyWeakerThan_KT {α : Type u_1} [Inhabited α] [DecidableEq α] :

𝐊𝐃 <ₛ 𝐊𝐓

source

theorem LO.Modal.K_strictlyWeakerThan_KT {α : Type u_1} [Inhabited α] [DecidableEq α] :

𝐊 <ₛ 𝐊𝐓

source

theorem LO.Modal.K4_strictlyWeakerThan_S4 {α : Type u_1} [Inhabited α] [DecidableEq α] :

𝐊𝟒 <ₛ 𝐒𝟒

source

theorem LO.Modal.S4_weakerThan_S5 {α : Type u_1} [Inhabited α] [DecidableEq α] :

𝐒𝟒 ≤ₛ 𝐒𝟓

source

theorem LO.Modal.S4_strictlyWeakerThan_S5 {α : Type u_1} [Inhabited α] [DecidableEq α] :

𝐒𝟒 <ₛ 𝐒𝟓

source

theorem LO.Modal.equiv_S5_KT4B {α : Type u_1} [Inhabited α] [DecidableEq α] :

𝐒𝟓 =ₛ 𝐊𝐓𝟒𝐁