Documentation

Foundation.Modal.Kripke.GL.Completeness

source
@[reducible, inline]
abbrev LO.Modal.Hilbert.GL.Kripke.miniCanonicalFrame (φ : Formula ℕ) :
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 {φ : Formula ℕ} :
    Irreflexive (miniCanonicalFrame φ).Rel
    source
    theorem LO.Modal.Hilbert.GL.Kripke.miniCanonicalFrame.is_transitive {φ : Formula ℕ} :
    Transitive (miniCanonicalFrame φ).Rel
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.GL.Kripke.miniCanonicalModel (φ : Formula ℕ) :
    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 {φ ψ : Formula ℕ} {X : CCF (Hilbert.GL ℕ) φ.subformulae} (hq : □ψ ∈ φ.subformulae) :
      Finset.prebox X.formulae ∪ (Finset.prebox X.formulae).box ∪ {□ψ, -ψ} ⊆ φ.subformulae⁻
      source
      theorem LO.Modal.Hilbert.GL.Kripke.truthlemma.lemma2 {φ ψ : Formula ℕ} {X : CCF (Hilbert.GL ℕ) φ.subformulae} (hq₁ : □ψ ∈ φ.subformulae) (hq₂ : □ψ ∉ X.formulae) :
      Formulae.Consistent (Hilbert.GL ℕ) (Finset.prebox X.formulae ∪ (Finset.prebox X.formulae).box ∪ {□ψ, -ψ})
      source
      theorem LO.Modal.Hilbert.GL.Kripke.truthlemma {φ ψ : Formula ℕ} {X : (miniCanonicalModel φ).World} (q_sub : ψ ∈ φ.subformulae) :
      Formula.Kripke.Satisfies (miniCanonicalModel φ) X ψ ↔ ψ ∈ X.formulae
      source
      instance LO.Modal.Hilbert.GL.Kripke.complete :
      Complete (Hilbert.GL ℕ) Kripke.TransitiveIrreflexiveFiniteFrameClass
      source
      instance LO.Modal.Hilbert.GL.Kripke.ffp :
      Kripke.FiniteFrameProperty (Hilbert.GL ℕ) Kripke.TransitiveIrreflexiveFiniteFrameClass