Foundation.Propositional.Entailment.Cl

source

@[reducible, inline]

abbrev LO.Axioms.DNE {F : Type u_1} [LogicalConnective F] (φ : F) :

Equations

LO.Axioms.DNE φ = ∼∼φ 🡒 φ

Instances For

source

@[reducible, inline]

abbrev LO.Axioms.LEM {F : Type u_1} [LogicalConnective F] (φ : F) :

Equations

LO.Axioms.LEM φ = φ ⋎ ∼φ

Instances For

source

@[reducible, inline]

abbrev LO.Axioms.Peirce {F : Type u_1} [LogicalConnective F] (φ ψ : F) :

Equations

LO.Axioms.Peirce φ ψ = ((φ 🡒 ψ) 🡒 φ) 🡒 φ

Instances For

source

@[reducible, inline]

abbrev LO.Axioms.ElimContra {F : Type u_1} [LogicalConnective F] (φ ψ : F) :

Equations

LO.Axioms.ElimContra φ ψ = (∼ψ 🡒 ∼φ) 🡒 φ 🡒 ψ

Instances For

source

class LO.Entailment.HasAxiomDNE {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] (𝓢 : S) :

Type (max u_2 u_3)

dne {φ : F} : 𝓢 ⊢! Axioms.DNE φ

Instances

source

@[simp]

theorem LO.Entailment.dne! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ : F} [HasAxiomDNE 𝓢] :

𝓢 ⊢ ∼∼φ 🡒 φ

source

def LO.Entailment.of_NN {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ : F} [ModusPonens 𝓢] [HasAxiomDNE 𝓢] (b : 𝓢 ⊢! ∼∼φ) :

𝓢 ⊢! φ

Equations

LO.Entailment.of_NN b = LO.Entailment.dne ⨀!b

Instances For

source

theorem LO.Entailment.of_NN! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ : F} [ModusPonens 𝓢] [HasAxiomDNE 𝓢] (h : 𝓢 ⊢ ∼∼φ) :

𝓢 ⊢ φ

source

@[implicit_reducible]

instance LO.Entailment.FiniteContext.instHasAxiomDNE {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [HasAxiomDNE 𝓢] (Γ : FiniteContext F 𝓢) :

HasAxiomDNE Γ

Equations

Γ.instHasAxiomDNE = { dne := fun {φ : F} => LO.Entailment.FiniteContext.of LO.Entailment.dne }

source

@[implicit_reducible]

instance LO.Entailment.Context.instHasAxiomDNE {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [HasAxiomDNE 𝓢] (Γ : Context F 𝓢) :

HasAxiomDNE Γ

Equations

Γ.instHasAxiomDNE = { dne := fun {φ : F} => LO.Entailment.Context.of LO.Entailment.dne }

source

class LO.Entailment.HasAxiomLEM {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] (𝓢 : S) :

Type (max u_2 u_3)

lem {φ : F} : 𝓢 ⊢! Axioms.LEM φ

Instances

source

@[simp]

theorem LO.Entailment.lem! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ : F} [HasAxiomLEM 𝓢] :

𝓢 ⊢ φ ⋎ ∼φ

source

@[implicit_reducible]

instance LO.Entailment.FiniteContext.instHasAxiomLEM {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [HasAxiomLEM 𝓢] (Γ : FiniteContext F 𝓢) :

HasAxiomLEM Γ

Equations

Γ.instHasAxiomLEM = { lem := fun {φ : F} => LO.Entailment.FiniteContext.of LO.Entailment.lem }

source

@[implicit_reducible]

instance LO.Entailment.Context.instHasAxiomLEM {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [HasAxiomLEM 𝓢] (Γ : Context F 𝓢) :

HasAxiomLEM Γ

Equations

Γ.instHasAxiomLEM = { lem := fun {φ : F} => LO.Entailment.Context.of LO.Entailment.lem }

source

class LO.Entailment.HasAxiomPeirce {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] (𝓢 : S) :

Type (max u_2 u_3)

peirce {φ ψ : F} : 𝓢 ⊢! Axioms.Peirce φ ψ

Instances

source

@[simp]

theorem LO.Entailment.peirce! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [HasAxiomPeirce 𝓢] :

𝓢 ⊢ ((φ 🡒 ψ) 🡒 φ) 🡒 φ

source

@[implicit_reducible]

instance LO.Entailment.FiniteContext.instHasAxiomPeirce {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [HasAxiomPeirce 𝓢] (Γ : FiniteContext F 𝓢) :

HasAxiomPeirce Γ

Equations

Γ.instHasAxiomPeirce = { peirce := fun {φ ψ : F} => LO.Entailment.FiniteContext.of LO.Entailment.peirce }

source

@[implicit_reducible]

instance LO.Entailment.Context.instHasAxiomPeirce {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [HasAxiomPeirce 𝓢] (Γ : Context F 𝓢) :

HasAxiomPeirce Γ

Equations

Γ.instHasAxiomPeirce = { peirce := fun {φ ψ : F} => LO.Entailment.Context.of LO.Entailment.peirce }

source

class LO.Entailment.HasAxiomElimContra {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] (𝓢 : S) :

Type (max u_2 u_3)

elimContra {φ ψ : F} : 𝓢 ⊢! Axioms.ElimContra φ ψ

Instances

source

@[simp]

theorem LO.Entailment.elim_contra! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [HasAxiomElimContra 𝓢] :

𝓢 ⊢ (∼ψ 🡒 ∼φ) 🡒 φ 🡒 ψ

source

class LO.Entailment.Cl {F : Type u_3} [LogicalConnective F] {S : Type u_4} [Entailment S F] (𝓢 : S) extends LO.Entailment.Minimal 𝓢, LO.Entailment.HasAxiomDNE 𝓢 :

Type (max u_3 u_5)

mdp {φ ψ : F} : 𝓢 ⊢! φ 🡒 ψ → 𝓢 ⊢! φ → 𝓢 ⊢! ψ
negEquiv {φ : F} : 𝓢 ⊢! Axioms.NegEquiv φ
verum : 𝓢 ⊢! Axioms.Verum
implyK {φ ψ : F} : 𝓢 ⊢! Axioms.ImplyK φ ψ
implyS {φ ψ χ : F} : 𝓢 ⊢! Axioms.ImplyS φ ψ χ
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 φ

Instances

source

@[implicit_reducible]

instance LO.Entailment.FiniteContext.instCl {F : Type u_3} [LogicalConnective F] {S : Type u_4} [Entailment S F] {𝓢 : S} [Entailment.Cl 𝓢] (Γ : FiniteContext F 𝓢) :

Entailment.Cl Γ

Equations

Γ.instCl = { toMinimal := Γ.instMinimal, toHasAxiomDNE := Γ.instHasAxiomDNE }

source

@[implicit_reducible]

instance LO.Entailment.Context.instCl {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} [Entailment.Cl 𝓢] (Γ : Context F 𝓢) :

Entailment.Cl Γ

Equations

Γ.instCl = { toMinimal := Γ.minimal, toHasAxiomDNE := Γ.instHasAxiomDNE }

source

def LO.Entailment.dn {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ : F} [Entailment.Cl 𝓢] :

𝓢 ⊢! φ 🡘 ∼∼φ

Equations

LO.Entailment.dn = LO.Entailment.E_intro LO.Entailment.dni LO.Entailment.dne

Instances For

source

@[simp]

theorem LO.Entailment.dn! {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ : F} [Entailment.Cl 𝓢] :

𝓢 ⊢ φ 🡘 ∼∼φ

source

def LO.Entailment.A_of_ANNNN {F : Type u_3} [LogicalConnective F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] (d : 𝓢 ⊢! ∼∼φ ⋎ ∼∼ψ) :

𝓢 ⊢! φ ⋎ ψ

Equations

LO.Entailment.A_of_ANNNN d = LO.Entailment.of_C_of_C_of_A (LO.Entailment.C_trans LO.Entailment.dne LO.Entailment.or₁) (LO.Entailment.C_trans LO.Entailment.dne LO.Entailment.or₂) d

Instances For

source

theorem LO.Entailment.A!_of_ANNNN! {F : Type u_3} [LogicalConnective F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] (d : 𝓢 ⊢ ∼∼φ ⋎ ∼∼ψ) :

𝓢 ⊢ φ ⋎ ψ

source

def LO.Entailment.CN_of_CN_left {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] (b : 𝓢 ⊢! ∼φ 🡒 ψ) :

𝓢 ⊢! ∼ψ 🡒 φ

Equations

LO.Entailment.CN_of_CN_left b = LO.Entailment.C_trans (LO.Entailment.contra b) LO.Entailment.dne

Instances For

source

theorem LO.Entailment.CN!_of_CN!_left {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] (b : 𝓢 ⊢ ∼φ 🡒 ψ) :

𝓢 ⊢ ∼ψ 🡒 φ

source

def LO.Entailment.CCNCN' {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] :

𝓢 ⊢! (∼φ 🡒 ψ) 🡒 ∼ψ 🡒 φ

Equations

LO.Entailment.CCNCN' = LO.Entailment.FiniteContext.deduct' (LO.Entailment.CN_of_CN_left LO.Entailment.FiniteContext.id)

Instances For

source

@[simp]

theorem LO.Entailment.CCNCN'! {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] :

𝓢 ⊢ (∼φ 🡒 ψ) 🡒 ∼ψ 🡒 φ

source

def LO.Entailment.C_of_CNN {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] (b : 𝓢 ⊢! ∼φ 🡒 ∼ψ) :

𝓢 ⊢! ψ 🡒 φ

Equations

LO.Entailment.C_of_CNN b = LO.Entailment.C_trans LO.Entailment.dni (LO.Entailment.CN_of_CN_left b)

Instances For

source

theorem LO.Entailment.C!_of_CNN! {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] (b : 𝓢 ⊢ ∼φ 🡒 ∼ψ) :

𝓢 ⊢ ψ 🡒 φ

source

def LO.Entailment.CCNNC {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] :

𝓢 ⊢! (∼φ 🡒 ∼ψ) 🡒 ψ 🡒 φ

Equations

LO.Entailment.CCNNC = LO.Entailment.FiniteContext.deduct' (LO.Entailment.C_of_CNN LO.Entailment.FiniteContext.id)

Instances For

source

@[simp]

theorem LO.Entailment.CCNNC! {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] :

𝓢 ⊢ (∼φ 🡒 ∼ψ) 🡒 ψ 🡒 φ

source

def LO.Entailment.EN_of_EN_right {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] (h : 𝓢 ⊢! φ 🡘 ∼ψ) :

𝓢 ⊢! ∼φ 🡘 ψ

Equations

LO.Entailment.EN_of_EN_right h = LO.Entailment.E_intro (LO.Entailment.CN_of_CN_left (LO.Entailment.K_right h)) (LO.Entailment.CN_of_CN_right (LO.Entailment.K_left h))

Instances For

source

theorem LO.Entailment.EN!_of_EN!_right {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] (h : 𝓢 ⊢ φ 🡘 ∼ψ) :

𝓢 ⊢ ∼φ 🡘 ψ

source

def LO.Entailment.EN_of_EN_left {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] (h : 𝓢 ⊢! ∼φ 🡘 ψ) :

𝓢 ⊢! φ 🡘 ∼ψ

Equations

LO.Entailment.EN_of_EN_left h = LO.Entailment.E_symm (LO.Entailment.EN_of_EN_right (LO.Entailment.E_symm h))

Instances For

source

theorem LO.Entailment.EN!_of_EN!_left {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] (h : 𝓢 ⊢ ∼φ 🡘 ψ) :

𝓢 ⊢ φ 🡘 ∼ψ

source

def LO.Entailment.ECCOO {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ : F} [Entailment.Cl 𝓢] :

𝓢 ⊢! φ 🡘 ((φ 🡒 ⊥) 🡒 ⊥)

Equations

LO.Entailment.ECCOO = LO.Entailment.E_trans LO.Entailment.dn LO.Entailment.ENNCCOO

Instances For

source

theorem LO.Entailment.ECCOO! {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ : F} [Entailment.Cl 𝓢] :

𝓢 ⊢ φ 🡘 ((φ 🡒 ⊥) 🡒 ⊥)

source

def LO.Entailment.CNKANN {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] :

𝓢 ⊢! ∼(φ ⋏ ψ) 🡒 ∼φ ⋎ ∼ψ

Equations

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

Instances For

source

@[simp]

theorem LO.Entailment.CNKANN! {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] :

𝓢 ⊢ ∼(φ ⋏ ψ) 🡒 ∼φ ⋎ ∼ψ

source

def LO.Entailment.ANN_of_NK {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] (b : 𝓢 ⊢! ∼(φ ⋏ ψ)) :

𝓢 ⊢! ∼φ ⋎ ∼ψ

Equations

LO.Entailment.ANN_of_NK b = LO.Entailment.CNKANN ⨀!b

Instances For

source

theorem LO.Entailment.ANN!_of_NK! {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] (b : 𝓢 ⊢ ∼(φ ⋏ ψ)) :

𝓢 ⊢ ∼φ ⋎ ∼ψ

source

def LO.Entailment.AN_of_C {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] (d : 𝓢 ⊢! φ 🡒 ψ) :

𝓢 ⊢! ∼φ ⋎ ψ

Equations

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

Instances For

source

theorem LO.Entailment.AN!_of_C! {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] (d : 𝓢 ⊢ φ 🡒 ψ) :

𝓢 ⊢ ∼φ ⋎ ψ

source

def LO.Entailment.CCAN {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] :

𝓢 ⊢! (φ 🡒 ψ) 🡒 ∼φ ⋎ ψ

Equations

LO.Entailment.CCAN = LO.Entailment.FiniteContext.deduct' (LO.Entailment.AN_of_C (LO.Entailment.FiniteContext.byAxm ⋯))

Instances For

source

theorem LO.Entailment.CCAN! {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] :

𝓢 ⊢ (φ 🡒 ψ) 🡒 ∼φ ⋎ ψ

source

@[implicit_reducible]

instance LO.Entailment.instHasAxiomEFQ {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} [Entailment.Cl 𝓢] :

HasAxiomEFQ 𝓢

Equations

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

source

@[implicit_reducible]

instance LO.Entailment.instInt {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} [Entailment.Cl 𝓢] :

Entailment.Int 𝓢

Equations

LO.Entailment.instInt = { toMinimal := inst✝.toMinimal, toHasAxiomEFQ := LO.Entailment.instHasAxiomEFQ }

source

@[implicit_reducible]

instance LO.Entailment.instHasAxiomElimContra {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} [Entailment.Cl 𝓢] :

HasAxiomElimContra 𝓢

Equations

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

source

@[implicit_reducible]

instance LO.Entailment.instHasAxiomLEM {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} [Entailment.Cl 𝓢] :

HasAxiomLEM 𝓢

Equations

LO.Entailment.instHasAxiomLEM = { lem := fun {φ : F} => LO.Entailment.A_of_ANNNN (LO.Entailment.AN_of_C LO.Entailment.dni) }

source

theorem LO.Entailment.not_imply_prem''! {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ ξ : F} [Entailment.Cl 𝓢] (hpq : 𝓢 ⊢ φ 🡒 ψ) (hpnr : 𝓢 ⊢ φ 🡒 ∼ξ) :

𝓢 ⊢ φ 🡒 ∼(ψ 🡒 ξ)

source

def LO.Entailment.ofAOfN {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] (b : 𝓢 ⊢! φ ⋎ ψ) (d : 𝓢 ⊢! ∼φ) :

𝓢 ⊢! ψ

Equations

LO.Entailment.ofAOfN b d = LO.Entailment.A_cases (LO.Entailment.C_of_CNN (LO.Entailment.dhyp d)) LO.Entailment.C_id b

Instances For

source

def LO.Entailment.of_a!_of_n! {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] (b : 𝓢 ⊢ φ ⋎ ψ) (d : 𝓢 ⊢ ∼φ) :

𝓢 ⊢ ψ

Equations

⋯ = ⋯

Instances For

source

def LO.Entailment.ECAN {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] :

𝓢 ⊢! (φ 🡒 ψ) 🡘 ∼φ ⋎ ψ

Equations

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

Instances For

source

def LO.Entailment.ECAN! {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] :

𝓢 ⊢ (φ 🡒 ψ) 🡘 ∼φ ⋎ ψ

Equations

⋯ = ⋯

Instances For

source

@[simp]

theorem LO.Entailment.CNDisj₂NConj₂! {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} [Entailment.Cl 𝓢] {Γ : List F} :

𝓢 ⊢ ∼⋁List.map (fun (x : F) => ∼x) Γ 🡒 ⋀Γ

source

theorem LO.Entailment.CNFdisj₂NFconj₂! {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} [Entailment.Cl 𝓢] {Γ : Finset F} :

𝓢 ⊢ ∼(Finset.image (fun (x : F) => ∼x) Γ).disj 🡒 Γ.conj

source

theorem LO.Entailment.provable_iff_inconsistent_adjoin {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} [AdjunctiveSet F S] [Axiomatized S] [Deduction S] [(𝓢 : S) → Entailment.Cl 𝓢] {φ : F} :

𝓢 ⊢ φ ↔ Inconsistent (adjoin (∼φ) 𝓢)

source

theorem LO.Entailment.unprovable_iff_consistent_adjoin {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} [AdjunctiveSet F S] [Axiomatized S] [Deduction S] [(𝓢 : S) → Entailment.Cl 𝓢] {φ : F} :

𝓢 ⊬ φ ↔ Consistent (adjoin (∼φ) 𝓢)

source

@[implicit_reducible]

instance LO.Entailment.deductiveExplosion {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] [(𝓢 : S) → Entailment.Cl 𝓢] :

DeductiveExplosion S

Equations

LO.Entailment.deductiveExplosion = inferInstance

source

@[implicit_reducible]

instance LO.Entailment.instHasAxiomPeirce {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} [Entailment.Cl 𝓢] :

HasAxiomPeirce 𝓢

Equations

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

source

@[implicit_reducible]

instance LO.Entailment.instHasAxiomEFQ_1 {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} [Entailment.Cl 𝓢] :

HasAxiomEFQ 𝓢

Equations

LO.Entailment.instHasAxiomEFQ_1 = inferInstance

source

@[implicit_reducible]

instance LO.Entailment.instInt_1 {F : Type u_3} [LogicalConnective F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} [Entailment.Cl 𝓢] :

Entailment.Int 𝓢

Equations

LO.Entailment.instInt_1 = { toMinimal := inst✝.toMinimal, toHasAxiomEFQ := LO.Entailment.instHasAxiomEFQ_1 }

source

def LO.Entailment.Cl.ofEquiv {F : Type u_3} [LogicalConnective F] {S : Type u_4} [Entailment S F] {G : Type u_5} {T : Type u_6} [Entailment T G] [LogicalConnective G] (𝓢 : S) [Entailment.Cl 𝓢] (𝓣 : T) (f : G →ˡᶜ F) (e : (φ : G) → 𝓢 ⊢! f φ ≃ 𝓣 ⊢! φ) :

Entailment.Cl 𝓣

Equations

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

Instances For

source

@[implicit_reducible]

instance LO.Entailment.instHasAxiomDNEOfHasAxiomLEM {S : Type u_5} {F : Type u_6} [LogicalConnective F] [DecidableEq F] [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] [HasAxiomLEM 𝓢] :

HasAxiomDNE 𝓢

Equations

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

source

@[implicit_reducible]

instance LO.Entailment.instClOfHasAxiomLEM {S : Type u_5} {F : Type u_6} [LogicalConnective F] [DecidableEq F] [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] [HasAxiomLEM 𝓢] :

Entailment.Cl 𝓢

Equations

LO.Entailment.instClOfHasAxiomLEM = { toMinimal := inst✝¹.toMinimal, toHasAxiomDNE := LO.Entailment.instHasAxiomDNEOfHasAxiomLEM }