Foundation.Propositional.Entailment.Int

source

@[reducible, inline]

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

Equations

LO.Axioms.EFQ φ = ⊥ 🡒 φ

Instances For

source

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

Type (max u_2 u_3)

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

Instances

source

@[simp]

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

𝓢 ⊢ ⊥ 🡒 φ

source

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

𝓢 ⊢! φ

Equations

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

Instances For

source

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

𝓢 ⊢ φ

source

@[implicit_reducible]

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

DeductiveExplosion S

Equations

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

source

@[implicit_reducible]

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

HasAxiomEFQ Γ

Equations

Γ.instHasAxiomEFQ = { efq := fun {φ : F} => LO.Entailment.FiniteContext.of LO.Entailment.efq }

source

@[implicit_reducible]

instance LO.Entailment.FiniteContext.instDeductiveExplosionOfHasAxiomEFQ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [HasAxiomEFQ 𝓢] :

DeductiveExplosion (FiniteContext F 𝓢)

Equations

LO.Entailment.FiniteContext.instDeductiveExplosionOfHasAxiomEFQ = inferInstance

source

@[implicit_reducible]

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

HasAxiomEFQ Γ

Equations

Γ.instHasAxiomEFQ = { efq := fun {φ : F} => LO.Entailment.Context.of LO.Entailment.efq }

source

@[implicit_reducible]

instance LO.Entailment.Context.instDeductiveExplosionFiniteContextOfHasAxiomEFQ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [HasAxiomEFQ 𝓢] :

DeductiveExplosion (FiniteContext F 𝓢)

Equations

LO.Entailment.Context.instDeductiveExplosionFiniteContextOfHasAxiomEFQ = inferInstance

source

class LO.Entailment.Int {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] (𝓢 : S) extends LO.Entailment.Minimal 𝓢, LO.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

@[implicit_reducible]

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

Entailment.Int Γ

Equations

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

source

@[implicit_reducible]

instance LO.Entailment.Context.instInt {F : Type u_1} [LogicalConnective 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 LO.Entailment.efq_of_mem_either {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} {Γ : List F} [Entailment.Int 𝓢] (h₁ : φ ∈ Γ) (h₂ : ∼φ ∈ Γ) :

Γ ⊢[𝓢]! ψ

Equations

LO.Entailment.efq_of_mem_either h₁ h₂ = LO.Entailment.of_O (LO.Entailment.bot_of_mem_either h₁ h₂)

Instances For

source

@[simp]

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

Γ ⊢[𝓢] ψ

source

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

𝓢 ⊢! ∼φ 🡒 φ 🡒 ψ

Equations

LO.Entailment.CNC = LO.Entailment.FiniteContext.deduct' (LO.Entailment.FiniteContext.deduct (LO.Entailment.efq_of_mem_either ⋯ ⋯))

Instances For

source

@[simp]

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

𝓢 ⊢ ∼φ 🡒 φ 🡒 ψ

source

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

𝓢 ⊢! φ 🡒 ∼φ 🡒 ψ

Equations

LO.Entailment.CCN = LO.Entailment.FiniteContext.deduct' (LO.Entailment.FiniteContext.deduct (LO.Entailment.efq_of_mem_either ⋯ ⋯))

Instances For

source

@[simp]

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

𝓢 ⊢ φ 🡒 ∼φ 🡒 ψ

source

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

𝓢 ⊢ φ 🡒 ψ

source

theorem LO.Entailment.CN!_of_! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Int 𝓢] (h : 𝓢 ⊢ φ) :

𝓢 ⊢ ∼φ 🡒 ψ

source

def LO.Entailment.CANC {F : Type u_1} [LogicalConnective 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 LO.Entailment.CANC! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Int 𝓢] :

𝓢 ⊢ ∼φ ⋎ ψ 🡒 φ 🡒 ψ

source

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

𝓢 ⊢! φ 🡒 ψ

Equations

LO.Entailment.C_of_AN b = LO.Entailment.CANC ⨀!b

Instances For

source

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

𝓢 ⊢ φ 🡒 ψ

source

def LO.Entailment.CCNNNNNNC {F : Type u_1} [LogicalConnective 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 LO.Entailment.CCNNNNNNC! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Int 𝓢] :

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

source

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

𝓢 ⊢! ∼∼(φ 🡒 ψ)

Equations

LO.Entailment.NNC_of_CNNNN b = LO.Entailment.CCNNNNNNC ⨀!b

Instances For

source

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

𝓢 ⊢ ∼∼(φ 🡒 ψ)

source

def LO.Entailment.left_Disj_intro {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ : F} [Entailment.Int 𝓢] (Γ : List F) (b : (ψ : F) → ψ ∈ Γ → 𝓢 ⊢! ψ 🡒 φ) :

𝓢 ⊢! Γ.disj 🡒 φ

Equations

LO.Entailment.left_Disj_intro [] b_2 = LO.Entailment.efq
LO.Entailment.left_Disj_intro (ψ :: Γ_2) b_2 = LO.Entailment.left_A_intro (b_2 ψ ⋯) (LO.Entailment.left_Disj_intro Γ_2 fun (ψ_1 : F) (h : ψ_1 ∈ Γ_2) => b_2 ψ_1 ⋯)

Instances For

source

def LO.Entailment.left_Disj!_intro {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ : F} [Entailment.Int 𝓢] (Γ : List F) (b : ∀ ψ ∈ Γ, 𝓢 ⊢ ψ 🡒 φ) :

𝓢 ⊢ Γ.disj 🡒 φ

Equations

⋯ = ⋯

Instances For

source

def LO.Entailment.left_Disj₂_intro {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ : F} [Entailment.Int 𝓢] (Γ : List F) (b : (ψ : F) → ψ ∈ Γ → 𝓢 ⊢! ψ 🡒 φ) :

𝓢 ⊢! ⋁Γ 🡒 φ

Equations

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

Instances For

source

theorem LO.Entailment.left_Disj₂!_intro {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ : F} [Entailment.Int 𝓢] (Γ : List F) (b : ∀ ψ ∈ Γ, 𝓢 ⊢ ψ 🡒 φ) :

𝓢 ⊢ ⋁Γ 🡒 φ

source

def LO.Entailment.left_Disj'_intro {F : Type u_1} [LogicalConnective 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 LO.Entailment.left_Disj'!_intro {F : Type u_1} [LogicalConnective 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 LO.Entailment.left_Fdisj!_intro {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ : F} [Entailment.Int 𝓢] (s : Finset F) (b : ∀ ψ ∈ s, 𝓢 ⊢ ψ 🡒 φ) :

𝓢 ⊢ s.disj 🡒 φ

source

theorem LO.Entailment.left_Fdisj'!_intro {F : Type u_1} [LogicalConnective 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 LO.Entailment.left_Udisj!_intro {F : Type u_1} [LogicalConnective 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 LO.Entailment.EDisj₂AppendADisj₂Disj₂! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} {Γ Δ : List F} [Entailment.Int 𝓢] :

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

source

theorem LO.Entailment.Disj₂Append!_iff_ADisj₂Disj₂! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} {Γ Δ : List F} [Entailment.Int 𝓢] :

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

source

theorem LO.Entailment.CDisj₂!_iff_CADisj₂! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} {Γ : List F} [Entailment.Int 𝓢] :

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

source

@[simp]

theorem LO.Entailment.CDisj₂ADisj₂Remove! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ : F} {Γ : List F} [Entailment.Int 𝓢] :

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

source

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

𝓢 ⊢ ⋁Γ 🡒 φ

source

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

𝓢 ⊢ φ

source

@[simp]

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

𝓢 ⊢ ⋁Γ.toList 🡒 Γ.disj

source

@[simp]

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

𝓢 ⊢ Γ.disj 🡒 ⋁Γ.toList

source

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

𝓢 ⊢ ⋁Γ 🡒 ⋁Δ

source

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

𝓢 ⊢ Γ.disj 🡒 Δ.disj

source

theorem LO.Entailment.EDisj₂FDisj {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ : List F} :

𝓢 ⊢ ⋁Γ 🡘 Γ.toFinset.disj

source

theorem LO.Entailment.EDisj₂FDisj!_doubleton {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Int 𝓢] :

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

source

theorem LO.Entailment.EConj₂_FConj!_doubleton {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Int 𝓢] :

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

source

@[simp]

theorem LO.Entailment.CAFDisjinsertFDisj! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ : F} [Entailment.Int 𝓢] {Γ : Finset F} :

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

source

@[simp]

theorem LO.Entailment.CinsertFDisjAFDisj! {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ : F} [Entailment.Int 𝓢] {Γ : Finset F} :

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

source

@[simp]

theorem LO.Entailment.CAFdisjFdisjUnion {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ Δ : Finset F} :

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

source

@[simp]

theorem LO.Entailment.CFdisjUnionAFdisj {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {Γ Δ : Finset F} :

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

source

theorem LO.Entailment.left_Fdisj!_intro' {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ : F} [Entailment.Int 𝓢] {Γ : Finset F} (hd : ∀ ψ ∈ Γ, ψ = φ) :

𝓢 ⊢ Γ.disj 🡒 φ

source

theorem LO.Entailment.CFConj_CDisj!_of_A {F : Type u_1} [LogicalConnective F] [DecidableEq F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Int 𝓢] {Γ Δ : Finset F} (hφψ : φ ⋎ ψ ∈ Γ) (hφ : φ ∈ Δ) (hψ : ψ ∈ Δ) :

𝓢 ⊢ Γ.conj 🡒 Δ.disj

source

@[simp]

theorem LO.Entailment.CNDisj₁Conj₂! {F : Type u_1} [LogicalConnective 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 LO.Entailment.CNFdisjFconj! {F : Type u_1} [LogicalConnective 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 LO.Entailment.CConj₂NNDisj₂! {F : Type u_1} [LogicalConnective 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 LO.Entailment.CFconjNNFconj! {F : Type u_1} [LogicalConnective 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 LO.Entailment.inconsistent_of_provable_of_unprovable {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Int 𝓢] {φ : F} (hp : 𝓢 ⊢ φ) (hn : 𝓢 ⊢ ∼φ) :

Inconsistent 𝓢