Supporting results for pointwise provable equality.

@[reducible, inline]

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

The DNE construction in FFL.Axioms.

Equations

• PointwiseComposition.FFL.Axioms.DNE φ = ∼∼φ ⇒ₗ φ

@[reducible, inline]

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

The LEM construction in FFL.Axioms.

Equations

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

@[reducible, inline]

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

The Peirce construction in FFL.Axioms.

Equations

• PointwiseComposition.FFL.Axioms.Peirce φ ψ = ((φ ⇒ₗ ψ) ⇒ₗ φ) ⇒ₗ φ

@[reducible, inline]

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

The Elim Contra construction in FFL.Axioms.

Equations

• PointwiseComposition.FFL.Axioms.ElimContra φ ψ = (∼ψ ⇒ₗ ∼φ) ⇒ₗ φ ⇒ₗ ψ

class PointwiseComposition.FFL.Entailment.HasAxiomDNE {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] (𝓢 : S) : Type (max u_2 u_3)

Proofs of double-negation elimination in the given proof system.

• dneProof {φ : F} : 𝓢 ⊢! Axioms.DNE φ

  The dne! construction in FFL.Entailment.

@[simp]

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

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

The of NN! construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.ofNNProof b = PointwiseComposition.FFL.Entailment.dneProof⨀!b

theorem PointwiseComposition.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 PointwiseComposition.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 = { dneProof := fun {φ : F} => PointwiseComposition.FFL.Entailment.FiniteContext.ofProof PointwiseComposition.FFL.Entailment.dneProof }

@[instance_reducible]

instance PointwiseComposition.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 = { dneProof := fun {φ : F} => PointwiseComposition.FFL.Entailment.Context.ofProof PointwiseComposition.FFL.Entailment.dneProof }

class PointwiseComposition.FFL.Entailment.HasAxiomLEM {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] (𝓢 : S) : Type (max u_2 u_3)

Proofs of excluded middle in the given proof system.

• lemProof {φ : F} : 𝓢 ⊢! Axioms.LEM φ

  The lem! construction in FFL.Entailment.

@[simp]

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

@[instance_reducible]

instance PointwiseComposition.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 = { lemProof := fun {φ : F} => PointwiseComposition.FFL.Entailment.FiniteContext.ofProof PointwiseComposition.FFL.Entailment.lemProof }

@[instance_reducible]

instance PointwiseComposition.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 = { lemProof := fun {φ : F} => PointwiseComposition.FFL.Entailment.Context.ofProof PointwiseComposition.FFL.Entailment.lemProof }

class PointwiseComposition.FFL.Entailment.HasAxiomPeirce {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] (𝓢 : S) : Type (max u_2 u_3)

Proofs of Peirce's law in the given proof system.

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

  The peirce! construction in FFL.Entailment.

@[simp]

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

@[instance_reducible]

instance PointwiseComposition.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 = { peirceProof := fun {φ ψ : F} => PointwiseComposition.FFL.Entailment.FiniteContext.ofProof PointwiseComposition.FFL.Entailment.peirceProof }

@[instance_reducible]

instance PointwiseComposition.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 = { peirceProof := fun {φ ψ : F} => PointwiseComposition.FFL.Entailment.Context.ofProof PointwiseComposition.FFL.Entailment.peirceProof }

class PointwiseComposition.FFL.Entailment.HasAxiomElimContra {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] (𝓢 : S) : Type (max u_2 u_3)

Data and laws for Has Axiom Elim Contra in FFL.Entailment.

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

  The elim Contra! construction in FFL.Entailment.

@[simp]

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

class PointwiseComposition.FFL.Entailment.Cl {F : Type u_3} [LogicalConnective F] [LogicalNeutral F] {S : Type u_4} [Entailment S F] (𝓢 : S) extends PointwiseComposition.FFL.Entailment.Minimal 𝓢, PointwiseComposition.FFL.Entailment.HasAxiomDNE 𝓢 : Type (max u_3 u_5)

Data and laws for Cl in FFL.Entailment.

• mdpProof {φ ψ : F} : 𝓢 ⊢! φ ⇒ₗ ψ → 𝓢 ⊢! φ → 𝓢 ⊢! ψ
• negEquivProof {φ : F} : 𝓢 ⊢! Axioms.NegEquiv φ
• verumProof : 𝓢 ⊢! Axioms.Verum
• implyKProof {φ ψ : F} : 𝓢 ⊢! Axioms.ImplyK φ ψ
• implySProof {φ ψ χ : F} : 𝓢 ⊢! Axioms.ImplyS φ ψ χ
• and₁Proof {φ ψ : F} : 𝓢 ⊢! Axioms.AndElim₁ φ ψ
• and₂Proof {φ ψ : F} : 𝓢 ⊢! Axioms.AndElim₂ φ ψ
• and₃Proof {φ ψ : F} : 𝓢 ⊢! Axioms.AndInst φ ψ
• or₁Proof {φ ψ : F} : 𝓢 ⊢! Axioms.OrInst₁ φ ψ
• or₂Proof {φ ψ : F} : 𝓢 ⊢! Axioms.OrInst₂ φ ψ
• or₃Proof {φ ψ χ : F} : 𝓢 ⊢! Axioms.OrElim φ ψ χ
• dneProof {φ : F} : 𝓢 ⊢! Axioms.DNE φ

@[instance_reducible]

instance PointwiseComposition.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 PointwiseComposition.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 PointwiseComposition.FFL.Entailment.dnProof {F : Type u_3} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ : F} [Entailment.Cl 𝓢] : 𝓢 ⊢! φ ⇔ₗ ∼∼φ

The dn! construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.dnProof = PointwiseComposition.FFL.Entailment.EProofIntro PointwiseComposition.FFL.Entailment.dniProof PointwiseComposition.FFL.Entailment.dneProof

@[simp]

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

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

The A! of ANNNN! construction in FFL.Entailment.

Equations

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

theorem PointwiseComposition.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 PointwiseComposition.FFL.Entailment.CNProofOfCNProofLeft {F : Type u_3} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] (b : 𝓢 ⊢! ∼φ ⇒ₗ ψ) : 𝓢 ⊢! ∼ψ ⇒ₗ φ

The CN! of CN! left construction in FFL.Entailment.

Equations

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

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

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

The CCNCN'! construction in FFL.Entailment.

Equations

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

@[simp]

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

def PointwiseComposition.FFL.Entailment.CProofOfCNNProof {F : Type u_3} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] (b : 𝓢 ⊢! ∼φ ⇒ₗ ∼ψ) : 𝓢 ⊢! ψ ⇒ₗ φ

The C! of CNN! construction in FFL.Entailment.

Equations

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

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

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

The CCNNC! construction in FFL.Entailment.

Equations

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

@[simp]

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

def PointwiseComposition.FFL.Entailment.ENProofOfENProofRight {F : Type u_3} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] (h : 𝓢 ⊢! φ ⇔ₗ ∼ψ) : 𝓢 ⊢! ∼φ ⇔ₗ ψ

The EN! of EN! right construction in FFL.Entailment.

Equations

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

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

def PointwiseComposition.FFL.Entailment.ENProofOfENProofLeft {F : Type u_3} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] (h : 𝓢 ⊢! ∼φ ⇔ₗ ψ) : 𝓢 ⊢! φ ⇔ₗ ∼ψ

The EN! of EN! left construction in FFL.Entailment.

Equations

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

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

def PointwiseComposition.FFL.Entailment.ECCOOProof {F : Type u_3} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ : F} [Entailment.Cl 𝓢] : 𝓢 ⊢! φ ⇔ₗ ((φ ⇒ₗ ⊥) ⇒ₗ ⊥)

The ECCOO! construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.ECCOOProof = PointwiseComposition.FFL.Entailment.EProofTrans PointwiseComposition.FFL.Entailment.dnProof PointwiseComposition.FFL.Entailment.ENNCCOOProof

theorem PointwiseComposition.FFL.Entailment.ECCOO {F : Type u_3} [LogicalConnective F] [LogicalNeutral F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ : F} [Entailment.Cl 𝓢] : 𝓢 ⊢ φ ⇔ₗ ((φ ⇒ₗ ⊥) ⇒ₗ ⊥)

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

The CNKANN! construction in FFL.Entailment.

Equations

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

@[simp]

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

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

The ANN! of NK! construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.ANNProofOfNKProof b = PointwiseComposition.FFL.Entailment.CNKANNProof⨀!b

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

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

The AN! of C! construction in FFL.Entailment.

Equations

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

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

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

The CCAN! construction in FFL.Entailment.

Equations

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

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

@[instance_reducible]

instance PointwiseComposition.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 PointwiseComposition.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

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

@[instance_reducible]

instance PointwiseComposition.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 PointwiseComposition.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

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

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

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

The of A! of N! construction in FFL.Entailment.

Equations

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

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

def PointwiseComposition.FFL.Entailment.ECANProof {F : Type u_3} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] : 𝓢 ⊢! (φ ⇒ₗ ψ) ⇔ₗ ∼φ ⋎ ψ

The ECAN! construction in FFL.Entailment.

Equations

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

theorem PointwiseComposition.FFL.Entailment.ECAN {F : Type u_3} [LogicalConnective F] [LogicalNeutral F] {S : Type u_4} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Cl 𝓢] : 𝓢 ⊢ (φ ⇒ₗ ψ) ⇔ₗ ∼φ ⋎ ψ

@[simp]

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

theorem PointwiseComposition.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.disj (Finset.image (fun (x : F) => ∼x) Γ) ⇒ₗ Finset.conj Γ

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

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

• PointwiseComposition.FFL.Entailment.deductiveExplosion = inferInstance

@[instance_reducible]

instance PointwiseComposition.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 PointwiseComposition.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

• PointwiseComposition.FFL.Entailment.instHasAxiomEFQ_1 = inferInstance

@[instance_reducible]

instance PointwiseComposition.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

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

@[reducible, inline]

abbrev PointwiseComposition.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 𝓣

The of Equiv construction in FFL.Entailment.Cl.

Equations

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

@[instance_reducible]

instance PointwiseComposition.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 PointwiseComposition.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

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