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} → [inst : DecidableEq α] → DecidableEq (LO.Modal.Formula α)

Equations

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

@[reducible, inline]

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

Equations

• p.neg = p.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} (p : LO.Modal.Formula α) (q : LO.Modal.Formula α) : LO.Modal.Formula α

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

• p.dia = p.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

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

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

Equations

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

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 ++ "}"
• p.box.toStr = "\\Box " ++ p.toStr
• (p.imp q).toStr = "\\left(" ++ p.toStr ++ " \\to " ++ q.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} (p : LO.Modal.Formula α) (q : LO.Modal.Formula α) : p.or q = p ⋎ q

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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
• (p.imp q).complexity = max p.complexity q.complexity + 1
• p.box.complexity = p.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
• (p.imp q).degree = max p.degree q.degree
• p.box.degree = p.degree + 1

@[simp]

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

@[simp]

theorem LO.Modal.Formula.degree_imp {α : Type u} (p : LO.Modal.Formula α) (q : LO.Modal.Formula α) : (p ➝ q).degree = max p.degree q.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 : (p q : LO.Modal.Formula α) → C (p ➝ q)) (hbox : (p : LO.Modal.Formula α) → C (□p)) (p : LO.Modal.Formula α) : C p

Equations

• LO.Modal.Formula.cases' hfalsum hatom himp hbox x = match x with | LO.Modal.Formula.falsum => hfalsum | LO.Modal.Formula.atom a => hatom a | p.box => hbox p | p.imp q => himp p q

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

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 (p.imp q) = himp p q (LO.Modal.Formula.rec' hfalsum hatom himp hbox p) (LO.Modal.Formula.rec' hfalsum hatom himp hbox q)
• LO.Modal.Formula.rec' hfalsum hatom himp hbox p.box = hbox p (LO.Modal.Formula.rec' hfalsum hatom himp hbox p)

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

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

• x.isBox = match x with | a.box => true | x => 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.Subformulas {α : Type u_1} [DecidableEq α] : LO.Modal.Formula α → LO.Modal.Formulae α

Equations

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

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

Equations

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

@[simp]

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

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

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

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

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

@[simp]

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

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

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

theorem LO.Modal.Formulae.SubformulaClosed.imp_closed {α : Type u_1} {X : LO.Modal.Formulae α} [self : X.SubformulaClosed] {p : LO.Modal.Formula α} {q : LO.Modal.Formula α} : p ➝ q ∈ X → p ∈ X ∧ q ∈ X

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

instance LO.Modal.SubformulaClosed.instSubformulaClosedSubformulas {α : Type u_1} [DecidableEq α] {p : LO.Modal.Formula α} : (𝒮 p).SubformulaClosed

Equations

• LO.Modal.SubformulaClosed.instSubformulaClosedSubformulas = { imp_closed := ⋯, box_closed := ⋯ }

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

theorem LO.Modal.SubformulaClosed.sub_mem_imp {α : Type u_1} {p : LO.Modal.Formula α} {X : LO.Modal.Formulae α} [T_closed : X.SubformulaClosed] {q : LO.Modal.Formula α} (h : p ➝ q ∈ X) : p ∈ X ∧ q ∈ X

theorem LO.Modal.SubformulaClosed.sub_mem_imp₁ {α : Type u_1} {p : LO.Modal.Formula α} {X : LO.Modal.Formulae α} [T_closed : X.SubformulaClosed] {q : LO.Modal.Formula α} (h : p ➝ q ∈ X) : p ∈ X

theorem LO.Modal.SubformulaClosed.sub_mem_imp₂ {α : Type u_1} {p : LO.Modal.Formula α} {X : LO.Modal.Formulae α} [T_closed : X.SubformulaClosed] {q : LO.Modal.Formula α} (h : p ➝ q ∈ X) : q ∈ X

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

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

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

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

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

Equations

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

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

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

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

theorem LO.Modal.Theory.SubformulaClosed.sub_mem_imp₂ {α : Type u_1} {p : LO.Modal.Formula α} {T : LO.Modal.Theory α} [T_closed : T.SubformulaClosed] {q : LO.Modal.Formula α} (h : p ➝ q ∈ T) : q ∈ 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 : (p : LO.Modal.Formula α) → C (∼p)) (himp : (p q : LO.Modal.Formula α) → q ≠ ⊥ → C (p ➝ q)) (hbox : (p : LO.Modal.Formula α) → C (□p)) (p : LO.Modal.Formula α) : C p

Equations

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

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 : (p : LO.Modal.Formula α) → C p → C (∼p)) (himp : (p q : LO.Modal.Formula α) → q ≠ ⊥ → C p → C q → C (p ➝ q)) (hbox : (p : LO.Modal.Formula α) → C p → C (□p)) (p : LO.Modal.Formula α) : C p

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 p.box = hbox p (LO.Modal.Formula.rec_neg hfalsum hatom hneg himp hbox p)
• LO.Modal.Formula.rec_neg hfalsum hatom hneg himp hbox (p.imp LO.Modal.Formula.falsum) = hneg p (LO.Modal.Formula.rec_neg hfalsum hatom hneg himp hbox p)

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

Equations

• x.negated = match x with | a.imp LO.Modal.Formula.falsum => decide True | x => decide False

@[simp]

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

@[simp]

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

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

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

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 : (p : LO.Modal.Formula α) → C p → C (∼p)) (himp : (p q : LO.Modal.Formula α) → ¬(p ➝ q).negated = true → C p → C q → C (p ➝ q)) (hbox : (p : LO.Modal.Formula α) → C p → C (□p)) (p : LO.Modal.Formula α) : C p

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 p.box = hbox p (LO.Modal.Formula.rec_negated hfalsum hatom hneg himp hbox p)
• LO.Modal.Formula.rec_negated hfalsum hatom hneg himp hbox (p.imp LO.Modal.Formula.falsum) = hneg p (LO.Modal.Formula.rec_negated hfalsum hatom hneg himp hbox p)

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
• p.box.toNat = Nat.pair 2 p.toNat + 1
• (p.imp q).toNat = Nat.pair 3 (Nat.pair p.toNat q.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 α] (p : LO.Modal.Formula α) : LO.Modal.Formula.ofNat p.toNat = some p

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 := ⋯ }