Documentation

Foundation.InterpretabilityLogic.Formula.Basic

inductive LO.InterpretabilityLogic.Formula (α : Type u_2) :

Type u_2

atom {α : Type u_2} : α → Formula α
falsum {α : Type u_2} : Formula α
imp {α : Type u_2} : Formula α → Formula α → Formula α
box {α : Type u_2} : Formula α → Formula α
rhd {α : Type u_2} : Formula α → Formula α → Formula α

Instances For

@[reducible, inline]

abbrev LO.InterpretabilityLogic.FormulaSet (α : Type u_2) :

Type u_2

Equations

LO.InterpretabilityLogic.FormulaSet α = Set (LO.InterpretabilityLogic.Formula α)

Instances For

@[reducible, inline]

abbrev LO.InterpretabilityLogic.FormulaFinset (α : Type u_2) :

Type u_2

Equations

LO.InterpretabilityLogic.FormulaFinset α = Finset (LO.InterpretabilityLogic.Formula α)

Instances For

@[reducible, inline]

abbrev LO.InterpretabilityLogic.FormulaSeq (α : Type u_2) :

Type u_2

Equations

LO.InterpretabilityLogic.FormulaSeq α = List (LO.InterpretabilityLogic.Formula α)

Instances For

@[reducible, inline]

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

Equations

φ.neg = φ.imp LO.InterpretabilityLogic.Formula.falsum

Instances For

@[reducible, inline]

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

Equations

LO.InterpretabilityLogic.Formula.verum = LO.InterpretabilityLogic.Formula.falsum.imp LO.InterpretabilityLogic.Formula.falsum

Instances For

@[reducible, inline]

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

Equations

LO.InterpretabilityLogic.Formula.top = LO.InterpretabilityLogic.Formula.falsum.imp LO.InterpretabilityLogic.Formula.falsum

Instances For

@[reducible, inline]

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

Equations

φ.or ψ = φ.neg.imp ψ

Instances For

@[reducible, inline]

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

Equations

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

Instances For

@[reducible, inline]

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

Equations

φ.dia = φ.neg.box.neg

Instances For

instance LO.InterpretabilityLogic.Formula.instInterpretabilityLogicalConnective {α : Type u_1} :

InterpretabilityLogicalConnective (Formula α)

Equations

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

instance LO.InterpretabilityLogic.Formula.instŁukasiewiczAbbrev {α : Type u_1} :

ŁukasiewiczAbbrev (Formula α)

instance LO.InterpretabilityLogic.Formula.instDiaByBox {α : Type u_1} :

DiaByBox (Formula α)

theorem LO.InterpretabilityLogic.Formula.eq_falsum {α : Type u_1} :

theorem LO.InterpretabilityLogic.Formula.eq_or {α : Type u_1} {φ ψ : Formula α} :

φ.or ψ = φ ⋎ ψ

theorem LO.InterpretabilityLogic.Formula.eq_and {α : Type u_1} {φ ψ : Formula α} :

φ.and ψ = φ ⋏ ψ

theorem LO.InterpretabilityLogic.Formula.eq_imp {α : Type u_1} {φ ψ : Formula α} :

φ.imp ψ = φ ➝ ψ

theorem LO.InterpretabilityLogic.Formula.eq_rhd {α : Type u_1} {φ ψ : Formula α} :

φ.rhd ψ = φ ▷ ψ

theorem LO.InterpretabilityLogic.Formula.eq_neg {α : Type u_1} {φ : Formula α} :

φ.neg = ∼φ

theorem LO.InterpretabilityLogic.Formula.eq_box {α : Type u_1} {φ : Formula α} :

φ.box = □φ

theorem LO.InterpretabilityLogic.Formula.eq_dia {α : Type u_1} {φ : Formula α} :

φ.dia = ◇φ

theorem LO.InterpretabilityLogic.Formula.eq_iff {α : Type u_1} {φ ψ : Formula α} :

φ ⭤ ψ = (φ ➝ ψ) ⋏ (ψ ➝ φ)

@[simp]

theorem LO.InterpretabilityLogic.Formula.inj_and {α : Type u_1} {φ₁ φ₂ ψ₁ ψ₂ : Formula α} :

φ₁ ⋏ φ₂ = ψ₁ ⋏ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂

@[simp]

theorem LO.InterpretabilityLogic.Formula.inj_or {α : Type u_1} {φ₁ φ₂ ψ₁ ψ₂ : Formula α} :

φ₁ ⋎ φ₂ = ψ₁ ⋎ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂

@[simp]

theorem LO.InterpretabilityLogic.Formula.inj_imp {α : Type u_1} {φ₁ φ₂ ψ₁ ψ₂ : Formula α} :

φ₁ ➝ φ₂ = ψ₁ ➝ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂

@[simp]

theorem LO.InterpretabilityLogic.Formula.inj_rhd {α : Type u_1} {φ₁ φ₂ ψ₁ ψ₂ : Formula α} :

φ₁ ▷ φ₂ = ψ₁ ▷ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂

@[simp]

theorem LO.InterpretabilityLogic.Formula.inj_neg {α : Type u_1} {φ ψ : Formula α} :

∼φ = ∼ψ ↔ φ = ψ

@[simp]

theorem LO.InterpretabilityLogic.Formula.inj_box {α : Type u_1} {φ ψ : Formula α} :

□φ = □ψ ↔ φ = ψ

@[simp]

theorem LO.InterpretabilityLogic.Formula.inj_dia {α : Type u_1} {φ ψ : Formula α} :

◇φ = ◇ψ ↔ φ = ψ

@[simp]

theorem LO.InterpretabilityLogic.Formula.inj_iff {α : Type u_1} {φ₁ φ₂ ψ₁ ψ₂ : Formula α} :

φ₁ ⭤ φ₂ = ψ₁ ⭤ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂

def LO.InterpretabilityLogic.Formula.toStr {α : Type u_1} [ToString α] :

Formula α → String

Equations

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

Instances For

instance LO.InterpretabilityLogic.Formula.instRepr {α : Type u_1} [ToString α] :

Repr (Formula α)

Equations

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

instance LO.InterpretabilityLogic.Formula.instToString {α : Type u_1} [ToString α] :

ToString (Formula α)

Equations

LO.InterpretabilityLogic.Formula.instToString = { toString := LO.InterpretabilityLogic.Formula.toStr }

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

C φ

Equations

LO.InterpretabilityLogic.Formula.cases' hfalsum hatom himp hbox hrhd LO.InterpretabilityLogic.Formula.falsum = hfalsum
LO.InterpretabilityLogic.Formula.cases' hfalsum hatom himp hbox hrhd (LO.InterpretabilityLogic.Formula.atom a) = hatom a
LO.InterpretabilityLogic.Formula.cases' hfalsum hatom himp hbox hrhd φ.box = hbox φ
LO.InterpretabilityLogic.Formula.cases' hfalsum hatom himp hbox hrhd (φ.imp ψ) = himp φ ψ
LO.InterpretabilityLogic.Formula.cases' hfalsum hatom himp hbox hrhd (φ.rhd ψ) = hrhd φ ψ

Instances For

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

C φ

Equations

One or more equations did not get rendered due to their size.
LO.InterpretabilityLogic.Formula.rec' hfalsum hatom himp hbox hrhd LO.InterpretabilityLogic.Formula.falsum = hfalsum
LO.InterpretabilityLogic.Formula.rec' hfalsum hatom himp hbox hrhd (LO.InterpretabilityLogic.Formula.atom a) = hatom a
LO.InterpretabilityLogic.Formula.rec' hfalsum hatom himp hbox hrhd φ.box = hbox φ (LO.InterpretabilityLogic.Formula.rec' hfalsum hatom himp hbox hrhd φ)

Instances For

def LO.InterpretabilityLogic.Formula.hasDecEq {α : Type u_1} [DecidableEq α] (φ ψ : Formula α) :

Decidable (φ = ψ)

Equations

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

Instances For

instance LO.InterpretabilityLogic.Formula.instDecidableEq {α : Type u_1} [DecidableEq α] :

DecidableEq (Formula α)

Equations

LO.InterpretabilityLogic.Formula.instDecidableEq = LO.InterpretabilityLogic.Formula.hasDecEq