Formula

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

Imported declaration from the Incompleteness formalization.

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

def LO.Modal.instDecidableEqFormula.decEq {α✝ : Type u_1} [DecidableEq α✝] (x✝ x✝¹ : Formula α✝) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• LO.Modal.instDecidableEqFormula.decEq (LO.Modal.Formula.atom a) (LO.Modal.Formula.atom b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• LO.Modal.instDecidableEqFormula.decEq (LO.Modal.Formula.atom a) LO.Modal.Formula.falsum = isFalse ⋯
• LO.Modal.instDecidableEqFormula.decEq (LO.Modal.Formula.atom a) (a_1.imp a_2) = isFalse ⋯
• LO.Modal.instDecidableEqFormula.decEq (LO.Modal.Formula.atom a) a_1.box = isFalse ⋯
• LO.Modal.instDecidableEqFormula.decEq LO.Modal.Formula.falsum (LO.Modal.Formula.atom a) = isFalse ⋯
• LO.Modal.instDecidableEqFormula.decEq LO.Modal.Formula.falsum LO.Modal.Formula.falsum = isTrue ⋯
• LO.Modal.instDecidableEqFormula.decEq LO.Modal.Formula.falsum (a.imp a_1) = isFalse ⋯
• LO.Modal.instDecidableEqFormula.decEq LO.Modal.Formula.falsum a.box = isFalse ⋯
• LO.Modal.instDecidableEqFormula.decEq (a.imp a_1) (LO.Modal.Formula.atom a_2) = isFalse ⋯
• LO.Modal.instDecidableEqFormula.decEq (a.imp a_1) LO.Modal.Formula.falsum = isFalse ⋯
• LO.Modal.instDecidableEqFormula.decEq (a.imp a_1) a_2.box = isFalse ⋯
• LO.Modal.instDecidableEqFormula.decEq a.box (LO.Modal.Formula.atom a_1) = isFalse ⋯
• LO.Modal.instDecidableEqFormula.decEq a.box LO.Modal.Formula.falsum = isFalse ⋯
• LO.Modal.instDecidableEqFormula.decEq a.box (a_1.imp a_2) = isFalse ⋯
• LO.Modal.instDecidableEqFormula.decEq a.box b.box = if h : a = b then h ▸ have inst := LO.Modal.instDecidableEqFormula.decEq a a; isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

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

Equations

• LO.Modal.instDecidableEqFormula = LO.Modal.instDecidableEqFormula.decEq

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

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

Equations

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

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

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

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

Imported declaration from the Incompleteness formalization.

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)"

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance LO.Modal.Formula.instCoe {α : Type u} : Coe α (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} (φ ψ : Formula α) : φ.or ψ = φ ⋎ ψ

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Formula complexity

Equations

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

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

Max numbers of □

Equations

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

@[simp]

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

@[simp]

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

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

Imported declaration from the Incompleteness formalization.

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 : Formula α → Sort w} (hfalsum : C ⊥) (hatom : (a : α) → C (atom a)) (himp : (φ ψ : Formula α) → C φ → C ψ → C (φ ==> ψ)) (hbox : (φ : Formula α) → C φ → C (□φ)) (φ : Formula α) : C φ

Imported declaration from the Incompleteness formalization.

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 α] (φ ψ : Formula α) : Decidable (φ = ψ)

Imported declaration from the Incompleteness formalization.

Equations

• x✝¹.hasDecEq x✝ = inferInstance

@[implicit_reducible]

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

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

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

@[simp]

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

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

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

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 (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 α] (φ : Formula α) : ofNat φ.toNat = some φ

@[implicit_reducible]

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

Equations

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