Documentation

Foundation.Modal.Formula

source
inductive LO.Modal.Formula (α : Type u) :
Type u
Instances For
source
instance LO.Modal.instDecidableEqFormula {α✝ : Type u_1} [DecidableEq α✝] :
DecidableEq (Formula α✝)
Equations
source
@[reducible, inline]
abbrev LO.Modal.Formula.neg {α : Type u_1} (φ : Formula α) :
Formula α
Equations
source
@[reducible, inline]
abbrev LO.Modal.Formula.verum {α : Type u_1} :
Formula α
Equations
source
@[reducible, inline]
abbrev LO.Modal.Formula.top {α : Type u_1} :
Formula α
Equations
source
@[reducible, inline]
abbrev LO.Modal.Formula.or {α : Type u_1} (φ ψ : Formula α) :
Formula α
Equations
  • φ.or ψ = φ.neg.imp ψ
source
@[reducible, inline]
abbrev LO.Modal.Formula.and {α : Type u_1} (φ ψ : Formula α) :
Formula α
Equations
  • φ.and ψ = (φ.imp ψ.neg).neg
source
@[reducible, inline]
abbrev LO.Modal.Formula.dia {α : Type u_1} (φ : Formula α) :
Formula α
Equations
  • φ.dia = φ.neg.box.neg
source
instance LO.Modal.Formula.instBasicModalLogicalConnective {α : Type u} :
BasicModalLogicalConnective (Formula α)
Equations
source
instance LO.Modal.Formula.instLukasiewiczAbbrev {α : Type u} :
LukasiewiczAbbrev (Formula α)
source
instance LO.Modal.Formula.instDiaAbbrev {α : Type u} :
DiaAbbrev (Formula α)
source
def LO.Modal.Formula.toStr {α : Type u} [ToString α] :
Formula α → String
Equations
source
instance LO.Modal.Formula.instRepr {α : Type u} [ToString α] :
Repr (Formula α)
Equations
source
instance LO.Modal.Formula.instToString {α : Type u} [ToString α] :
ToString (Formula α)
Equations
source
instance LO.Modal.Formula.instCoe {α : Type u} :
Coe α (Formula α)
Equations
source
@[simp]
theorem LO.Modal.Formula.neg_bot {α : Type u} :
∼⊥ = ⊤
source
theorem LO.Modal.Formula.or_eq {α : Type u} (φ ψ : Formula α) :
φ.or ψ = φ ⋎ ψ
source
theorem LO.Modal.Formula.and_eq {α : Type u} (φ ψ : Formula α) :
φ.and ψ = φ ⋏ ψ
source
theorem LO.Modal.Formula.imp_eq {α : Type u} (φ ψ : Formula α) :
φ.imp ψ = φ ➝ ψ
source
theorem LO.Modal.Formula.neg_eq {α : Type u} (φ : Formula α) :
φ.neg = ∼φ
source
theorem LO.Modal.Formula.box_eq {α : Type u} (φ : Formula α) :
φ.box = □φ
source
theorem LO.Modal.Formula.dia_eq {α : Type u} (φ : Formula α) :
φ.dia = ◇φ
source
theorem LO.Modal.Formula.iff_eq {α : Type u} (φ ψ : Formula α) :
φ ⭤ ψ = (φ ➝ ψ) ⋏ (ψ ➝ φ)
source
theorem LO.Modal.Formula.falsum_eq {α : Type u} :
falsum = ⊥
source
@[simp]
theorem LO.Modal.Formula.and_inj {α : Type u} (φ₁ ψ₁ φ₂ ψ₂ : Formula α) :
φ₁ ⋏ φ₂ = ψ₁ ⋏ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂
source
@[simp]
theorem LO.Modal.Formula.or_inj {α : Type u} (φ₁ ψ₁ φ₂ ψ₂ : Formula α) :
φ₁ ⋎ φ₂ = ψ₁ ⋎ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂
source
@[simp]
theorem LO.Modal.Formula.imp_inj {α : Type u} (φ₁ ψ₁ φ₂ ψ₂ : Formula α) :
φ₁ ➝ φ₂ = ψ₁ ➝ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂
source
@[simp]
theorem LO.Modal.Formula.neg_inj {α : Type u} (φ ψ : Formula α) :
∼φ = ∼ψ ↔ φ = ψ
source
def LO.Modal.Formula.complexity {α : Type u} :
Formula α → ℕ

Formula complexity

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

Max numbers of □

Equations
source
@[simp]
theorem LO.Modal.Formula.degree_neg {α : Type u} (φ : Formula α) :
(∼φ).degree = φ.degree
source
@[simp]
theorem LO.Modal.Formula.degree_imp {α : Type u} (φ ψ : Formula α) :
(φ ➝ ψ).degree = φ.degree ⊔ ψ.degree
source
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 φ
Equations
source
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 φ
Equations
source
def LO.Modal.Formula.hasDecEq {α : Type u} [DecidableEq α] (φ ψ : Formula α) :
Decidable (φ = ψ)
Equations
  • One or more equations did not get rendered due to their size.
source
instance LO.Modal.Formula.instDecidableEq {α : Type u} [DecidableEq α] :
DecidableEq (Formula α)
Equations
source
def LO.Modal.Formula.isBox {α : Type u} :
Formula α → Bool
Equations
source
@[reducible, inline]
abbrev LO.Modal.Formulae (α : Type u_1) :
Type u_1
Equations
source
@[reducible, inline]
abbrev LO.Modal.Theory (α : Type u_1) :
Type u_1
Equations
Instances For
source
instance LO.Modal.instCollectionFormulaTheory {α : Type u_1} :
Collection (Formula α) (Theory α)
Equations
source
def LO.Modal.Formula.subformulae {α : Type u_1} [DecidableEq α] :
Formula α → Formulae α
Equations
Instances For
source
@[simp]
theorem LO.Modal.Formula.subformulae.mem_self {α : Type u_1} [DecidableEq α] {φ : Formula α} :
φ ∈ φ.subformulae
source
theorem LO.Modal.Formula.subformulae.mem_imp {α : Type u_1} [DecidableEq α] {φ ψ χ : Formula α} (h : ψ ➝ χ ∈ φ.subformulae) :
ψ ∈ φ.subformulae ∧ χ ∈ φ.subformulae
source
theorem LO.Modal.Formula.subformulae.mem_imp₁ {α : Type u_1} [DecidableEq α] {φ ψ χ : Formula α} (h : ψ ➝ χ ∈ φ.subformulae) :
ψ ∈ φ.subformulae
source
theorem LO.Modal.Formula.subformulae.mem_imp₂ {α : Type u_1} [DecidableEq α] {φ ψ χ : Formula α} (h : ψ ➝ χ ∈ φ.subformulae) :
χ ∈ φ.subformulae
source
theorem LO.Modal.Formula.subformulae.mem_box {α : Type u_1} [DecidableEq α] {φ ψ : Formula α} (h : □ψ ∈ φ.subformulae := by assumption) :
ψ ∈ φ.subformulae
source
@[simp]
theorem LO.Modal.Formula.subformulae.complexity_lower {α : Type u_1} [DecidableEq α] {φ ψ : Formula α} (h : ψ ∈ φ.subformulae) :
ψ.complexity ≤ φ.complexity
source
class LO.Modal.Formulae.SubformulaClosed {α : Type u_1} (X : Formulae α) :
Prop
Instances
source
instance LO.Modal.SubformulaClosed.instSubformulaClosedSubformulae {α : Type u_1} [DecidableEq α] {φ : Formula α} :
φ.subformulae.SubformulaClosed
source
theorem LO.Modal.SubformulaClosed.mem_box {α : Type u_1} {φ : Formula α} {X : Formulae α} [closed : X.SubformulaClosed] (h : □φ ∈ X) :
φ ∈ X
source
theorem LO.Modal.SubformulaClosed.mem_imp {α : Type u_1} {φ : Formula α} {X : Formulae α} [closed : X.SubformulaClosed] {ψ : Formula α} (h : φ ➝ ψ ∈ X) :
φ ∈ X ∧ ψ ∈ X
source
theorem LO.Modal.SubformulaClosed.mem_imp₁ {α : Type u_1} {φ : Formula α} {X : Formulae α} [closed : X.SubformulaClosed] {ψ : Formula α} (h : φ ➝ ψ ∈ X) :
φ ∈ X
source
theorem LO.Modal.SubformulaClosed.mem_imp₂ {α : Type u_1} {φ : Formula α} {X : Formulae α} [closed : X.SubformulaClosed] {ψ : Formula α} (h : φ ➝ ψ ∈ X) :
ψ ∈ X
source
class LO.Modal.Theory.SubformulaClosed {α : Type u_1} (T : Theory α) :
Prop
Instances
source
instance LO.Modal.Theory.SubformulaClosed.instToSetFormulaSubformulae {α : Type u_1} {φ : Formula α} [DecidableEq α] :
SubformulaClosed ↑φ.subformulae
source
theorem LO.Modal.Theory.SubformulaClosed.mem_box {α : Type u_1} {φ : Formula α} {T : Theory α} [T_closed : T.SubformulaClosed] (h : □φ ∈ T) :
φ ∈ T
source
theorem LO.Modal.Theory.SubformulaClosed.mem_imp {α : Type u_1} {φ : Formula α} {T : Theory α} [T_closed : T.SubformulaClosed] {ψ : Formula α} (h : φ ➝ ψ ∈ T) :
φ ∈ T ∧ ψ ∈ T
source
theorem LO.Modal.Theory.SubformulaClosed.mem_imp₁ {α : Type u_1} {φ : Formula α} {T : Theory α} [T_closed : T.SubformulaClosed] {ψ : Formula α} (h : φ ➝ ψ ∈ T) :
φ ∈ T
source
theorem LO.Modal.Theory.SubformulaClosed.mem_imp₂ {α : Type u_1} {φ : Formula α} {T : Theory α} [T_closed : T.SubformulaClosed] {ψ : Formula α} (h : φ ➝ ψ ∈ T) :
ψ ∈ T
source
def LO.Modal.Formula.cases_neg {α : 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 φ
Equations
source
def LO.Modal.Formula.rec_neg {α : 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 φ
Equations
source
def LO.Modal.Formula.negated {α : Type u_1} :
Formula α → Bool
Equations
source
@[simp]
theorem LO.Modal.Formula.negated_def {α : Type u_1} {φ : Formula α} :
(∼φ).negated = true
source
@[simp]
theorem LO.Modal.Formula.negated_imp {α : Type u_1} {φ ψ : Formula α} :
(φ ➝ ψ).negated = true ↔ ψ = ⊥
source
theorem LO.Modal.Formula.negated_iff {α : Type u_1} {φ : Formula α} [DecidableEq α] :
φ.negated = true ↔ ∃ (ψ : Formula α), φ = ∼ψ
source
theorem LO.Modal.Formula.not_negated_iff {α : Type u_1} {φ : Formula α} [DecidableEq α] :
¬φ.negated = true ↔ ∀ (ψ : Formula α), φ ≠ ∼ψ
source
def LO.Modal.Formula.rec_negated {α : 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 φ
Equations
source
def LO.Modal.Formula.toNat {α : Type u_1} [Encodable α] :
Formula α → ℕ
Equations
source
@[irreducible]
def LO.Modal.Formula.ofNat {α : Type u_1} [Encodable α] :
ℕ → Option (Formula α)
Equations
source
theorem LO.Modal.Formula.ofNat_toNat {α : Type u_1} [Encodable α] (φ : Formula α) :
ofNat φ.toNat = some φ
source
instance LO.Modal.Formula.instEncodable {α : Type u_1} [Encodable α] :
Encodable (Formula α)
Equations
source
def LO.Modal.Formula.subst {α : Type u_1} (σ : α → Formula α) :
Formula α → Formula α
Equations
source
@[simp]
theorem LO.Modal.Formula.subst_atom {α : Type u_1} {σ : α → Formula α} {a : α} :
subst σ (atom a) = σ a
source
@[simp]
theorem LO.Modal.Formula.subst_bot {α : Type u_1} {σ : α → Formula α} :
subst σ ⊥ = ⊥
source
@[simp]
theorem LO.Modal.Formula.subst_imp {α : Type u_1} {φ ψ : Formula α} {σ : α → Formula α} :
subst σ (φ ➝ ψ) = subst σ φ ➝ subst σ ψ
source
@[simp]
theorem LO.Modal.Formula.subst_neg {α : Type u_1} {φ : Formula α} {σ : α → Formula α} :
subst σ (∼φ) = ∼subst σ φ
source
@[simp]
theorem LO.Modal.Formula.subst_and {α : Type u_1} {φ ψ : Formula α} {σ : α → Formula α} :
subst σ (φ ⋏ ψ) = subst σ φ ⋏ subst σ ψ
source
@[simp]
theorem LO.Modal.Formula.subst_or {α : Type u_1} {φ ψ : Formula α} {σ : α → Formula α} :
subst σ (φ ⋎ ψ) = subst σ φ ⋎ subst σ ψ
source
@[simp]
theorem LO.Modal.Formula.subst_iff {α : Type u_1} {φ ψ : Formula α} {σ : α → Formula α} :
subst σ (φ ⭤ ψ) = subst σ φ ⭤ subst σ ψ
source
@[simp]
theorem LO.Modal.Formula.subst_box {α : Type u_1} {φ : Formula α} {σ : α → Formula α} :
subst σ (□φ) = □subst σ φ
source
@[simp]
theorem LO.Modal.Formula.subst_dia {α : Type u_1} {φ : Formula α} {σ : α → Formula α} :
subst σ (◇φ) = ◇subst σ φ
source
class LO.Modal.Theory.SubstClosed {α : Type u_1} (T : Theory α) :
Prop
Instances
source
def LO.Modal.Theory.instSubstClosed {α : Type u_1} {T : Theory α} (hAtom : ∀ (a : α), Formula.atom a ∈ T → ∀ {σ : α → Formula α}, Formula.subst σ (Formula.atom a) ∈ T) (hImp : ∀ {φ ψ : Formula α}, φ ➝ ψ ∈ T → ∀ {σ : α → Formula α}, Formula.subst σ (φ ➝ ψ) ∈ T) (hBox : ∀ {φ : Formula α}, □φ ∈ T → ∀ {σ : α → Formula α}, Formula.subst σ (□φ) ∈ T) :
T.SubstClosed
Equations
  • ⋯ = ⋯
source
theorem LO.Modal.Theory.SubstClosed.mem_atom {α : Type u_1} {T : Theory α} [T.SubstClosed] {a : α} {σ : α → Formula α} (h : Formula.atom a ∈ T) :
Formula.subst σ (Formula.atom a) ∈ T
source
theorem LO.Modal.Theory.SubstClosed.mem_bot {α : Type u_1} {T : Theory α} [T.SubstClosed] {σ : α → Formula α} (h : ⊥ ∈ T) :
Formula.subst σ ⊥ ∈ T
source
theorem LO.Modal.Theory.SubstClosed.mem_imp {α : Type u_1} {T : Theory α} [T.SubstClosed] {φ ψ : Formula α} {σ : α → Formula α} (h : φ ➝ ψ ∈ T) :
Formula.subst σ (φ ➝ ψ) ∈ T
source
theorem LO.Modal.Theory.SubstClosed.mem_neg {α : Type u_1} {T : Theory α} [T.SubstClosed] {φ : Formula α} {σ : α → Formula α} (h : ∼φ ∈ T) :
Formula.subst σ (∼φ) ∈ T
source
theorem LO.Modal.Theory.SubstClosed.mem_and {α : Type u_1} {T : Theory α} [T.SubstClosed] {φ ψ : Formula α} {σ : α → Formula α} (h : φ ⋏ ψ ∈ T) :
Formula.subst σ (φ ⋏ ψ) ∈ T
source
theorem LO.Modal.Theory.SubstClosed.mem_or {α : Type u_1} {T : Theory α} [T.SubstClosed] {φ ψ : Formula α} {σ : α → Formula α} (h : φ ⋎ ψ ∈ T) :
Formula.subst σ (φ ⋎ ψ) ∈ T
source
theorem LO.Modal.Theory.SubstClosed.mem_box {α : Type u_1} {T : Theory α} [T.SubstClosed] {φ : Formula α} {σ : α → Formula α} (h : □φ ∈ T) :
Formula.subst σ (□φ) ∈ T
source
instance LO.Modal.Theory.SubstClosed.union {α : Type u_1} {T₁ T₂ : Theory α} [T₁_closed : T₁.SubstClosed] [T₂_closed : T₂.SubstClosed] :
(T₁ ∪ T₂).SubstClosed