Foundation.Propositional.Entailment.Int

@[reducible, inline]

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

Equations

FFL.Axioms.EFQ φ = ⊥ 🡒 φ

Instances For

class 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)

efq! {φ : F} : 𝓢 ⊢! Axioms.EFQ φ

Instances

source

@[simp]

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

𝓢 ⊢ ⊥ 🡒 φ

source

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

𝓢 ⊢! φ

Equations

FFL.Entailment.of_O! b = FFL.Entailment.efq!⨀!b

Instances For

source

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

𝓢 ⊢ φ

source

@[instance_reducible]

instance 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

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

source

@[instance_reducible]

instance 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 = { efq! := fun {φ : F} => FFL.Entailment.FiniteContext.of! FFL.Entailment.efq! }

source

@[instance_reducible]

instance 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

FFL.Entailment.FiniteContext.instDeductiveExplosionOfHasAxiomEFQ = inferInstance

source

@[instance_reducible]

instance 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 = { efq! := fun {φ : F} => FFL.Entailment.Context.of! FFL.Entailment.efq! }

source

@[instance_reducible]

instance 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

FFL.Entailment.Context.instDeductiveExplosionFiniteContextOfHasAxiomEFQ = inferInstance

source

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

Type (max u_1 u_3)

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 φ ψ χ
efq! {φ : F} : 𝓢 ⊢! Axioms.EFQ φ

Instances

source

@[instance_reducible]

instance 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 }

source

@[instance_reducible]

instance 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 }

source

def FFL.Entailment.efq_of_mem_either! {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₂ : ∼φ ∈ Γ) :

Γ ⊢[𝓢]! ψ

Equations

FFL.Entailment.efq_of_mem_either! h₁ h₂ = FFL.Entailment.of_O! (FFL.Entailment.bot_of_mem_either! h₁ h₂)

Instances For

source

@[simp]

theorem FFL.Entailment.efq_of_mem_either {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₂ : ∼φ ∈ Γ) :

Γ ⊢[𝓢] ψ

source

def FFL.Entailment.CNC! {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Int 𝓢] :

𝓢 ⊢! ∼φ 🡒 φ 🡒 ψ

Equations

FFL.Entailment.CNC! = FFL.Entailment.FiniteContext.deduct'! (FFL.Entailment.FiniteContext.deduct! (FFL.Entailment.efq_of_mem_either! ⋯ ⋯))

Instances For

source

@[simp]

theorem FFL.Entailment.CNC {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Int 𝓢] :

𝓢 ⊢ ∼φ 🡒 φ 🡒 ψ

source

def FFL.Entailment.CCN! {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Int 𝓢] :

𝓢 ⊢! φ 🡒 ∼φ 🡒 ψ

Equations

FFL.Entailment.CCN! = FFL.Entailment.FiniteContext.deduct'! (FFL.Entailment.FiniteContext.deduct! (FFL.Entailment.efq_of_mem_either! ⋯ ⋯))

Instances For

source

@[simp]

theorem FFL.Entailment.CCN {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Int 𝓢] :

𝓢 ⊢ φ 🡒 ∼φ 🡒 ψ

source

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

𝓢 ⊢ φ 🡒 ψ

source

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

𝓢 ⊢ ∼φ 🡒 ψ

source

def FFL.Entailment.CANC! {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Int 𝓢] :

𝓢 ⊢! ∼φ ⋎ ψ 🡒 φ 🡒 ψ

Equations

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

Instances For

source

@[simp]

theorem FFL.Entailment.CANC {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Int 𝓢] :

𝓢 ⊢ ∼φ ⋎ ψ 🡒 φ 🡒 ψ

source

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

𝓢 ⊢! φ 🡒 ψ

Equations

FFL.Entailment.C!_of_AN! b = FFL.Entailment.CANC!⨀!b

Instances For

source

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

𝓢 ⊢ φ 🡒 ψ

source

def FFL.Entailment.CCNNNNNNC! {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Int 𝓢] :

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

Equations

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

Instances For

source

@[simp]

theorem FFL.Entailment.CCNNNNNNC {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Int 𝓢] :

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

source

def FFL.Entailment.NNC!_of_CNNNN! {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Int 𝓢] (b : 𝓢 ⊢! ∼∼φ 🡒 ∼∼ψ) :

𝓢 ⊢! ∼∼(φ 🡒 ψ)

Equations

FFL.Entailment.NNC!_of_CNNNN! b = FFL.Entailment.CCNNNNNNC!⨀!b

Instances For

source

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

𝓢 ⊢ ∼∼(φ 🡒 ψ)

source

def 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 : (ψ : F) → ψ ∈ Γ → 𝓢 ⊢! ψ 🡒 φ) :

𝓢 ⊢! Γ.disj 🡒 φ

Equations

FFL.Entailment.left_Disj!_intro [] b_2 = FFL.Entailment.efq!
FFL.Entailment.left_Disj!_intro (ψ :: Γ_2) b_2 = FFL.Entailment.left_A!_intro (b_2 ψ ⋯) (FFL.Entailment.left_Disj!_intro Γ_2 fun (ψ_1 : F) (h : ψ_1 ∈ Γ_2) => b_2 ψ_1 ⋯)

Instances For

source

theorem 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 : ∀ ψ ∈ Γ, 𝓢 ⊢ ψ 🡒 φ) :

𝓢 ⊢ Γ.disj 🡒 φ

source

def 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 : (ψ : F) → ψ ∈ Γ → 𝓢 ⊢! ψ 🡒 φ) :

𝓢 ⊢! ⋁Γ 🡒 φ

Equations

FFL.Entailment.left_Disj₂!_intro [] b_2 = FFL.Entailment.efq!
FFL.Entailment.left_Disj₂!_intro [ψ] b_2 = b_2 (⋁[ψ]) ⋯
FFL.Entailment.left_Disj₂!_intro (ψ :: χ :: Γ_2) b_2 = FFL.Entailment.left_A!_intro (b_2 ψ ⋯) (FFL.Entailment.left_Disj₂!_intro (χ :: Γ_2) fun (ψ_1 : F) (h : ψ_1 ∈ χ :: Γ_2) => b_2 ψ_1 ⋯)

Instances For

source

theorem 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 : ∀ ψ ∈ Γ, 𝓢 ⊢ ψ 🡒 φ) :

𝓢 ⊢ ⋁Γ 🡒 φ

source

def FFL.Entailment.left_Disj'!_intro {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 🡒 φ) :

𝓢 ⊢! List.disj' ψ l 🡒 φ

Equations

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

Instances For

source

theorem FFL.Entailment.left_Disj'_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ : F} [Entailment.Int 𝓢] {ι : Type u_3} (l : List ι) (ψ : ι → F) (b : ∀ i ∈ l, 𝓢 ⊢ ψ i 🡒 φ) :

𝓢 ⊢ List.disj' ψ l 🡒 φ

source

theorem 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, 𝓢 ⊢ ψ 🡒 φ) :

𝓢 ⊢ s.disj 🡒 φ

source

theorem 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 𝓢] {ι : Type u_3} (s : Finset ι) (ψ : ι → F) (b : ∀ i ∈ s, 𝓢 ⊢ ψ i 🡒 φ) :

𝓢 ⊢ (⩖ (i : ι) ∈ s, ψ i) 🡒 φ

source

theorem 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} [DecidableEq F] [Fintype ι] (ψ : ι → F) (b : ∀ (i : ι), 𝓢 ⊢ ψ i 🡒 φ) :

𝓢 ⊢ (⩖ (i : ι), ψ i) 🡒 φ

source

theorem 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 𝓢] :

𝓢 ⊢ ⋁(Γ ++ Δ) 🡘 ⋁Γ ⋎ ⋁Δ

source

theorem 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 𝓢] :

𝓢 ⊢ ⋁(Γ ++ Δ) ↔ 𝓢 ⊢ ⋁Γ ⋎ ⋁Δ

source

theorem 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 𝓢] :

𝓢 ⊢ φ 🡒 ⋁(ψ :: Γ) ↔ 𝓢 ⊢ φ 🡒 ψ ⋎ ⋁Γ

source

@[simp]

theorem 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 𝓢] :

𝓢 ⊢ ⋁Γ 🡒 φ ⋎ ⋁List.remove φ Γ

source

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

𝓢 ⊢ ⋁Γ 🡒 φ

source

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

𝓢 ⊢ φ

source

@[simp]

theorem FFL.Entailment.CDisj₂FDisj {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ : Finset F} :

𝓢 ⊢ ⋁Γ.toList 🡒 Γ.disj

source

@[simp]

theorem FFL.Entailment.CFDisjDisj₂ {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ : Finset F} :

𝓢 ⊢ Γ.disj 🡒 ⋁Γ.toList

source

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

𝓢 ⊢ ⋁Γ 🡒 ⋁Δ

source

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

𝓢 ⊢ Γ.disj 🡒 Δ.disj

source

theorem 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} :

𝓢 ⊢ ⋁Γ 🡘 Γ.toFinset.disj

source

theorem 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 𝓢] :

𝓢 ⊢ ⋁[φ, ψ] 🡘 {φ, ψ}.disj

source

theorem 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 𝓢] :

𝓢 ⊢ ⋁[φ, ψ] ↔ 𝓢 ⊢ {φ, ψ}.disj

source

@[simp]

theorem 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} :

𝓢 ⊢ φ ⋎ Γ.disj 🡒 (insert φ Γ).disj

source

@[simp]

theorem 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} :

𝓢 ⊢ (insert φ Γ).disj 🡒 φ ⋎ Γ.disj

source

@[simp]

theorem 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} :

𝓢 ⊢ Γ.disj ⋎ Δ.disj 🡒 (Γ ∪ Δ).disj

source

@[simp]

theorem 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} :

𝓢 ⊢ (Γ ∪ Δ).disj 🡒 Γ.disj ⋎ Δ.disj

source

theorem 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 : ∀ ψ ∈ Γ, ψ = φ) :

𝓢 ⊢ Γ.disj 🡒 φ

source

theorem 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ψ : ψ ∈ Δ) :

𝓢 ⊢ Γ.conj 🡒 Δ.disj

source

@[simp]

theorem FFL.Entailment.CNDisj₁Conj₂ {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {Γ : List F} [Entailment.Int 𝓢] :

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

List version of CNAKNN

source

@[simp]

theorem 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} :

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

Finset version of CNAKNN

source

@[simp]

theorem FFL.Entailment.CConj₂NNDisj₂ {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {Γ : List F} [Entailment.Int 𝓢] :

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

Finset version of CKNNNA

source

@[simp]

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

Finset version of CKNNNA

source

theorem 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 𝓢