Foundation.Modal.System.K

source

def LO.System.multibox_axiomK {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} {φ ψ : F} :

𝓢 ⊢ □^[n](φ ➝ ψ) ➝ □^[n]φ ➝ □^[n]ψ

Equations

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

source

@[simp]

theorem LO.System.multibox_axiomK! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} {φ ψ : F} :

𝓢 ⊢! □^[n](φ ➝ ψ) ➝ □^[n]φ ➝ □^[n]ψ

source

def LO.System.multibox_axiomK' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} {φ ψ : F} (h : 𝓢 ⊢ □^[n](φ ➝ ψ)) :

𝓢 ⊢ □^[n]φ ➝ □^[n]ψ

Equations

LO.System.multibox_axiomK' h = LO.System.multibox_axiomK ⨀h

source

@[simp]

theorem LO.System.multibox_axiomK'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} {φ ψ : F} (h : 𝓢 ⊢! □^[n](φ ➝ ψ)) :

𝓢 ⊢! □^[n]φ ➝ □^[n]ψ

source

def LO.System.multiboxedImplyDistribute {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} {φ ψ : F} (h : 𝓢 ⊢ □^[n](φ ➝ ψ)) :

𝓢 ⊢ □^[n]φ ➝ □^[n]ψ

Alias of LO.System.multibox_axiomK'.

Equations

@LO.System.multiboxedImplyDistribute = @LO.System.multibox_axiomK'

source

theorem LO.System.multiboxed_imply_distribute! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} {φ ψ : F} (h : 𝓢 ⊢! □^[n](φ ➝ ψ)) :

𝓢 ⊢! □^[n]φ ➝ □^[n]ψ

Alias of LO.System.multibox_axiomK'!.

source

def LO.System.boxIff' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {φ ψ : F} (h : 𝓢 ⊢ φ ⭤ ψ) :

𝓢 ⊢ □φ ⭤ □ψ

Equations

LO.System.boxIff' h = LO.System.iffIntro (LO.System.axiomK' (LO.System.nec (LO.System.and₁' h))) (LO.System.axiomK' (LO.System.nec (LO.System.and₂' h)))

source

@[simp]

theorem LO.System.box_iff! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {φ ψ : F} (h : 𝓢 ⊢! φ ⭤ ψ) :

𝓢 ⊢! □φ ⭤ □ψ

source

def LO.System.multiboxIff' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {φ ψ : F} {n : ℕ} (h : 𝓢 ⊢ φ ⭤ ψ) :

𝓢 ⊢ □^[n]φ ⭤ □^[n]ψ

Equations

LO.System.multiboxIff' h = Nat.recAux (id h) (fun (n : ℕ) (ih : 𝓢 ⊢ □^[n]φ ⭤ □^[n]ψ) => ⋯.mpr (LO.System.boxIff' ih)) n

source

@[simp]

theorem LO.System.multibox_iff! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {φ ψ : F} {n : ℕ} (h : 𝓢 ⊢! φ ⭤ ψ) :

𝓢 ⊢! □^[n]φ ⭤ □^[n]ψ

source

def LO.System.diaDuality_mp {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {φ : F} :

𝓢 ⊢ ◇φ ➝ ∼□(∼φ)

Equations

LO.System.diaDuality_mp = LO.System.and₁' LO.System.diaDuality

source

@[simp]

theorem LO.System.diaDuality_mp! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {φ : F} :

𝓢 ⊢! ◇φ ➝ ∼□(∼φ)

source

def LO.System.diaDuality_mpr {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {φ : F} :

𝓢 ⊢ ∼□(∼φ) ➝ ◇φ

Equations

LO.System.diaDuality_mpr = LO.System.and₂' LO.System.diaDuality

source

@[simp]

theorem LO.System.diaDuality_mpr! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {φ : F} :

𝓢 ⊢! ∼□(∼φ) ➝ ◇φ

source

def LO.System.diaDuality'.mp {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {φ : F} (h : 𝓢 ⊢ ◇φ) :

𝓢 ⊢ ∼□(∼φ)

Equations

LO.System.diaDuality'.mp h = LO.System.and₁' LO.System.diaDuality⨀h

source

def LO.System.diaDuality'.mpr {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {φ : F} (h : 𝓢 ⊢ ∼□(∼φ)) :

𝓢 ⊢ ◇φ

Equations

LO.System.diaDuality'.mpr h = LO.System.and₂' LO.System.diaDuality⨀h

source

theorem LO.System.dia_duality'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {φ : F} :

𝓢 ⊢! ◇φ ↔ 𝓢 ⊢! ∼□(∼φ)

source

def LO.System.multiDiaDuality {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} {φ : F} :

𝓢 ⊢ ◇^[n]φ ⭤ ∼□^[n](∼φ)

Equations

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

source

theorem LO.System.multidia_duality! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} {φ : F} :

𝓢 ⊢! ◇^[n]φ ⭤ ∼□^[n](∼φ)

source

theorem LO.System.multidia_duality'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} {φ : F} :

𝓢 ⊢! ◇^[n]φ ↔ 𝓢 ⊢! ∼□^[n](∼φ)

source

def LO.System.diaIff' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {φ ψ : F} (h : 𝓢 ⊢ φ ⭤ ψ) :

𝓢 ⊢ ◇φ ⭤ ◇ψ

Equations

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

source

@[simp]

theorem LO.System.dia_iff! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {φ ψ : F} (h : 𝓢 ⊢! φ ⭤ ψ) :

𝓢 ⊢! ◇φ ⭤ ◇ψ

source

def LO.System.multidiaIff' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {φ ψ : F} {n : ℕ} (h : 𝓢 ⊢ φ ⭤ ψ) :

𝓢 ⊢ ◇^[n]φ ⭤ ◇^[n]ψ

Equations

LO.System.multidiaIff' h = Nat.recAux (id h) (fun (n : ℕ) (ih : 𝓢 ⊢ ◇^[n]φ ⭤ ◇^[n]ψ) => ⋯.mpr (LO.System.diaIff' ih)) n

source

@[simp]

theorem LO.System.multidia_iff! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {φ ψ : F} {n : ℕ} (h : 𝓢 ⊢! φ ⭤ ψ) :

𝓢 ⊢! ◇^[n]φ ⭤ ◇^[n]ψ

source

def LO.System.multiboxDuality {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} {φ : F} :

𝓢 ⊢ □^[n]φ ⭤ ∼◇^[n](∼φ)

Equations

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

source

@[simp]

theorem LO.System.multibox_duality! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} {φ : F} :

𝓢 ⊢! □^[n]φ ⭤ ∼◇^[n](∼φ)

source

def LO.System.boxDuality {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {φ : F} :

𝓢 ⊢ □φ ⭤ ∼◇(∼φ)

Equations

LO.System.boxDuality = LO.System.multiboxDuality

source

@[simp]

theorem LO.System.box_duality! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {φ : F} :

𝓢 ⊢! □φ ⭤ ∼◇(∼φ)

source

def LO.System.boxDuality_mp {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {φ : F} :

𝓢 ⊢ □φ ➝ ∼◇(∼φ)

Equations

LO.System.boxDuality_mp = LO.System.and₁' LO.System.boxDuality

source

@[simp]

theorem LO.System.boxDuality_mp! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {φ : F} :

𝓢 ⊢! □φ ➝ ∼◇(∼φ)

source

def LO.System.boxDuality_mp' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {φ : F} (h : 𝓢 ⊢ □φ) :

𝓢 ⊢ ∼◇(∼φ)

Equations

LO.System.boxDuality_mp' h = LO.System.boxDuality_mp ⨀h

source

theorem LO.System.boxDuality_mp'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {φ : F} (h : 𝓢 ⊢! □φ) :

𝓢 ⊢! ∼◇(∼φ)

source

def LO.System.boxDuality_mpr {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {φ : F} :

𝓢 ⊢ ∼◇(∼φ) ➝ □φ

Equations

LO.System.boxDuality_mpr = LO.System.and₂' LO.System.boxDuality

source

@[simp]

theorem LO.System.boxDuality_mpr! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {φ : F} :

𝓢 ⊢! ∼◇(∼φ) ➝ □φ

source

def LO.System.boxDuality_mpr' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {φ : F} (h : 𝓢 ⊢ ∼◇(∼φ)) :

𝓢 ⊢ □φ

Equations

LO.System.boxDuality_mpr' h = LO.System.boxDuality_mpr ⨀h

source

theorem LO.System.boxDuality_mpr'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {φ : F} (h : 𝓢 ⊢! ∼◇(∼φ)) :

𝓢 ⊢! □φ

source

theorem LO.System.multibox_duality'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} {φ : F} :

𝓢 ⊢! □^[n]φ ↔ 𝓢 ⊢! ∼◇^[n](∼φ)

source

theorem LO.System.box_duality'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {φ : F} :

𝓢 ⊢! □φ ↔ 𝓢 ⊢! ∼◇(∼φ)

source

def LO.System.box_dne {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {φ : F} :

𝓢 ⊢ □(∼∼φ) ➝ □φ

Equations

LO.System.box_dne = LO.System.axiomK' (LO.System.nec LO.System.dne)

source

@[simp]

theorem LO.System.box_dne! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {φ : F} :

𝓢 ⊢! □(∼∼φ) ➝ □φ

source

def LO.System.box_dne' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {φ : F} (h : 𝓢 ⊢ □(∼∼φ)) :

𝓢 ⊢ □φ

Equations

LO.System.box_dne' h = LO.System.box_dne ⨀h

source

theorem LO.System.box_dne'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {φ : F} (h : 𝓢 ⊢! □(∼∼φ)) :

𝓢 ⊢! □φ

source

def LO.System.multiboxverum {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} :

𝓢 ⊢ □^[n]⊤

Equations

LO.System.multiboxverum = LO.System.multinec LO.System.verum

source

@[simp]

theorem LO.System.multiboxverum! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} :

𝓢 ⊢! □^[n]⊤

source

def LO.System.boxverum {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] :

𝓢 ⊢ □⊤

Equations

LO.System.boxverum = LO.System.multiboxverum

source

@[simp]

theorem LO.System.boxverum! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] :

𝓢 ⊢! □⊤

source

def LO.System.boxdotverum {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] :

𝓢 ⊢ ⊡⊤

Equations

LO.System.boxdotverum = LO.System.andIntro LO.System.verum LO.System.boxverum

source

@[simp]

theorem LO.System.boxdotverum! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] :

𝓢 ⊢! ⊡⊤

source

def LO.System.implyMultiboxDistribute' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {φ ψ : F} {n : ℕ} (h : 𝓢 ⊢ φ ➝ ψ) :

𝓢 ⊢ □^[n]φ ➝ □^[n]ψ

Equations

LO.System.implyMultiboxDistribute' h = LO.System.multibox_axiomK' (LO.System.multinec h)

source

theorem LO.System.imply_multibox_distribute'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {φ ψ : F} {n : ℕ} (h : 𝓢 ⊢! φ ➝ ψ) :

𝓢 ⊢! □^[n]φ ➝ □^[n]ψ

source

def LO.System.implyBoxDistribute' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {φ ψ : F} (h : 𝓢 ⊢ φ ➝ ψ) :

𝓢 ⊢ □φ ➝ □ψ

Equations

LO.System.implyBoxDistribute' h = LO.System.implyMultiboxDistribute' h

source

theorem LO.System.imply_box_distribute'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {φ ψ : F} (h : 𝓢 ⊢! φ ➝ ψ) :

𝓢 ⊢! □φ ➝ □ψ

source

def LO.System.distribute_multibox_and {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} {φ ψ : F} :

𝓢 ⊢ □^[n](φ ⋏ ψ) ➝ □^[n]φ ⋏ □^[n]ψ

Equations

LO.System.distribute_multibox_and = LO.System.implyRightAnd (LO.System.implyMultiboxDistribute' LO.System.and₁) (LO.System.implyMultiboxDistribute' LO.System.and₂)

source

@[simp]

theorem LO.System.distribute_multibox_and! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} {φ ψ : F} :

𝓢 ⊢! □^[n](φ ⋏ ψ) ➝ □^[n]φ ⋏ □^[n]ψ

source

def LO.System.distribute_box_and {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {φ ψ : F} :

𝓢 ⊢ □(φ ⋏ ψ) ➝ □φ ⋏ □ψ

Equations

LO.System.distribute_box_and = LO.System.distribute_multibox_and

source

@[simp]

theorem LO.System.distribute_box_and! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {φ ψ : F} :

𝓢 ⊢! □(φ ⋏ ψ) ➝ □φ ⋏ □ψ

source

def LO.System.distribute_multibox_and' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} {φ ψ : F} (h : 𝓢 ⊢ □^[n](φ ⋏ ψ)) :

𝓢 ⊢ □^[n]φ ⋏ □^[n]ψ

Equations

LO.System.distribute_multibox_and' h = LO.System.distribute_multibox_and ⨀h

source

theorem LO.System.distribute_multibox_and'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} {φ ψ : F} (d : 𝓢 ⊢! □^[n](φ ⋏ ψ)) :

𝓢 ⊢! □^[n]φ ⋏ □^[n]ψ

source

def LO.System.distribute_box_and' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {φ ψ : F} (h : 𝓢 ⊢ □(φ ⋏ ψ)) :

𝓢 ⊢ □φ ⋏ □ψ

Equations

LO.System.distribute_box_and' h = LO.System.distribute_multibox_and' h

source

theorem LO.System.distribute_box_and'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {φ ψ : F} (d : 𝓢 ⊢! □(φ ⋏ ψ)) :

𝓢 ⊢! □φ ⋏ □ψ

source

theorem LO.System.conj_cons! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {φ : F} {Γ : List F} :

𝓢 ⊢! φ ⋏ ⋀Γ ⭤ ⋀(φ :: Γ)

source

@[simp]

theorem LO.System.distribute_multibox_conj! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} {Γ : List F} :

𝓢 ⊢! □^[n]⋀Γ ➝ ⋀□'^[n]Γ

source

@[simp]

theorem LO.System.distribute_box_conj! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {Γ : List F} :

𝓢 ⊢! □⋀Γ ➝ ⋀□'Γ

source

def LO.System.collect_multibox_and {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} {φ ψ : F} :

𝓢 ⊢ □^[n]φ ⋏ □^[n]ψ ➝ □^[n](φ ⋏ ψ)

Equations

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

source

@[simp]

theorem LO.System.collect_multibox_and! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} {φ ψ : F} :

𝓢 ⊢! □^[n]φ ⋏ □^[n]ψ ➝ □^[n](φ ⋏ ψ)

source

def LO.System.collect_box_and {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {φ ψ : F} :

𝓢 ⊢ □φ ⋏ □ψ ➝ □(φ ⋏ ψ)

Equations

LO.System.collect_box_and = LO.System.collect_multibox_and

source

@[simp]

theorem LO.System.collect_box_and! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {φ ψ : F} :

𝓢 ⊢! □φ ⋏ □ψ ➝ □(φ ⋏ ψ)

source

def LO.System.collect_multibox_and' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} {φ ψ : F} (h : 𝓢 ⊢ □^[n]φ ⋏ □^[n]ψ) :

𝓢 ⊢ □^[n](φ ⋏ ψ)

Equations

LO.System.collect_multibox_and' h = LO.System.collect_multibox_and ⨀h

source

theorem LO.System.collect_multibox_and'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} {φ ψ : F} (h : 𝓢 ⊢! □^[n]φ ⋏ □^[n]ψ) :

𝓢 ⊢! □^[n](φ ⋏ ψ)

source

def LO.System.collect_box_and' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {φ ψ : F} (h : 𝓢 ⊢ □φ ⋏ □ψ) :

𝓢 ⊢ □(φ ⋏ ψ)

Equations

LO.System.collect_box_and' h = LO.System.collect_multibox_and' h

source

theorem LO.System.collect_box_and'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {φ ψ : F} (h : 𝓢 ⊢! □φ ⋏ □ψ) :

𝓢 ⊢! □(φ ⋏ ψ)

source

theorem LO.System.multiboxConj'_iff! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} {Γ : List F} :

𝓢 ⊢! □^[n]⋀Γ ↔ ∀ φ ∈ Γ, 𝓢 ⊢! □^[n]φ

source

theorem LO.System.boxConj'_iff! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {Γ : List F} :

𝓢 ⊢! □⋀Γ ↔ ∀ φ ∈ Γ, 𝓢 ⊢! □φ

source

theorem LO.System.multiboxconj_of_conjmultibox! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} {Γ : List F} (d : 𝓢 ⊢! ⋀□'^[n]Γ) :

𝓢 ⊢! □^[n]⋀Γ

source

@[simp]

theorem LO.System.multibox_cons_conjAux₁! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} {φ : F} {Γ : List F} :

𝓢 ⊢! ⋀□'^[n](φ :: Γ) ➝ ⋀□'^[n]Γ

source

@[simp]

theorem LO.System.multibox_cons_conjAux₂! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} {φ : F} {Γ : List F} :

𝓢 ⊢! ⋀□'^[n](φ :: Γ) ➝ □^[n]φ

source

@[simp]

theorem LO.System.multibox_cons_conj! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} {φ : F} {Γ : List F} :

𝓢 ⊢! ⋀□'^[n](φ :: Γ) ➝ ⋀□'^[n]Γ ⋏ □^[n]φ

source

@[simp]

theorem LO.System.collect_multibox_conj! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} {Γ : List F} :

𝓢 ⊢! ⋀□'^[n]Γ ➝ □^[n]⋀Γ

source

@[simp]

theorem LO.System.collect_box_conj! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {Γ : List F} :

𝓢 ⊢! ⋀□'Γ ➝ □⋀Γ

source

def LO.System.collect_multibox_or {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} {φ ψ : F} :

𝓢 ⊢ □^[n]φ ⋎ □^[n]ψ ➝ □^[n](φ ⋎ ψ)

Equations

LO.System.collect_multibox_or = LO.System.or₃'' (LO.System.multibox_axiomK' (LO.System.multinec LO.System.or₁)) (LO.System.multibox_axiomK' (LO.System.multinec LO.System.or₂))

source

@[simp]

theorem LO.System.collect_multibox_or! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} {φ ψ : F} :

𝓢 ⊢! □^[n]φ ⋎ □^[n]ψ ➝ □^[n](φ ⋎ ψ)

source

def LO.System.collect_box_or {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {φ ψ : F} :

𝓢 ⊢ □φ ⋎ □ψ ➝ □(φ ⋎ ψ)

Equations

LO.System.collect_box_or = LO.System.collect_multibox_or

source

@[simp]

theorem LO.System.collect_box_or! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {φ ψ : F} :

𝓢 ⊢! □φ ⋎ □ψ ➝ □(φ ⋎ ψ)

source

def LO.System.collect_multibox_or' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} {φ ψ : F} (h : 𝓢 ⊢ □^[n]φ ⋎ □^[n]ψ) :

𝓢 ⊢ □^[n](φ ⋎ ψ)

Equations

LO.System.collect_multibox_or' h = LO.System.collect_multibox_or ⨀h

source

theorem LO.System.collect_multibox_or'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} {φ ψ : F} (h : 𝓢 ⊢! □^[n]φ ⋎ □^[n]ψ) :

𝓢 ⊢! □^[n](φ ⋎ ψ)

source

def LO.System.collect_box_or' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {φ ψ : F} (h : 𝓢 ⊢ □φ ⋎ □ψ) :

𝓢 ⊢ □(φ ⋎ ψ)

Equations

LO.System.collect_box_or' h = LO.System.collect_multibox_or' h

source

theorem LO.System.collect_box_or'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {φ ψ : F} (h : 𝓢 ⊢! □φ ⋎ □ψ) :

𝓢 ⊢! □(φ ⋎ ψ)

source

def LO.System.diaOrInst₁ {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {φ ψ : F} :

𝓢 ⊢ ◇φ ➝ ◇(φ ⋎ ψ)

Equations

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

source

@[simp]

theorem LO.System.dia_or_inst₁! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {φ ψ : F} :

𝓢 ⊢! ◇φ ➝ ◇(φ ⋎ ψ)

source

def LO.System.diaOrInst₂ {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {ψ φ : F} :

𝓢 ⊢ ◇ψ ➝ ◇(φ ⋎ ψ)

Equations

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

source

@[simp]

theorem LO.System.dia_or_inst₂! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {ψ φ : F} :

𝓢 ⊢! ◇ψ ➝ ◇(φ ⋎ ψ)

source

def LO.System.collect_dia_or {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {φ ψ : F} :

𝓢 ⊢ ◇φ ⋎ ◇ψ ➝ ◇(φ ⋎ ψ)

Equations

LO.System.collect_dia_or = LO.System.or₃'' LO.System.diaOrInst₁ LO.System.diaOrInst₂

source

@[simp]

theorem LO.System.collect_dia_or! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {φ ψ : F} :

𝓢 ⊢! ◇φ ⋎ ◇ψ ➝ ◇(φ ⋎ ψ)

source

def LO.System.collect_dia_or' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {φ ψ : F} (h : 𝓢 ⊢ ◇φ ⋎ ◇ψ) :

𝓢 ⊢ ◇(φ ⋎ ψ)

Equations

LO.System.collect_dia_or' h = LO.System.collect_dia_or ⨀h

source

@[simp]

theorem LO.System.collect_dia_or'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {φ ψ : F} (h : 𝓢 ⊢! ◇φ ⋎ ◇ψ) :

𝓢 ⊢! ◇(φ ⋎ ψ)

source

@[simp]

theorem LO.System.distribute_multidia_and! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} {φ ψ : F} :

𝓢 ⊢! ◇^[n](φ ⋏ ψ) ➝ ◇^[n]φ ⋏ ◇^[n]ψ

source

@[simp]

theorem LO.System.distribute_dia_and! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {φ ψ : F} :

𝓢 ⊢! ◇(φ ⋏ ψ) ➝ ◇φ ⋏ ◇ψ

source

@[simp]

theorem LO.System.iff_conjmultidia_multidiaconj! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {n : ℕ} {Γ : List F} :

𝓢 ⊢! ◇^[n]⋀Γ ➝ ⋀◇'^[n]Γ

source

theorem LO.System.distribute_dia_and'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {φ ψ : F} (h : 𝓢 ⊢! ◇(φ ⋏ ψ)) :

𝓢 ⊢! ◇φ ⋏ ◇ψ

source

def LO.System.boxdotAxiomK {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {φ ψ : F} :

𝓢 ⊢ ⊡(φ ➝ ψ) ➝ ⊡φ ➝ ⊡ψ

Equations

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

source

@[simp]

theorem LO.System.boxdot_axiomK! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {φ ψ : F} :

𝓢 ⊢! ⊡(φ ➝ ψ) ➝ ⊡φ ➝ ⊡ψ

source

def LO.System.boxdotAxiomT {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {φ : F} :

𝓢 ⊢ ⊡φ ➝ φ

Equations

LO.System.boxdotAxiomT = LO.System.and₁

source

@[simp]

theorem LO.System.boxdot_axiomT! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {φ : F} :

𝓢 ⊢! ⊡φ ➝ φ

source

def LO.System.boxdotNec {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {φ : F} (d : 𝓢 ⊢ φ) :

𝓢 ⊢ ⊡φ

Equations

LO.System.boxdotNec d = LO.System.and₃' d (LO.System.nec d)

source

theorem LO.System.boxdot_nec! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {φ : F} (d : 𝓢 ⊢! φ) :

𝓢 ⊢! ⊡φ

source

def LO.System.boxdotBox {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {φ : F} :

𝓢 ⊢ ⊡φ ➝ □φ

Equations

LO.System.boxdotBox = LO.System.and₂

source

theorem LO.System.boxdot_box! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [System F S] {𝓢 : S} [System.K 𝓢] {φ : F} :

𝓢 ⊢! ⊡φ ➝ □φ

source

def LO.System.BoxBoxdot_BoxDotbox {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {φ : F} :

𝓢 ⊢ □⊡φ ➝ ⊡□φ

Equations

LO.System.BoxBoxdot_BoxDotbox = LO.System.impTrans'' LO.System.distribute_box_and (LO.System.impId (□φ ⋏ □□φ))

source

theorem LO.System.boxboxdot_boxdotbox {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {φ : F} :

𝓢 ⊢! □⊡φ ➝ ⊡□φ

source

noncomputable def LO.System.lemma_Grz₁ {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {φ : F} :

𝓢 ⊢ □φ ➝ □(□(φ ⋏ (□φ ➝ □□φ) ➝ □(φ ⋏ (□φ ➝ □□φ))) ➝ φ ⋏ (□φ ➝ □□φ))

Equations

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

source

theorem LO.System.lemma_Grz₁! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {φ : F} :

𝓢 ⊢! □φ ➝ □(□(φ ⋏ (□φ ➝ □□φ) ➝ □(φ ⋏ (□φ ➝ □□φ))) ➝ φ ⋏ (□φ ➝ □□φ))

source

theorem LO.System.contextual_nec! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {Γ : List F} {φ : F} (h : Γ ⊢[𝓢]! φ) :

(□'Γ) ⊢[𝓢]! □φ

source

theorem LO.System.Context.provable_iff_boxed {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K 𝓢] {X : Set F} {φ : F} :

(□''X) *⊢[𝓢]! φ ↔ ∃ (Δ : List F), (∀ ψ ∈ □'Δ, ψ ∈ □''X) ∧ (□'Δ) ⊢[𝓢]! φ