Syntax of Basic Modal Logic

Here we supply basic definitions, abbreviations, and lemmas about the syntax of BML.

inductive Formula : Type

Type of BML Formulas.

• bottom : Formula
• top : Formula
• atom : ℕ → Formula
• negAtom : ℕ → Formula
• and : Formula → Formula → Formula
• or : Formula → Formula → Formula
• box : Formula → Formula
• diamond : Formula → Formula

def instReprFormula.repr : Formula → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• instReprFormula.repr Formula.bottom prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Formula.bottom")).group prec✝
• instReprFormula.repr Formula.top prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Formula.top")).group prec✝
• instReprFormula.repr (at a) prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Formula.atom" ++ Std.Format.line ++ reprArg a)).group prec✝

instance instReprFormula : Repr Formula

Equations

• instReprFormula = { reprPrec := instReprFormula.repr }

def instDecidableEqFormula.decEq (x✝ x✝¹ : Formula) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• instDecidableEqFormula.decEq Formula.bottom Formula.bottom = isTrue ⋯
• instDecidableEqFormula.decEq Formula.bottom Formula.top = isFalse instDecidableEqFormula.decEq._proof_1
• instDecidableEqFormula.decEq Formula.bottom (at a) = isFalse ⋯
• instDecidableEqFormula.decEq Formula.bottom (na a) = isFalse ⋯
• instDecidableEqFormula.decEq Formula.bottom (a&a_1) = isFalse ⋯
• instDecidableEqFormula.decEq Formula.bottom (a v a_1) = isFalse ⋯
• instDecidableEqFormula.decEq Formula.bottom (□a) = isFalse ⋯
• instDecidableEqFormula.decEq Formula.bottom (◇a) = isFalse ⋯
• instDecidableEqFormula.decEq Formula.top Formula.bottom = isFalse instDecidableEqFormula.decEq._proof_8
• instDecidableEqFormula.decEq Formula.top Formula.top = isTrue ⋯
• instDecidableEqFormula.decEq Formula.top (at a) = isFalse ⋯
• instDecidableEqFormula.decEq Formula.top (na a) = isFalse ⋯
• instDecidableEqFormula.decEq Formula.top (a&a_1) = isFalse ⋯
• instDecidableEqFormula.decEq Formula.top (a v a_1) = isFalse ⋯
• instDecidableEqFormula.decEq Formula.top (□a) = isFalse ⋯
• instDecidableEqFormula.decEq Formula.top (◇a) = isFalse ⋯
• instDecidableEqFormula.decEq (at a) Formula.bottom = isFalse ⋯
• instDecidableEqFormula.decEq (at a) Formula.top = isFalse ⋯
• instDecidableEqFormula.decEq (at a) (at b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqFormula.decEq (at a) (na a_1) = isFalse ⋯
• instDecidableEqFormula.decEq (at a) (a_1&a_2) = isFalse ⋯
• instDecidableEqFormula.decEq (at a) (a_1 v a_2) = isFalse ⋯
• instDecidableEqFormula.decEq (at a) (□a_1) = isFalse ⋯
• instDecidableEqFormula.decEq (at a) (◇a_1) = isFalse ⋯
• instDecidableEqFormula.decEq (na a) Formula.bottom = isFalse ⋯
• instDecidableEqFormula.decEq (na a) Formula.top = isFalse ⋯
• instDecidableEqFormula.decEq (na a) (at a_1) = isFalse ⋯
• instDecidableEqFormula.decEq (na a) (na b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• instDecidableEqFormula.decEq (na a) (a_1&a_2) = isFalse ⋯
• instDecidableEqFormula.decEq (na a) (a_1 v a_2) = isFalse ⋯
• instDecidableEqFormula.decEq (na a) (□a_1) = isFalse ⋯
• instDecidableEqFormula.decEq (na a) (◇a_1) = isFalse ⋯
• instDecidableEqFormula.decEq (a&a_1) Formula.bottom = isFalse ⋯
• instDecidableEqFormula.decEq (a&a_1) Formula.top = isFalse ⋯
• instDecidableEqFormula.decEq (a&a_1) (at a_2) = isFalse ⋯
• instDecidableEqFormula.decEq (a&a_1) (na a_2) = isFalse ⋯
• instDecidableEqFormula.decEq (a&a_1) (a_2 v a_3) = isFalse ⋯
• instDecidableEqFormula.decEq (a&a_1) (□a_2) = isFalse ⋯
• instDecidableEqFormula.decEq (a&a_1) (◇a_2) = isFalse ⋯
• instDecidableEqFormula.decEq (a v a_1) Formula.bottom = isFalse ⋯
• instDecidableEqFormula.decEq (a v a_1) Formula.top = isFalse ⋯
• instDecidableEqFormula.decEq (a v a_1) (at a_2) = isFalse ⋯
• instDecidableEqFormula.decEq (a v a_1) (na a_2) = isFalse ⋯
• instDecidableEqFormula.decEq (a v a_1) (a_2&a_3) = isFalse ⋯
• instDecidableEqFormula.decEq (a v a_1) (□a_2) = isFalse ⋯
• instDecidableEqFormula.decEq (a v a_1) (◇a_2) = isFalse ⋯
• instDecidableEqFormula.decEq (□a) Formula.bottom = isFalse ⋯
• instDecidableEqFormula.decEq (□a) Formula.top = isFalse ⋯
• instDecidableEqFormula.decEq (□a) (at a_1) = isFalse ⋯
• instDecidableEqFormula.decEq (□a) (na a_1) = isFalse ⋯
• instDecidableEqFormula.decEq (□a) (a_1&a_2) = isFalse ⋯
• instDecidableEqFormula.decEq (□a) (a_1 v a_2) = isFalse ⋯
• instDecidableEqFormula.decEq (□a) (□b) = if h : a = b then h ▸ have inst := instDecidableEqFormula.decEq a a; isTrue ⋯ else isFalse ⋯
• instDecidableEqFormula.decEq (□a) (◇a_1) = isFalse ⋯
• instDecidableEqFormula.decEq (◇a) Formula.bottom = isFalse ⋯
• instDecidableEqFormula.decEq (◇a) Formula.top = isFalse ⋯
• instDecidableEqFormula.decEq (◇a) (at a_1) = isFalse ⋯
• instDecidableEqFormula.decEq (◇a) (na a_1) = isFalse ⋯
• instDecidableEqFormula.decEq (◇a) (a_1&a_2) = isFalse ⋯
• instDecidableEqFormula.decEq (◇a) (a_1 v a_2) = isFalse ⋯
• instDecidableEqFormula.decEq (◇a) (□a_1) = isFalse ⋯
• instDecidableEqFormula.decEq (◇a) (◇b) = if h : a = b then h ▸ have inst := instDecidableEqFormula.decEq a a; isTrue ⋯ else isFalse ⋯

instance instDecidableEqFormula : DecidableEq Formula

Equations

• instDecidableEqFormula = instDecidableEqFormula.decEq

@[reducible, inline]

abbrev Sequent : Type

A sequent is a finite set of formulas, read disjunctively.

Equations

• Sequent = Finset Formula

def Formula.termAt_ : Lean.ParserDescr

Equations

• Formula.termAt_ = Lean.ParserDescr.node `Formula.termAt_ 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "at") (Lean.ParserDescr.cat `term 70))

def Formula.termNa_ : Lean.ParserDescr

Equations

• Formula.termNa_ = Lean.ParserDescr.node `Formula.termNa_ 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "na") (Lean.ParserDescr.cat `term 70))

def Formula.«term□_» : Lean.ParserDescr

Equations

• Formula.«term□_» = Lean.ParserDescr.node `Formula.«term□_» 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "□") (Lean.ParserDescr.cat `term 70))

def Formula.«term◇_» : Lean.ParserDescr

Equations

• Formula.«term◇_» = Lean.ParserDescr.node `Formula.«term◇_» 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "◇") (Lean.ParserDescr.cat `term 70))

def Formula.«term_&_» : Lean.TrailingParserDescr

Equations

• Formula.«term_&_» = Lean.ParserDescr.trailingNode `Formula.«term_&_» 6 7 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "&") (Lean.ParserDescr.cat `term 6))

def Formula.term_V_ : Lean.TrailingParserDescr

Equations

• Formula.term_V_ = Lean.ParserDescr.trailingNode `Formula.term_V_ 6 7 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "v") (Lean.ParserDescr.cat `term 6))

instance Formula.instBot : Bot Formula

Equations

• Formula.instBot = { bot := Formula.bottom }

instance Formula.instTop : Top Formula

Equations

• Formula.instTop = { top := Formula.top }

def Formula.neg : Formula → Formula

Negation of a BML Formula.

Equations

• (~Formula.bottom) = ⊤
• (~Formula.top) = ⊥
• (~at a) = na a
• (~na a) = at a
• (~(a&a_1)) = (~a v~a_1)
• (~(a v a_1)) = (~a&~a_1)
• (~□a) = ◇(~a)
• (~◇a) = □(~a)

def Formula.«term~_» : Lean.ParserDescr

Equations

• Formula.«term~_» = Lean.ParserDescr.node `Formula.«term~_» 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "~") (Lean.ParserDescr.cat `term 50))

def Formula.«term_↣_» : Lean.TrailingParserDescr

Equations

• Formula.«term_↣_» = Lean.ParserDescr.trailingNode `Formula.«term_↣_» 55 56 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↣ ") (Lean.ParserDescr.cat `term 55))

def Formula.«term_⟷_» : Lean.TrailingParserDescr

Equations

• Formula.«term_⟷_» = Lean.ParserDescr.trailingNode `Formula.«term_⟷_» 55 56 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⟷ ") (Lean.ParserDescr.cat `term 55))

def Formula.«term⊡_» : Lean.ParserDescr

Equations

• Formula.«term⊡_» = Lean.ParserDescr.node `Formula.«term⊡_» 50 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊡ ") (Lean.ParserDescr.cat `term 50))

Basic operations and simp lemmas for Formulas

def Formula.isAtomic : Formula → Bool

Returns true if the formula is a propositional atom at n.

Equations

• (at a).isAtomic = true
• x✝.isAtomic = false

def Formula.isNegAtomic : Formula → Bool

Returns true if the formula is a negated atom na n.

Equations

• (na a).isNegAtomic = true
• x✝.isNegAtomic = false

def Formula.isDiamond : Formula → Bool

Returns true if the formula is a diamond formula ◇ φ.

Equations

• (◇a).isDiamond = true
• x✝.isDiamond = false

def Formula.opUnDi (φ : Formula) : Option Formula

Returns some φ if the formula is ◇ φ, otherwise none.

Equations

• (◇a).opUnDi = some a
• φ.opUnDi = none

@[simp]

theorem Formula.opUnDi_eq {φ ψ : Formula} : φ.opUnDi = some ψ ↔ φ = ◇ψ

def Formula.unDi (φ : Formula) (h : φ.isDiamond = true) : Formula

Extracts φ from ◇ φ, given a proof that the formula is a diamond.

Equations

• (◇φ_2).unDi h_2 = φ_2

def Formula.isBox : Formula → Bool

Returns true if the formula is a box formula □ φ.

Equations

• (□a).isBox = true
• x✝.isBox = false

@[simp]

theorem Formula.neg_eq {φ ψ : Formula} : (~φ) = (~ψ) → φ = ψ

Negation is injective.

@[simp]

theorem Formula.neg_neg_eq (φ : Formula) : (~~φ) = φ

Negation is involutive.

def Formula.length : Formula → ℕ

Length of a BML Formula.

Equations

• Formula.bottom.length = 0
• Formula.top.length = 0
• (at a).length = 1
• (na a).length = 1
• (a&a_1).length = a.length + a_1.length + 1
• (a v a_1).length = a.length + a_1.length + 1
• (□a).length = a.length + 1
• (◇a).length = a.length + 1

def Formula.vocab : Formula → Finset ℕ

Vocab of a BML Formula. Expressed as underlying natural numbers.

Equations

• Formula.bottom.vocab = ∅
• Formula.top.vocab = ∅
• (at a).vocab = {a}
• (na a).vocab = {a}
• (a&a_1).vocab = a.vocab ∪ a_1.vocab
• (a v a_1).vocab = a.vocab ∪ a_1.vocab
• (□a).vocab = a.vocab
• (◇a).vocab = a.vocab

def Formula.atoms : Formula → Finset ℕ

Atoms of a BML Formula. Expressed as underlying natural numbers.

Equations

• Formula.bottom.atoms = ∅
• Formula.top.atoms = ∅
• (at a).atoms = {a}
• (na a).atoms = ∅
• (a&a_1).atoms = a.vocab ∪ a_1.vocab
• (a v a_1).atoms = a.vocab ∪ a_1.vocab
• (□a).atoms = a.vocab
• (◇a).atoms = a.vocab

def Formula.lit : Formula → Finset (ℕ ⊕ ℕ)

Literals of a BML Formula. Expressed as underlying natural numbers.

Equations

• Formula.bottom.lit = ∅
• Formula.top.lit = ∅
• (at a).lit = {Sum.inl a}
• (na a).lit = {Sum.inr a}
• (a&a_1).lit = a.lit ∪ a_1.lit
• (a v a_1).lit = a.lit ∪ a_1.lit
• (□a).lit = a.lit
• (◇a).lit = a.lit

def Formula.freshVar : Formula → ℕ

Get a fresh variable not occuring in a BML Formula.

Equations

• Formula.top.freshVar = 0
• Formula.bottom.freshVar = 0
• (at n).freshVar = n + 1
• (na n).freshVar = n + 1
• (φ&ψ).freshVar = max φ.freshVar ψ.freshVar
• (φ v ψ).freshVar = max φ.freshVar ψ.freshVar
• (□φ).freshVar = φ.freshVar
• (◇φ).freshVar = φ.freshVar

def Formula.FL : Formula → Sequent

Fischer-Ladner closure of a BML Formula.

Equations

• Formula.bottom.FL = {⊥}
• Formula.top.FL = {⊤}
• (at n).FL = {at n}
• (na n).FL = {na n}
• (φ v ψ).FL = {φ v ψ} ∪ φ.FL ∪ ψ.FL
• (φ&ψ).FL = {φ&ψ} ∪ φ.FL ∪ ψ.FL
• (□φ).FL = {□φ} ∪ φ.FL
• (◇φ).FL = {◇φ} ∪ φ.FL

Lemmas about FL Closure of BML Formulas

theorem Formula.FL_refl {φ : Formula} : φ ∈ φ.FL

Fischer-Ladner closure is reflexive.

theorem Formula.FL_mon {φ ψ : Formula} (ψ_sub_φ : ψ ∈ φ.FL) : ψ.FL ⊆ φ.FL

Fischer-Ladner closure is monotone.

Basic operations and simp lemmas for Sequents

def Sequent.length (Γ : Sequent) : ℕ

Length of a sequent.

Equations

• Γ.length = Finset.sum Γ Formula.length

def Sequent.vocab (Γ : Sequent) : Finset ℕ

Equations

• Γ.vocab = Finset.biUnion Γ Formula.vocab

def Sequent.lit (Γ : Sequent) : Finset (ℕ ⊕ ℕ)

Equations

• Γ.lit = Finset.biUnion Γ Formula.lit

def Sequent.neg (Γ : Sequent) : Finset Formula

Equations

• Γ.neg = Finset.biUnion Γ fun (φ : Formula) => {~φ}

def Sequent.freshVar (Γ : Finset Formula) : ℕ

Equations

• Sequent.freshVar Γ = if h : Γ = ∅ then 0 else (Finset.image Formula.freshVar Γ).max' ⋯

def Sequent.D (Γ : Sequent) : Sequent

Equations

• Γ.D = {x ∈ Γ | decide (x.isDiamond = true) = true} ∪ Finset.filterMap Formula.opUnDi Γ Sequent.D._proof_1

theorem Sequent.form_in_seq_size_le {A : Formula} {Δ : Sequent} : A ∈ Δ → A.length ≤ Δ.length

def Sequent.FL : Sequent → Sequent

Fischer-Ladner closure of a sequent.

Equations

• Δ.FL = Finset.biUnion Δ Formula.FL

Lemmas about FL Closure of Sequents

theorem Sequent.FL_refl {Δ : Sequent} : Δ ⊆ Δ.FL

theorem Sequent.FL_mon {Δ Γ : Sequent} (Δ_sub_Γ : Δ ⊆ Γ) : Δ.FL ⊆ Γ.FL

theorem Sequent.FL_idem {Δ : Sequent} : Δ.FL.FL = Δ.FL

@[reducible, inline]

abbrev SplitFormula : Type

Equations

• SplitFormula = (Formula ⊕ Formula)

@[reducible, inline]

abbrev SplitSequent : Type

Equations

• SplitSequent = Finset SplitFormula

Basic operations and simp lemmas for Split Sequents

def SplitFormula.isDiamond : SplitFormula → Bool

Equations

• SplitFormula.isDiamond (Sum.inl (◇a)) = true
• SplitFormula.isDiamond (Sum.inr (◇a)) = true
• x✝.isDiamond = false

def SplitFormula.opUnDi (φ : SplitFormula) : Option SplitFormula

Equations

• SplitFormula.opUnDi (Sum.inl (◇a)) = some (Sum.inl a)
• SplitFormula.opUnDi (Sum.inr (◇a)) = some (Sum.inr a)
• φ.opUnDi = none

def SplitFormula.length : Formula ⊕ Formula → ℕ

Equations

• SplitFormula.length (Sum.inl φ) = φ.length
• SplitFormula.length (Sum.inr φ) = φ.length

@[irreducible]

def SplitFormula.FL : SplitFormula → SplitSequent

Equations

• SplitFormula.FL (Sum.inl Formula.bottom) = {Sum.inl ⊥}
• SplitFormula.FL (Sum.inr Formula.bottom) = {Sum.inr ⊥}
• SplitFormula.FL (Sum.inl Formula.top) = {Sum.inl ⊤}
• SplitFormula.FL (Sum.inr Formula.top) = {Sum.inr ⊤}
• SplitFormula.FL (Sum.inl (at n)) = {Sum.inl (at n)}
• SplitFormula.FL (Sum.inr (at n)) = {Sum.inr (at n)}
• SplitFormula.FL (Sum.inl (na n)) = {Sum.inl (na n)}
• SplitFormula.FL (Sum.inr (na n)) = {Sum.inr (na n)}
• SplitFormula.FL (Sum.inl (φ v ψ)) = {Sum.inl (φ v ψ)} ∪ SplitFormula.FL (Sum.inl φ) ∪ SplitFormula.FL (Sum.inl ψ)
• SplitFormula.FL (Sum.inr (φ v ψ)) = {Sum.inr (φ v ψ)} ∪ SplitFormula.FL (Sum.inr φ) ∪ SplitFormula.FL (Sum.inr ψ)
• SplitFormula.FL (Sum.inl (φ&ψ)) = {Sum.inl (φ&ψ)} ∪ SplitFormula.FL (Sum.inl φ) ∪ SplitFormula.FL (Sum.inl ψ)
• SplitFormula.FL (Sum.inr (φ&ψ)) = {Sum.inr (φ&ψ)} ∪ SplitFormula.FL (Sum.inr φ) ∪ SplitFormula.FL (Sum.inr ψ)
• SplitFormula.FL (Sum.inl (□φ)) = {Sum.inl (□φ)} ∪ SplitFormula.FL (Sum.inl φ)
• SplitFormula.FL (Sum.inr (□φ)) = {Sum.inr (□φ)} ∪ SplitFormula.FL (Sum.inr φ)
• SplitFormula.FL (Sum.inl (◇φ)) = {Sum.inl (◇φ)} ∪ SplitFormula.FL (Sum.inl φ)
• SplitFormula.FL (Sum.inr (◇φ)) = {Sum.inr (◇φ)} ∪ SplitFormula.FL (Sum.inr φ)

Lemmas about FL Closure of Split Formulas

theorem SplitFormula.FL_SplitFormula_left_eq_FL_Formula_map (φ : Formula) : FL (Sum.inl φ) = Finset.map { toFun := Sum.inl, inj' := ⋯ } φ.FL

theorem SplitFormula.FL_SplitFormula_right_eq_FL_Formula_map (φ : Formula) : FL (Sum.inr φ) = Finset.map { toFun := Sum.inr, inj' := ⋯ } φ.FL

theorem SplitFormula.in_FL_SplitFormula_left {φ : Formula} {ψ : SplitFormula} (ψ_sub_φ : ψ ∈ FL (Sum.inl φ)) : Sum.isLeft ψ = true

theorem SplitFormula.in_FL_SplitFormula_right {φ : Formula} {ψ : SplitFormula} (ψ_sub_φ : ψ ∈ FL (Sum.inr φ)) : Sum.isRight ψ = true

theorem SplitFormula.in_FL_of_in_FL_SplitFormula_left {φ : Formula} {ψ : SplitFormula} (ψ_sub_φ : ψ ∈ FL (Sum.inl φ)) : Sum.elim id id ψ ∈ φ.FL

theorem SplitFormula.in_FL_of_in_FL_SplitFormula_right {φ : Formula} {ψ : SplitFormula} (ψ_sub_φ : ψ ∈ FL (Sum.inr φ)) : Sum.elim id id ψ ∈ φ.FL

theorem SplitFormula.FL_refl {φ : SplitFormula} : φ ∈ φ.FL

Fischer-Ladner Closure is reflexive.

theorem SplitFormula.FL_mon {φ ψ : SplitFormula} (ψ_sub_φ : ψ ∈ φ.FL) : ψ.FL ⊆ φ.FL

Fischer-Ladner Closure is monotone.

Lemmas about FL Closure of Split Sequents

def SplitSequent.FL : SplitSequent → SplitSequent

Equations

• Δ.FL = Finset.biUnion Δ SplitFormula.FL

theorem SplitSequent.FL_refl {Δ : SplitSequent} : Δ ⊆ Δ.FL

Fischer-Ladner Closure is reflexive.

theorem SplitSequent.FL_mon {Δ Γ : SplitSequent} (Δ_sub_Γ : Δ ⊆ Γ) : Δ.FL ⊆ Γ.FL

Fischer-Ladner Closure is monotone.

theorem SplitSequent.FL_idem {Δ : SplitSequent} : Δ.FL.FL = Δ.FL

Fischer-Ladner Closure is idempotent.

def SplitSequent.D (Γ : SplitSequent) : SplitSequent

□₄⁻¹ operator for Split Sequents.

Equations

• Γ.D = {x ∈ Γ | decide (x.isDiamond = true) = true} ∪ Finset.filterMap SplitFormula.opUnDi Γ SplitSequent.D._proof_1

Basic operations and simp lemmas for Split Sequents

def SplitSequent.toSequent (Δ : SplitSequent) : Sequent

Find underlying Sequent of a Split Sequent.

Equations

• Δ.toSequent = Finset.image (Sum.elim id id) Δ

def SplitSequent.length (Δ : SplitSequent) : ℕ

Length of a Split Sequent.

Equations

• Δ.length = Finset.sum Δ SplitFormula.length

@[simp]

theorem SplitSequent.opUnDi_eqₗₗ {φ ψ : Formula} : SplitFormula.opUnDi (Sum.inl φ) = some (Sum.inl ψ) ↔ φ = ◇ψ

@[simp]

theorem SplitSequent.opUnDi_eqᵣᵣ {φ ψ : Formula} : SplitFormula.opUnDi (Sum.inr φ) = some (Sum.inr ψ) ↔ φ = ◇ψ

@[simp]

theorem SplitSequent.opUnDi_eqₗᵣ {φ ψ : Formula} : ¬SplitFormula.opUnDi (Sum.inl φ) = some (Sum.inr ψ)

@[simp]

theorem SplitSequent.opUnDi_eqᵣₗ {φ ψ : Formula} : ¬SplitFormula.opUnDi (Sum.inr φ) = some (Sum.inl ψ)

noncomputable def SplitSequent.filterLeft : SplitSequent → SplitSequent

Equations

• SplitSequent.filterLeft = Finset.filter fun (x : SplitFormula) => match x with | Sum.inl val => true = true | Sum.inr val => false = true

noncomputable def SplitSequent.filterRight : SplitSequent → SplitSequent

Equations

• SplitSequent.filterRight = Finset.filter fun (x : SplitFormula) => match x with | Sum.inl val => false = true | Sum.inr val => true = true

def SplitSequent.left (Γ : SplitSequent) : Sequent

Equations

• Γ.left = Finset.filterMap Sum.getLeft? Γ SplitSequent.left._proof_1

def SplitSequent.right (Γ : SplitSequent) : Sequent

Equations

• Γ.right = Finset.filterMap Sum.getRight? Γ SplitSequent.right._proof_1

Properties of Substitutions

def single (n : ℕ) (ψ : Formula) : Formula → Formula

Substiting p with ψ in φ (φ[ψ/p]). -

Equations

• single n ψ Formula.bottom = ⊥
• single n ψ Formula.top = ⊤
• single n ψ (at a) = if (a == n) = true then ψ else at a
• single n ψ (na a) = if (a == n) = true then ~ψ else na a
• single n ψ (a&a_1) = (single n ψ a&single n ψ a_1)
• single n ψ (a v a_1) = (single n ψ a v single n ψ a_1)
• single n ψ (□a) = □single n ψ a
• single n ψ (◇a) = ◇single n ψ a

theorem single_neg (n : ℕ) (φ ψ : Formula) : single n ψ (~φ) = (~single n ψ φ)

theorem single_imp (n : ℕ) (C D E : Formula) : single n C (~D v E) = (~single n C D v single n C E)

theorem single_iff (n : ℕ) (C D E : Formula) : single n C ((~D v E)&~E v D) = ((~single n C D v single n C E)&~single n C E v single n C D)

@[simp]

theorem single_identity (n : ℕ) (φ : Formula) : single n (at n) φ = φ

def partial_ {c : ℕ → Prop} [DecidablePred c] (σ : Subtype c → Formula) : Formula → Formula

Simultaneous substitution for p meeting criteria c. -

Equations

• partial_ σ Formula.bottom = ⊥
• partial_ σ Formula.top = ⊤
• partial_ σ (at a) = if h : c a then σ ⟨a, h⟩ else at a
• partial_ σ (na a) = if h : c a then ~σ ⟨a, h⟩ else na a
• partial_ σ (a&a_1) = (partial_ σ a&partial_ σ a_1)
• partial_ σ (a v a_1) = (partial_ σ a v partial_ σ a_1)
• partial_ σ (□a) = □partial_ σ a
• partial_ σ (◇a) = ◇partial_ σ a

@[irreducible]

def full (σ : ℕ → Formula) (A : Formula) : Formula

Full substitution of all p.

Equations

• full σ Formula.bottom = ⊥
• full σ Formula.top = ⊤
• full σ (at a) = σ a
• full σ (na a) = (~σ a)
• full σ (a&a_1) = (full σ a&full σ a_1)
• full σ (a v a_1) = (full σ a v full σ a_1)
• full σ (□a) = □full σ a
• full σ (◇a) = ◇full σ a

Properties of Vocab

@[simp]

theorem in_neg_voc_iff {n : ℕ} {φ : Formula} : n ∈ (~φ).vocab ↔ n ∈ φ.vocab

theorem in_single_voc (m n : ℕ) (φ ψ : Formula) : m ∉ φ.vocab → (m ≠ n → m ∉ ψ.vocab) → n ∉ φ.vocab → m ∉ (single n φ ψ).vocab

theorem not_in_single_voc (n : ℕ) (φ ψ : Formula) : n ∉ φ.vocab → single n ψ φ = φ

theorem not_in_single_top_voc (n : ℕ) (φ : Formula) : n ∉ (single n ⊤ φ).vocab

theorem not_in_single_bot_voc (n : ℕ) (φ : Formula) : n ∉ (single n ⊥ φ).vocab

theorem in_single_voc' {m n : ℕ} {φ ψ : Formula} : m ∈ (single n φ ψ).vocab → m ∈ φ.vocab ∧ n ∈ ψ.vocab ∨ m ∈ ψ.vocab ∧ m ≠ n

Some very specific lemmas about Finset.sum

Ideally grind or aesop or some other tactic could sort out these simple helper lemmas, but I could not figure out how.

theorem sub_add_left {n m l : ℕ} : n + m = l → n = l - m

theorem lt_and_le_imp_add_lt {a b c : ℕ} : b ≤ a → c < b → a - b + c < a

theorem Finset.sum_diff_singleton_lt {α : Type} [DecidableEq α] {A C : Finset α} {b : α} {f : α → ℕ} : b ∈ A → C.sum f < f b → (A \ {b} ∪ C).sum f < A.sum f