@[reducible, inline]

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

Equations

• FFL.Axioms.DNE φ = ∼∼φ 🡒 φ

@[reducible, inline]

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

Equations

• FFL.Axioms.LEM φ = φ ⋎ ∼φ

@[reducible, inline]

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

Equations

• FFL.Axioms.Peirce φ ψ = ((φ 🡒 ψ) 🡒 φ) 🡒 φ

@[reducible, inline]

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

Equations

• FFL.Axioms.ElimContra φ ψ = (∼ψ 🡒 ∼φ) 🡒 φ 🡒 ψ

class FFL.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 φ

@[simp]

theorem FFL.Entailment.dne {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ : F} [HasAxiomDNE 𝓢] : 𝓢 ⊢ ∼∼φ 🡒 φ

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

Equations

• FFL.Entailment.of_NN! b = FFL.Entailment.dne!⨀!b

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

@[instance_reducible]

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

Equations

• Γ.instHasAxiomDNE = { dne! := fun {φ : F} => FFL.Entailment.FiniteContext.of! FFL.Entailment.dne! }

@[instance_reducible]

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

Equations

• Γ.instHasAxiomDNE = { dne! := fun {φ : F} => FFL.Entailment.Context.of! FFL.Entailment.dne! }

class FFL.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 φ

@[simp]

theorem FFL.Entailment.lem {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ : F} [HasAxiomLEM 𝓢] : 𝓢 ⊢ φ ⋎ ∼φ

@[instance_reducible]

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

Equations

• Γ.instHasAxiomLEM = { lem! := fun {φ : F} => FFL.Entailment.FiniteContext.of! FFL.Entailment.lem! }

@[instance_reducible]

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

Equations

• Γ.instHasAxiomLEM = { lem! := fun {φ : F} => FFL.Entailment.Context.of! FFL.Entailment.lem! }

class FFL.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 φ ψ

@[simp]

theorem FFL.Entailment.peirce {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [LogicalNeutral F] [HasAxiomPeirce 𝓢] : 𝓢 ⊢ ((φ 🡒 ψ) 🡒 φ) 🡒 φ

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

class FFL.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 φ ψ

@[simp]

theorem FFL.Entailment.elim_contra {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [HasAxiomElimContra 𝓢] : 𝓢 ⊢ (∼ψ 🡒 ∼φ) 🡒 φ 🡒 ψ

class FFL.Entailment.Cl {F : Type u_3} [LogicalConnective F] [LogicalNeutral F] {S : Type u_4} [Entailment S F] (𝓢 : S) extends FFL.Entailment.Minimal 𝓢, FFL.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 φ

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

def FFL.Entailment.dn! {F : Type u_3} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ : F} [Entailment.Cl 𝓢] : 𝓢 ⊢! φ 🡘 ∼∼φ

Equations

• FFL.Entailment.dn! = FFL.Entailment.E!_intro FFL.Entailment.dni! FFL.Entailment.dne!

@[simp]

theorem FFL.Entailment.dn {F : Type u_3} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ : F} [Entailment.Cl 𝓢] : 𝓢 ⊢ φ 🡘 ∼∼φ

def FFL.Entailment.A!_of_ANNNN! {F : Type u_3} [LogicalConnective F] [LogicalNeutral 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.

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

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

Equations

• FFL.Entailment.CN!_of_CN!_left b = FFL.Entailment.C!_trans (FFL.Entailment.contra! b) FFL.Entailment.dne!

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

def FFL.Entailment.CCNCN'! {F : Type u_3} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] : 𝓢 ⊢! (∼φ 🡒 ψ) 🡒 ∼ψ 🡒 φ

Equations

• FFL.Entailment.CCNCN'! = FFL.Entailment.FiniteContext.deduct'! (FFL.Entailment.CN!_of_CN!_left FFL.Entailment.FiniteContext.id!)

@[simp]

theorem FFL.Entailment.CCNCN' {F : Type u_3} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] : 𝓢 ⊢ (∼φ 🡒 ψ) 🡒 ∼ψ 🡒 φ

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

Equations

• FFL.Entailment.C!_of_CNN! b = FFL.Entailment.C!_trans FFL.Entailment.dni! (FFL.Entailment.CN!_of_CN!_left b)

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

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

Equations

• FFL.Entailment.CCNNC! = FFL.Entailment.FiniteContext.deduct'! (FFL.Entailment.C!_of_CNN! FFL.Entailment.FiniteContext.id!)

@[simp]

theorem FFL.Entailment.CCNNC {F : Type u_3} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] : 𝓢 ⊢ (∼φ 🡒 ∼ψ) 🡒 ψ 🡒 φ

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

Equations

• FFL.Entailment.EN!_of_EN!_right h = FFL.Entailment.E!_intro (FFL.Entailment.CN!_of_CN!_left (FFL.Entailment.K!_right h)) (FFL.Entailment.CN!_of_CN!_right (FFL.Entailment.K!_left h))

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

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

Equations

• FFL.Entailment.EN!_of_EN!_left h = FFL.Entailment.E!_symm (FFL.Entailment.EN!_of_EN!_right (FFL.Entailment.E!_symm h))

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

def FFL.Entailment.ECCOO! {F : Type u_3} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ : F} [Entailment.Cl 𝓢] : 𝓢 ⊢! φ 🡘 ((φ 🡒 ⊥) 🡒 ⊥)

Equations

• FFL.Entailment.ECCOO! = FFL.Entailment.E!_trans FFL.Entailment.dn! FFL.Entailment.ENNCCOO!

theorem FFL.Entailment.ECCOO {F : Type u_3} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ : F} [Entailment.Cl 𝓢] : 𝓢 ⊢ φ 🡘 ((φ 🡒 ⊥) 🡒 ⊥)

def FFL.Entailment.CNKANN! {F : Type u_3} [LogicalConnective F] [LogicalNeutral 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.

@[simp]

theorem FFL.Entailment.CNKANN {F : Type u_3} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] : 𝓢 ⊢ ∼(φ ⋏ ψ) 🡒 ∼φ ⋎ ∼ψ

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

Equations

• FFL.Entailment.ANN!_of_NK! b = FFL.Entailment.CNKANN!⨀!b

theorem FFL.Entailment.ANN_of_NK {F : Type u_3} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] (b : 𝓢 ⊢ ∼(φ ⋏ ψ)) : 𝓢 ⊢ ∼φ ⋎ ∼ψ

def FFL.Entailment.AN!_of_C! {F : Type u_3} [LogicalConnective F] [LogicalNeutral 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.

theorem FFL.Entailment.AN_of_C {F : Type u_3} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] (d : 𝓢 ⊢ φ 🡒 ψ) : 𝓢 ⊢ ∼φ ⋎ ψ

def FFL.Entailment.CCAN! {F : Type u_3} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] : 𝓢 ⊢! (φ 🡒 ψ) 🡒 ∼φ ⋎ ψ

Equations

• FFL.Entailment.CCAN! = FFL.Entailment.FiniteContext.deduct'! (FFL.Entailment.AN!_of_C! (FFL.Entailment.FiniteContext.byAxm! ⋯))

theorem FFL.Entailment.CCAN {F : Type u_3} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] : 𝓢 ⊢ (φ 🡒 ψ) 🡒 ∼φ ⋎ ψ

@[instance_reducible]

instance FFL.Entailment.instHasAxiomEFQ {F : Type u_3} [LogicalConnective F] [LogicalNeutral 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.

@[instance_reducible]

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

Equations

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

@[instance_reducible]

instance FFL.Entailment.instHasAxiomElimContra {F : Type u_3} [LogicalConnective F] [LogicalNeutral 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.

@[instance_reducible]

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

Equations

• FFL.Entailment.instHasAxiomLEM = { lem! := fun {φ : F} => FFL.Entailment.A!_of_ANNNN! (FFL.Entailment.AN!_of_C! FFL.Entailment.dni!) }

theorem FFL.Entailment.CNC_of_C_of_CN {F : Type u_3} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ ξ : F} [Entailment.Cl 𝓢] (hpq : 𝓢 ⊢ φ 🡒 ψ) (hpnr : 𝓢 ⊢ φ 🡒 ∼ξ) : 𝓢 ⊢ φ 🡒 ∼(ψ 🡒 ξ)

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

Equations

• FFL.Entailment.of_A!_of_N! b d = FFL.Entailment.A!_cases (FFL.Entailment.C!_of_CNN! (FFL.Entailment.dhyp! d)) FFL.Entailment.C!_id b

theorem FFL.Entailment.of_A_of_N {F : Type u_3} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] (b : 𝓢 ⊢ φ ⋎ ψ) (d : 𝓢 ⊢ ∼φ) : 𝓢 ⊢ ψ

def FFL.Entailment.ECAN! {F : Type u_3} [LogicalConnective F] [LogicalNeutral 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.

theorem FFL.Entailment.ECAN {F : Type u_3} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] : 𝓢 ⊢ (φ 🡒 ψ) 🡘 ∼φ ⋎ ψ

@[simp]

theorem FFL.Entailment.CNDisj₂NConj₂ {F : Type u_3} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} [Entailment.Cl 𝓢] {Γ : List F} : 𝓢 ⊢ ∼⋁List.map (fun (x : F) => ∼x) Γ 🡒 ⋀Γ

theorem FFL.Entailment.CNFdisj₂NFconj₂ {F : Type u_3} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} [Entailment.Cl 𝓢] {Γ : Finset F} : 𝓢 ⊢ ∼(Finset.image (fun (x : F) => ∼x) Γ).disj 🡒 Γ.conj

theorem FFL.Entailment.provable_iff_inconsistent_adjoin {F : Type u_3} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} [AdjunctiveSet F S] [Axiomatized S] [Deduction S] [(𝓢 : S) → Entailment.Cl 𝓢] {φ : F} : 𝓢 ⊢ φ ↔ Inconsistent (adjoin (∼φ) 𝓢)

theorem FFL.Entailment.unprovable_iff_consistent_adjoin {F : Type u_3} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} [AdjunctiveSet F S] [Axiomatized S] [Deduction S] [(𝓢 : S) → Entailment.Cl 𝓢] {φ : F} : 𝓢 ⊬ φ ↔ Consistent (adjoin (∼φ) 𝓢)

@[instance_reducible]

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

Equations

• FFL.Entailment.deductiveExplosion = inferInstance

@[instance_reducible]

instance FFL.Entailment.instHasAxiomPeirce {F : Type u_3} [LogicalConnective F] [LogicalNeutral 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.

@[instance_reducible]

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

Equations

• FFL.Entailment.instHasAxiomEFQ_1 = inferInstance

@[instance_reducible]

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

Equations

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

@[reducible, inline]

abbrev FFL.Entailment.Cl.ofEquiv {F : Type u_3} [LogicalConnective F] [LogicalNeutral F] {S : Type u_4} [Entailment S F] {G : Type u_5} {T : Type u_6} [Entailment T G] [LogicalConnective G] [LogicalNeutral 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.

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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