Documentation

Foundation.Modal.Kripke.GL.Completeness

@[reducible, inline]
Equations
  • One or more equations did not get rendered due to their size.
@[reducible, inline]
Equations
  • One or more equations did not get rendered due to their size.
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
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 {ψ, -ψ})
theorem LO.Modal.Hilbert.GL.Kripke.truthlemma {φ ψ : Formula } {X : (miniCanonicalModel φ).World} (q_sub : ψ φ.subformulae) :