inductive LO.Modal.Formula (α : Type u) : Type u

• atom: {α : Type u} → α → LO.Modal.Formula α
• falsum: {α : Type u} → LO.Modal.Formula α
• imp: {α : Type u} → LO.Modal.Formula α → LO.Modal.Formula α → LO.Modal.Formula α
• box: {α : Type u} → LO.Modal.Formula α → LO.Modal.Formula α

instance LO.Modal.instDecidableEqFormula {α✝ : Type u_1} [DecidableEq α✝] : DecidableEq (LO.Modal.Formula α✝)

Equations

• LO.Modal.instDecidableEqFormula = LO.Modal.decEqFormula✝

@[reducible, inline]

abbrev LO.Modal.Formula.neg {α : Type u_1} (φ : LO.Modal.Formula α) : LO.Modal.Formula α

Equations

• φ.neg = φ.imp LO.Modal.Formula.falsum

@[reducible, inline]

abbrev LO.Modal.Formula.verum {α : Type u_1} : LO.Modal.Formula α

Equations

• LO.Modal.Formula.verum = LO.Modal.Formula.falsum.imp LO.Modal.Formula.falsum

@[reducible, inline]

abbrev LO.Modal.Formula.top {α : Type u_1} : LO.Modal.Formula α

Equations

• LO.Modal.Formula.top = LO.Modal.Formula.falsum.imp LO.Modal.Formula.falsum

@[reducible, inline]

abbrev LO.Modal.Formula.or {α : Type u_1} (φ ψ : LO.Modal.Formula α) : LO.Modal.Formula α

Equations

• φ.or ψ = φ.neg.imp ψ

@[reducible, inline]

abbrev LO.Modal.Formula.and {α : Type u_1} (φ ψ : LO.Modal.Formula α) : LO.Modal.Formula α

Equations

• φ.and ψ = (φ.imp ψ.neg).neg

@[reducible, inline]

abbrev LO.Modal.Formula.dia {α : Type u_1} (φ : LO.Modal.Formula α) : LO.Modal.Formula α

Equations

• φ.dia = φ.neg.box.neg

instance LO.Modal.Formula.instBasicModalLogicalConnective {α : Type u} : LO.BasicModalLogicalConnective (LO.Modal.Formula α)

Equations

• LO.Modal.Formula.instBasicModalLogicalConnective = LO.BasicModalLogicalConnective.mk

instance LO.Modal.Formula.instLukasiewiczAbbrev {α : Type u} : LO.LukasiewiczAbbrev (LO.Modal.Formula α)

Equations

• ⋯ = ⋯

instance LO.Modal.Formula.instDiaAbbrev {α : Type u} : LO.DiaAbbrev (LO.Modal.Formula α)

Equations

• ⋯ = ⋯

def LO.Modal.Formula.toStr {α : Type u} [ToString α] : LO.Modal.Formula α → String

Equations

• LO.Modal.Formula.falsum.toStr = "\\bot"
• (LO.Modal.Formula.atom a).toStr = "{" ++ toString a ++ "}"
• φ.box.toStr = "\\Box " ++ φ.toStr
• (φ.imp ψ).toStr = "\\left(" ++ φ.toStr ++ " \\to " ++ ψ.toStr ++ "\\right)"

instance LO.Modal.Formula.instRepr {α : Type u} [ToString α] : Repr (LO.Modal.Formula α)

Equations

• LO.Modal.Formula.instRepr = { reprPrec := fun (t : LO.Modal.Formula α) (x : ℕ) => Std.Format.text t.toStr }

instance LO.Modal.Formula.instToString {α : Type u} [ToString α] : ToString (LO.Modal.Formula α)

Equations

• LO.Modal.Formula.instToString = { toString := LO.Modal.Formula.toStr }

instance LO.Modal.Formula.instCoe {α : Type u} : Coe α (LO.Modal.Formula α)

Equations

• LO.Modal.Formula.instCoe = { coe := LO.Modal.Formula.atom }

@[simp]

theorem LO.Modal.Formula.neg_bot {α : Type u} : ∼⊥ = ⊤

theorem LO.Modal.Formula.or_eq {α : Type u} (φ ψ : LO.Modal.Formula α) : φ.or ψ = φ ⋎ ψ

theorem LO.Modal.Formula.and_eq {α : Type u} (φ ψ : LO.Modal.Formula α) : φ.and ψ = φ ⋏ ψ

theorem LO.Modal.Formula.imp_eq {α : Type u} (φ ψ : LO.Modal.Formula α) : φ.imp ψ = φ ➝ ψ

theorem LO.Modal.Formula.neg_eq {α : Type u} (φ : LO.Modal.Formula α) : φ.neg = ∼φ

theorem LO.Modal.Formula.box_eq {α : Type u} (φ : LO.Modal.Formula α) : φ.box = □φ

theorem LO.Modal.Formula.dia_eq {α : Type u} (φ : LO.Modal.Formula α) : φ.dia = ◇φ

theorem LO.Modal.Formula.iff_eq {α : Type u} (φ ψ : LO.Modal.Formula α) : φ ⭤ ψ = (φ ➝ ψ) ⋏ (ψ ➝ φ)

theorem LO.Modal.Formula.falsum_eq {α : Type u} : LO.Modal.Formula.falsum = ⊥

@[simp]

theorem LO.Modal.Formula.and_inj {α : Type u} (φ₁ ψ₁ φ₂ ψ₂ : LO.Modal.Formula α) : φ₁ ⋏ φ₂ = ψ₁ ⋏ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂

@[simp]

theorem LO.Modal.Formula.or_inj {α : Type u} (φ₁ ψ₁ φ₂ ψ₂ : LO.Modal.Formula α) : φ₁ ⋎ φ₂ = ψ₁ ⋎ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂

@[simp]

theorem LO.Modal.Formula.imp_inj {α : Type u} (φ₁ ψ₁ φ₂ ψ₂ : LO.Modal.Formula α) : φ₁ ➝ φ₂ = ψ₁ ➝ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂

@[simp]

theorem LO.Modal.Formula.neg_inj {α : Type u} (φ ψ : LO.Modal.Formula α) : ∼φ = ∼ψ ↔ φ = ψ

def LO.Modal.Formula.complexity {α : Type u} : LO.Modal.Formula α → ℕ

Formula complexity

Equations

• (LO.Modal.Formula.atom a).complexity = 0
• LO.Modal.Formula.falsum.complexity = 0
• (φ.imp ψ).complexity = φ.complexity ⊔ ψ.complexity + 1
• φ.box.complexity = φ.complexity + 1

def LO.Modal.Formula.degree {α : Type u} : LO.Modal.Formula α → ℕ

Max numbers of □

Equations

• (LO.Modal.Formula.atom a).degree = 0
• LO.Modal.Formula.falsum.degree = 0
• (φ.imp ψ).degree = φ.degree ⊔ ψ.degree
• φ.box.degree = φ.degree + 1

@[simp]

theorem LO.Modal.Formula.degree_neg {α : Type u} (φ : LO.Modal.Formula α) : (∼φ).degree = φ.degree

@[simp]

theorem LO.Modal.Formula.degree_imp {α : Type u} (φ ψ : LO.Modal.Formula α) : (φ ➝ ψ).degree = φ.degree ⊔ ψ.degree

def LO.Modal.Formula.cases' {α : Type u} {C : LO.Modal.Formula α → Sort w} (hfalsum : C ⊥) (hatom : (a : α) → C (LO.Modal.Formula.atom a)) (himp : (φ ψ : LO.Modal.Formula α) → C (φ ➝ ψ)) (hbox : (φ : LO.Modal.Formula α) → C (□φ)) (φ : LO.Modal.Formula α) : C φ

Equations

• LO.Modal.Formula.cases' hfalsum hatom himp hbox LO.Modal.Formula.falsum = hfalsum
• LO.Modal.Formula.cases' hfalsum hatom himp hbox (LO.Modal.Formula.atom a) = hatom a
• LO.Modal.Formula.cases' hfalsum hatom himp hbox φ.box = hbox φ
• LO.Modal.Formula.cases' hfalsum hatom himp hbox (φ.imp ψ) = himp φ ψ

def LO.Modal.Formula.rec' {α : Type u} {C : LO.Modal.Formula α → Sort w} (hfalsum : C ⊥) (hatom : (a : α) → C (LO.Modal.Formula.atom a)) (himp : (φ ψ : LO.Modal.Formula α) → C φ → C ψ → C (φ ➝ ψ)) (hbox : (φ : LO.Modal.Formula α) → C φ → C (□φ)) (φ : LO.Modal.Formula α) : C φ

Equations

• LO.Modal.Formula.rec' hfalsum hatom himp hbox LO.Modal.Formula.falsum = hfalsum
• LO.Modal.Formula.rec' hfalsum hatom himp hbox (LO.Modal.Formula.atom a) = hatom a
• LO.Modal.Formula.rec' hfalsum hatom himp hbox (φ.imp ψ) = himp φ ψ (LO.Modal.Formula.rec' hfalsum hatom himp hbox φ) (LO.Modal.Formula.rec' hfalsum hatom himp hbox ψ)
• LO.Modal.Formula.rec' hfalsum hatom himp hbox φ.box = hbox φ (LO.Modal.Formula.rec' hfalsum hatom himp hbox φ)

def LO.Modal.Formula.hasDecEq {α : Type u} [DecidableEq α] (φ ψ : LO.Modal.Formula α) : Decidable (φ = ψ)

Equations

• One or more equations did not get rendered due to their size.

instance LO.Modal.Formula.instDecidableEq {α : Type u} [DecidableEq α] : DecidableEq (LO.Modal.Formula α)

Equations

• LO.Modal.Formula.instDecidableEq = LO.Modal.Formula.hasDecEq

def LO.Modal.Formula.isBox {α : Type u} : LO.Modal.Formula α → Bool

Equations

• a.box.isBox = true
• x.isBox = false

@[reducible, inline]

abbrev LO.Modal.Formulae (α : Type u_1) : Type u_1

Equations

• LO.Modal.Formulae α = Finset (LO.Modal.Formula α)

@[reducible, inline]

abbrev LO.Modal.Theory (α : Type u_1) : Type u_1

Equations

• LO.Modal.Theory α = Set (LO.Modal.Formula α)

instance LO.Modal.instCollectionFormulaTheory {α : Type u_1} : Collection (LO.Modal.Formula α) (LO.Modal.Theory α)

Equations

• LO.Modal.instCollectionFormulaTheory = inferInstance

def LO.Modal.Formula.subformulae {α : Type u_1} [DecidableEq α] : LO.Modal.Formula α → LO.Modal.Formulae α

Equations

• (LO.Modal.Formula.atom a).subformulae = {LO.Modal.Formula.atom a}
• LO.Modal.Formula.falsum.subformulae = {⊥}
• (φ.imp ψ).subformulae = insert (φ ➝ ψ) (φ.subformulae ∪ ψ.subformulae)
• φ.box.subformulae = insert (□φ) φ.subformulae

@[simp]

theorem LO.Modal.Formula.subformulae.mem_self {α : Type u_1} [DecidableEq α] {φ : LO.Modal.Formula α} : φ ∈ φ.subformulae

theorem LO.Modal.Formula.subformulae.mem_imp {α : Type u_1} [DecidableEq α] {φ ψ χ : LO.Modal.Formula α} (h : ψ ➝ χ ∈ φ.subformulae) : ψ ∈ φ.subformulae ∧ χ ∈ φ.subformulae

theorem LO.Modal.Formula.subformulae.mem_imp₁ {α : Type u_1} [DecidableEq α] {φ ψ χ : LO.Modal.Formula α} (h : ψ ➝ χ ∈ φ.subformulae) : ψ ∈ φ.subformulae

theorem LO.Modal.Formula.subformulae.mem_imp₂ {α : Type u_1} [DecidableEq α] {φ ψ χ : LO.Modal.Formula α} (h : ψ ➝ χ ∈ φ.subformulae) : χ ∈ φ.subformulae

theorem LO.Modal.Formula.subformulae.mem_box {α : Type u_1} [DecidableEq α] {φ ψ : LO.Modal.Formula α} (h : □ψ ∈ φ.subformulae := by assumption) : ψ ∈ φ.subformulae

@[simp]

theorem LO.Modal.Formula.subformulae.complexity_lower {α : Type u_1} [DecidableEq α] {φ ψ : LO.Modal.Formula α} (h : ψ ∈ φ.subformulae) : ψ.complexity ≤ φ.complexity

class LO.Modal.Formulae.SubformulaClosed {α : Type u_1} (X : LO.Modal.Formulae α) : Prop

• imp_closed : ∀ {φ ψ : LO.Modal.Formula α}, φ ➝ ψ ∈ X → φ ∈ X ∧ ψ ∈ X
• box_closed : ∀ {φ : LO.Modal.Formula α}, □φ ∈ X → φ ∈ X

instance LO.Modal.SubformulaClosed.instSubformulaClosedSubformulae {α : Type u_1} [DecidableEq α] {φ : LO.Modal.Formula α} : φ.subformulae.SubformulaClosed

Equations

• ⋯ = ⋯

theorem LO.Modal.SubformulaClosed.mem_box {α : Type u_1} {φ : LO.Modal.Formula α} {X : LO.Modal.Formulae α} [closed : X.SubformulaClosed] (h : □φ ∈ X) : φ ∈ X

theorem LO.Modal.SubformulaClosed.mem_imp {α : Type u_1} {φ : LO.Modal.Formula α} {X : LO.Modal.Formulae α} [closed : X.SubformulaClosed] {ψ : LO.Modal.Formula α} (h : φ ➝ ψ ∈ X) : φ ∈ X ∧ ψ ∈ X

theorem LO.Modal.SubformulaClosed.mem_imp₁ {α : Type u_1} {φ : LO.Modal.Formula α} {X : LO.Modal.Formulae α} [closed : X.SubformulaClosed] {ψ : LO.Modal.Formula α} (h : φ ➝ ψ ∈ X) : φ ∈ X

theorem LO.Modal.SubformulaClosed.mem_imp₂ {α : Type u_1} {φ : LO.Modal.Formula α} {X : LO.Modal.Formulae α} [closed : X.SubformulaClosed] {ψ : LO.Modal.Formula α} (h : φ ➝ ψ ∈ X) : ψ ∈ X

class LO.Modal.Theory.SubformulaClosed {α : Type u_1} (T : LO.Modal.Theory α) : Prop

• imp_closed : ∀ {φ ψ : LO.Modal.Formula α}, φ ➝ ψ ∈ T → φ ∈ T ∧ ψ ∈ T
• box_closed : ∀ {φ : LO.Modal.Formula α}, □φ ∈ T → φ ∈ T

instance LO.Modal.Theory.SubformulaClosed.instToSetFormulaSubformulae {α : Type u_1} {φ : LO.Modal.Formula α} [DecidableEq α] : LO.Modal.Theory.SubformulaClosed ↑φ.subformulae

Equations

• ⋯ = ⋯

theorem LO.Modal.Theory.SubformulaClosed.mem_box {α : Type u_1} {φ : LO.Modal.Formula α} {T : LO.Modal.Theory α} [T_closed : T.SubformulaClosed] (h : □φ ∈ T) : φ ∈ T

theorem LO.Modal.Theory.SubformulaClosed.mem_imp {α : Type u_1} {φ : LO.Modal.Formula α} {T : LO.Modal.Theory α} [T_closed : T.SubformulaClosed] {ψ : LO.Modal.Formula α} (h : φ ➝ ψ ∈ T) : φ ∈ T ∧ ψ ∈ T

theorem LO.Modal.Theory.SubformulaClosed.mem_imp₁ {α : Type u_1} {φ : LO.Modal.Formula α} {T : LO.Modal.Theory α} [T_closed : T.SubformulaClosed] {ψ : LO.Modal.Formula α} (h : φ ➝ ψ ∈ T) : φ ∈ T

theorem LO.Modal.Theory.SubformulaClosed.mem_imp₂ {α : Type u_1} {φ : LO.Modal.Formula α} {T : LO.Modal.Theory α} [T_closed : T.SubformulaClosed] {ψ : LO.Modal.Formula α} (h : φ ➝ ψ ∈ T) : ψ ∈ T

def LO.Modal.Formula.cases_neg {α : Type u_1} [DecidableEq α] {C : LO.Modal.Formula α → Sort w} (hfalsum : C ⊥) (hatom : (a : α) → C (LO.Modal.Formula.atom a)) (hneg : (φ : LO.Modal.Formula α) → C (∼φ)) (himp : (φ ψ : LO.Modal.Formula α) → ψ ≠ ⊥ → C (φ ➝ ψ)) (hbox : (φ : LO.Modal.Formula α) → C (□φ)) (φ : LO.Modal.Formula α) : C φ

Equations

• LO.Modal.Formula.cases_neg hfalsum hatom hneg himp hbox LO.Modal.Formula.falsum = hfalsum
• LO.Modal.Formula.cases_neg hfalsum hatom hneg himp hbox (LO.Modal.Formula.atom a) = hatom a
• LO.Modal.Formula.cases_neg hfalsum hatom hneg himp hbox φ.box = hbox φ
• LO.Modal.Formula.cases_neg hfalsum hatom hneg himp hbox (φ.imp LO.Modal.Formula.falsum) = hneg φ
• LO.Modal.Formula.cases_neg hfalsum hatom hneg himp hbox (φ.imp ψ) = if e : ψ = ⊥ then ⋯ ▸ hneg φ else himp φ ψ e

def LO.Modal.Formula.rec_neg {α : Type u_1} [DecidableEq α] {C : LO.Modal.Formula α → Sort w} (hfalsum : C ⊥) (hatom : (a : α) → C (LO.Modal.Formula.atom a)) (hneg : (φ : LO.Modal.Formula α) → C φ → C (∼φ)) (himp : (φ ψ : LO.Modal.Formula α) → ψ ≠ ⊥ → C φ → C ψ → C (φ ➝ ψ)) (hbox : (φ : LO.Modal.Formula α) → C φ → C (□φ)) (φ : LO.Modal.Formula α) : C φ

Equations

• One or more equations did not get rendered due to their size.
• LO.Modal.Formula.rec_neg hfalsum hatom hneg himp hbox LO.Modal.Formula.falsum = hfalsum
• LO.Modal.Formula.rec_neg hfalsum hatom hneg himp hbox (LO.Modal.Formula.atom a) = hatom a
• LO.Modal.Formula.rec_neg hfalsum hatom hneg himp hbox φ.box = hbox φ (LO.Modal.Formula.rec_neg hfalsum hatom hneg himp hbox φ)
• LO.Modal.Formula.rec_neg hfalsum hatom hneg himp hbox (φ.imp LO.Modal.Formula.falsum) = hneg φ (LO.Modal.Formula.rec_neg hfalsum hatom hneg himp hbox φ)

def LO.Modal.Formula.negated {α : Type u_1} : LO.Modal.Formula α → Bool

Equations

• (a.imp LO.Modal.Formula.falsum).negated = decide True
• x.negated = decide False

@[simp]

theorem LO.Modal.Formula.negated_def {α : Type u_1} {φ : LO.Modal.Formula α} : (∼φ).negated = true

@[simp]

theorem LO.Modal.Formula.negated_imp {α : Type u_1} {φ ψ : LO.Modal.Formula α} : (φ ➝ ψ).negated = true ↔ ψ = ⊥

theorem LO.Modal.Formula.negated_iff {α : Type u_1} {φ : LO.Modal.Formula α} [DecidableEq α] : φ.negated = true ↔ ∃ (ψ : LO.Modal.Formula α), φ = ∼ψ

theorem LO.Modal.Formula.not_negated_iff {α : Type u_1} {φ : LO.Modal.Formula α} [DecidableEq α] : ¬φ.negated = true ↔ ∀ (ψ : LO.Modal.Formula α), φ ≠ ∼ψ

def LO.Modal.Formula.rec_negated {α : Type u_1} [DecidableEq α] {C : LO.Modal.Formula α → Sort w} (hfalsum : C ⊥) (hatom : (a : α) → C (LO.Modal.Formula.atom a)) (hneg : (φ : LO.Modal.Formula α) → C φ → C (∼φ)) (himp : (φ ψ : LO.Modal.Formula α) → ¬(φ ➝ ψ).negated = true → C φ → C ψ → C (φ ➝ ψ)) (hbox : (φ : LO.Modal.Formula α) → C φ → C (□φ)) (φ : LO.Modal.Formula α) : C φ

Equations

• One or more equations did not get rendered due to their size.
• LO.Modal.Formula.rec_negated hfalsum hatom hneg himp hbox LO.Modal.Formula.falsum = hfalsum
• LO.Modal.Formula.rec_negated hfalsum hatom hneg himp hbox (LO.Modal.Formula.atom a) = hatom a
• LO.Modal.Formula.rec_negated hfalsum hatom hneg himp hbox φ.box = hbox φ (LO.Modal.Formula.rec_negated hfalsum hatom hneg himp hbox φ)
• LO.Modal.Formula.rec_negated hfalsum hatom hneg himp hbox (φ.imp LO.Modal.Formula.falsum) = hneg φ (LO.Modal.Formula.rec_negated hfalsum hatom hneg himp hbox φ)

def LO.Modal.Formula.toNat {α : Type u_1} [Encodable α] : LO.Modal.Formula α → ℕ

Equations

• (LO.Modal.Formula.atom a).toNat = Nat.pair 0 (Encodable.encode a) + 1
• LO.Modal.Formula.falsum.toNat = Nat.pair 1 0 + 1
• φ.box.toNat = Nat.pair 2 φ.toNat + 1
• (φ.imp ψ).toNat = Nat.pair 3 (Nat.pair φ.toNat ψ.toNat) + 1

@[irreducible]

def LO.Modal.Formula.ofNat {α : Type u_1} [Encodable α] : ℕ → Option (LO.Modal.Formula α)

Equations

• One or more equations did not get rendered due to their size.
• LO.Modal.Formula.ofNat 0 = none

theorem LO.Modal.Formula.ofNat_toNat {α : Type u_1} [Encodable α] (φ : LO.Modal.Formula α) : LO.Modal.Formula.ofNat φ.toNat = some φ

instance LO.Modal.Formula.instEncodable {α : Type u_1} [Encodable α] : Encodable (LO.Modal.Formula α)

Equations

• LO.Modal.Formula.instEncodable = { encode := LO.Modal.Formula.toNat, decode := LO.Modal.Formula.ofNat, encodek := ⋯ }

def LO.Modal.Formula.subst {α : Type u_1} (σ : α → LO.Modal.Formula α) : LO.Modal.Formula α → LO.Modal.Formula α

Equations

• LO.Modal.Formula.subst σ (LO.Modal.Formula.atom a) = σ a
• LO.Modal.Formula.subst σ LO.Modal.Formula.falsum = ⊥
• LO.Modal.Formula.subst σ φ.box = □LO.Modal.Formula.subst σ φ
• LO.Modal.Formula.subst σ (φ.imp ψ) = LO.Modal.Formula.subst σ φ ➝ LO.Modal.Formula.subst σ ψ

@[simp]

theorem LO.Modal.Formula.subst_atom {α : Type u_1} {σ : α → LO.Modal.Formula α} {a : α} : LO.Modal.Formula.subst σ (LO.Modal.Formula.atom a) = σ a

@[simp]

theorem LO.Modal.Formula.subst_bot {α : Type u_1} {σ : α → LO.Modal.Formula α} : LO.Modal.Formula.subst σ ⊥ = ⊥

@[simp]

theorem LO.Modal.Formula.subst_imp {α : Type u_1} {φ ψ : LO.Modal.Formula α} {σ : α → LO.Modal.Formula α} : LO.Modal.Formula.subst σ (φ ➝ ψ) = LO.Modal.Formula.subst σ φ ➝ LO.Modal.Formula.subst σ ψ

@[simp]

theorem LO.Modal.Formula.subst_neg {α : Type u_1} {φ : LO.Modal.Formula α} {σ : α → LO.Modal.Formula α} : LO.Modal.Formula.subst σ (∼φ) = ∼LO.Modal.Formula.subst σ φ

@[simp]

theorem LO.Modal.Formula.subst_and {α : Type u_1} {φ ψ : LO.Modal.Formula α} {σ : α → LO.Modal.Formula α} : LO.Modal.Formula.subst σ (φ ⋏ ψ) = LO.Modal.Formula.subst σ φ ⋏ LO.Modal.Formula.subst σ ψ

@[simp]

theorem LO.Modal.Formula.subst_or {α : Type u_1} {φ ψ : LO.Modal.Formula α} {σ : α → LO.Modal.Formula α} : LO.Modal.Formula.subst σ (φ ⋎ ψ) = LO.Modal.Formula.subst σ φ ⋎ LO.Modal.Formula.subst σ ψ

@[simp]

theorem LO.Modal.Formula.subst_iff {α : Type u_1} {φ ψ : LO.Modal.Formula α} {σ : α → LO.Modal.Formula α} : LO.Modal.Formula.subst σ (φ ⭤ ψ) = LO.Modal.Formula.subst σ φ ⭤ LO.Modal.Formula.subst σ ψ

@[simp]

theorem LO.Modal.Formula.subst_box {α : Type u_1} {φ : LO.Modal.Formula α} {σ : α → LO.Modal.Formula α} : LO.Modal.Formula.subst σ (□φ) = □LO.Modal.Formula.subst σ φ

@[simp]

theorem LO.Modal.Formula.subst_dia {α : Type u_1} {φ : LO.Modal.Formula α} {σ : α → LO.Modal.Formula α} : LO.Modal.Formula.subst σ (◇φ) = ◇LO.Modal.Formula.subst σ φ

class LO.Modal.Theory.SubstClosed {α : Type u_1} (T : LO.Modal.Theory α) : Prop

• closed : ∀ {φ : LO.Modal.Formula α}, φ ∈ T → ∀ {σ : α → LO.Modal.Formula α}, LO.Modal.Formula.subst σ φ ∈ T

def LO.Modal.Theory.instSubstClosed {α : Type u_1} {T : LO.Modal.Theory α} (hAtom : ∀ (a : α), LO.Modal.Formula.atom a ∈ T → ∀ {σ : α → LO.Modal.Formula α}, LO.Modal.Formula.subst σ (LO.Modal.Formula.atom a) ∈ T) (hImp : ∀ {φ ψ : LO.Modal.Formula α}, φ ➝ ψ ∈ T → ∀ {σ : α → LO.Modal.Formula α}, LO.Modal.Formula.subst σ (φ ➝ ψ) ∈ T) (hBox : ∀ {φ : LO.Modal.Formula α}, □φ ∈ T → ∀ {σ : α → LO.Modal.Formula α}, LO.Modal.Formula.subst σ (□φ) ∈ T) : T.SubstClosed

Equations

• ⋯ = ⋯

theorem LO.Modal.Theory.SubstClosed.mem_atom {α : Type u_1} {T : LO.Modal.Theory α} [T.SubstClosed] {a : α} {σ : α → LO.Modal.Formula α} (h : LO.Modal.Formula.atom a ∈ T) : LO.Modal.Formula.subst σ (LO.Modal.Formula.atom a) ∈ T

theorem LO.Modal.Theory.SubstClosed.mem_bot {α : Type u_1} {T : LO.Modal.Theory α} [T.SubstClosed] {σ : α → LO.Modal.Formula α} (h : ⊥ ∈ T) : LO.Modal.Formula.subst σ ⊥ ∈ T

theorem LO.Modal.Theory.SubstClosed.mem_imp {α : Type u_1} {T : LO.Modal.Theory α} [T.SubstClosed] {φ ψ : LO.Modal.Formula α} {σ : α → LO.Modal.Formula α} (h : φ ➝ ψ ∈ T) : LO.Modal.Formula.subst σ (φ ➝ ψ) ∈ T

theorem LO.Modal.Theory.SubstClosed.mem_neg {α : Type u_1} {T : LO.Modal.Theory α} [T.SubstClosed] {φ : LO.Modal.Formula α} {σ : α → LO.Modal.Formula α} (h : ∼φ ∈ T) : LO.Modal.Formula.subst σ (∼φ) ∈ T

theorem LO.Modal.Theory.SubstClosed.mem_and {α : Type u_1} {T : LO.Modal.Theory α} [T.SubstClosed] {φ ψ : LO.Modal.Formula α} {σ : α → LO.Modal.Formula α} (h : φ ⋏ ψ ∈ T) : LO.Modal.Formula.subst σ (φ ⋏ ψ) ∈ T

theorem LO.Modal.Theory.SubstClosed.mem_or {α : Type u_1} {T : LO.Modal.Theory α} [T.SubstClosed] {φ ψ : LO.Modal.Formula α} {σ : α → LO.Modal.Formula α} (h : φ ⋎ ψ ∈ T) : LO.Modal.Formula.subst σ (φ ⋎ ψ) ∈ T

theorem LO.Modal.Theory.SubstClosed.mem_box {α : Type u_1} {T : LO.Modal.Theory α} [T.SubstClosed] {φ : LO.Modal.Formula α} {σ : α → LO.Modal.Formula α} (h : □φ ∈ T) : LO.Modal.Formula.subst σ (□φ) ∈ T

instance LO.Modal.Theory.SubstClosed.union {α : Type u_1} {T₁ T₂ : LO.Modal.Theory α} [T₁_closed : T₁.SubstClosed] [T₂_closed : T₂.SubstClosed] : (T₁ ∪ T₂).SubstClosed

Equations

• ⋯ = ⋯