- 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 α
Instances For
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]
Equations
- p.neg = p.imp LO.Modal.Standard.Formula.falsum
Instances For
@[reducible, inline]
Equations
- LO.Modal.Standard.Formula.verum = LO.Modal.Standard.Formula.falsum.imp LO.Modal.Standard.Formula.falsum
Instances For
@[reducible, inline]
Equations
- LO.Modal.Standard.Formula.top = LO.Modal.Standard.Formula.falsum.imp LO.Modal.Standard.Formula.falsum
Instances For
@[reducible, inline]
abbrev
LO.Modal.Standard.Formula.or
{α : Type u_1}
(p : LO.Modal.Standard.Formula α)
(q : LO.Modal.Standard.Formula α)
:
Equations
- p.or q = p.neg.imp q
Instances For
@[reducible, inline]
abbrev
LO.Modal.Standard.Formula.and
{α : Type u_1}
(p : LO.Modal.Standard.Formula α)
(q : LO.Modal.Standard.Formula α)
:
Equations
- p.and q = (p.imp q.neg).neg
Instances For
@[reducible, inline]
Equations
- p.dia = p.neg.box.neg
Instances For
Equations
- LO.Modal.Standard.Formula.instBasicModalLogicalConnective = LO.BasicModalLogicalConnective.mk
Equations
- LO.Modal.Standard.Formula.instLukasiewiczAbbrev = { top := ⋯, neg := ⋯, or := ⋯, and := ⋯ }
Equations
- LO.Modal.Standard.Formula.instDiaAbbrev = { dia_abbrev := ⋯ }
Equations
Instances For
Equations
- LO.Modal.Standard.Formula.instRepr = { reprPrec := fun (t : LO.Modal.Standard.Formula α) (x : ℕ) => Std.Format.text t.toStr }
Equations
- LO.Modal.Standard.Formula.instToString = { toString := LO.Modal.Standard.Formula.toStr }
Equations
- LO.Modal.Standard.Formula.instCoe = { coe := LO.Modal.Standard.Formula.atom }
theorem
LO.Modal.Standard.Formula.or_eq
{α : Type u}
(p : LO.Modal.Standard.Formula α)
(q : LO.Modal.Standard.Formula α)
:
theorem
LO.Modal.Standard.Formula.and_eq
{α : Type u}
(p : LO.Modal.Standard.Formula α)
(q : LO.Modal.Standard.Formula α)
:
theorem
LO.Modal.Standard.Formula.imp_eq
{α : Type u}
(p : LO.Modal.Standard.Formula α)
(q : LO.Modal.Standard.Formula α)
:
theorem
LO.Modal.Standard.Formula.iff_eq
{α : Type u}
(p : LO.Modal.Standard.Formula α)
(q : LO.Modal.Standard.Formula α)
:
@[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 α)
:
@[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 α)
:
@[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 α)
:
@[simp]
theorem
LO.Modal.Standard.Formula.neg_inj
{α : Type u}
(p : LO.Modal.Standard.Formula α)
(q : LO.Modal.Standard.Formula α)
:
Formula complexity
Equations
Instances For
Max numbers of □
Equations
Instances For
@[simp]
@[simp]
theorem
LO.Modal.Standard.Formula.degree_imp
{α : Type u}
(p : LO.Modal.Standard.Formula α)
(q : LO.Modal.Standard.Formula α)
:
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.
Instances For
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)
Instances For
def
LO.Modal.Standard.Formula.hasDecEq
{α : Type u}
[DecidableEq α]
(p : LO.Modal.Standard.Formula α)
(q : LO.Modal.Standard.Formula α)
:
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- LO.Modal.Standard.Formula.instDecidableEq = LO.Modal.Standard.Formula.hasDecEq
Instances For
@[reducible, inline]
Equations
Instances For
@[reducible, inline]
Equations
Instances For
Equations
- LO.Modal.Standard.instCollectionFormulaTheory = inferInstance
@[reducible, inline]
Equations
Instances For
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))
Instances For
@[simp]
theorem
LO.Modal.Standard.Formula.Subformulas.mem_self
{α : Type u_1}
[DecidableEq α]
(p : LO.Modal.Standard.Formula α)
:
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✝)
:
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✝)
:
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✝)
:
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✝)
:
@[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.Formulae.SubformulaClosed
{α : Type u_1}
(X : LO.Modal.Standard.Formulae α)
:
- box_closed : ∀ {p : LO.Modal.Standard.Formula α}, □p ∈ X → p ∈ X
Instances
theorem
LO.Modal.Standard.Formulae.SubformulaClosed.imp_closed
{α : Type u_1}
{X : LO.Modal.Standard.Formulae α}
[self : X.SubformulaClosed]
{p : LO.Modal.Standard.Formula α}
{q : LO.Modal.Standard.Formula α}
:
theorem
LO.Modal.Standard.Formulae.SubformulaClosed.box_closed
{α : Type u_1}
{X : LO.Modal.Standard.Formulae α}
[self : X.SubformulaClosed]
{p : LO.Modal.Standard.Formula α}
:
instance
LO.Modal.Standard.SubformulaClosed.instSubformulaClosedSubformulas
{α : Type u_1}
[DecidableEq α]
{p : LO.Modal.Standard.Formula α}
:
(𝒮 p).SubformulaClosed
Equations
- LO.Modal.Standard.SubformulaClosed.instSubformulaClosedSubformulas = { imp_closed := ⋯, box_closed := ⋯ }
theorem
LO.Modal.Standard.SubformulaClosed.sub_mem_box
{α : Type u_1}
{p : LO.Modal.Standard.Formula α}
{X : LO.Modal.Standard.Formulae α}
[T_closed : X.SubformulaClosed]
(h : □p ∈ X)
:
p ∈ X
theorem
LO.Modal.Standard.SubformulaClosed.sub_mem_imp
{α : Type u_1}
{p : LO.Modal.Standard.Formula α}
{X : LO.Modal.Standard.Formulae α}
[T_closed : X.SubformulaClosed]
{q : LO.Modal.Standard.Formula α}
(h : p ⟶ q ∈ X)
:
theorem
LO.Modal.Standard.SubformulaClosed.sub_mem_imp₁
{α : Type u_1}
{p : LO.Modal.Standard.Formula α}
{X : LO.Modal.Standard.Formulae α}
[T_closed : X.SubformulaClosed]
{q : LO.Modal.Standard.Formula α}
(h : p ⟶ q ∈ X)
:
p ∈ X
theorem
LO.Modal.Standard.SubformulaClosed.sub_mem_imp₂
{α : Type u_1}
{p : LO.Modal.Standard.Formula α}
{X : LO.Modal.Standard.Formulae α}
[T_closed : X.SubformulaClosed]
{q : LO.Modal.Standard.Formula α}
(h : p ⟶ q ∈ X)
:
q ∈ X
- box_closed : ∀ {p : LO.Modal.Standard.Formula α}, □p ∈ T → p ∈ T
Instances
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 α}
:
theorem
LO.Modal.Standard.Theory.SubformulaClosed.box_closed
{α : Type u_1}
{T : LO.Modal.Standard.Theory α}
[self : T.SubformulaClosed]
{p : LO.Modal.Standard.Formula α}
:
instance
LO.Modal.Standard.Theory.SubformulaClosed.instToSetFormulaSubformulas
{α : Type u_1}
[DecidableEq α]
{p : LO.Modal.Standard.Formula α}
:
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)
:
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
def
LO.Modal.Standard.Formula.cases_neg
{α : Type u_1}
[DecidableEq α]
{C : LO.Modal.Standard.Formula α → Sort w}
(hfalsum : C ⊥)
(hatom : (a : α) → C (LO.Modal.Standard.Formula.atom a))
(hneg : (p : LO.Modal.Standard.Formula α) → C (~p))
(himp : (p q : LO.Modal.Standard.Formula α) → q ≠ ⊥ → 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.
Instances For
def
LO.Modal.Standard.Formula.rec_neg
{α : Type u_1}
[DecidableEq α]
{C : LO.Modal.Standard.Formula α → Sort w}
(hfalsum : C ⊥)
(hatom : (a : α) → C (LO.Modal.Standard.Formula.atom a))
(hneg : (p : LO.Modal.Standard.Formula α) → C p → C (~p))
(himp : (p q : LO.Modal.Standard.Formula α) → q ≠ ⊥ → 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
- One or more equations did not get rendered due to their size.
- LO.Modal.Standard.Formula.rec_neg hfalsum hatom hneg himp hbox LO.Modal.Standard.Formula.falsum = hfalsum
- LO.Modal.Standard.Formula.rec_neg hfalsum hatom hneg himp hbox (LO.Modal.Standard.Formula.atom a) = hatom a
- LO.Modal.Standard.Formula.rec_neg hfalsum hatom hneg himp hbox p.box = hbox p (LO.Modal.Standard.Formula.rec_neg hfalsum hatom hneg himp hbox p)
- LO.Modal.Standard.Formula.rec_neg hfalsum hatom hneg himp hbox (p.imp LO.Modal.Standard.Formula.falsum) = hneg p (LO.Modal.Standard.Formula.rec_neg hfalsum hatom hneg himp hbox p)
Instances For
Equations
Instances For
@[simp]
@[simp]
theorem
LO.Modal.Standard.Formula.negated_imp
{α : Type u_1}
{p : LO.Modal.Standard.Formula α}
{q : LO.Modal.Standard.Formula α}
:
theorem
LO.Modal.Standard.Formula.negated_iff
{α : Type u_1}
[DecidableEq α]
{p : LO.Modal.Standard.Formula α}
:
theorem
LO.Modal.Standard.Formula.not_negated_iff
{α : Type u_1}
[DecidableEq α]
{p : LO.Modal.Standard.Formula α}
:
def
LO.Modal.Standard.Formula.rec_negated
{α : Type u_1}
[DecidableEq α]
{C : LO.Modal.Standard.Formula α → Sort w}
(hfalsum : C ⊥)
(hatom : (a : α) → C (LO.Modal.Standard.Formula.atom a))
(hneg : (p : LO.Modal.Standard.Formula α) → C p → C (~p))
(himp : (p q : LO.Modal.Standard.Formula α) → ¬(p ⟶ q).negated = true → 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
- One or more equations did not get rendered due to their size.
- LO.Modal.Standard.Formula.rec_negated hfalsum hatom hneg himp hbox LO.Modal.Standard.Formula.falsum = hfalsum
- LO.Modal.Standard.Formula.rec_negated hfalsum hatom hneg himp hbox (LO.Modal.Standard.Formula.atom a) = hatom a
- LO.Modal.Standard.Formula.rec_negated hfalsum hatom hneg himp hbox p.box = hbox p (LO.Modal.Standard.Formula.rec_negated hfalsum hatom hneg himp hbox p)
- LO.Modal.Standard.Formula.rec_negated hfalsum hatom hneg himp hbox (p.imp LO.Modal.Standard.Formula.falsum) = hneg p (LO.Modal.Standard.Formula.rec_negated hfalsum hatom hneg himp hbox p)
Instances For
Equations
Instances For
@[irreducible]
def
LO.Modal.Standard.Formula.ofNat
{α : Type u_1}
[Encodable α]
:
ℕ → Option (LO.Modal.Standard.Formula α)
Equations
- One or more equations did not get rendered due to their size.
- LO.Modal.Standard.Formula.ofNat 0 = none
Instances For
theorem
LO.Modal.Standard.Formula.ofNat_toNat
{α : Type u_1}
[Encodable α]
(p : LO.Modal.Standard.Formula α)
:
LO.Modal.Standard.Formula.ofNat p.toNat = some p
Equations
- LO.Modal.Standard.Formula.instEncodable = { encode := LO.Modal.Standard.Formula.toNat, decode := LO.Modal.Standard.Formula.ofNat, encodek := ⋯ }