Foundation.Modal.Hilbert.Equiv.GL

source

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

Type (max u_2 u_3)

mdp {φ ψ : F} : 𝓢 ⊢ φ ➝ ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
neg_equiv (φ : F) : 𝓢 ⊢ Axioms.NegEquiv φ
verum : 𝓢 ⊢ Axioms.Verum
imply₁ (φ ψ : F) : 𝓢 ⊢ Axioms.Imply₁ φ ψ
imply₂ (φ ψ χ : F) : 𝓢 ⊢ Axioms.Imply₂ φ ψ χ
and₁ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₁ φ ψ
and₂ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₂ φ ψ
and₃ (φ ψ : F) : 𝓢 ⊢ Axioms.AndInst φ ψ
or₁ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₁ φ ψ
or₂ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₂ φ ψ
or₃ (φ ψ χ : F) : 𝓢 ⊢ Axioms.OrElim φ ψ χ
dne (φ : F) : 𝓢 ⊢ Axioms.DNE φ
nec {φ : F} : 𝓢 ⊢ φ → 𝓢 ⊢ □φ
K (φ ψ : F) : 𝓢 ⊢ Axioms.K φ ψ
dia_dual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
Four (φ : F) : 𝓢 ⊢ Axioms.Four φ
loeb {φ : F} : 𝓢 ⊢ □φ ➝ φ → 𝓢 ⊢ φ

Instances

LO.Modal.Hilbert.instK4LoebFormulaK4Loeb

source

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

𝓢 ⊢ Axioms.L φ

Equations

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

source

instance LO.System.K4Loeb.instHasAxiomL {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.K4Loeb 𝓢] :

HasAxiomL 𝓢

Equations

LO.System.K4Loeb.instHasAxiomL = { L := fun (x : F) => LO.System.K4Loeb.axiomL }

source

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

Type (max u_2 u_3)

mdp {φ ψ : F} : 𝓢 ⊢ φ ➝ ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
neg_equiv (φ : F) : 𝓢 ⊢ Axioms.NegEquiv φ
verum : 𝓢 ⊢ Axioms.Verum
imply₁ (φ ψ : F) : 𝓢 ⊢ Axioms.Imply₁ φ ψ
imply₂ (φ ψ χ : F) : 𝓢 ⊢ Axioms.Imply₂ φ ψ χ
and₁ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₁ φ ψ
and₂ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₂ φ ψ
and₃ (φ ψ : F) : 𝓢 ⊢ Axioms.AndInst φ ψ
or₁ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₁ φ ψ
or₂ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₂ φ ψ
or₃ (φ ψ χ : F) : 𝓢 ⊢ Axioms.OrElim φ ψ χ
dne (φ : F) : 𝓢 ⊢ Axioms.DNE φ
nec {φ : F} : 𝓢 ⊢ φ → 𝓢 ⊢ □φ
K (φ ψ : F) : 𝓢 ⊢ Axioms.K φ ψ
dia_dual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
Four (φ : F) : 𝓢 ⊢ Axioms.Four φ
henkin {φ : F} : 𝓢 ⊢ □φ ⭤ φ → 𝓢 ⊢ φ

Instances

LO.Modal.Hilbert.instK4HenkinFormulaK4Henkin

source

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

LoebRule 𝓢

Equations

LO.System.K4Henkin.instLoebRule = { loeb := fun {φ : F} (h : 𝓢 ⊢ □φ ➝ φ) => h⨀LO.System.henkin (LO.System.iffIntro (LO.System.axiomK' (LO.System.nec h)) LO.System.axiomFour) }

source

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

Type (max u_2 u_3)

mdp {φ ψ : F} : 𝓢 ⊢ φ ➝ ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
neg_equiv (φ : F) : 𝓢 ⊢ Axioms.NegEquiv φ
verum : 𝓢 ⊢ Axioms.Verum
imply₁ (φ ψ : F) : 𝓢 ⊢ Axioms.Imply₁ φ ψ
imply₂ (φ ψ χ : F) : 𝓢 ⊢ Axioms.Imply₂ φ ψ χ
and₁ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₁ φ ψ
and₂ (φ ψ : F) : 𝓢 ⊢ Axioms.AndElim₂ φ ψ
and₃ (φ ψ : F) : 𝓢 ⊢ Axioms.AndInst φ ψ
or₁ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₁ φ ψ
or₂ (φ ψ : F) : 𝓢 ⊢ Axioms.OrInst₂ φ ψ
or₃ (φ ψ χ : F) : 𝓢 ⊢ Axioms.OrElim φ ψ χ
dne (φ : F) : 𝓢 ⊢ Axioms.DNE φ
nec {φ : F} : 𝓢 ⊢ φ → 𝓢 ⊢ □φ
K (φ ψ : F) : 𝓢 ⊢ Axioms.K φ ψ
dia_dual (φ : F) : 𝓢 ⊢ Axioms.DiaDuality φ
Four (φ : F) : 𝓢 ⊢ Axioms.Four φ
H (φ : F) : 𝓢 ⊢ Axioms.H φ

Instances

LO.Modal.Hilbert.instK4HFormulaK4H

source

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

HenkinRule 𝓢

Equations

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

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.K4H (α : Type u_1) :

Hilbert α

Equations

LO.Modal.Hilbert.K4H α = LO.Modal.Hilbert.ExtK (𝟰 ∪ 𝗛)

source

instance LO.Modal.Hilbert.instK4HFormulaK4H {α : Type u_1} :

System.K4H (Hilbert.K4H α)

Equations

LO.Modal.Hilbert.instK4HFormulaK4H = LO.System.K4H.mk

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.K4Loeb (α : Type u_1) :

Hilbert α

Equations

LO.Modal.Hilbert.K4Loeb α = { axioms := 𝗞 ∪ 𝟰, rules := ⟮Nec⟯ ∪ ⟮Loeb⟯ }

source

instance LO.Modal.Hilbert.instHasAxiomKK4Loeb {α : Type u_1} :

(Hilbert.K4Loeb α).HasAxiomK

source

instance LO.Modal.Hilbert.instHasNecessitationK4Loeb {α : Type u_1} :

(Hilbert.K4Loeb α).HasNecessitation

source

instance LO.Modal.Hilbert.instHasLoebRuleK4Loeb {α : Type u_1} :

(Hilbert.K4Loeb α).HasLoebRule

source

instance LO.Modal.Hilbert.instK4LoebFormulaK4Loeb {α : Type u_1} :

System.K4Loeb (Hilbert.K4Loeb α)

Equations

LO.Modal.Hilbert.instK4LoebFormulaK4Loeb = LO.System.K4Loeb.mk

source

@[reducible, inline]

abbrev LO.Modal.Hilbert.K4Henkin (α : Type u_1) :

Hilbert α

Equations

LO.Modal.Hilbert.K4Henkin α = { axioms := 𝗞 ∪ 𝟰, rules := ⟮Nec⟯ ∪ ⟮Henkin⟯ }

source

instance LO.Modal.Hilbert.instHasAxiomKK4Henkin {α : Type u_1} :

(Hilbert.K4Henkin α).HasAxiomK

source

instance LO.Modal.Hilbert.instHasNecessitationK4Henkin {α : Type u_1} :

(Hilbert.K4Henkin α).HasNecessitation

source

instance LO.Modal.Hilbert.instHasHenkinRuleK4Henkin {α : Type u_1} :

(Hilbert.K4Henkin α).HasHenkinRule

source

instance LO.Modal.Hilbert.instK4HenkinFormulaK4Henkin {α : Type u_1} :

System.K4Henkin (Hilbert.K4Henkin α)

Equations

LO.Modal.Hilbert.instK4HenkinFormulaK4Henkin = LO.System.K4Henkin.mk

source

theorem LO.Modal.Hilbert.GL_weakerThan_K4Loeb {α : Type u_1} [DecidableEq α] :

Hilbert.GL α ≤ₛ Hilbert.K4Loeb α

source

theorem LO.Modal.Hilbert.K4Loeb_weakerThan_K4Henkin {α : Type u_1} [DecidableEq α] :

Hilbert.K4Loeb α ≤ₛ Hilbert.K4Henkin α

source

theorem LO.Modal.Hilbert.K4Henkin_weakerThan_K4H {α : Type u_1} [DecidableEq α] :

Hilbert.K4Henkin α ≤ₛ Hilbert.K4H α

source

theorem LO.Modal.Hilbert.K4Henkin_weakerThan_GL {α : Type u_1} [DecidableEq α] :

Hilbert.K4H α ≤ₛ Hilbert.GL α

source

theorem LO.Modal.Hilbert.GL_equiv_K4Loeb {α : Type u_1} [DecidableEq α] :

Hilbert.GL α =ₛ Hilbert.K4Loeb α