Logic.Modal.System

source

class LO.System.HasDiaDuality {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :

Type (max u_2 u_3)

dia_dual : (p : F) → 𝓢 ⊢ LO.Axioms.DiaDuality p

Instances

source

class LO.System.Necessitation {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :

Type (max u_2 u_3)

nec : {p : F} → 𝓢 ⊢ p → 𝓢 ⊢ □p

Instances

LO.Modal.Hilbert.instNecessitationFormulaOfHasNecessitation

source

class LO.System.Unnecessitation {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :

Type (max u_2 u_3)

unnec : {p : F} → 𝓢 ⊢ □p → 𝓢 ⊢ p

Instances

source

class LO.System.LoebRule {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :

Type (max u_2 u_3)

loeb : {p : F} → 𝓢 ⊢ □p ➝ p → 𝓢 ⊢ p

Instances

source

class LO.System.HenkinRule {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :

Type (max u_2 u_3)

henkin : {p : F} → 𝓢 ⊢ □p ⭤ p → 𝓢 ⊢ p

Instances

source

class LO.System.HasAxiomK {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :

Type (max u_2 u_3)

K : (p q : F) → 𝓢 ⊢ LO.Axioms.K p q

Instances

source

class LO.System.HasAxiomT {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :

Type (max u_2 u_3)

T : (p : F) → 𝓢 ⊢ LO.Axioms.T p

Instances

source

class LO.System.HasAxiomD {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :

Type (max u_2 u_3)

D : (p : F) → 𝓢 ⊢ LO.Axioms.D p

Instances

source

class LO.System.HasAxiomD₂ {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :

Type u_3

D₂ : 𝓢 ⊢ LO.Axioms.D₂

Instances

source

class LO.System.HasAxiomB {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :

Type (max u_2 u_3)

B : (p : F) → 𝓢 ⊢ LO.Axioms.B p

Instances

source

class LO.System.HasAxiomFour {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :

Type (max u_2 u_3)

Four : (p : F) → 𝓢 ⊢ LO.Axioms.Four p

Instances

source

class LO.System.HasAxiomFive {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :

Type (max u_2 u_3)

Five : (p : F) → 𝓢 ⊢ LO.Axioms.Five p

Instances

source

class LO.System.HasAxiomL {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :

Type (max u_2 u_3)

L : (p : F) → 𝓢 ⊢ LO.Axioms.L p

Instances

source

class LO.System.HasAxiomDot2 {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :

Type (max u_2 u_3)

Dot2 : (p : F) → 𝓢 ⊢ LO.Axioms.Dot2 p

Instances

source

class LO.System.HasAxiomDot3 {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :

Type (max u_2 u_3)

Dot3 : (p q : F) → 𝓢 ⊢ LO.Axioms.Dot3 p q

Instances

source

class LO.System.HasAxiomGrz {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :

Type (max u_2 u_3)

Grz : (p : F) → 𝓢 ⊢ LO.Axioms.Grz p

Instances

source

class LO.System.HasAxiomTc {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :

Type (max u_2 u_3)

Tc : (p : F) → 𝓢 ⊢ LO.Axioms.Tc p

Instances

source

class LO.System.HasAxiomVer {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :

Type (max u_2 u_3)

Ver : (p : F) → 𝓢 ⊢ LO.Axioms.Ver p

Instances

source

class LO.System.HasAxiomH {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) :

Type (max u_2 u_3)

H : (p : F) → 𝓢 ⊢ LO.Axioms.H p

Instances

source

class LO.System.K {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.Classical , LO.System.Necessitation , LO.System.HasAxiomK , LO.System.HasDiaDuality :

Type (max u_2 u_3)

Instances

source

class LO.System.KT {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K , LO.System.HasAxiomT :

Type (max u_2 u_3)

Instances

source

class LO.System.KD {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K , LO.System.HasAxiomD :

Type (max u_2 u_3)

Instances

LO.Modal.instKDHilbertFormulaKD

source

class LO.System.K4 {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K , LO.System.HasAxiomFour :

Type (max u_2 u_3)

Instances

source

class LO.System.S4 {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K , LO.System.HasAxiomT , LO.System.HasAxiomFour :

Type (max u_2 u_3)

Instances

LO.Modal.instS4HilbertFormulaS4

source

class LO.System.S5 {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K , LO.System.HasAxiomT , LO.System.HasAxiomFive :

Type (max u_2 u_3)

Instances

source

class LO.System.S4Dot2 {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.S4 , LO.System.HasAxiomDot2 :

Type (max u_2 u_3)

Instances

source

class LO.System.S4Dot3 {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.S4 , LO.System.HasAxiomDot3 :

Type (max u_2 u_3)

Instances

source

class LO.System.S4Grz {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.S4 , LO.System.HasAxiomGrz :

Type (max u_2 u_3)

Instances

source

class LO.System.GL {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K , LO.System.HasAxiomL :

Type (max u_2 u_3)

Instances

LO.Modal.instGLHilbertFormulaGL

source

class LO.System.Grz {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K , LO.System.HasAxiomGrz :

Type (max u_2 u_3)

Instances

LO.Modal.instGrzHilbertFormulaGrz

source

class LO.System.Triv {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K , LO.System.HasAxiomT , LO.System.HasAxiomTc :

Type (max u_2 u_3)

Instances

LO.Modal.instTrivHilbertFormulaTriv

source

class LO.System.Ver {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K , LO.System.HasAxiomVer :

Type (max u_2 u_3)

Instances

LO.Modal.instVerHilbertFormulaVer

source

class LO.System.K4H {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K4 , LO.System.HasAxiomH :

Type (max u_2 u_3)

Instances

LO.Modal.instK4HHilbertFormulaK4H

source

class LO.System.K4Loeb {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K4 , LO.System.LoebRule :

Type (max u_2 u_3)

Instances

LO.Modal.instK4LoebHilbertFormulaK4Loeb

source

class LO.System.K4Henkin {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.K4 , LO.System.HenkinRule :

Type (max u_2 u_3)

Instances

LO.Modal.instK4HenkinHilbertFormulaK4Henkin

source

def LO.System.nec {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [self : LO.System.Necessitation 𝓢] {p : F} :

𝓢 ⊢ p → 𝓢 ⊢ □p

Alias of LO.System.Necessitation.nec.

Equations

@LO.System.nec = @LO.System.Necessitation.nec

source

theorem LO.System.nec! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Necessitation 𝓢] :

𝓢 ⊢! p → 𝓢 ⊢! □p

source

def LO.System.multinec {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Necessitation 𝓢] {n : ℕ} :

𝓢 ⊢ p → 𝓢 ⊢ □^[n]p

Equations

LO.System.multinec h = Nat.recAux (id h) (fun (n : ℕ) (ih : 𝓢 ⊢ □^[n]p) => ⋯.mpr (LO.System.nec ih)) n

source

theorem LO.System.multinec! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Necessitation 𝓢] {n : ℕ} :

𝓢 ⊢! p → 𝓢 ⊢! □^[n]p

source

def LO.System.axiomK {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.HasAxiomK 𝓢] :

𝓢 ⊢ □(p ➝ q) ➝ □p ➝ □q

Equations

LO.System.axiomK = LO.System.HasAxiomK.K p q

source

@[simp]

theorem LO.System.axiomK! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.HasAxiomK 𝓢] :

𝓢 ⊢! □(p ➝ q) ➝ □p ➝ □q

source

instance LO.System.instHasAxiomKFiniteContext {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomK 𝓢] (Γ : LO.System.FiniteContext F 𝓢) :

LO.System.HasAxiomK Γ

Equations

LO.System.instHasAxiomKFiniteContext Γ = { K := fun (x x_1 : F) => LO.System.FiniteContext.of LO.System.axiomK }

source

instance LO.System.instHasAxiomKContext {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomK 𝓢] (Γ : LO.System.Context F 𝓢) :

LO.System.HasAxiomK Γ

Equations

LO.System.instHasAxiomKContext Γ = { K := fun (x x_1 : F) => LO.System.Context.of LO.System.axiomK }

source

def LO.System.axiomK' {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomK 𝓢] (h : 𝓢 ⊢ □(p ➝ q)) :

𝓢 ⊢ □p ➝ □q

Equations

LO.System.axiomK' h = LO.System.axiomK⨀h

source

@[simp]

theorem LO.System.axiomK'! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomK 𝓢] (h : 𝓢 ⊢! □(p ➝ q)) :

𝓢 ⊢! □p ➝ □q

source

def LO.System.axiomK'' {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomK 𝓢] (h₁ : 𝓢 ⊢ □(p ➝ q)) (h₂ : 𝓢 ⊢ □p) :

𝓢 ⊢ □q

Equations

LO.System.axiomK'' h₁ h₂ = LO.System.axiomK' h₁⨀h₂

source

@[simp]

theorem LO.System.axiomK''! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomK 𝓢] (h₁ : 𝓢 ⊢! □(p ➝ q)) (h₂ : 𝓢 ⊢! □p) :

𝓢 ⊢! □q

source

def LO.System.multibox_axiomK {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : ℕ} :

𝓢 ⊢ □^[n](p ➝ q) ➝ □^[n]p ➝ □^[n]q

Equations

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

source

@[simp]

theorem LO.System.multibox_axiomK! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : ℕ} :

𝓢 ⊢! □^[n](p ➝ q) ➝ □^[n]p ➝ □^[n]q

source

def LO.System.multibox_axiomK' {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : ℕ} (h : 𝓢 ⊢ □^[n](p ➝ q)) :

𝓢 ⊢ □^[n]p ➝ □^[n]q

Equations

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

source

@[simp]

theorem LO.System.multibox_axiomK'! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : ℕ} (h : 𝓢 ⊢! □^[n](p ➝ q)) :

𝓢 ⊢! □^[n]p ➝ □^[n]q

source

def LO.System.multiboxedImplyDistribute {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : ℕ} (h : 𝓢 ⊢ □^[n](p ➝ q)) :

𝓢 ⊢ □^[n]p ➝ □^[n]q

Alias of LO.System.multibox_axiomK'.

Equations

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

source

theorem LO.System.multiboxed_imply_distribute! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : ℕ} (h : 𝓢 ⊢! □^[n](p ➝ q)) :

𝓢 ⊢! □^[n]p ➝ □^[n]q

Alias of LO.System.multibox_axiomK'!.

source

def LO.System.boxIff' {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] (h : 𝓢 ⊢ p ⭤ q) :

𝓢 ⊢ □p ⭤ □q

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! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] (h : 𝓢 ⊢! p ⭤ q) :

𝓢 ⊢! □p ⭤ □q

source

def LO.System.multiboxIff' {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : ℕ} (h : 𝓢 ⊢ p ⭤ q) :

𝓢 ⊢ □^[n]p ⭤ □^[n]q

Equations

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

source

@[simp]

theorem LO.System.multibox_iff! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : ℕ} (h : 𝓢 ⊢! p ⭤ q) :

𝓢 ⊢! □^[n]p ⭤ □^[n]q

source

instance LO.System.instHasDiaDualityOfModalDeMorganOfHasAxiomDNE {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.ModalDeMorgan F] [LO.System.HasAxiomDNE 𝓢] :

LO.System.HasDiaDuality 𝓢

Equations

LO.System.instHasDiaDualityOfModalDeMorganOfHasAxiomDNE = { dia_dual := fun (p : F) => ⋯.mpr (LO.System.iffId (◇p)) }

source

instance LO.System.instHasDiaDualityOfDiaAbbrev {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.DiaAbbrev F] :

LO.System.HasDiaDuality 𝓢

Equations

LO.System.instHasDiaDualityOfDiaAbbrev = { dia_dual := fun (p : F) => ⋯.mpr (LO.System.iffId (∼□(∼p))) }

source

def LO.System.diaDuality {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasDiaDuality 𝓢] :

𝓢 ⊢ ◇p ⭤ ∼□(∼p)

Equations

LO.System.diaDuality = LO.System.HasDiaDuality.dia_dual p

source

@[simp]

theorem LO.System.dia_duality! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasDiaDuality 𝓢] :

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

source

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

𝓢 ⊢ ∼□(∼p)

Equations

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

source

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

𝓢 ⊢ ◇p

Equations

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

source

theorem LO.System.dia_duality'! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasDiaDuality 𝓢] :

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

source

def LO.System.multiDiaDuality {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : ℕ} [LO.System.HasDiaDuality 𝓢] :

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

Equations

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

source

theorem LO.System.multidia_duality! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : ℕ} [LO.System.HasDiaDuality 𝓢] :

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

source

theorem LO.System.multidia_duality'! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasDiaDuality 𝓢] {n : ℕ} :

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

source

def LO.System.diaIff' {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasDiaDuality 𝓢] (h : 𝓢 ⊢ p ⭤ q) :

𝓢 ⊢ ◇p ⭤ ◇q

Equations

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

source

@[simp]

theorem LO.System.dia_iff! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasDiaDuality 𝓢] (h : 𝓢 ⊢! p ⭤ q) :

𝓢 ⊢! ◇p ⭤ ◇q

source

def LO.System.multidiaIff' {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasDiaDuality 𝓢] {n : ℕ} (h : 𝓢 ⊢ p ⭤ q) :

𝓢 ⊢ ◇^[n]p ⭤ ◇^[n]q

Equations

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

source

@[simp]

theorem LO.System.multidia_iff! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasDiaDuality 𝓢] {n : ℕ} (h : 𝓢 ⊢! p ⭤ q) :

𝓢 ⊢! ◇^[n]p ⭤ ◇^[n]q

source

def LO.System.multiboxDuality {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasDiaDuality 𝓢] {n : ℕ} :

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

Equations

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

source

@[simp]

theorem LO.System.multibox_duality! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasDiaDuality 𝓢] {n : ℕ} :

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

source

def LO.System.boxDuality {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasDiaDuality 𝓢] :

𝓢 ⊢ □p ⭤ ∼◇(∼p)

Equations

LO.System.boxDuality = LO.System.multiboxDuality

source

@[simp]

theorem LO.System.box_duality! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasDiaDuality 𝓢] :

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

source

theorem LO.System.multibox_duality'! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasDiaDuality 𝓢] {n : ℕ} :

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

source

theorem LO.System.box_duality'! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasDiaDuality 𝓢] :

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

source

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

𝓢 ⊢ □^[n]⊤

Equations

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

source

@[simp]

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

𝓢 ⊢! □^[n]⊤

source

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

𝓢 ⊢ □⊤

Equations

LO.System.boxverum = LO.System.multiboxverum

source

@[simp]

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

𝓢 ⊢! □⊤

source

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

𝓢 ⊢ ⊡⊤

Equations

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

source

@[simp]

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

𝓢 ⊢! ⊡⊤

source

def LO.System.implyMultiboxDistribute' {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : ℕ} (h : 𝓢 ⊢ p ➝ q) :

𝓢 ⊢ □^[n]p ➝ □^[n]q

Equations

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

source

theorem LO.System.imply_multibox_distribute'! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : ℕ} (h : 𝓢 ⊢! p ➝ q) :

𝓢 ⊢! □^[n]p ➝ □^[n]q

source

def LO.System.implyBoxDistribute' {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] (h : 𝓢 ⊢ p ➝ q) :

𝓢 ⊢ □p ➝ □q

Equations

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

source

theorem LO.System.imply_box_distribute'! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] (h : 𝓢 ⊢! p ➝ q) :

𝓢 ⊢! □p ➝ □q

source

def LO.System.distribute_multibox_and {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : ℕ} :

𝓢 ⊢ □^[n](p ⋏ q) ➝ □^[n]p ⋏ □^[n]q

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! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : ℕ} :

𝓢 ⊢! □^[n](p ⋏ q) ➝ □^[n]p ⋏ □^[n]q

source

def LO.System.distribute_box_and {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] :

𝓢 ⊢ □(p ⋏ q) ➝ □p ⋏ □q

Equations

LO.System.distribute_box_and = LO.System.distribute_multibox_and

source

@[simp]

theorem LO.System.distribute_box_and! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] :

𝓢 ⊢! □(p ⋏ q) ➝ □p ⋏ □q

source

def LO.System.distribute_multibox_and' {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : ℕ} (h : 𝓢 ⊢ □^[n](p ⋏ q)) :

𝓢 ⊢ □^[n]p ⋏ □^[n]q

Equations

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

source

theorem LO.System.distribute_multibox_and'! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : ℕ} (d : 𝓢 ⊢! □^[n](p ⋏ q)) :

𝓢 ⊢! □^[n]p ⋏ □^[n]q

source

def LO.System.distribute_box_and' {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] (h : 𝓢 ⊢ □(p ⋏ q)) :

𝓢 ⊢ □p ⋏ □q

Equations

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

source

theorem LO.System.distribute_box_and'! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] (d : 𝓢 ⊢! □(p ⋏ q)) :

𝓢 ⊢! □p ⋏ □q

source

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

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

source

@[simp]

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

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

source

@[simp]

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

𝓢 ⊢! □⋀Γ ➝ ⋀□'Γ

source

def LO.System.collect_multibox_and {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : ℕ} :

𝓢 ⊢ □^[n]p ⋏ □^[n]q ➝ □^[n](p ⋏ q)

Equations

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

source

@[simp]

theorem LO.System.collect_multibox_and! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : ℕ} :

𝓢 ⊢! □^[n]p ⋏ □^[n]q ➝ □^[n](p ⋏ q)

source

def LO.System.collect_box_and {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] :

𝓢 ⊢ □p ⋏ □q ➝ □(p ⋏ q)

Equations

LO.System.collect_box_and = LO.System.collect_multibox_and

source

@[simp]

theorem LO.System.collect_box_and! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] :

𝓢 ⊢! □p ⋏ □q ➝ □(p ⋏ q)

source

def LO.System.collect_multibox_and' {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : ℕ} (h : 𝓢 ⊢ □^[n]p ⋏ □^[n]q) :

𝓢 ⊢ □^[n](p ⋏ q)

Equations

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

source

theorem LO.System.collect_multibox_and'! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : ℕ} (h : 𝓢 ⊢! □^[n]p ⋏ □^[n]q) :

𝓢 ⊢! □^[n](p ⋏ q)

source

def LO.System.collect_box_and' {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] (h : 𝓢 ⊢ □p ⋏ □q) :

𝓢 ⊢ □(p ⋏ q)

Equations

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

source

theorem LO.System.collect_box_and'! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] (h : 𝓢 ⊢! □p ⋏ □q) :

𝓢 ⊢! □(p ⋏ q)

source

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

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

source

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

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

source

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

𝓢 ⊢! □^[n]⋀Γ

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

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

source

@[simp]

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

𝓢 ⊢! ⋀□'Γ ➝ □⋀Γ

source

def LO.System.collect_multibox_or {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : ℕ} :

𝓢 ⊢ □^[n]p ⋎ □^[n]q ➝ □^[n](p ⋎ q)

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! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : ℕ} :

𝓢 ⊢! □^[n]p ⋎ □^[n]q ➝ □^[n](p ⋎ q)

source

def LO.System.collect_box_or {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] :

𝓢 ⊢ □p ⋎ □q ➝ □(p ⋎ q)

Equations

LO.System.collect_box_or = LO.System.collect_multibox_or

source

@[simp]

theorem LO.System.collect_box_or! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] :

𝓢 ⊢! □p ⋎ □q ➝ □(p ⋎ q)

source

def LO.System.collect_multibox_or' {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : ℕ} (h : 𝓢 ⊢ □^[n]p ⋎ □^[n]q) :

𝓢 ⊢ □^[n](p ⋎ q)

Equations

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

source

theorem LO.System.collect_multibox_or'! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] {n : ℕ} (h : 𝓢 ⊢! □^[n]p ⋎ □^[n]q) :

𝓢 ⊢! □^[n](p ⋎ q)

source

def LO.System.collect_box_or' {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] (h : 𝓢 ⊢ □p ⋎ □q) :

𝓢 ⊢ □(p ⋎ q)

Equations

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

source

theorem LO.System.collect_box_or'! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] (h : 𝓢 ⊢! □p ⋎ □q) :

𝓢 ⊢! □(p ⋎ q)

source

def LO.System.diaOrInst₁ {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasDiaDuality 𝓢] :

𝓢 ⊢ ◇p ➝ ◇(p ⋎ q)

Equations

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

source

@[simp]

theorem LO.System.dia_or_inst₁! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasDiaDuality 𝓢] :

𝓢 ⊢! ◇p ➝ ◇(p ⋎ q)

source

def LO.System.diaOrInst₂ {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasDiaDuality 𝓢] :

𝓢 ⊢ ◇q ➝ ◇(p ⋎ q)

Equations

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

source

@[simp]

theorem LO.System.dia_or_inst₂! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasDiaDuality 𝓢] :

𝓢 ⊢! ◇q ➝ ◇(p ⋎ q)

source

def LO.System.collect_dia_or {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasDiaDuality 𝓢] :

𝓢 ⊢ ◇p ⋎ ◇q ➝ ◇(p ⋎ q)

Equations

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

source

@[simp]

theorem LO.System.collect_dia_or! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasDiaDuality 𝓢] :

𝓢 ⊢! ◇p ⋎ ◇q ➝ ◇(p ⋎ q)

source

def LO.System.collect_dia_or' {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasDiaDuality 𝓢] (h : 𝓢 ⊢ ◇p ⋎ ◇q) :

𝓢 ⊢ ◇(p ⋎ q)

Equations

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

source

@[simp]

theorem LO.System.collect_dia_or'! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasDiaDuality 𝓢] (h : 𝓢 ⊢! ◇p ⋎ ◇q) :

𝓢 ⊢! ◇(p ⋎ q)

source

@[simp]

theorem LO.System.distribute_multidia_and! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasDiaDuality 𝓢] {n : ℕ} :

𝓢 ⊢! ◇^[n](p ⋏ q) ➝ ◇^[n]p ⋏ ◇^[n]q

source

@[simp]

theorem LO.System.distribute_dia_and! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasDiaDuality 𝓢] :

𝓢 ⊢! ◇(p ⋏ q) ➝ ◇p ⋏ ◇q

source

@[simp]

theorem LO.System.iff_conjmultidia_multidiaconj! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {Γ : List F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasDiaDuality 𝓢] {n : ℕ} :

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

source

theorem LO.System.distribute_dia_and'! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasDiaDuality 𝓢] (h : 𝓢 ⊢! ◇(p ⋏ q)) :

𝓢 ⊢! ◇p ⋏ ◇q

source

def LO.System.boxdotAxiomK {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomK 𝓢] :

𝓢 ⊢ ⊡(p ➝ q) ➝ ⊡p ➝ ⊡q

Equations

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

source

@[simp]

theorem LO.System.boxdot_axiomK! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomK 𝓢] :

𝓢 ⊢! ⊡(p ➝ q) ➝ ⊡p ➝ ⊡q

source

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

𝓢 ⊢ ⊡p ➝ p

Equations

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

source

@[simp]

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

𝓢 ⊢! ⊡p ➝ p

source

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

𝓢 ⊢ ⊡p

Equations

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

source

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

𝓢 ⊢! ⊡p

source

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

𝓢 ⊢ ⊡p ➝ □p

Equations

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

source

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

𝓢 ⊢! ⊡p ➝ □p

source

def LO.System.BoxBoxdot_BoxDotbox {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] :

𝓢 ⊢ □⊡p ➝ ⊡□p

Equations

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

source

theorem LO.System.boxboxdot_boxdotbox {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] :

𝓢 ⊢! □⊡p ➝ ⊡□p

source

def LO.System.axiomT {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomT 𝓢] :

𝓢 ⊢ □p ➝ p

Equations

LO.System.axiomT = LO.System.HasAxiomT.T p

source

@[simp]

theorem LO.System.axiomT! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomT 𝓢] :

𝓢 ⊢! □p ➝ p

source

instance LO.System.instHasAxiomTFiniteContext {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomT 𝓢] (Γ : LO.System.FiniteContext F 𝓢) :

LO.System.HasAxiomT Γ

Equations

LO.System.instHasAxiomTFiniteContext Γ = { T := fun (x : F) => LO.System.FiniteContext.of LO.System.axiomT }

source

instance LO.System.instHasAxiomTContext {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomT 𝓢] (Γ : LO.System.Context F 𝓢) :

LO.System.HasAxiomT Γ

Equations

LO.System.instHasAxiomTContext Γ = { T := fun (x : F) => LO.System.Context.of LO.System.axiomT }

source

def LO.System.axiomT' {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomT 𝓢] (h : 𝓢 ⊢ □p) :

𝓢 ⊢ p

Equations

LO.System.axiomT' h = LO.System.axiomT⨀h

source

@[simp]

theorem LO.System.axiomT'! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomT 𝓢] (h : 𝓢 ⊢! □p) :

𝓢 ⊢! p

source

def LO.System.diaTc {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.HasDiaDuality 𝓢] [LO.System.HasAxiomT 𝓢] :

𝓢 ⊢ p ➝ ◇p

Equations

LO.System.diaTc = LO.System.impTrans'' (LO.System.impTrans'' LO.System.dni (LO.System.contra₀' LO.System.axiomT)) (LO.System.and₂' LO.System.diaDuality)

source

@[simp]

theorem LO.System.diaTc! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.HasDiaDuality 𝓢] [LO.System.HasAxiomT 𝓢] :

𝓢 ⊢! p ➝ ◇p

source

def LO.System.diaTc' {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.HasDiaDuality 𝓢] [LO.System.HasAxiomT 𝓢] (h : 𝓢 ⊢ p) :

𝓢 ⊢ ◇p

Equations

LO.System.diaTc' h = LO.System.diaTc⨀h

source

theorem LO.System.diaTc'! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.HasDiaDuality 𝓢] [LO.System.HasAxiomT 𝓢] (h : 𝓢 ⊢! p) :

𝓢 ⊢! ◇p

source

def LO.System.axiomB {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomB 𝓢] :

𝓢 ⊢ p ➝ □◇p

Equations

LO.System.axiomB = LO.System.HasAxiomB.B p

source

@[simp]

theorem LO.System.axiomB! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomB 𝓢] :

𝓢 ⊢! p ➝ □◇p

source

instance LO.System.instHasAxiomBFiniteContext {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomB 𝓢] (Γ : LO.System.FiniteContext F 𝓢) :

LO.System.HasAxiomB Γ

Equations

LO.System.instHasAxiomBFiniteContext Γ = { B := fun (x : F) => LO.System.FiniteContext.of LO.System.axiomB }

source

instance LO.System.instHasAxiomBContext {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomB 𝓢] (Γ : LO.System.Context F 𝓢) :

LO.System.HasAxiomB Γ

Equations

LO.System.instHasAxiomBContext Γ = { B := fun (x : F) => LO.System.Context.of LO.System.axiomB }

source

def LO.System.axiomD {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomD 𝓢] :

𝓢 ⊢ □p ➝ ◇p

Equations

LO.System.axiomD = LO.System.HasAxiomD.D p

source

@[simp]

theorem LO.System.axiomD! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomD 𝓢] :

𝓢 ⊢! □p ➝ ◇p

source

instance LO.System.instHasAxiomDFiniteContext {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomD 𝓢] (Γ : LO.System.FiniteContext F 𝓢) :

LO.System.HasAxiomD Γ

Equations

LO.System.instHasAxiomDFiniteContext Γ = { D := fun (x : F) => LO.System.FiniteContext.of LO.System.axiomD }

source

instance LO.System.instHasAxiomDContext {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomD 𝓢] (Γ : LO.System.Context F 𝓢) :

LO.System.HasAxiomD Γ

Equations

LO.System.instHasAxiomDContext Γ = { D := fun (x : F) => LO.System.Context.of LO.System.axiomD }

source

def LO.System.notbot {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] :

𝓢 ⊢ ∼⊥

Equations

LO.System.notbot = LO.System.neg_equiv'.mpr (LO.System.impId ⊥)

source

instance LO.System.instHasAxiomD₂ {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasDiaDuality 𝓢] [LO.System.HasAxiomD 𝓢] :

LO.System.HasAxiomD₂ 𝓢

Equations

LO.System.instHasAxiomD₂ = { D₂ := LO.System.D₂_of_D }

source

def LO.System.axiomD₂ {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.HasAxiomD₂ 𝓢] :

𝓢 ⊢ ∼□⊥

Equations

LO.System.axiomD₂ = LO.System.HasAxiomD₂.D₂

source

@[simp]

theorem LO.System.axiomD₂! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.HasAxiomD₂ 𝓢] :

𝓢 ⊢! ∼□⊥

source

instance LO.System.instHasAxiomD₂FiniteContext {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomD₂ 𝓢] (Γ : LO.System.FiniteContext F 𝓢) :

LO.System.HasAxiomD₂ Γ

Equations

LO.System.instHasAxiomD₂FiniteContext Γ = { D₂ := LO.System.FiniteContext.of LO.System.axiomD₂ }

source

instance LO.System.instHasAxiomD₂Context {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomD₂ 𝓢] (Γ : LO.System.Context F 𝓢) :

LO.System.HasAxiomD₂ Γ

Equations

LO.System.instHasAxiomD₂Context Γ = { D₂ := LO.System.Context.of LO.System.axiomD₂ }

source

instance LO.System.instHasAxiomD {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasDiaDuality 𝓢] [LO.System.HasAxiomD₂ 𝓢] :

LO.System.HasAxiomD 𝓢

Equations

LO.System.instHasAxiomD = { D := fun (x : F) => LO.System.D_of_D₂ }

source

def LO.System.axiomFour {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomFour 𝓢] :

𝓢 ⊢ □p ➝ □□p

Equations

LO.System.axiomFour = LO.System.HasAxiomFour.Four p

source

@[simp]

theorem LO.System.axiomFour! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomFour 𝓢] :

𝓢 ⊢! □p ➝ □□p

source

instance LO.System.instHasAxiomFourFiniteContext {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomFour 𝓢] (Γ : LO.System.FiniteContext F 𝓢) :

LO.System.HasAxiomFour Γ

Equations

LO.System.instHasAxiomFourFiniteContext Γ = { Four := fun (x : F) => LO.System.FiniteContext.of LO.System.axiomFour }

source

instance LO.System.instHasAxiomFourContext {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomFour 𝓢] (Γ : LO.System.Context F 𝓢) :

LO.System.HasAxiomFour Γ

Equations

LO.System.instHasAxiomFourContext Γ = { Four := fun (x : F) => LO.System.Context.of LO.System.axiomFour }

source

def LO.System.axiomFour' {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomFour 𝓢] (h : 𝓢 ⊢ □p) :

𝓢 ⊢ □□p

Equations

LO.System.axiomFour' h = LO.System.axiomFour⨀h

source

def LO.System.axiomFour'! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomFour 𝓢] (h : 𝓢 ⊢! □p) :

𝓢 ⊢! □□p

Equations

⋯ = ⋯

source

def LO.System.imply_BoxBoxdot_Box {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] :

𝓢 ⊢ □⊡p ➝ □p

Equations

LO.System.imply_BoxBoxdot_Box = LO.System.impTrans'' LO.System.distribute_box_and LO.System.and₁

source

@[simp]

theorem LO.System.imply_boxboxdot_box {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] :

𝓢 ⊢! □⊡p ➝ □p

source

def LO.System.imply_Box_BoxBoxdot {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasAxiomFour 𝓢] :

𝓢 ⊢ □p ➝ □⊡p

Equations

LO.System.imply_Box_BoxBoxdot = LO.System.impTrans'' (LO.System.implyRightAnd (LO.System.impId (□p)) LO.System.axiomFour) LO.System.collect_box_and

source

@[simp]

theorem LO.System.imply_box_boxboxdot! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasAxiomFour 𝓢] :

𝓢 ⊢! □p ➝ □⊡p

source

def LO.System.imply_Box_BoxBoxdot' {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasAxiomFour 𝓢] (h : 𝓢 ⊢ □p) :

𝓢 ⊢ □⊡p

Equations

LO.System.imply_Box_BoxBoxdot' h = LO.System.imply_Box_BoxBoxdot⨀h

source

def LO.System.imply_Box_BoxBoxdot'! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasAxiomFour 𝓢] (h : 𝓢 ⊢! □p) :

𝓢 ⊢! □⊡p

Equations

⋯ = ⋯

source

def LO.System.iff_Box_BoxBoxdot {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasAxiomFour 𝓢] :

𝓢 ⊢ □p ⭤ □⊡p

Equations

LO.System.iff_Box_BoxBoxdot = LO.System.iffIntro LO.System.imply_Box_BoxBoxdot LO.System.imply_BoxBoxdot_Box

source

@[simp]

theorem LO.System.iff_box_boxboxdot! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasAxiomFour 𝓢] :

𝓢 ⊢! □p ⭤ □⊡p

source

def LO.System.iff_Box_BoxdotBox {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomFour 𝓢] :

𝓢 ⊢ □p ⭤ ⊡□p

Equations

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

source

@[simp]

theorem LO.System.iff_box_boxdotbox! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomFour 𝓢] :

𝓢 ⊢! □p ⭤ ⊡□p

source

def LO.System.iff_Boxdot_BoxdotBoxdot {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasAxiomFour 𝓢] :

𝓢 ⊢ ⊡p ⭤ ⊡⊡p

Equations

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

source

@[simp]

theorem LO.System.iff_boxdot_boxdotboxdot {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasAxiomFour 𝓢] :

𝓢 ⊢! ⊡p ⭤ ⊡⊡p

source

def LO.System.boxdotAxiomFour {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasAxiomFour 𝓢] :

𝓢 ⊢ ⊡p ➝ ⊡⊡p

Equations

LO.System.boxdotAxiomFour = LO.System.and₁' LO.System.iff_Boxdot_BoxdotBoxdot

source

@[simp]

theorem LO.System.boxdot_axiomFour! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasAxiomFour 𝓢] :

𝓢 ⊢! ⊡p ➝ ⊡⊡p

source

def LO.System.iff_box_boxdot {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomT 𝓢] :

𝓢 ⊢ □p ⭤ ⊡p

Equations

LO.System.iff_box_boxdot = LO.System.iffIntro (LO.System.implyRightAnd LO.System.axiomT (LO.System.impId (□p))) LO.System.and₂

source

@[simp]

theorem LO.System.iff_box_boxdot! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomT 𝓢] :

𝓢 ⊢! □p ⭤ ⊡p

source

def LO.System.iff_dia_diadot {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.HasDiaDuality 𝓢] [LO.System.HasAxiomT 𝓢] [LO.System.HasAxiomFour 𝓢] :

𝓢 ⊢ ◇p ⭤ ⟐p

Equations

LO.System.iff_dia_diadot = LO.System.iffIntro LO.System.or₂ (LO.System.or₃'' LO.System.diaTc (LO.System.impId (◇p)))

source

@[simp]

theorem LO.System.iff_dia_diadot! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.HasDiaDuality 𝓢] [LO.System.HasAxiomT 𝓢] [LO.System.HasAxiomFour 𝓢] :

𝓢 ⊢! ◇p ⭤ ⟐p

source

def LO.System.axiomFive {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomFive 𝓢] :

𝓢 ⊢ ◇p ➝ □◇p

Equations

LO.System.axiomFive = LO.System.HasAxiomFive.Five p

source

@[simp]

theorem LO.System.axiomFive! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomFive 𝓢] :

𝓢 ⊢! ◇p ➝ □◇p

source

instance LO.System.instHasAxiomFiveFiniteContext {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomFive 𝓢] (Γ : LO.System.FiniteContext F 𝓢) :

LO.System.HasAxiomFive Γ

Equations

LO.System.instHasAxiomFiveFiniteContext Γ = { Five := fun (x : F) => LO.System.FiniteContext.of LO.System.axiomFive }

source

instance LO.System.instHasAxiomFiveContext {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomFive 𝓢] (Γ : LO.System.Context F 𝓢) :

LO.System.HasAxiomFive Γ

Equations

LO.System.instHasAxiomFiveContext Γ = { Five := fun (x : F) => LO.System.Context.of LO.System.axiomFive }

source

def LO.System.axiomTc {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomTc 𝓢] :

𝓢 ⊢ p ➝ □p

Equations

LO.System.axiomTc = LO.System.HasAxiomTc.Tc p

source

@[simp]

theorem LO.System.axiomTc! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomTc 𝓢] :

𝓢 ⊢! p ➝ □p

source

instance LO.System.instHasAxiomTcFiniteContext {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomTc 𝓢] (Γ : LO.System.FiniteContext F 𝓢) :

LO.System.HasAxiomTc Γ

Equations

LO.System.instHasAxiomTcFiniteContext Γ = { Tc := fun (x : F) => LO.System.FiniteContext.of LO.System.axiomTc }

source

instance LO.System.instHasAxiomTcContext {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomTc 𝓢] (Γ : LO.System.Context F 𝓢) :

LO.System.HasAxiomTc Γ

Equations

LO.System.instHasAxiomTcContext Γ = { Tc := fun (x : F) => LO.System.Context.of LO.System.axiomTc }

source

instance LO.System.instHasAxiomFourOfHasAxiomTc {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.HasAxiomTc 𝓢] :

LO.System.HasAxiomFour 𝓢

Equations

LO.System.instHasAxiomFourOfHasAxiomTc = { Four := fun (x : F) => LO.System.axiomFour_of_Tc }

source

def LO.System.diaT {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.HasDiaDuality 𝓢] [LO.System.HasAxiomTc 𝓢] :

𝓢 ⊢ ◇p ➝ p

Equations

LO.System.diaT = LO.System.impTrans'' (LO.System.and₁' LO.System.diaDuality) (LO.System.contra₂' LO.System.axiomTc)

source

@[simp]

theorem LO.System.diaT! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.HasDiaDuality 𝓢] [LO.System.HasAxiomTc 𝓢] :

𝓢 ⊢! ◇p ➝ p

source

def LO.System.diaT' {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.HasDiaDuality 𝓢] [LO.System.HasAxiomTc 𝓢] (h : 𝓢 ⊢ ◇p) :

𝓢 ⊢ p

Equations

LO.System.diaT' h = LO.System.diaT⨀h

source

theorem LO.System.diaT'! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.HasDiaDuality 𝓢] [LO.System.HasAxiomTc 𝓢] (h : 𝓢 ⊢! ◇p) :

𝓢 ⊢! p

source

def LO.System.axiomVer {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomVer 𝓢] :

𝓢 ⊢ □p

Equations

LO.System.axiomVer = LO.System.HasAxiomVer.Ver p

source

@[simp]

theorem LO.System.axiomVer! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomVer 𝓢] :

𝓢 ⊢! □p

source

instance LO.System.instHasAxiomVerFiniteContext {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomVer 𝓢] (Γ : LO.System.FiniteContext F 𝓢) :

LO.System.HasAxiomVer Γ

Equations

LO.System.instHasAxiomVerFiniteContext Γ = { Ver := fun (x : F) => LO.System.FiniteContext.of LO.System.axiomVer }

source

instance LO.System.instHasAxiomVerContext {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomVer 𝓢] (Γ : LO.System.Context F 𝓢) :

LO.System.HasAxiomVer Γ

Equations

LO.System.instHasAxiomVerContext Γ = { Ver := fun (x : F) => LO.System.Context.of LO.System.axiomVer }

source

instance LO.System.instHasAxiomTcOfHasAxiomVer {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomVer 𝓢] :

LO.System.HasAxiomTc 𝓢

Equations

LO.System.instHasAxiomTcOfHasAxiomVer = { Tc := fun (x : F) => LO.System.axiomTc_of_Ver }

source

instance LO.System.instHasAxiomLOfHasAxiomVer {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomVer 𝓢] :

LO.System.HasAxiomL 𝓢

Equations

LO.System.instHasAxiomLOfHasAxiomVer = { L := fun (x : F) => LO.System.axiomL_of_Ver }

source

def LO.System.bot_of_dia {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.HasDiaDuality 𝓢] [LO.System.HasAxiomVer 𝓢] :

𝓢 ⊢ ◇p ➝ ⊥

Equations

LO.System.bot_of_dia = let_fun this := LO.System.and₁' LO.System.neg_equiv; this⨀(LO.System.contra₀' (LO.System.and₁' LO.System.diaDuality)⨀LO.System.dni' LO.System.axiomVer)

source

theorem LO.System.bot_of_dia! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.HasDiaDuality 𝓢] [LO.System.HasAxiomVer 𝓢] :

𝓢 ⊢! ◇p ➝ ⊥

source

def LO.System.bot_of_dia' {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.HasDiaDuality 𝓢] [LO.System.HasAxiomVer 𝓢] (h : 𝓢 ⊢ ◇p) :

𝓢 ⊢ ⊥

Equations

LO.System.bot_of_dia' h = LO.System.bot_of_dia⨀h

source

theorem LO.System.bot_of_dia'! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.HasDiaDuality 𝓢] [LO.System.HasAxiomVer 𝓢] (h : 𝓢 ⊢! ◇p) :

𝓢 ⊢! ⊥

source

def LO.System.axiomL {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomL 𝓢] :

𝓢 ⊢ □(□p ➝ p) ➝ □p

Equations

LO.System.axiomL = LO.System.HasAxiomL.L p

source

@[simp]

theorem LO.System.axiomL! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomL 𝓢] :

𝓢 ⊢! □(□p ➝ p) ➝ □p

source

instance LO.System.instHasAxiomLFiniteContext {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomL 𝓢] (Γ : LO.System.FiniteContext F 𝓢) :

LO.System.HasAxiomL Γ

Equations

LO.System.instHasAxiomLFiniteContext Γ = { L := fun (x : F) => LO.System.FiniteContext.of LO.System.axiomL }

source

instance LO.System.instHasAxiomLContext {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomL 𝓢] (Γ : LO.System.Context F 𝓢) :

LO.System.HasAxiomL Γ

Equations

LO.System.instHasAxiomLContext Γ = { L := fun (x : F) => LO.System.Context.of LO.System.axiomL }

source

instance LO.System.instHasAxiomFourOfHasAxiomL {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasAxiomL 𝓢] :

LO.System.HasAxiomFour 𝓢

Equations

LO.System.instHasAxiomFourOfHasAxiomL = { Four := fun (x : F) => LO.System.axiomFour_of_L }

source

def LO.System.goedel2 {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasAxiomL 𝓢] :

𝓢 ⊢ ∼□⊥ ⭤ ∼□(∼□⊥)

Equations

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

source

theorem LO.System.goedel2! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasAxiomL 𝓢] :

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

source

def LO.System.goedel2'.mp {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasAxiomL 𝓢] :

𝓢 ⊢ ∼□⊥ → 𝓢 ⊢ ∼□(∼□⊥)

Equations

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

source

def LO.System.goedel2'.mpr {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasAxiomL 𝓢] :

𝓢 ⊢ ∼□(∼□⊥) → 𝓢 ⊢ ∼□⊥

Equations

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

source

theorem LO.System.goedel2'! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasAxiomL 𝓢] :

𝓢 ⊢! ∼□⊥ ↔ 𝓢 ⊢! ∼□(∼□⊥)

source

def LO.System.axiomH {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomH 𝓢] :

𝓢 ⊢ □(□p ⭤ p) ➝ □p

Equations

LO.System.axiomH = LO.System.HasAxiomH.H p

source

@[simp]

theorem LO.System.axiomH! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomH 𝓢] :

𝓢 ⊢! □(□p ⭤ p) ➝ □p

source

instance LO.System.instHasAxiomHFiniteContext {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomH 𝓢] (Γ : LO.System.FiniteContext F 𝓢) :

LO.System.HasAxiomH Γ

Equations

LO.System.instHasAxiomHFiniteContext Γ = { H := fun (x : F) => LO.System.FiniteContext.of LO.System.axiomH }

source

instance LO.System.instHasAxiomHContext {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomH 𝓢] (Γ : LO.System.Context F 𝓢) :

LO.System.HasAxiomH Γ

Equations

LO.System.instHasAxiomHContext Γ = { H := fun (x : F) => LO.System.Context.of LO.System.axiomH }

source

def LO.System.loeb {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [self : LO.System.LoebRule 𝓢] {p : F} :

𝓢 ⊢ □p ➝ p → 𝓢 ⊢ p

Alias of LO.System.LoebRule.loeb.

Equations

@LO.System.loeb = @LO.System.LoebRule.loeb

source

theorem LO.System.loeb! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.LoebRule 𝓢] :

𝓢 ⊢! □p ➝ p → 𝓢 ⊢! p

source

def LO.System.henkin {S : Type u_1} {F : Type u_2} [LO.LogicalConnective F] [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [self : LO.System.HenkinRule 𝓢] {p : F} :

𝓢 ⊢ □p ⭤ p → 𝓢 ⊢ p

Alias of LO.System.HenkinRule.henkin.

Equations

@LO.System.henkin = @LO.System.HenkinRule.henkin

source

theorem LO.System.henkin! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HenkinRule 𝓢] :

𝓢 ⊢! □p ⭤ p → 𝓢 ⊢! p

source

instance LO.System.instHasAxiomLOfK4Loeb {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasAxiomFour 𝓢] [LO.System.K4Loeb 𝓢] :

LO.System.HasAxiomL 𝓢

Equations

LO.System.instHasAxiomLOfK4Loeb = { L := fun (x : F) => LO.System.axiomL_of_K4Loeb }

source

instance LO.System.instLoebRuleOfHasAxiomFourOfHenkinRule {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasAxiomFour 𝓢] [LO.System.HenkinRule 𝓢] :

LO.System.LoebRule 𝓢

Equations

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

source

instance LO.System.instHenkinRuleOfHasAxiomFourOfHasAxiomH {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomFour 𝓢] [LO.System.HasAxiomH 𝓢] :

LO.System.HenkinRule 𝓢

Equations

LO.System.instHenkinRuleOfHasAxiomFourOfHasAxiomH = { henkin := fun {p : F} (h : 𝓢 ⊢ □p ⭤ p) => LO.System.and₁' h⨀(LO.System.axiomH⨀LO.System.nec h) }

source

instance LO.System.instHasAxiomHOfHasAxiomL {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasAxiomL 𝓢] :

LO.System.HasAxiomH 𝓢

Equations

LO.System.instHasAxiomHOfHasAxiomL = { H := fun (x : F) => LO.System.axiomH_of_GL }

source

def LO.System.unnec {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] {𝓢 : S} [self : LO.System.Unnecessitation 𝓢] {p : F} :

𝓢 ⊢ □p → 𝓢 ⊢ p

Alias of LO.System.Unnecessitation.unnec.

Equations

@LO.System.unnec = @LO.System.Unnecessitation.unnec

source

theorem LO.System.unnec! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Unnecessitation 𝓢] :

𝓢 ⊢! □p → 𝓢 ⊢! p

source

def LO.System.multiunnec {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Unnecessitation 𝓢] {n : ℕ} :

𝓢 ⊢ □^[n]p → 𝓢 ⊢ p

Equations

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

source

theorem LO.System.multiunnec! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Unnecessitation 𝓢] {n : ℕ} :

𝓢 ⊢! □^[n]p → 𝓢 ⊢! p

source

instance LO.System.instUnnecessitationOfHasAxiomT {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomT 𝓢] :

LO.System.Unnecessitation 𝓢

Equations

LO.System.instUnnecessitationOfHasAxiomT = { unnec := fun {p : F} (hp : 𝓢 ⊢ □p) => LO.System.axiomT⨀hp }

source

def LO.System.imply_boxdot_boxdot_of_imply_boxdot_plain {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasAxiomFour 𝓢] (h : 𝓢 ⊢ ⊡p ➝ q) :

𝓢 ⊢ ⊡p ➝ ⊡q

Equations

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

source

theorem LO.System.imply_boxdot_boxdot_of_imply_boxdot_plain! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasAxiomFour 𝓢] (h : 𝓢 ⊢! ⊡p ➝ q) :

𝓢 ⊢! ⊡p ➝ ⊡q

source

def LO.System.imply_boxdot_axiomT_of_imply_boxdot_boxdot {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] (h : 𝓢 ⊢ ⊡p ➝ ⊡q) :

𝓢 ⊢ ⊡p ➝ □q ➝ q

Equations

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

source

theorem LO.System.imply_boxdot_axiomT_of_imply_boxdot_boxdot! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] (h : 𝓢 ⊢! ⊡p ➝ ⊡q) :

𝓢 ⊢! ⊡p ➝ □q ➝ q

source

def LO.System.imply_box_box_of_imply_boxdot_axiomT {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasAxiomFour 𝓢] [LO.System.HasAxiomL 𝓢] (h : 𝓢 ⊢ ⊡p ➝ □q ➝ q) :

𝓢 ⊢ □p ➝ □q

Equations

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

source

theorem LO.System.imply_box_box_of_imply_boxdot_axiomT! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasAxiomFour 𝓢] [LO.System.HasAxiomL 𝓢] (h : 𝓢 ⊢! ⊡p ➝ □q ➝ q) :

𝓢 ⊢! □p ➝ □q

source

theorem LO.System.imply_box_box_of_imply_boxdot_plain! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasAxiomFour 𝓢] [LO.System.HasAxiomL 𝓢] (h : 𝓢 ⊢! ⊡p ➝ q) :

𝓢 ⊢! □p ➝ □q

source

def LO.System.axiomGrz {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomGrz 𝓢] :

𝓢 ⊢ □(□(p ➝ □p) ➝ p) ➝ p

Equations

LO.System.axiomGrz = LO.System.HasAxiomGrz.Grz p

source

@[simp]

theorem LO.System.axiomGrz! {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.HasAxiomGrz 𝓢] :

𝓢 ⊢! □(□(p ➝ □p) ➝ p) ➝ p

source

instance LO.System.instHasAxiomGrzFiniteContext {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomGrz 𝓢] (Γ : LO.System.FiniteContext F 𝓢) :

LO.System.HasAxiomGrz Γ

Equations

LO.System.instHasAxiomGrzFiniteContext Γ = { Grz := fun (x : F) => LO.System.FiniteContext.of LO.System.axiomGrz }

source

instance LO.System.instHasAxiomGrzContext {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.HasAxiomGrz 𝓢] (Γ : LO.System.Context F 𝓢) :

LO.System.HasAxiomGrz Γ

Equations

LO.System.instHasAxiomGrzContext Γ = { Grz := fun (x : F) => LO.System.Context.of LO.System.axiomGrz }

source

def LO.System.dhyp_imp {F : Type u_1} [LO.BasicModalLogicalConnective F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {r : F} {𝓢 : S} [LO.System.Classical 𝓢] (h : 𝓢 ⊢ p ➝ q) :

𝓢 ⊢ (r ➝ p) ➝ r ➝ q

Equations

LO.System.dhyp_imp h = LO.System.imply₂⨀LO.System.dhyp r h

source

def LO.System.ppq {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {q : F} {𝓢 : S} [LO.System.Classical 𝓢] (h : 𝓢 ⊢ p ➝ p ➝ q) :

𝓢 ⊢ p ➝ q

Equations

LO.System.ppq h = LO.System.FiniteContext.deduct' (let_fun this := LO.System.FiniteContext.of h; this⨀LO.System.FiniteContext.byAxm ⋯⨀LO.System.FiniteContext.byAxm ⋯)

source

noncomputable def LO.System.lemma_Grz₁ {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] :

𝓢 ⊢ □p ➝ □(□(p ⋏ (□p ➝ □□p) ➝ □(p ⋏ (□p ➝ □□p))) ➝ p ⋏ (□p ➝ □□p))

Equations

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

source

theorem LO.System.lemma_Grz₁! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] :

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

source

noncomputable def LO.System.lemma_Grz₂ {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasAxiomGrz 𝓢] :

𝓢 ⊢ □p ➝ p ⋏ (□p ➝ □□p)

Equations

LO.System.lemma_Grz₂ = LO.System.impTrans'' LO.System.lemma_Grz₁ LO.System.axiomGrz

source

noncomputable instance LO.System.instHasAxiomFour {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasAxiomGrz 𝓢] :

LO.System.HasAxiomFour 𝓢

Equations

LO.System.instHasAxiomFour = { Four := fun (x : F) => LO.System.Four_of_Grz }

source

noncomputable instance LO.System.instHasAxiomT {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasAxiomGrz 𝓢] :

LO.System.HasAxiomT 𝓢

Equations

LO.System.instHasAxiomT = { T := fun (x : F) => LO.System.T_of_Grz }

source

noncomputable def LO.System.boxdot_Grz_of_L {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasAxiomFour 𝓢] [LO.System.HasAxiomL 𝓢] :

𝓢 ⊢ ⊡(⊡(p ➝ ⊡p) ➝ p) ➝ p

Equations

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

source

@[simp]

theorem LO.System.boxdot_Grz_of_L! {F : Type u_1} [LO.BasicModalLogicalConnective F] [DecidableEq F] {S : Type u_2} [LO.System F S] {p : F} {𝓢 : S} [LO.System.Classical 𝓢] [LO.System.NegationEquiv 𝓢] [LO.System.Necessitation 𝓢] [LO.System.HasAxiomK 𝓢] [LO.System.HasAxiomFour 𝓢] [LO.System.HasAxiomL 𝓢] :

𝓢 ⊢! ⊡(⊡(p ➝ ⊡p) ➝ p) ➝ p

source

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

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

source

class LO.System.ModalDisjunctive {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] {S : Type u_2} [LO.System F S] (𝓢 : S) :

Prop

modal_disjunctive : ∀ {p q : F}, 𝓢 ⊢! □p ⋎ □q → 𝓢 ⊢! p ∨ 𝓢 ⊢! q

Instances

LO.Modal.instModalDisjunctiveFormulaHilbertGL

source

theorem LO.System.ModalDisjunctive.modal_disjunctive {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] {S : Type u_2} [LO.System F S] {𝓢 : S} [self : LO.System.ModalDisjunctive 𝓢] {p : F} {q : F} :

𝓢 ⊢! □p ⋎ □q → 𝓢 ⊢! p ∨ 𝓢 ⊢! q

source

theorem LO.System.Context.provable_iff_boxed {F : Type u_1} [LO.LogicalConnective F] [LO.Box F] {S : Type u_2} [LO.System F S] [DecidableEq F] {𝓢 : S} [LO.System.Minimal 𝓢] {X : Set F} {p : F} :

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