@[reducible, inline]
Equations
- One or more equations did not get rendered due to their size.
theorem
LO.Modal.Hilbert.GL.Kripke.miniCanonicalFrame.is_irreflexive
{φ : Formula ℕ}
:
Irreflexive (miniCanonicalFrame φ).Rel
theorem
LO.Modal.Hilbert.GL.Kripke.miniCanonicalFrame.is_transitive
{φ : Formula ℕ}
:
Transitive (miniCanonicalFrame φ).Rel
@[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)
:
Formula.Kripke.Satisfies (miniCanonicalModel φ) X ψ ↔ ψ ∈ X.formulae