Documentation

LeanPool.Incompleteness.Foundation.Modal.Kripke.Hilbert.GL.Completeness

Completeness #

source
@[reducible, inline]
abbrev LO.Modal.Hilbert.GL.Kripke.miniCanonicalFrame (φ : Formula ℕ) :
Kripke.FiniteFrame

Imported declaration from the Incompleteness formalization.

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 ℕ} :
    Std.Irrefl (miniCanonicalFrame φ).Rel
    source
    theorem LO.Modal.Hilbert.GL.Kripke.miniCanonicalFrame.is_transitive {φ : Formula ℕ} :
    IsTrans (miniCanonicalFrame φ).World (miniCanonicalFrame φ).Rel
    source
    @[reducible, inline]
    abbrev LO.Modal.Hilbert.GL.Kripke.miniCanonicalModel (φ : Formula ℕ) :
    Kripke.Model

    Imported declaration from the Incompleteness formalization.

    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 : ComplementClosedConsistentFinset Hilbert.GL φ.subformulas} (hq : □ψ ∈ φ.subformulas) :
      Finset.prebox ↑X ∪ (Finset.prebox ↑X).modalBox ∪ {□ψ, -ψ} ⊆ φ.subformulas⁻
      source
      theorem LO.Modal.Hilbert.GL.Kripke.truthlemma_lemma2 {φ ψ : Formula ℕ} {X : ComplementClosedConsistentFinset Hilbert.GL φ.subformulas} (hq₁ : □ψ ∈ φ.subformulas) (hq₂ : □ψ ∉ X) :
      FormulaFinset.Consistent Hilbert.GL (Finset.prebox ↑X ∪ (Finset.prebox ↑X).modalBox ∪ {□ψ, -ψ})
      source
      theorem LO.Modal.Hilbert.GL.Kripke.truthlemma {φ ψ : Formula ℕ} {X : (miniCanonicalModel φ).World} (q_sub : ψ ∈ φ.subformulas) :
      Formula.Kripke.Satisfies (miniCanonicalModel φ) X ψ ↔ ψ ∈ X
      source
      instance LO.Modal.Hilbert.GL.Kripke.finiteComplete :
      Complete Hilbert.GL Kripke.TransitiveIrreflexiveFiniteFrameClass