GL #

source

def LO.Entailment.goedel2 {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.GL 𝓢] :

𝓢 ⊢ ∼□⊥ <=> ∼□(∼□⊥)

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

source

theorem LO.Entailment.goedel2! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.GL 𝓢] :

𝓢 ⊢! ∼□⊥ <=> ∼□(∼□⊥)

source

def LO.Entailment.goedel2'.mp {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.GL 𝓢] :

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

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

source

def LO.Entailment.goedel2'.mpr {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.GL 𝓢] :

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

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

source

theorem LO.Entailment.goedel2'! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.GL 𝓢] :

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

source

def LO.Entailment.GL.axiomFour {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.GL 𝓢] {φ : F} :

𝓢 ⊢ Axioms.Four φ

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

source

@[implicit_reducible]

instance LO.Entailment.GL.instHasAxiomFour {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.GL 𝓢] :

HasAxiomFour 𝓢

Equations

LO.Entailment.GL.instHasAxiomFour = { Four := fun (x : F) => LO.Entailment.GL.axiomFour }

source

@[implicit_reducible]

instance LO.Entailment.GL.instK4 {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.GL 𝓢] :

Entailment.K4 𝓢

Equations

LO.Entailment.GL.instK4 = { toK := inst✝.toK, toHasAxiomFour := LO.Entailment.GL.instHasAxiomFour }

source

def LO.Entailment.GL.axiomH {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.GL 𝓢] {φ : F} :

𝓢 ⊢ Axioms.H φ

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.GL.axiomH = LO.Entailment.impTrans'' (LO.Entailment.implyBoxDistribute' LO.Entailment.and₁) LO.Entailment.axiomL

Instances For

source

@[implicit_reducible]

instance LO.Entailment.GL.instHasAxiomH {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.GL 𝓢] :

HasAxiomH 𝓢

Equations

LO.Entailment.GL.instHasAxiomH = { H := fun (x : F) => LO.Entailment.GL.axiomH }

source

noncomputable def LO.Entailment.boxdotGrzOfL {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.GL 𝓢] {φ : F} :

𝓢 ⊢ ⊡(⊡(φ ==> ⊡φ) ==> φ) ==> φ

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

source

@[simp]

theorem LO.Entailment.boxdotGrzOfL! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.GL 𝓢] {φ : F} :

𝓢 ⊢! ⊡(⊡(φ ==> ⊡φ) ==> φ) ==> φ

source

def LO.Entailment.implyBoxdotBoxdotOfImplyBoxdotPlain {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.GL 𝓢] {φ ψ : F} (h : 𝓢 ⊢ ⊡φ ==> ψ) :

𝓢 ⊢ ⊡φ ==> ⊡ψ

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

source

theorem LO.Entailment.implyBoxdotBoxdotOfImplyBoxdotPlain! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.GL 𝓢] {φ ψ : F} (h : 𝓢 ⊢! ⊡φ ==> ψ) :

𝓢 ⊢! ⊡φ ==> ⊡ψ

source

def LO.Entailment.implyBoxdotAxiomTOfImplyBoxdotBoxdot {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.GL 𝓢] {φ ψ : F} (h : 𝓢 ⊢ ⊡φ ==> ⊡ψ) :

𝓢 ⊢ ⊡φ ==> □ψ ==> ψ

Imported declaration from the Incompleteness formalization.

Equations

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

Instances For

source

theorem LO.Entailment.implyBoxdotAxiomTOfImplyBoxdotBoxdot! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.GL 𝓢] {φ ψ : F} (h : 𝓢 ⊢! ⊡φ ==> ⊡ψ) :

𝓢 ⊢! ⊡φ ==> □ψ ==> ψ

source

def LO.Entailment.implyBoxBoxOfImplyBoxdotAxiomT {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.GL 𝓢] {φ ψ : F} (h : 𝓢 ⊢ ⊡φ ==> □ψ ==> ψ) :

𝓢 ⊢ □φ ==> □ψ

Imported declaration from the Incompleteness formalization.

Equations

LO.Entailment.implyBoxBoxOfImplyBoxdotAxiomT h = LO.Entailment.impTrans'' LO.Entailment.implyBoxBoxBoxdot (LO.Entailment.impTrans'' (LO.Entailment.implyBoxDistribute' h) LO.Entailment.axiomL)

Instances For

source

theorem LO.Entailment.implyBoxBoxOfImplyBoxdotAxiomT! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.GL 𝓢] {φ ψ : F} (h : 𝓢 ⊢! ⊡φ ==> □ψ ==> ψ) :

𝓢 ⊢! □φ ==> □ψ

source

theorem LO.Entailment.imply_box_box_of_imply_boxdot_plain! {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.GL 𝓢] {φ ψ : F} (h : 𝓢 ⊢! ⊡φ ==> ψ) :

𝓢 ⊢! □φ ==> □ψ

Documentation

LeanPool.Incompleteness.Foundation.Modal.Entailment.GL

GL #