Geach

@[reducible, inline]

abbrev LO.Modal.Kripke.MultiGeacheanConfluentFrameClass (G : Set Geachean.Taple) : FrameClass

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Kripke.MultiGeacheanConfluentFrameClass G = {F : LO.Modal.Kripke.Frame | MultiGeachean G F.Rel}

instance LO.Modal.Kripke.instIsNonemptyMultiGeacheanConfluentFrameClass {G : Set Geachean.Taple} : (MultiGeacheanConfluentFrameClass G).IsNonempty

instance LO.Modal.Kripke.MultiGeacheanFrameClass.isDefinedByGeachAxioms (G : Set Geachean.Taple) : (MultiGeacheanConfluentFrameClass G).DefinedBy ((fun (t : Geachean.Taple) => Axioms.Geach t (Formula.atom 0)) '' G)

instance LO.Modal.Kripke.MultiGeacheanFrameClass.isDefinedByGeachHilbertAxioms (ts : Set Geachean.Taple) : (MultiGeacheanConfluentFrameClass ts).DefinedBy (Hilbert.Geach ts).axioms

theorem LO.Modal.Kripke.reflexive_of_validate_AxiomT {F : Frame} (h : F ⊧ Axioms.T (Formula.atom 0)) : Std.Refl F.Rel

theorem LO.Modal.Kripke.transitive_of_validate_AxiomFour {F : Frame} (h : F ⊧ Axioms.Four (Formula.atom 0)) : IsTrans F.World F.Rel

theorem LO.Modal.Kripke.canonicalFrame.multigeachean_of_provable_geach {S : Type u_1} [Entailment (Formula ℕ) S] {𝓢 : S} [Entailment.Consistent 𝓢] [Entailment.K 𝓢] {G : Set Geachean.Taple} (hG : ∀ g ∈ G, ∀ (φ : Formula ℕ), 𝓢 ⊢! ◇^[g.i](□^[g.m]φ) ==> □^[g.j](◇^[g.n]φ)) : MultiGeachean G (canonicalFrame 𝓢).Rel

instance LO.Modal.Hilbert.Geach.Kripke.sound {G : Set Geachean.Taple} : Sound (Hilbert.Geach G) (Kripke.MultiGeacheanConfluentFrameClass G)

instance LO.Modal.Hilbert.Geach.Kripke.Consistent {G : Set Geachean.Taple} : Entailment.Consistent (Hilbert.Geach G)

instance LO.Modal.Hilbert.Geach.Kripke.Canonical {G : Set Geachean.Taple} : Modal.Kripke.Canonical (Hilbert.Geach G) (Kripke.MultiGeacheanConfluentFrameClass G)

instance LO.Modal.Hilbert.Geach.Kripke.Complete {G : Set Geachean.Taple} : LO.Complete (Hilbert.Geach G) (Kripke.MultiGeacheanConfluentFrameClass G)