Documentation

Foundation.Propositional.Entailment.Int

@[reducible, inline]

abbrev FFL.Axioms.EFQ {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] (φ : 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) :

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

Instances

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

𝓢 ⊢ φ

theorem FFL.Entailment.unprovable_bot {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] [HasAxiomEFQ 𝓢] [Consistent 𝓢] :

𝓢 ⊬ ⊥

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

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 𝓢) :

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

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 𝓢) :

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

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

mdp {φ ψ : F} : 𝓢 ⊢ φ 🡒 ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
neg_equiv {φ : 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

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 Γ

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

Entailment.Int Γ

@[simp]

theorem 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₂ : ∼φ ∈ Γ) :

Γ ⊢[𝓢] ψ

@[simp]

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

𝓢 ⊢ ∼φ 🡒 φ 🡒 ψ

@[simp]

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

𝓢 ⊢ φ 🡒 ∼φ 🡒 ψ

theorem 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 FFL.Entailment.CN_of_ {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} {φ ψ : F} [Entailment.Int 𝓢] (h : 𝓢 ⊢ φ) :

𝓢 ⊢ ∼φ 🡒 ψ

@[simp]

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

𝓢 ⊢ ∼φ ⋎ ψ 🡒 φ 🡒 ψ

theorem 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 : 𝓢 ⊢ ∼φ ⋎ ψ) :

𝓢 ⊢ φ 🡒 ψ

@[simp]

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

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

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

𝓢 ⊢ ∼∼(φ 🡒 ψ)

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 🡒 φ

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

𝓢 ⊢ ⋁Γ 🡒 φ

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

𝓢 ⊢ List.disj' ψ l 🡒 φ

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 🡒 φ

theorem 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 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 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 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 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 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 φ Γ

theorem 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 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 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 🡒 Γ.disj

@[simp]

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

𝓢 ⊢ Γ.disj 🡒 ⋁Γ.toList

theorem 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 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 : Γ ⊆ Δ) :

𝓢 ⊢ Γ.disj 🡒 Δ.disj

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

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

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

@[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

@[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

@[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

@[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

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 🡒 φ

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

@[simp]

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

@[simp]

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

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 𝓢