Foundation.Modal.Entailment.E

source

def LO.Modal.Entailment.multire {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {φ ψ : F} {n : ℕ} (h : 𝓢 ⊢! φ ⭤ ψ) :

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

Equations

LO.Modal.Entailment.multire h = Nat.recAux (id h) (fun (n : ℕ) (ih : 𝓢 ⊢! □^[n]φ ⭤ □^[n]ψ) => ⋯.mpr (LO.Modal.Entailment.re ih)) n

Instances For

source

theorem LO.Modal.Entailment.multire! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {φ ψ : F} {n : ℕ} (h : 𝓢 ⊢ φ ⭤ ψ) :

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

source

def LO.Modal.Entailment.multi_ELLNN! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {n : ℕ} {φ : F} [DecidableEq F] :

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

Equations

LO.Modal.Entailment.multi_ELLNN! = LO.Modal.Entailment.multire LO.Entailment.dn

Instances For

source

@[simp]

theorem LO.Modal.Entailment.multi_ELLNN {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {n : ℕ} {φ : F} [DecidableEq F] :

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

source

def LO.Modal.Entailment.ELLNN! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {φ : F} [DecidableEq F] :

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

Equations

LO.Modal.Entailment.ELLNN! = LO.Modal.Entailment.multi_ELLNN!

Instances For

source

@[simp]

theorem LO.Modal.Entailment.ELLNN {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {φ : F} [DecidableEq F] :

𝓢 ⊢ □φ ⭤ □(∼∼φ)

source

def LO.Modal.Entailment.ILLNN! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {φ : F} [DecidableEq F] :

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

Equations

LO.Modal.Entailment.ILLNN! = LO.Entailment.K_left LO.Modal.Entailment.ELLNN!

Instances For

source

@[simp]

theorem LO.Modal.Entailment.ILLNN {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {φ : F} [DecidableEq F] :

𝓢 ⊢ □φ ➝ □(∼∼φ)

source

def LO.Modal.Entailment.box_dni {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {φ : F} [DecidableEq F] :

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

Alias of LO.Modal.Entailment.ILLNN!.

Equations

@LO.Modal.Entailment.box_dni = @LO.Modal.Entailment.ILLNN!

Instances For

source

theorem LO.Modal.Entailment.box_dni! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {φ : F} [DecidableEq F] :

𝓢 ⊢ □φ ➝ □(∼∼φ)

Alias of LO.Modal.Entailment.ILLNN.

source

def LO.Modal.Entailment.ILNNL! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {φ : F} [DecidableEq F] :

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

Equations

LO.Modal.Entailment.ILNNL! = LO.Entailment.K_right LO.Modal.Entailment.ELLNN!

Instances For

source

@[simp]

theorem LO.Modal.Entailment.ILNNL {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {φ : F} [DecidableEq F] :

𝓢 ⊢ □(∼∼φ) ➝ □φ

source

def LO.Modal.Entailment.box_dne {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {φ : F} [DecidableEq F] :

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

Alias of LO.Modal.Entailment.ILNNL!.

Equations

@LO.Modal.Entailment.box_dne = @LO.Modal.Entailment.ILNNL!

Instances For

source

theorem LO.Modal.Entailment.box_dne! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {φ : F} [DecidableEq F] :

𝓢 ⊢ □(∼∼φ) ➝ □φ

Alias of LO.Modal.Entailment.ILNNL.

source

def LO.Modal.Entailment.box_dne' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {φ : F} [DecidableEq F] (h : 𝓢 ⊢! □(∼∼φ)) :

𝓢 ⊢! □φ

Equations

LO.Modal.Entailment.box_dne' h = LO.Modal.Entailment.box_dne ⨀h

Instances For

source

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

𝓢 ⊢ □φ

source

def LO.Modal.Entailment.INMNL! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {φ : F} [DecidableEq F] :

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

Equations

LO.Modal.Entailment.INMNL! = LO.Entailment.CN_of_CN_left (LO.Entailment.C_trans (LO.Entailment.contra LO.Modal.Entailment.ILNNL!) LO.Modal.Entailment.INLNM!)

Instances For

source

@[simp]

theorem LO.Modal.Entailment.INMNL {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {φ : F} [DecidableEq F] :

𝓢 ⊢ ∼◇(∼φ) ➝ □φ

source

def LO.Modal.Entailment.INLMN! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {φ : F} [DecidableEq F] :

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

Equations

LO.Modal.Entailment.INLMN! = LO.Entailment.CN_of_CN_left LO.Modal.Entailment.INMNL!

Instances For

source

@[simp]

theorem LO.Modal.Entailment.INLMN {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {φ : F} [DecidableEq F] :

𝓢 ⊢ ∼□φ ➝ ◇(∼φ)

source

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

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

Equations

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

Instances For

source

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

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

source

def LO.Modal.Entailment.multidiaDuality_mp {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {n : ℕ} {φ : F} [DecidableEq F] :

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

Equations

LO.Modal.Entailment.multidiaDuality_mp = LO.Entailment.K_left LO.Modal.Entailment.multiDiaDuality

Instances For

source

def LO.Modal.Entailment.diaDuality_mp {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {φ : F} [DecidableEq F] :

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

Equations

LO.Modal.Entailment.diaDuality_mp = LO.Modal.Entailment.multidiaDuality_mp

Instances For

source

def LO.Modal.Entailment.multidiaDuality_mpr {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {n : ℕ} {φ : F} [DecidableEq F] :

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

Equations

LO.Modal.Entailment.multidiaDuality_mpr = LO.Entailment.K_right LO.Modal.Entailment.multiDiaDuality

Instances For

source

def LO.Modal.Entailment.diaDuality_mpr {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {φ : F} [DecidableEq F] :

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

Equations

LO.Modal.Entailment.diaDuality_mpr = LO.Modal.Entailment.multidiaDuality_mpr

Instances For

source

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

𝓢 ⊢! ∼□(∼φ)

Equations

LO.Modal.Entailment.diaDuality'.mp h = LO.Entailment.K_left LO.Modal.Entailment.diaDuality⨀h

Instances For

source

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

𝓢 ⊢! ◇φ

Equations

LO.Modal.Entailment.diaDuality'.mpr h = LO.Entailment.K_right LO.Modal.Entailment.diaDuality⨀h

Instances For

source

@[simp]

theorem LO.Modal.Entailment.multidia_duality!_mp {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {n : ℕ} {φ : F} [DecidableEq F] :

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

source

@[simp]

theorem LO.Modal.Entailment.dia_duality!_mp {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {φ : F} [DecidableEq F] :

𝓢 ⊢ ◇φ ➝ ∼□(∼φ)

source

@[simp]

theorem LO.Modal.Entailment.multidia_duality!_mpr {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {n : ℕ} {φ : F} [DecidableEq F] :

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

source

@[simp]

theorem LO.Modal.Entailment.dia_duality!_mpr {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {φ : F} [DecidableEq F] :

𝓢 ⊢ ∼□(∼φ) ➝ ◇φ

source

theorem LO.Modal.Entailment.dia_duality'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {φ : F} :

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

source

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

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

source

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

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

Equations

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

Instances For

source

@[simp]

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

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

source

def LO.Modal.Entailment.multiboxDuality_mp {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {n : ℕ} {φ : F} [DecidableEq F] :

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

Equations

LO.Modal.Entailment.multiboxDuality_mp = LO.Entailment.K_left LO.Modal.Entailment.multiboxDuality

Instances For

source

def LO.Modal.Entailment.boxDuality_mp {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {φ : F} [DecidableEq F] :

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

Equations

LO.Modal.Entailment.boxDuality_mp = LO.Modal.Entailment.multiboxDuality_mp

Instances For

source

def LO.Modal.Entailment.multiboxDuality_mpr {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {n : ℕ} {φ : F} [DecidableEq F] :

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

Equations

LO.Modal.Entailment.multiboxDuality_mpr = LO.Entailment.K_right LO.Modal.Entailment.multiboxDuality

Instances For

source

def LO.Modal.Entailment.boxDuality_mpr {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {φ : F} [DecidableEq F] :

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

Equations

LO.Modal.Entailment.boxDuality_mpr = LO.Modal.Entailment.multiboxDuality_mpr

Instances For

source

@[simp]

theorem LO.Modal.Entailment.multibox_duality_mp! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {n : ℕ} {φ : F} [DecidableEq F] :

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

source

theorem LO.Modal.Entailment.multibox_duality_mp'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {n : ℕ} {φ : F} [DecidableEq F] (h : 𝓢 ⊢ □^[n]φ) :

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

source

@[simp]

theorem LO.Modal.Entailment.multibox_duality_mpr! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {n : ℕ} {φ : F} [DecidableEq F] :

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

source

theorem LO.Modal.Entailment.multibox_duality_mpr'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {n : ℕ} {φ : F} [DecidableEq F] (h : 𝓢 ⊢ ∼◇^[n](∼φ)) :

𝓢 ⊢ □^[n]φ

source

def LO.Modal.Entailment.boxDuality {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {φ : F} [DecidableEq F] :

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

Equations

LO.Modal.Entailment.boxDuality = LO.Modal.Entailment.multiboxDuality

Instances For

source

@[simp]

theorem LO.Modal.Entailment.box_duality! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {φ : F} [DecidableEq F] :

𝓢 ⊢ □φ ⭤ ∼◇(∼φ)

source

@[simp]

theorem LO.Modal.Entailment.boxDuality_mp! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {φ : F} [DecidableEq F] :

𝓢 ⊢ □φ ➝ ∼◇(∼φ)

source

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

𝓢 ⊢! ∼◇(∼φ)

Equations

LO.Modal.Entailment.boxDuality_mp' h = LO.Modal.Entailment.boxDuality_mp ⨀h

Instances For

source

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

𝓢 ⊢ ∼◇(∼φ)

source

@[simp]

theorem LO.Modal.Entailment.boxDuality_mpr! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.E 𝓢] {φ : F} [DecidableEq F] :

𝓢 ⊢ ∼◇(∼φ) ➝ □φ

source

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

𝓢 ⊢! □φ

Equations

LO.Modal.Entailment.boxDuality_mpr' h = LO.Modal.Entailment.boxDuality_mpr ⨀h

Instances For

source

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

𝓢 ⊢ □φ