Documentation

Foundation.Modal.Kripke.GL.Completeness

source
@[reducible, inline]
abbrev LO.Modal.Hilbert.GL.Kripke.miniCanonicalFrame (φ : LO.Modal.Formula ℕ) :
LO.Modal.Kripke.FiniteFrame
Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem LO.Modal.Hilbert.GL.Kripke.miniCanonicalFrame.is_irreflexive {φ : LO.Modal.Formula ℕ} :
    Irreflexive (LO.Modal.Hilbert.GL.Kripke.miniCanonicalFrame φ).Rel
    source
    theorem LO.Modal.Hilbert.GL.Kripke.miniCanonicalFrame.is_transitive {φ : LO.Modal.Formula ℕ} :
    Transitive (LO.Modal.Hilbert.GL.Kripke.miniCanonicalFrame φ).Rel
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.GL.Kripke.miniCanonicalModel (φ : LO.Modal.Formula ℕ) :
    LO.Modal.Kripke.Model
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem LO.Modal.Hilbert.GL.Kripke.truthlemma.lemma1 {φ ψ : LO.Modal.Formula ℕ} {X : LO.Modal.CCF (LO.Modal.Hilbert.GL ℕ) φ.subformulae} (hq : □ψ ∈ φ.subformulae) :
      Finset.prebox X.formulae ∪ (Finset.prebox X.formulae).box ∪ {□ψ, -ψ} ⊆ φ.subformulae⁻
      source
      theorem LO.Modal.Hilbert.GL.Kripke.truthlemma.lemma2 {φ ψ : LO.Modal.Formula ℕ} {X : LO.Modal.CCF (LO.Modal.Hilbert.GL ℕ) φ.subformulae} (hq₁ : □ψ ∈ φ.subformulae) (hq₂ : □ψ ∉ X.formulae) :
      LO.Modal.Formulae.Consistent (LO.Modal.Hilbert.GL ℕ) (Finset.prebox X.formulae ∪ (Finset.prebox X.formulae).box ∪ {□ψ, -ψ})
      source
      theorem LO.Modal.Hilbert.GL.Kripke.truthlemma {φ ψ : LO.Modal.Formula ℕ} {X : (LO.Modal.Hilbert.GL.Kripke.miniCanonicalModel φ).World} (q_sub : ψ ∈ φ.subformulae) :
      LO.Modal.Formula.Kripke.Satisfies (LO.Modal.Hilbert.GL.Kripke.miniCanonicalModel φ) X ψ ↔ ψ ∈ X.formulae
      source
      instance LO.Modal.Hilbert.GL.Kripke.complete :
      LO.Complete (LO.Modal.Hilbert.GL ℕ) LO.Modal.Kripke.TransitiveIrreflexiveFiniteFrameClass
      Equations
      source
      instance LO.Modal.Hilbert.GL.Kripke.ffp :
      LO.Modal.Hilbert.Kripke.FiniteFrameProperty (LO.Modal.Hilbert.GL ℕ) LO.Modal.Kripke.TransitiveIrreflexiveFiniteFrameClass
      Equations