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

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

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

Equations

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

@[reducible, inline]

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

Equations

• p.neg = p.imp LO.Modal.Standard.Formula.falsum

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

abbrev LO.Modal.Standard.Formula.or {α : Type u_1} (p : LO.Modal.Standard.Formula α) (q : LO.Modal.Standard.Formula α) : LO.Modal.Standard.Formula α

Equations

• p.or q = p.neg.imp q

@[reducible, inline]

abbrev LO.Modal.Standard.Formula.and {α : Type u_1} (p : LO.Modal.Standard.Formula α) (q : LO.Modal.Standard.Formula α) : LO.Modal.Standard.Formula α

Equations

• p.and q = (p.imp q.neg).neg

@[reducible, inline]

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

Equations

• p.dia = p.neg.box.neg

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

Equations

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

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

Equations

• LO.Modal.Standard.Formula.instLukasiewiczAbbrev = { top := ⋯, neg := ⋯, or := ⋯, and := ⋯ }

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

Equations

• LO.Modal.Standard.Formula.instDiaAbbrev = { dia_abbrev := ⋯ }

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

@[simp]

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

theorem LO.Modal.Standard.Formula.or_eq {α : Type u} (p : LO.Modal.Standard.Formula α) (q : LO.Modal.Standard.Formula α) : p.or q = p ⋎ q

theorem LO.Modal.Standard.Formula.and_eq {α : Type u} (p : LO.Modal.Standard.Formula α) (q : LO.Modal.Standard.Formula α) : p.and q = p ⋏ q

theorem LO.Modal.Standard.Formula.imp_eq {α : Type u} (p : LO.Modal.Standard.Formula α) (q : LO.Modal.Standard.Formula α) : p.imp q = p ⟶ q

theorem LO.Modal.Standard.Formula.neg_eq {α : Type u} (p : LO.Modal.Standard.Formula α) : p.neg = ~p

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

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

theorem LO.Modal.Standard.Formula.iff_eq {α : Type u} (p : LO.Modal.Standard.Formula α) (q : LO.Modal.Standard.Formula α) : p ⟷ q = (p ⟶ q) ⋏ (q ⟶ p)

@[simp]

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

@[simp]

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

@[simp]

theorem LO.Modal.Standard.Formula.imp_inj {α : Type u} (p₁ : LO.Modal.Standard.Formula α) (q₁ : LO.Modal.Standard.Formula α) (p₂ : LO.Modal.Standard.Formula α) (q₂ : LO.Modal.Standard.Formula α) : p₁ ⟶ p₂ = q₁ ⟶ q₂ ↔ p₁ = q₁ ∧ p₂ = q₂

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

Formula complexity

Equations

• (LO.Modal.Standard.Formula.atom a).complexity = 0
• LO.Modal.Standard.Formula.falsum.complexity = 0
• (p.imp q).complexity = max p.complexity q.complexity + 1
• p.box.complexity = p.complexity + 1

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

Max numbers of □

Equations

• (LO.Modal.Standard.Formula.atom a).degree = 0
• LO.Modal.Standard.Formula.falsum.degree = 0
• (p.imp q).degree = max p.degree q.degree
• p.box.degree = p.degree + 1

@[simp]

theorem LO.Modal.Standard.Formula.degree_neg {α : Type u} (p : LO.Modal.Standard.Formula α) : (~p).degree = p.degree

@[simp]

theorem LO.Modal.Standard.Formula.degree_imp {α : Type u} (p : LO.Modal.Standard.Formula α) (q : LO.Modal.Standard.Formula α) : (p ⟶ q).degree = max p.degree q.degree

def LO.Modal.Standard.Formula.cases' {α : Type u} {C : LO.Modal.Standard.Formula α → Sort w} (hfalsum : C ⊥) (hatom : (a : α) → C (LO.Modal.Standard.Formula.atom a)) (himp : (p q : LO.Modal.Standard.Formula α) → C (p ⟶ q)) (hbox : (p : LO.Modal.Standard.Formula α) → C (□p)) (p : LO.Modal.Standard.Formula α) : C p

Equations

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

def LO.Modal.Standard.Formula.rec' {α : Type u} {C : LO.Modal.Standard.Formula α → Sort w} (hfalsum : C ⊥) (hatom : (a : α) → C (LO.Modal.Standard.Formula.atom a)) (himp : (p q : LO.Modal.Standard.Formula α) → C p → C q → C (p ⟶ q)) (hbox : (p : LO.Modal.Standard.Formula α) → C p → C (□p)) (p : LO.Modal.Standard.Formula α) : C p

Equations

• LO.Modal.Standard.Formula.rec' hfalsum hatom himp hbox LO.Modal.Standard.Formula.falsum = hfalsum
• LO.Modal.Standard.Formula.rec' hfalsum hatom himp hbox (LO.Modal.Standard.Formula.atom a) = hatom a
• LO.Modal.Standard.Formula.rec' hfalsum hatom himp hbox (p.imp q) = himp p q (LO.Modal.Standard.Formula.rec' hfalsum hatom himp hbox p) (LO.Modal.Standard.Formula.rec' hfalsum hatom himp hbox q)
• LO.Modal.Standard.Formula.rec' hfalsum hatom himp hbox p.box = hbox p (LO.Modal.Standard.Formula.rec' hfalsum hatom himp hbox p)

def LO.Modal.Standard.Formula.hasDecEq {α : Type u} [DecidableEq α] (p : LO.Modal.Standard.Formula α) (q : LO.Modal.Standard.Formula α) : Decidable (p = q)

Equations

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

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

Equations

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

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

Equations

• x.isBox = match x with | a.box => true | x => false

@[reducible, inline]

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

Equations

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

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

Equations

• LO.Modal.Standard.instCollectionFormulaTheory = inferInstance

@[reducible, inline]

abbrev LO.Modal.Standard.AxiomSet (α : Type u_1) : Type u_1

Equations

• LO.Modal.Standard.AxiomSet α = Set (LO.Modal.Standard.Formula α)

def LO.Modal.Standard.Formula.Subformulas {α : Type u_1} [DecidableEq α] : LO.Modal.Standard.Formula α → Finset (LO.Modal.Standard.Formula α)

Equations

• 𝒮 LO.Modal.Standard.Formula.atom a = {LO.Modal.Standard.Formula.atom a}
• 𝒮 LO.Modal.Standard.Formula.falsum = {⊥}
• 𝒮 p.imp q = insert (p ⟶ q) (𝒮 p ∪ 𝒮 q)
• 𝒮 p.box = insert (□p) (𝒮 p)

def LO.Modal.Standard.term𝒮_ : Lean.ParserDescr

Equations

• LO.Modal.Standard.term𝒮_ = Lean.ParserDescr.node `LO.Modal.Standard.term𝒮_ 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "𝒮 ") (Lean.ParserDescr.cat `term 70))

@[simp]

theorem LO.Modal.Standard.Formula.Subformulas.mem_self {α : Type u_1} [DecidableEq α] (p : LO.Modal.Standard.Formula α) : p ∈ 𝒮 p

theorem LO.Modal.Standard.Formula.Subformulas.mem_imp {α : Type u_1} [DecidableEq α] {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} {r : LO.Modal.Standard.Formula α} (h : autoParam (q ⟶ r ∈ 𝒮 p) _auto✝) : q ∈ 𝒮 p ∧ r ∈ 𝒮 p

theorem LO.Modal.Standard.Formula.Subformulas.mem_imp₁ {α : Type u_1} [DecidableEq α] {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} {r : LO.Modal.Standard.Formula α} (h : autoParam (q ⟶ r ∈ 𝒮 p) _auto✝) : q ∈ 𝒮 p

theorem LO.Modal.Standard.Formula.Subformulas.mem_imp₂ {α : Type u_1} [DecidableEq α] {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} {r : LO.Modal.Standard.Formula α} (h : autoParam (q ⟶ r ∈ 𝒮 p) _auto✝) : r ∈ 𝒮 p

theorem LO.Modal.Standard.Formula.Subformulas.mem_box {α : Type u_1} [DecidableEq α] {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} (h : autoParam (□q ∈ 𝒮 p) _auto✝) : q ∈ 𝒮 p

@[simp]

theorem LO.Modal.Standard.Formula.Subformulas.complexity_lower {α : Type u_1} [DecidableEq α] {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} (h : q ∈ 𝒮 p) : q.complexity ≤ p.complexity

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

• imp_closed : ∀ {p q : LO.Modal.Standard.Formula α}, p ⟶ q ∈ T → p ∈ T ∧ q ∈ T
• box_closed : ∀ {p : LO.Modal.Standard.Formula α}, □p ∈ T → p ∈ T

theorem LO.Modal.Standard.Theory.SubformulaClosed.imp_closed {α : Type u_1} {T : LO.Modal.Standard.Theory α} [self : T.SubformulaClosed] {p : LO.Modal.Standard.Formula α} {q : LO.Modal.Standard.Formula α} : p ⟶ q ∈ T → p ∈ T ∧ q ∈ T

theorem LO.Modal.Standard.Theory.SubformulaClosed.box_closed {α : Type u_1} {T : LO.Modal.Standard.Theory α} [self : T.SubformulaClosed] {p : LO.Modal.Standard.Formula α} : □p ∈ T → p ∈ T

instance LO.Modal.Standard.Theory.SubformulaClosed.instToSetFormulaSubformulas {α : Type u_1} [DecidableEq α] {p : LO.Modal.Standard.Formula α} : LO.Modal.Standard.Theory.SubformulaClosed ↑(𝒮 p)

Equations

• LO.Modal.Standard.Theory.SubformulaClosed.instToSetFormulaSubformulas = { imp_closed := ⋯, box_closed := ⋯ }

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

theorem LO.Modal.Standard.Theory.SubformulaClosed.sub_mem_imp {α : Type u_1} {p : LO.Modal.Standard.Formula α} {T : LO.Modal.Standard.Theory α} [T_closed : T.SubformulaClosed] {q : LO.Modal.Standard.Formula α} (h : p ⟶ q ∈ T) : p ∈ T ∧ q ∈ T

theorem LO.Modal.Standard.Theory.SubformulaClosed.sub_mem_imp₁ {α : Type u_1} {p : LO.Modal.Standard.Formula α} {T : LO.Modal.Standard.Theory α} [T_closed : T.SubformulaClosed] {q : LO.Modal.Standard.Formula α} (h : p ⟶ q ∈ T) : p ∈ T

theorem LO.Modal.Standard.Theory.SubformulaClosed.sub_mem_imp₂ {α : Type u_1} {p : LO.Modal.Standard.Formula α} {T : LO.Modal.Standard.Theory α} [T_closed : T.SubformulaClosed] {q : LO.Modal.Standard.Formula α} (h : p ⟶ q ∈ T) : q ∈ T