Supporting results for pointwise provable equality.

@[reducible, inline]

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

The EFQ construction in FFL.Axioms.

Equations

• PointwiseComposition.FFL.Axioms.EFQ φ = ⊥ ⇒ₗ φ

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

Data and laws for Has Axiom EFQ in FFL.Entailment.

• efqProof {φ : F} : 𝓢 ⊢! Axioms.EFQ φ

  The efq! construction in FFL.Entailment.

@[simp]

theorem PointwiseComposition.FFL.Entailment.efq {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] {𝓢 : S} {φ : F} [HasAxiomEFQ 𝓢] : 𝓢 ⊢ ⊥ ⇒ₗ φ

def PointwiseComposition.FFL.Entailment.ofOProof {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] {𝓢 : S} {φ : F} [ModusPonens 𝓢] [HasAxiomEFQ 𝓢] (b : 𝓢 ⊢! ⊥) : 𝓢 ⊢! φ

The of O! construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.ofOProof b = PointwiseComposition.FFL.Entailment.efqProof⨀!b

theorem PointwiseComposition.FFL.Entailment.of_O {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] {𝓢 : S} {φ : F} [ModusPonens 𝓢] [HasAxiomEFQ 𝓢] (h : 𝓢 ⊢ ⊥) : 𝓢 ⊢ φ

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.instDeductiveExplosionOfModusPonensOfHasAxiomEFQ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] [(𝓢 : S) → ModusPonens 𝓢] [(𝓢 : S) → HasAxiomEFQ 𝓢] : DeductiveExplosion S

Equations

• PointwiseComposition.FFL.Entailment.instDeductiveExplosionOfModusPonensOfHasAxiomEFQ = { dexp := fun {𝓢 : S} (b : 𝓢 ⊢! ⊥) (x : F) => PointwiseComposition.FFL.Entailment.efqProof⨀!b }

@[instance_reducible]

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

Equations

• Γ.instHasAxiomEFQ = { efqProof := fun {φ : F} => PointwiseComposition.FFL.Entailment.FiniteContext.ofProof PointwiseComposition.FFL.Entailment.efqProof }

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.FiniteContext.instDeductiveExplosionOfHasAxiomEFQ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [HasAxiomEFQ 𝓢] : DeductiveExplosion (FiniteContext F 𝓢)

Equations

• PointwiseComposition.FFL.Entailment.FiniteContext.instDeductiveExplosionOfHasAxiomEFQ = inferInstance

@[instance_reducible]

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

Equations

• Γ.instHasAxiomEFQ = { efqProof := fun {φ : F} => PointwiseComposition.FFL.Entailment.Context.ofProof PointwiseComposition.FFL.Entailment.efqProof }

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.Context.instDeductiveExplosionFiniteContextOfHasAxiomEFQ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [HasAxiomEFQ 𝓢] : DeductiveExplosion (FiniteContext F 𝓢)

Equations

• PointwiseComposition.FFL.Entailment.Context.instDeductiveExplosionFiniteContextOfHasAxiomEFQ = inferInstance

class PointwiseComposition.FFL.Entailment.Int {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] (𝓢 : S) extends PointwiseComposition.FFL.Entailment.Minimal 𝓢, PointwiseComposition.FFL.Entailment.HasAxiomEFQ 𝓢 : Type (max u_1 u_3)

Data and laws for Int 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 φ ψ χ
• efqProof {φ : F} : 𝓢 ⊢! Axioms.EFQ φ

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.FiniteContext.instInt {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] (Γ : FiniteContext F 𝓢) : Entailment.Int Γ

Equations

• Γ.instInt = { toMinimal := Γ.instMinimal, toHasAxiomEFQ := Γ.instHasAxiomEFQ }

@[instance_reducible]

instance PointwiseComposition.FFL.Entailment.Context.instInt {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] (Γ : Context F 𝓢) : Entailment.Int Γ

Equations

• Γ.instInt = { toMinimal := Γ.minimal, toHasAxiomEFQ := Γ.instHasAxiomEFQ }

def PointwiseComposition.FFL.Entailment.efqOfMemEitherProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} {Γ : List F} [Entailment.Int 𝓢] (h₁ : φ ∈ Γ) (h₂ : ∼φ ∈ Γ) : Γ ⊢[𝓢]! ψ

The efq of mem either! construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.efqOfMemEitherProof h₁ h₂ = PointwiseComposition.FFL.Entailment.ofOProof (PointwiseComposition.FFL.Entailment.botOfMemEitherProof h₁ h₂)

theorem PointwiseComposition.FFL.Entailment.efq_of_mem_either {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} {Γ : List F} [Entailment.Int 𝓢] (h₁ : φ ∈ Γ) (h₂ : ∼φ ∈ Γ) : Γ ⊢[𝓢] ψ

def PointwiseComposition.FFL.Entailment.CNCProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Int 𝓢] : 𝓢 ⊢! ∼φ ⇒ₗ φ ⇒ₗ ψ

The CNC! construction in FFL.Entailment.

Equations

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

@[simp]

theorem PointwiseComposition.FFL.Entailment.CNC {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Int 𝓢] : 𝓢 ⊢ ∼φ ⇒ₗ φ ⇒ₗ ψ

def PointwiseComposition.FFL.Entailment.CCNProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Int 𝓢] : 𝓢 ⊢! φ ⇒ₗ ∼φ ⇒ₗ ψ

The CCN! construction in FFL.Entailment.

Equations

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

@[simp]

theorem PointwiseComposition.FFL.Entailment.CCN {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Int 𝓢] : 𝓢 ⊢ φ ⇒ₗ ∼φ ⇒ₗ ψ

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

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

def PointwiseComposition.FFL.Entailment.CANCProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Int 𝓢] : 𝓢 ⊢! ∼φ ⋎ ψ ⇒ₗ φ ⇒ₗ ψ

The CANC! construction in FFL.Entailment.

Equations

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

@[simp]

theorem PointwiseComposition.FFL.Entailment.CANC {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Int 𝓢] : 𝓢 ⊢ ∼φ ⋎ ψ ⇒ₗ φ ⇒ₗ ψ

def PointwiseComposition.FFL.Entailment.CProofOfANProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Int 𝓢] (b : 𝓢 ⊢! ∼φ ⋎ ψ) : 𝓢 ⊢! φ ⇒ₗ ψ

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

Equations

• PointwiseComposition.FFL.Entailment.CProofOfANProof b = PointwiseComposition.FFL.Entailment.CANCProof⨀!b

theorem PointwiseComposition.FFL.Entailment.C_of_AN {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Int 𝓢] (b : 𝓢 ⊢ ∼φ ⋎ ψ) : 𝓢 ⊢ φ ⇒ₗ ψ

def PointwiseComposition.FFL.Entailment.CCNNNNNNCProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Int 𝓢] : 𝓢 ⊢! (∼∼φ ⇒ₗ ∼∼ψ) ⇒ₗ ∼∼(φ ⇒ₗ ψ)

The CCNNNNNNC! construction in FFL.Entailment.

Equations

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

@[simp]

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

def PointwiseComposition.FFL.Entailment.NNCProofOfCNNNNProof {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Int 𝓢] (b : 𝓢 ⊢! ∼∼φ ⇒ₗ ∼∼ψ) : 𝓢 ⊢! ∼∼(φ ⇒ₗ ψ)

The NNC! of CNNNN! construction in FFL.Entailment.

Equations

• PointwiseComposition.FFL.Entailment.NNCProofOfCNNNNProof b = PointwiseComposition.FFL.Entailment.CCNNNNNNCProof⨀!b

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

def PointwiseComposition.FFL.Entailment.leftDisjProofIntro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ : F} [Entailment.Int 𝓢] (Γ : List F) (b : (ψ : F) → ψ ∈ Γ → 𝓢 ⊢! ψ ⇒ₗ φ) : 𝓢 ⊢! List.disj Γ ⇒ₗ φ

The left Disj! intro construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FFL.Entailment.leftDisjProofIntro [] b_2 = PointwiseComposition.FFL.Entailment.efqProof

theorem PointwiseComposition.FFL.Entailment.left_Disj_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ : F} [Entailment.Int 𝓢] (Γ : List F) (b : ∀ ψ ∈ Γ, 𝓢 ⊢ ψ ⇒ₗ φ) : 𝓢 ⊢ List.disj Γ ⇒ₗ φ

def PointwiseComposition.FFL.Entailment.leftDisj₂ProofIntro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ : F} [Entailment.Int 𝓢] (Γ : List F) (b : (ψ : F) → ψ ∈ Γ → 𝓢 ⊢! ψ ⇒ₗ φ) : 𝓢 ⊢! ⋁Γ ⇒ₗ φ

The left Disj₂! intro construction in FFL.Entailment.

Equations

• One or more equations did not get rendered due to their size.
• PointwiseComposition.FFL.Entailment.leftDisj₂ProofIntro [] b_2 = PointwiseComposition.FFL.Entailment.efqProof
• PointwiseComposition.FFL.Entailment.leftDisj₂ProofIntro [ψ] b_2 = b_2 (⋁[ψ]) ⋯

theorem PointwiseComposition.FFL.Entailment.left_Disj₂_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ : F} [Entailment.Int 𝓢] (Γ : List F) (b : ∀ ψ ∈ Γ, 𝓢 ⊢ ψ ⇒ₗ φ) : 𝓢 ⊢ ⋁Γ ⇒ₗ φ

def PointwiseComposition.FFL.Entailment.leftDisj'ProofIntro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ : F} [Entailment.Int 𝓢] {ι : Type u_4} (l : List ι) (ψ : ι → F) (b : (i : ι) → i ∈ l → 𝓢 ⊢! ψ i ⇒ₗ φ) : 𝓢 ⊢! (fun (x : ι → F) => List.disj' x l) ψ ⇒ₗ φ

The left Disj'! intro construction in FFL.Entailment.

Equations

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

theorem PointwiseComposition.FFL.Entailment.left_Disj'_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ : F} [Entailment.Int 𝓢] {ι : Type u_3} (l : List ι) (ψ : ι → F) (b : ∀ i ∈ l, 𝓢 ⊢ ψ i ⇒ₗ φ) : 𝓢 ⊢ (fun (x : ι → F) => List.disj' x l) ψ ⇒ₗ φ

theorem PointwiseComposition.FFL.Entailment.left_Fdisj_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ : F} [Entailment.Int 𝓢] (s : Finset F) (b : ∀ ψ ∈ s, 𝓢 ⊢ ψ ⇒ₗ φ) : 𝓢 ⊢ Finset.disj s ⇒ₗ φ

theorem PointwiseComposition.FFL.Entailment.left_Fdisj'_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ : F} [Entailment.Int 𝓢] {ι : Type u_3} (s : Finset ι) (ψ : ι → F) (b : ∀ i ∈ s, 𝓢 ⊢ ψ i ⇒ₗ φ) : 𝓢 ⊢ (⋁ (i : ι) ∈ s, ψ i) ⇒ₗ φ

theorem PointwiseComposition.FFL.Entailment.left_Udisj_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ : F} [Entailment.Int 𝓢] {ι : Type u_3} [Fintype ι] (ψ : ι → F) (b : ∀ (i : ι), 𝓢 ⊢ ψ i ⇒ₗ φ) : 𝓢 ⊢ (⋁ (i : ι), ψ i) ⇒ₗ φ

theorem PointwiseComposition.FFL.Entailment.EDisj₂AppendADisj₂Disj₂ {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {Γ Δ : List F} [Entailment.Int 𝓢] : 𝓢 ⊢ ⋁(Γ ++ Δ) ⇔ₗ ⋁Γ ⋎ ⋁Δ

theorem PointwiseComposition.FFL.Entailment.Disj₂Append_iff_ADisj₂Disj₂ {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {Γ Δ : List F} [Entailment.Int 𝓢] : 𝓢 ⊢ ⋁(Γ ++ Δ) ↔ 𝓢 ⊢ ⋁Γ ⋎ ⋁Δ

theorem PointwiseComposition.FFL.Entailment.CDisj₂_iff_CADisj₂ {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} {Γ : List F} [Entailment.Int 𝓢] : 𝓢 ⊢ φ ⇒ₗ ⋁(ψ :: Γ) ↔ 𝓢 ⊢ φ ⇒ₗ ψ ⋎ ⋁Γ

@[simp]

theorem PointwiseComposition.FFL.Entailment.CDisj₂ADisj₂Remove {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ : F} {Γ : List F} [Entailment.Int 𝓢] : 𝓢 ⊢ ⋁Γ ⇒ₗ φ ⋎ ⋁(fun (x : F) => List.remove x Γ) φ

theorem PointwiseComposition.FFL.Entailment.left_Disj₂_intro' {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ : F} {Γ : List F} [Entailment.Int 𝓢] (hd : ∀ ψ ∈ Γ, ψ = φ) : 𝓢 ⊢ ⋁Γ ⇒ₗ φ

theorem PointwiseComposition.FFL.Entailment.of_Disj₂_of_mem_eq {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ : F} {Γ : List F} [Entailment.Int 𝓢] (hd : ∀ ψ ∈ Γ, ψ = φ) (h : 𝓢 ⊢ ⋁Γ) : 𝓢 ⊢ φ

@[simp]

theorem PointwiseComposition.FFL.Entailment.CDisj₂FDisj {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ : Finset F} : 𝓢 ⊢ ⋁Γ.toList ⇒ₗ Finset.disj Γ

@[simp]

theorem PointwiseComposition.FFL.Entailment.CFDisjDisj₂ {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ : Finset F} : 𝓢 ⊢ Finset.disj Γ ⇒ₗ ⋁Γ.toList

theorem PointwiseComposition.FFL.Entailment.CDisj₂Disj₂_of_subset {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ Δ : List F} (h : ∀ φ ∈ Γ, φ ∈ Δ) : 𝓢 ⊢ ⋁Γ ⇒ₗ ⋁Δ

theorem PointwiseComposition.FFL.Entailment.CFDisjFDisj_of_subset {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ Δ : Finset F} (h : Γ ⊆ Δ) : 𝓢 ⊢ Finset.disj Γ ⇒ₗ Finset.disj Δ

theorem PointwiseComposition.FFL.Entailment.EDisj₂FDisj {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ : List F} : 𝓢 ⊢ ⋁Γ ⇔ₗ Finset.disj Γ.toFinset

theorem PointwiseComposition.FFL.Entailment.EDisj₂FDisj_doubleton {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Int 𝓢] : 𝓢 ⊢ ⋁[φ, ψ] ⇔ₗ Finset.disj {φ, ψ}

theorem PointwiseComposition.FFL.Entailment.EConj₂FConj_doubleton {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Int 𝓢] : 𝓢 ⊢ ⋁[φ, ψ] ↔ 𝓢 ⊢ Finset.disj {φ, ψ}

@[simp]

theorem PointwiseComposition.FFL.Entailment.CAFDisjinsertFDisj {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ : F} [Entailment.Int 𝓢] {Γ : Finset F} : 𝓢 ⊢ φ ⋎ Finset.disj Γ ⇒ₗ Finset.disj (insert φ Γ)

@[simp]

theorem PointwiseComposition.FFL.Entailment.CinsertFDisjAFDisj {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ : F} [Entailment.Int 𝓢] {Γ : Finset F} : 𝓢 ⊢ Finset.disj (insert φ Γ) ⇒ₗ φ ⋎ Finset.disj Γ

@[simp]

theorem PointwiseComposition.FFL.Entailment.CAFdisjFdisjUnion {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ Δ : Finset F} : 𝓢 ⊢ Finset.disj Γ ⋎ Finset.disj Δ ⇒ₗ Finset.disj (Γ ∪ Δ)

@[simp]

theorem PointwiseComposition.FFL.Entailment.CFdisjUnionAFdisj {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ Δ : Finset F} : 𝓢 ⊢ Finset.disj (Γ ∪ Δ) ⇒ₗ Finset.disj Γ ⋎ Finset.disj Δ

theorem PointwiseComposition.FFL.Entailment.left_Fdisj_intro' {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ : F} [Entailment.Int 𝓢] {Γ : Finset F} (hd : ∀ ψ ∈ Γ, ψ = φ) : 𝓢 ⊢ Finset.disj Γ ⇒ₗ φ

theorem PointwiseComposition.FFL.Entailment.CFConjFDisj_of_A {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Int 𝓢] {Γ Δ : Finset F} (hφψ : φ ⋎ ψ ∈ Γ) (hφ : φ ∈ Δ) (hψ : ψ ∈ Δ) : 𝓢 ⊢ Finset.conj Γ ⇒ₗ Finset.disj Δ

@[simp]

theorem PointwiseComposition.FFL.Entailment.CNDisj₁Conj₂ {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {Γ : List F} [Entailment.Int 𝓢] : 𝓢 ⊢ ∼⋁Γ ⇒ₗ ⋀List.map (fun (x : F) => ∼x) Γ

List version of CNAKNN

@[simp]

theorem PointwiseComposition.FFL.Entailment.CNFdisjFconj {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ : Finset F} : 𝓢 ⊢ ∼Finset.disj Γ ⇒ₗ Finset.conj (Finset.image (fun (x : F) => ∼x) Γ)

• Finset version of CNAKNN

@[simp]

theorem PointwiseComposition.FFL.Entailment.CConj₂NNDisj₂ {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {Γ : List F} [Entailment.Int 𝓢] : 𝓢 ⊢ ⋀List.map (fun (x : F) => ∼x) Γ ⇒ₗ ∼⋁Γ

• Finset version of CKNNNA

@[simp]

theorem PointwiseComposition.FFL.Entailment.CFconjNNFconj {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ : Finset F} : 𝓢 ⊢ Finset.conj (Finset.image (fun (x : F) => ∼x) Γ) ⇒ₗ ∼Finset.disj Γ

• Finset version of CKNNNA

theorem PointwiseComposition.FFL.Entailment.inconsistent_of_provable_of_unprovable {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {φ : F} (hp : 𝓢 ⊢ φ) (hn : 𝓢 ⊢ ∼φ) : Inconsistent 𝓢