@[reducible, inline]

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

Equations

• LO.Axioms.NegEquiv φ = ∼φ 🡘 (φ 🡒 ⊥)

@[reducible, inline]

abbrev LO.Axioms.Verum {F : Type u_1} [LogicalConnective F] : F

Equations

• LO.Axioms.Verum = ⊤

@[reducible, inline]

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

Equations

• LO.Axioms.ImplyK φ ψ = φ 🡒 ψ 🡒 φ

@[reducible, inline]

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

Equations

• LO.Axioms.ImplyS φ ψ χ = (φ 🡒 ψ 🡒 χ) 🡒 (φ 🡒 ψ) 🡒 φ 🡒 χ

@[reducible, inline]

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

Equations

• LO.Axioms.AndElim₁ φ ψ = φ ⋏ ψ 🡒 φ

@[reducible, inline]

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

Equations

• LO.Axioms.AndElim₂ φ ψ = φ ⋏ ψ 🡒 ψ

@[reducible, inline]

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

Equations

• LO.Axioms.AndInst φ ψ = φ 🡒 ψ 🡒 φ ⋏ ψ

@[reducible, inline]

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

Equations

• LO.Axioms.OrInst₁ φ ψ = φ 🡒 φ ⋎ ψ

@[reducible, inline]

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

Equations

• LO.Axioms.OrInst₂ φ ψ = ψ 🡒 φ ⋎ ψ

@[reducible, inline]

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

Equations

• LO.Axioms.OrElim φ ψ χ = (φ 🡒 χ) 🡒 (ψ 🡒 χ) 🡒 φ ⋎ ψ 🡒 χ

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

• mdp {φ ψ : F} : 𝓢 ⊢! φ 🡒 ψ → 𝓢 ⊢! φ → 𝓢 ⊢! ψ

def LO.Entailment.mdp {S : Type u_1} {F : Type u_2} {inst✝ : LogicalConnective F} {inst✝¹ : Entailment S F} {𝓢 : S} [self : ModusPonens 𝓢] {φ ψ : F} : 𝓢 ⊢! φ 🡒 ψ → 𝓢 ⊢! φ → 𝓢 ⊢! ψ

Alias of LO.Entailment.ModusPonens.mdp.

Equations

• @LO.Entailment.mdp = @LO.Entailment.ModusPonens.mdp

def LO.Entailment.«term_⨀_» : Lean.TrailingParserDescr

Equations

• LO.Entailment.«term_⨀_» = Lean.ParserDescr.trailingNode `LO.Entailment.«term_⨀_» 90 90 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⨀") (Lean.ParserDescr.cat `term 91))

theorem LO.Entailment.mdp! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] : 𝓢 ⊢ φ 🡒 ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ

def LO.Entailment.«term_⨀__1» : Lean.TrailingParserDescr

Equations

• LO.Entailment.«term_⨀__1» = Lean.ParserDescr.trailingNode `LO.Entailment.«term_⨀__1» 90 90 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⨀") (Lean.ParserDescr.cat `term 91))

def LO.Entailment.«term_⨀!_» : Lean.TrailingParserDescr

Equations

• LO.Entailment.«term_⨀!_» = Lean.ParserDescr.trailingNode `LO.Entailment.«term_⨀!_» 90 90 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⨀!") (Lean.ParserDescr.cat `term 91))

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

Negation ∼φ is equivalent to φ 🡒 ⊥ on system.

This is weaker asssumption than "introducing ∼φ as an abbreviation of φ 🡒 ⊥" (NegAbbrev).

• negEquiv {φ : F} : 𝓢 ⊢! Axioms.NegEquiv φ

@[simp]

theorem LO.Entailment.neg_equiv! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ : F} [NegationEquiv 𝓢] : 𝓢 ⊢ ∼φ 🡘 (φ 🡒 ⊥)

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

• verum : 𝓢 ⊢! Axioms.Verum

def LO.Entailment.verum {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [HasAxiomVerum 𝓢] : 𝓢 ⊢! ⊤

Equations

• LO.Entailment.verum = LO.Entailment.HasAxiomVerum.verum

@[simp]

theorem LO.Entailment.verum! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [HasAxiomVerum 𝓢] : 𝓢 ⊢ ⊤

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

• implyK {φ ψ : F} : 𝓢 ⊢! Axioms.ImplyK φ ψ

@[simp]

theorem LO.Entailment.implyK! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [HasAxiomImplyK 𝓢] : 𝓢 ⊢ φ 🡒 ψ 🡒 φ

def LO.Entailment.C_of_conseq {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomImplyK 𝓢] (h : 𝓢 ⊢! φ) : 𝓢 ⊢! ψ 🡒 φ

Equations

• LO.Entailment.C_of_conseq h = LO.Entailment.implyK⨀!h

def LO.Entailment.dhyp {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomImplyK 𝓢] (h : 𝓢 ⊢! φ) : 𝓢 ⊢! ψ 🡒 φ

Alias of LO.Entailment.C_of_conseq.

Equations

• @LO.Entailment.dhyp = @LO.Entailment.C_of_conseq

theorem LO.Entailment.C!_of_conseq! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomImplyK 𝓢] (d : 𝓢 ⊢ φ) : 𝓢 ⊢ ψ 🡒 φ

theorem LO.Entailment.dhyp! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomImplyK 𝓢] (d : 𝓢 ⊢ φ) : 𝓢 ⊢ ψ 🡒 φ

Alias of LO.Entailment.C!_of_conseq!.

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

• implyS {φ ψ χ : F} : 𝓢 ⊢! Axioms.ImplyS φ ψ χ

@[simp]

theorem LO.Entailment.implyS! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ χ : F} [HasAxiomImplyS 𝓢] : 𝓢 ⊢ (φ 🡒 ψ 🡒 χ) 🡒 (φ 🡒 ψ) 🡒 φ 🡒 χ

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

• and₁ {φ ψ : F} : 𝓢 ⊢! Axioms.AndElim₁ φ ψ
• and₂ {φ ψ : F} : 𝓢 ⊢! Axioms.AndElim₂ φ ψ

@[simp]

theorem LO.Entailment.and₁! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [HasAxiomAndElim 𝓢] : 𝓢 ⊢ φ ⋏ ψ 🡒 φ

def LO.Entailment.K_left {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndElim 𝓢] (d : 𝓢 ⊢! φ ⋏ ψ) : 𝓢 ⊢! φ

Equations

• LO.Entailment.K_left d = LO.Entailment.and₁⨀!d

theorem LO.Entailment.K!_left {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndElim 𝓢] (d : 𝓢 ⊢ φ ⋏ ψ) : 𝓢 ⊢ φ

@[simp]

theorem LO.Entailment.and₂! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [HasAxiomAndElim 𝓢] : 𝓢 ⊢ φ ⋏ ψ 🡒 ψ

def LO.Entailment.K_right {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndElim 𝓢] (d : 𝓢 ⊢! φ ⋏ ψ) : 𝓢 ⊢! ψ

Equations

• LO.Entailment.K_right d = LO.Entailment.and₂⨀!d

theorem LO.Entailment.K!_right {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndElim 𝓢] (d : 𝓢 ⊢ φ ⋏ ψ) : 𝓢 ⊢ ψ

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

• and₃ {φ ψ : F} : 𝓢 ⊢! Axioms.AndInst φ ψ

@[simp]

theorem LO.Entailment.and₃! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [HasAxiomAndInst 𝓢] : 𝓢 ⊢ φ 🡒 ψ 🡒 φ ⋏ ψ

def LO.Entailment.K_intro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] (d₁ : 𝓢 ⊢! φ) (d₂ : 𝓢 ⊢! ψ) : 𝓢 ⊢! φ ⋏ ψ

Equations

• LO.Entailment.K_intro d₁ d₂ = LO.Entailment.and₃⨀!d₁⨀!d₂

theorem LO.Entailment.K!_intro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] (d₁ : 𝓢 ⊢ φ) (d₂ : 𝓢 ⊢ ψ) : 𝓢 ⊢ φ ⋏ ψ

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

• or₁ {φ ψ : F} : 𝓢 ⊢! Axioms.OrInst₁ φ ψ
• or₂ {φ ψ : F} : 𝓢 ⊢! Axioms.OrInst₂ φ ψ

@[simp]

theorem LO.Entailment.or₁! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [HasAxiomOrInst 𝓢] : 𝓢 ⊢ φ 🡒 φ ⋎ ψ

def LO.Entailment.A_intro_left {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [HasAxiomOrInst 𝓢] [ModusPonens 𝓢] (d : 𝓢 ⊢! φ) : 𝓢 ⊢! φ ⋎ ψ

Equations

• LO.Entailment.A_intro_left d = LO.Entailment.or₁⨀!d

theorem LO.Entailment.A!_intro_left {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [HasAxiomOrInst 𝓢] [ModusPonens 𝓢] (d : 𝓢 ⊢ φ) : 𝓢 ⊢ φ ⋎ ψ

@[simp]

theorem LO.Entailment.or₂! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [HasAxiomOrInst 𝓢] : 𝓢 ⊢ ψ 🡒 φ ⋎ ψ

def LO.Entailment.A_intro_right {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [HasAxiomOrInst 𝓢] [ModusPonens 𝓢] (d : 𝓢 ⊢! ψ) : 𝓢 ⊢! φ ⋎ ψ

Equations

• LO.Entailment.A_intro_right d = LO.Entailment.or₂⨀!d

theorem LO.Entailment.A!_intro_right {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [HasAxiomOrInst 𝓢] [ModusPonens 𝓢] (d : 𝓢 ⊢ ψ) : 𝓢 ⊢ φ ⋎ ψ

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

• or₃ {φ ψ χ : F} : 𝓢 ⊢! Axioms.OrElim φ ψ χ

@[simp]

theorem LO.Entailment.or₃! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ χ : F} [HasAxiomOrElim 𝓢] : 𝓢 ⊢ (φ 🡒 χ) 🡒 (ψ 🡒 χ) 🡒 φ ⋎ ψ 🡒 χ

def LO.Entailment.left_A_intro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ χ : F} [HasAxiomOrElim 𝓢] [ModusPonens 𝓢] (d₁ : 𝓢 ⊢! φ 🡒 χ) (d₂ : 𝓢 ⊢! ψ 🡒 χ) : 𝓢 ⊢! φ ⋎ ψ 🡒 χ

Equations

• LO.Entailment.left_A_intro d₁ d₂ = LO.Entailment.or₃⨀!d₁⨀!d₂

def LO.Entailment.CA_of_C_of_C {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ χ : F} [HasAxiomOrElim 𝓢] [ModusPonens 𝓢] (d₁ : 𝓢 ⊢! φ 🡒 χ) (d₂ : 𝓢 ⊢! ψ 🡒 χ) : 𝓢 ⊢! φ ⋎ ψ 🡒 χ

Alias of LO.Entailment.left_A_intro.

Equations

• @LO.Entailment.CA_of_C_of_C = @LO.Entailment.left_A_intro

theorem LO.Entailment.left_A!_intro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ χ : F} [HasAxiomOrElim 𝓢] [ModusPonens 𝓢] (d₁ : 𝓢 ⊢ φ 🡒 χ) (d₂ : 𝓢 ⊢ ψ 🡒 χ) : 𝓢 ⊢ φ ⋎ ψ 🡒 χ

theorem LO.Entailment.CA!_of_C!_of_C! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ χ : F} [HasAxiomOrElim 𝓢] [ModusPonens 𝓢] (d₁ : 𝓢 ⊢ φ 🡒 χ) (d₂ : 𝓢 ⊢ ψ 🡒 χ) : 𝓢 ⊢ φ ⋎ ψ 🡒 χ

Alias of LO.Entailment.left_A!_intro.

def LO.Entailment.of_C_of_C_of_A {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ χ : F} [HasAxiomOrElim 𝓢] [ModusPonens 𝓢] (d₁ : 𝓢 ⊢! φ 🡒 χ) (d₂ : 𝓢 ⊢! ψ 🡒 χ) (d₃ : 𝓢 ⊢! φ ⋎ ψ) : 𝓢 ⊢! χ

Equations

• LO.Entailment.of_C_of_C_of_A d₁ d₂ d₃ = LO.Entailment.or₃⨀!d₁⨀!d₂⨀!d₃

def LO.Entailment.A_cases {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ χ : F} [HasAxiomOrElim 𝓢] [ModusPonens 𝓢] (d₁ : 𝓢 ⊢! φ 🡒 χ) (d₂ : 𝓢 ⊢! ψ 🡒 χ) (d₃ : 𝓢 ⊢! φ ⋎ ψ) : 𝓢 ⊢! χ

Alias of LO.Entailment.of_C_of_C_of_A.

Equations

• @LO.Entailment.A_cases = @LO.Entailment.of_C_of_C_of_A

theorem LO.Entailment.of_C!_of_C!_of_A! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ χ : F} [HasAxiomOrElim 𝓢] [ModusPonens 𝓢] (d₁ : 𝓢 ⊢ φ 🡒 χ) (d₂ : 𝓢 ⊢ ψ 🡒 χ) (d₃ : 𝓢 ⊢ φ ⋎ ψ) : 𝓢 ⊢ χ

theorem LO.Entailment.A!_cases {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ χ : F} [HasAxiomOrElim 𝓢] [ModusPonens 𝓢] (d₁ : 𝓢 ⊢ φ 🡒 χ) (d₂ : 𝓢 ⊢ ψ 🡒 χ) (d₃ : 𝓢 ⊢ φ ⋎ ψ) : 𝓢 ⊢ χ

Alias of LO.Entailment.of_C!_of_C!_of_A!.

class LO.Entailment.Minimal {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] (𝓢 : S) extends LO.Entailment.ModusPonens 𝓢, LO.Entailment.NegationEquiv 𝓢, LO.Entailment.HasAxiomVerum 𝓢, LO.Entailment.HasAxiomImplyK 𝓢, LO.Entailment.HasAxiomImplyS 𝓢, LO.Entailment.HasAxiomAndElim 𝓢, LO.Entailment.HasAxiomAndInst 𝓢, LO.Entailment.HasAxiomOrInst 𝓢, LO.Entailment.HasAxiomOrElim 𝓢 : Type (max u_2 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 φ ψ χ

def LO.Entailment.CO_of_N {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ : F} [HasAxiomAndElim 𝓢] [NegationEquiv 𝓢] : 𝓢 ⊢! ∼φ → 𝓢 ⊢! φ 🡒 ⊥

Equations

• LO.Entailment.CO_of_N h = LO.Entailment.K_left LO.Entailment.negEquiv⨀!h

def LO.Entailment.N_of_CO {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ : F} [HasAxiomAndElim 𝓢] [NegationEquiv 𝓢] : 𝓢 ⊢! φ 🡒 ⊥ → 𝓢 ⊢! ∼φ

Equations

• LO.Entailment.N_of_CO h = LO.Entailment.K_right LO.Entailment.negEquiv⨀!h

theorem LO.Entailment.N!_iff_CO! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ : F} [HasAxiomAndElim 𝓢] [NegationEquiv 𝓢] : 𝓢 ⊢ ∼φ ↔ 𝓢 ⊢ φ 🡒 ⊥

def LO.Entailment.E_intro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndInst 𝓢] (b₁ : 𝓢 ⊢! φ 🡒 ψ) (b₂ : 𝓢 ⊢! ψ 🡒 φ) : 𝓢 ⊢! φ 🡘 ψ

Equations

• LO.Entailment.E_intro b₁ b₂ = LO.Entailment.K_intro b₁ b₂

theorem LO.Entailment.E!_intro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndInst 𝓢] (h₁ : 𝓢 ⊢ φ 🡒 ψ) (h₂ : 𝓢 ⊢ ψ 🡒 φ) : 𝓢 ⊢ φ 🡘 ψ

theorem LO.Entailment.K!_intro_iff {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] : 𝓢 ⊢ φ ⋏ ψ ↔ 𝓢 ⊢ φ ∧ 𝓢 ⊢ ψ

theorem LO.Entailment.E!_intro_iff {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] : 𝓢 ⊢ φ 🡘 ψ ↔ 𝓢 ⊢ φ 🡒 ψ ∧ 𝓢 ⊢ ψ 🡒 φ

def LO.Entailment.C_of_E_mp {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] (h : 𝓢 ⊢! φ 🡘 ψ) : 𝓢 ⊢! φ 🡒 ψ

Equations

• LO.Entailment.C_of_E_mp h = LO.Entailment.K_left h

theorem LO.Entailment.C_of_E_mp! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] : 𝓢 ⊢ φ 🡘 ψ → 𝓢 ⊢ φ 🡒 ψ

def LO.Entailment.C_of_E_mpr {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] (h : 𝓢 ⊢! φ 🡘 ψ) : 𝓢 ⊢! ψ 🡒 φ

Equations

• LO.Entailment.C_of_E_mpr h = LO.Entailment.K_right h

theorem LO.Entailment.C_of_E_mpr! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] : 𝓢 ⊢ φ 🡘 ψ → 𝓢 ⊢ ψ 🡒 φ

theorem LO.Entailment.iff_of_E! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] (h : 𝓢 ⊢ φ 🡘 ψ) : 𝓢 ⊢ φ ↔ 𝓢 ⊢ ψ

def LO.Entailment.C_id {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] {φ : F} : 𝓢 ⊢! φ 🡒 φ

Equations

• LO.Entailment.C_id = LO.Entailment.implyS⨀!LO.Entailment.implyK⨀!LO.Entailment.implyK

@[simp]

def LO.Entailment.C!_id {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ : F} [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] : 𝓢 ⊢ φ 🡒 φ

Equations

• ⋯ = ⋯

def LO.Entailment.E_Id {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] [HasAxiomAndInst 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] {φ : F} : 𝓢 ⊢! φ 🡘 φ

Equations

• LO.Entailment.E_Id = LO.Entailment.K_intro LO.Entailment.C_id LO.Entailment.C_id

@[simp]

def LO.Entailment.E!_id {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ : F} [HasAxiomAndInst 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] : 𝓢 ⊢ φ 🡘 φ

Equations

• ⋯ = ⋯

@[implicit_reducible]

instance LO.Entailment.instNegationEquivOfNegAbbrevOfHasAxiomImplyKOfHasAxiomImplySOfHasAxiomAndInst {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] [NegAbbrev F] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] [HasAxiomAndInst 𝓢] : NegationEquiv 𝓢

Equations

• LO.Entailment.instNegationEquivOfNegAbbrevOfHasAxiomImplyKOfHasAxiomImplySOfHasAxiomAndInst = { negEquiv := fun {φ : F} => have this := LO.Entailment.E_Id; ⋯.mpr this }

def LO.Entailment.NO {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] [NegationEquiv 𝓢] [HasAxiomAndElim 𝓢] : 𝓢 ⊢! ∼⊥

Equations

• LO.Entailment.NO = LO.Entailment.N_of_CO LO.Entailment.C_id

@[simp]

theorem LO.Entailment.NO! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] [NegationEquiv 𝓢] [HasAxiomAndElim 𝓢] : 𝓢 ⊢ ∼⊥

def LO.Entailment.mdp₁ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ : F} [HasAxiomImplyS 𝓢] (bqr : 𝓢 ⊢! φ 🡒 ψ 🡒 χ) (bq : 𝓢 ⊢! φ 🡒 ψ) : 𝓢 ⊢! φ 🡒 χ

Equations

• bqr⨀₁bq = LO.Entailment.implyS⨀!bqr⨀!bq

theorem LO.Entailment.mdp₁! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ : F} [HasAxiomImplyS 𝓢] (hqr : 𝓢 ⊢ φ 🡒 ψ 🡒 χ) (hq : 𝓢 ⊢ φ 🡒 ψ) : 𝓢 ⊢ φ 🡒 χ

def LO.Entailment.«term_⨀₁_» : Lean.TrailingParserDescr

Equations

• LO.Entailment.«term_⨀₁_» = Lean.ParserDescr.trailingNode `LO.Entailment.«term_⨀₁_» 90 90 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⨀₁") (Lean.ParserDescr.cat `term 91))

def LO.Entailment.«term_⨀₁__1» : Lean.TrailingParserDescr

Equations

• LO.Entailment.«term_⨀₁__1» = Lean.ParserDescr.trailingNode `LO.Entailment.«term_⨀₁__1» 90 90 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⨀₁") (Lean.ParserDescr.cat `term 91))

def LO.Entailment.mdp₂ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ s : F} [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (bqr : 𝓢 ⊢! φ 🡒 ψ 🡒 χ 🡒 s) (bq : 𝓢 ⊢! φ 🡒 ψ 🡒 χ) : 𝓢 ⊢! φ 🡒 ψ 🡒 s

Equations

• bqr⨀₂bq = LO.Entailment.C_of_conseq LO.Entailment.implyS⨀₁bqr⨀₁bq

theorem LO.Entailment.mdp₂! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ s : F} [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (hqr : 𝓢 ⊢ φ 🡒 ψ 🡒 χ 🡒 s) (hq : 𝓢 ⊢ φ 🡒 ψ 🡒 χ) : 𝓢 ⊢ φ 🡒 ψ 🡒 s

def LO.Entailment.«term_⨀₂_» : Lean.TrailingParserDescr

Equations

• LO.Entailment.«term_⨀₂_» = Lean.ParserDescr.trailingNode `LO.Entailment.«term_⨀₂_» 90 90 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⨀₂") (Lean.ParserDescr.cat `term 91))

def LO.Entailment.«term_⨀₂__1» : Lean.TrailingParserDescr

Equations

• LO.Entailment.«term_⨀₂__1» = Lean.ParserDescr.trailingNode `LO.Entailment.«term_⨀₂__1» 90 90 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⨀₂") (Lean.ParserDescr.cat `term 91))

def LO.Entailment.mdp₃ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ s t : F} [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (bqr : 𝓢 ⊢! φ 🡒 ψ 🡒 χ 🡒 s 🡒 t) (bq : 𝓢 ⊢! φ 🡒 ψ 🡒 χ 🡒 s) : 𝓢 ⊢! φ 🡒 ψ 🡒 χ 🡒 t

Equations

• bqr⨀₃bq = LO.Entailment.C_of_conseq (LO.Entailment.C_of_conseq LO.Entailment.implyS)⨀₂bqr⨀₂bq

theorem LO.Entailment.mdp₃! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ s t : F} [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (hqr : 𝓢 ⊢ φ 🡒 ψ 🡒 χ 🡒 s 🡒 t) (hq : 𝓢 ⊢ φ 🡒 ψ 🡒 χ 🡒 s) : 𝓢 ⊢ φ 🡒 ψ 🡒 χ 🡒 t

def LO.Entailment.«term_⨀₃_» : Lean.TrailingParserDescr

Equations

• LO.Entailment.«term_⨀₃_» = Lean.ParserDescr.trailingNode `LO.Entailment.«term_⨀₃_» 90 90 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⨀₃") (Lean.ParserDescr.cat `term 91))

def LO.Entailment.«term_⨀₃__1» : Lean.TrailingParserDescr

Equations

• LO.Entailment.«term_⨀₃__1» = Lean.ParserDescr.trailingNode `LO.Entailment.«term_⨀₃__1» 90 90 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⨀₃") (Lean.ParserDescr.cat `term 91))

def LO.Entailment.mdp₄ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ s t u : F} [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (bqr : 𝓢 ⊢! φ 🡒 ψ 🡒 χ 🡒 s 🡒 t 🡒 u) (bq : 𝓢 ⊢! φ 🡒 ψ 🡒 χ 🡒 s 🡒 t) : 𝓢 ⊢! φ 🡒 ψ 🡒 χ 🡒 s 🡒 u

Equations

• bqr⨀₄bq = LO.Entailment.C_of_conseq (LO.Entailment.C_of_conseq (LO.Entailment.C_of_conseq LO.Entailment.implyS))⨀₃bqr⨀₃bq

theorem LO.Entailment.mdp₄! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ s t u : F} [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (hqr : 𝓢 ⊢ φ 🡒 ψ 🡒 χ 🡒 s 🡒 t 🡒 u) (hq : 𝓢 ⊢ φ 🡒 ψ 🡒 χ 🡒 s 🡒 t) : 𝓢 ⊢ φ 🡒 ψ 🡒 χ 🡒 s 🡒 u

def LO.Entailment.«term_⨀₄_» : Lean.TrailingParserDescr

Equations

• LO.Entailment.«term_⨀₄_» = Lean.ParserDescr.trailingNode `LO.Entailment.«term_⨀₄_» 90 90 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⨀₄") (Lean.ParserDescr.cat `term 91))

def LO.Entailment.«term_⨀₄__1» : Lean.TrailingParserDescr

Equations

• LO.Entailment.«term_⨀₄__1» = Lean.ParserDescr.trailingNode `LO.Entailment.«term_⨀₄__1» 90 90 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⨀₄") (Lean.ParserDescr.cat `term 91))

def LO.Entailment.C_trans {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ : F} [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (bpq : 𝓢 ⊢! φ 🡒 ψ) (bqr : 𝓢 ⊢! ψ 🡒 χ) : 𝓢 ⊢! φ 🡒 χ

Equations

• LO.Entailment.C_trans bpq bqr = LO.Entailment.implyS⨀!LO.Entailment.C_of_conseq bqr⨀!bpq

theorem LO.Entailment.C!_trans {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ : F} [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (hpq : 𝓢 ⊢ φ 🡒 ψ) (hqr : 𝓢 ⊢ ψ 🡒 χ) : 𝓢 ⊢ φ 🡒 χ

def LO.Entailment.C_replace {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {ψ₁ φ₁ φ₂ ψ₂ : F} [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (h₁ : 𝓢 ⊢! ψ₁ 🡒 φ₁) (h₂ : 𝓢 ⊢! φ₂ 🡒 ψ₂) : 𝓢 ⊢! φ₁ 🡒 φ₂ → 𝓢 ⊢! ψ₁ 🡒 ψ₂

Equations

• LO.Entailment.C_replace h₁ h₂ h = LO.Entailment.C_trans h₁ (LO.Entailment.C_trans h h₂)

theorem LO.Entailment.C!_replace {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {ψ₁ φ₁ φ₂ ψ₂ : F} [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (h₁ : 𝓢 ⊢ ψ₁ 🡒 φ₁) (h₂ : 𝓢 ⊢ φ₂ 🡒 ψ₂) : 𝓢 ⊢ φ₁ 🡒 φ₂ → 𝓢 ⊢ ψ₁ 🡒 ψ₂

def LO.Entailment.E_replace {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ₁ ψ₁ φ₂ ψ₂ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (h₁ : 𝓢 ⊢! φ₁ 🡘 ψ₁) (h₂ : 𝓢 ⊢! φ₂ 🡘 ψ₂) (h₃ : 𝓢 ⊢! φ₁ 🡘 φ₂) : 𝓢 ⊢! ψ₁ 🡘 ψ₂

Equations

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

theorem LO.Entailment.E!_replace {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ₁ ψ₁ φ₂ ψ₂ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] : 𝓢 ⊢ φ₁ 🡘 ψ₁ → 𝓢 ⊢ φ₂ 🡘 ψ₂ → 𝓢 ⊢ φ₁ 🡘 φ₂ → 𝓢 ⊢ ψ₁ 🡘 ψ₂

def LO.Entailment.E_trans {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (h₁ : 𝓢 ⊢! φ 🡘 ψ) (h₂ : 𝓢 ⊢! ψ 🡘 χ) : 𝓢 ⊢! φ 🡘 χ

Equations

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

theorem LO.Entailment.E!_trans {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (h₁ : 𝓢 ⊢ φ 🡘 ψ) (h₂ : 𝓢 ⊢ ψ 🡘 χ) : 𝓢 ⊢ φ 🡘 χ

def LO.Entailment.CCCC {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ : F} [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] : 𝓢 ⊢! φ 🡒 ψ 🡒 χ 🡒 φ

Equations

• LO.Entailment.CCCC = LO.Entailment.C_trans LO.Entailment.implyK LO.Entailment.implyK

theorem LO.Entailment.CCCC! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ : F} [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] : 𝓢 ⊢ φ 🡒 ψ 🡒 χ 🡒 φ

def LO.Entailment.CK_of_C_of_C {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (bq : 𝓢 ⊢! φ 🡒 ψ) (br : 𝓢 ⊢! φ 🡒 χ) : 𝓢 ⊢! φ 🡒 ψ ⋏ χ

Equations

• LO.Entailment.CK_of_C_of_C bq br = LO.Entailment.C_of_conseq LO.Entailment.and₃⨀₁bq⨀₁br

theorem LO.Entailment.CK!_of_C!_of_C! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (hq : 𝓢 ⊢ φ 🡒 ψ) (hr : 𝓢 ⊢ φ 🡒 χ) : 𝓢 ⊢ φ 🡒 ψ ⋏ χ

def LO.Entailment.CKK {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] : 𝓢 ⊢! φ ⋏ ψ 🡒 ψ ⋏ φ

Equations

• LO.Entailment.CKK = LO.Entailment.CK_of_C_of_C LO.Entailment.and₂ LO.Entailment.and₁

@[simp]

theorem LO.Entailment.CKK! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] : 𝓢 ⊢ φ ⋏ ψ 🡒 ψ ⋏ φ

def LO.Entailment.K_symm {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (h : 𝓢 ⊢! φ ⋏ ψ) : 𝓢 ⊢! ψ ⋏ φ

Equations

• LO.Entailment.K_symm h = LO.Entailment.CKK⨀!h

theorem LO.Entailment.K!_symm {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (h : 𝓢 ⊢ φ ⋏ ψ) : 𝓢 ⊢ ψ ⋏ φ

def LO.Entailment.CEE {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] : 𝓢 ⊢! φ 🡘 ψ 🡒 ψ 🡘 φ

Equations

• LO.Entailment.CEE = LO.Entailment.CKK

@[simp]

theorem LO.Entailment.CEE! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] : 𝓢 ⊢ φ 🡘 ψ 🡒 ψ 🡘 φ

def LO.Entailment.E_symm {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (h : 𝓢 ⊢! φ 🡘 ψ) : 𝓢 ⊢! ψ 🡘 φ

Equations

• LO.Entailment.E_symm h = LO.Entailment.CEE⨀!h

theorem LO.Entailment.E!_symm {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (h : 𝓢 ⊢ φ 🡘 ψ) : 𝓢 ⊢ ψ 🡘 φ

def LO.Entailment.ECKCC {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] : 𝓢 ⊢! (φ ⋏ ψ 🡒 χ) 🡘 (φ 🡒 ψ 🡒 χ)

Equations

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

@[simp]

theorem LO.Entailment.ECKCC! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] : 𝓢 ⊢ (φ ⋏ ψ 🡒 χ) 🡘 (φ 🡒 ψ 🡒 χ)

def LO.Entailment.CC_of_CK {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (d : 𝓢 ⊢! φ ⋏ ψ 🡒 χ) : 𝓢 ⊢! φ 🡒 ψ 🡒 χ

Equations

• LO.Entailment.CC_of_CK d = LO.Entailment.K_left LO.Entailment.ECKCC⨀!d

def LO.Entailment.CK_of_CC {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (d : 𝓢 ⊢! φ 🡒 ψ 🡒 χ) : 𝓢 ⊢! φ ⋏ ψ 🡒 χ

Equations

• LO.Entailment.CK_of_CC d = LO.Entailment.K_right LO.Entailment.ECKCC⨀!d

theorem LO.Entailment.CK!_iff_CC! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] : 𝓢 ⊢ φ ⋏ ψ 🡒 χ ↔ 𝓢 ⊢ φ 🡒 ψ 🡒 χ

def LO.Entailment.CV {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ : F} [HasAxiomVerum 𝓢] [HasAxiomImplyK 𝓢] : 𝓢 ⊢! φ 🡒 ⊤

Equations

• LO.Entailment.CV = LO.Entailment.C_of_conseq LO.Entailment.verum

@[simp]

theorem LO.Entailment.CV! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ : F} [HasAxiomImplyK 𝓢] [HasAxiomVerum 𝓢] : 𝓢 ⊢ φ 🡒 ⊤

theorem LO.Entailment.unprovable_C!_trans {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ : F} [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (hpq : 𝓢 ⊢ φ 🡒 ψ) : 𝓢 ⊬ φ 🡒 χ → 𝓢 ⊬ ψ 🡒 χ

theorem LO.Entailment.uniff_of_E! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] (H : 𝓢 ⊢ φ 🡘 ψ) : 𝓢 ⊬ φ ↔ 𝓢 ⊬ ψ

def LO.Entailment.conj₂Nth {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] (Γ : List F) (n : ℕ) (hn : n < Γ.length) : 𝓢 ⊢! ⋀Γ 🡒 Γ[n]

Equations

• LO.Entailment.conj₂Nth [] x x_1 = ⋯.elim
• LO.Entailment.conj₂Nth [ψ] 0 x_3 = LO.Entailment.C_id
• LO.Entailment.conj₂Nth (φ :: ψ :: Γ) 0 x_3 = LO.Entailment.and₁
• LO.Entailment.conj₂Nth (φ :: ψ :: Γ) n.succ hn = LO.Entailment.C_trans LO.Entailment.and₂ (LO.Entailment.conj₂Nth (ψ :: Γ) n ⋯)

def LO.Entailment.conj₂_nth! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] (Γ : List F) (n : ℕ) (hn : n < Γ.length) : 𝓢 ⊢ ⋀Γ 🡒 Γ[n]

Equations

• ⋯ = ⋯

def LO.Entailment.left_Conj_intro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] {Γ : List F} {φ : F} (h : φ ∈ Γ) : 𝓢 ⊢! Γ.conj 🡒 φ

Equations

• LO.Entailment.left_Conj_intro h_2 = ⋯.elim
• LO.Entailment.left_Conj_intro h_2 = if e : φ = ψ then e ▸ LO.Entailment.and₁ else have this := ⋯; LO.Entailment.C_trans LO.Entailment.and₂ (LO.Entailment.left_Conj_intro this)

theorem LO.Entailment.left_Conj!_intro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} {Γ : List F} [DecidableEq F] (h : φ ∈ Γ) : 𝓢 ⊢ Γ.conj 🡒 φ

def LO.Entailment.Conj_intro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] (Γ : List F) (b : (φ : F) → φ ∈ Γ → 𝓢 ⊢! φ) : 𝓢 ⊢! Γ.conj

Equations

• LO.Entailment.Conj_intro [] b_2 = LO.Entailment.verum
• LO.Entailment.Conj_intro (ψ :: Γ_2) b_2 = LO.Entailment.K_intro (b_2 ψ ⋯) (LO.Entailment.Conj_intro Γ_2 fun (ψ_1 : F) (hq : ψ_1 ∈ Γ_2) => b_2 ψ_1 ⋯)

theorem LO.Entailment.Conj!_intro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {Γ : List F} (b : ∀ φ ∈ Γ, 𝓢 ⊢ φ) : 𝓢 ⊢ Γ.conj

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

Equations

• LO.Entailment.right_Conj_intro φ [] b_2 = LO.Entailment.C_of_conseq LO.Entailment.verum
• LO.Entailment.right_Conj_intro φ (ψ :: Γ_2) b_2 = LO.Entailment.CK_of_C_of_C (b_2 ψ ⋯) (LO.Entailment.right_Conj_intro φ Γ_2 fun (ψ_1 : F) (hq : ψ_1 ∈ Γ_2) => b_2 ψ_1 ⋯)

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

Equations

• ⋯ = ⋯

def LO.Entailment.CConjConj {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {Γ Δ : List F} [DecidableEq F] (h : Δ ⊆ Γ) : 𝓢 ⊢! Γ.conj 🡒 Δ.conj

Equations

• LO.Entailment.CConjConj h = LO.Entailment.right_Conj_intro Γ.conj Δ fun (x : F) (hq : x ∈ Δ) => LO.Entailment.left_Conj_intro ⋯

def LO.Entailment.left_Conj₂_intro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] {Γ : List F} {φ : F} (h : φ ∈ Γ) : 𝓢 ⊢! ⋀Γ 🡒 φ

Equations

• LO.Entailment.left_Conj₂_intro h = LO.Entailment.cast (LO.Entailment.conj₂Nth Γ (List.idxOf φ Γ) ⋯) ⋯

theorem LO.Entailment.left_Conj₂!_intro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} {Γ : List F} [DecidableEq F] (h : φ ∈ Γ) : 𝓢 ⊢ ⋀Γ 🡒 φ

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

Equations

• LO.Entailment.Conj₂_intro [] b_2 = LO.Entailment.verum
• LO.Entailment.Conj₂_intro [ψ] b_2 = b_2 (⋀[ψ]) ⋯
• LO.Entailment.Conj₂_intro (ψ :: χ :: Γ_2) b_2 = LO.Entailment.K_intro (b_2 ψ ⋯) (LO.Entailment.Conj₂_intro (χ :: Γ_2) fun (φ_1 : F) (a : φ_1 ∈ χ :: Γ_2) => b_2 φ_1 ⋯)

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

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

Equations

• LO.Entailment.right_Conj₂_intro φ [] b_2 = LO.Entailment.C_of_conseq LO.Entailment.verum
• LO.Entailment.right_Conj₂_intro φ [ψ] b_2 = b_2 (⋀[ψ]) ⋯
• LO.Entailment.right_Conj₂_intro φ (ψ :: χ :: Γ_2) b_2 = LO.Entailment.CK_of_C_of_C (b_2 ψ ⋯) (LO.Entailment.right_Conj₂_intro φ (χ :: Γ_2) fun (ψ_1 : F) (hq : ψ_1 ∈ χ :: Γ_2) => b_2 ψ_1 ⋯)

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

def LO.Entailment.CConj₂Conj₂ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] {Γ Δ : List F} (h : Δ ⊆ Γ) : 𝓢 ⊢! ⋀Γ 🡒 ⋀Δ

Equations

• LO.Entailment.CConj₂Conj₂ h = LO.Entailment.right_Conj₂_intro (⋀Γ) Δ fun (x : F) (hq : x ∈ Δ) => LO.Entailment.left_Conj₂_intro ⋯

theorem LO.Entailment.CConj₂_Conj₂! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] {Γ Δ : List F} (h : Δ ⊆ Γ) : 𝓢 ⊢ ⋀Γ 🡒 ⋀Δ

@[reducible, inline]

abbrev LO.Entailment.Minimal.ofEquiv {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {G : Type u_3} {T : Type u_4} [Entailment T G] [LogicalConnective G] (𝓢 : S) [Entailment.Minimal 𝓢] (𝓣 : T) (f : G →ˡᶜ F) (e : (φ : G) → 𝓢 ⊢! f φ ≃ 𝓣 ⊢! φ) : Entailment.Minimal 𝓣

Equations

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

structure LO.Entailment.FiniteContext {S : Sort u_1} (F : Type u_2) (𝓢 : S) : Type u_2

• ctx : List F

@[implicit_reducible]

instance LO.Entailment.FiniteContext.instCoeList {F : Type u_1} {S : Sort u_2} {𝓢 : S} : Coe (List F) (FiniteContext F 𝓢)

Equations

• LO.Entailment.FiniteContext.instCoeList = { coe := LO.Entailment.FiniteContext.mk }

@[reducible, inline]

abbrev LO.Entailment.FiniteContext.conj {F : Type u_1} {S : Sort u_2} {𝓢 : S} [LogicalConnective F] (Γ : FiniteContext F 𝓢) : F

Equations

• Γ.conj = ⋀Γ.ctx

@[reducible, inline]

abbrev LO.Entailment.FiniteContext.disj {F : Type u_1} {S : Sort u_2} {𝓢 : S} [LogicalConnective F] (Γ : FiniteContext F 𝓢) : F

Equations

• Γ.disj = ⋁Γ.ctx

@[implicit_reducible]

instance LO.Entailment.FiniteContext.instEmptyCollection {F : Type u_1} {S : Sort u_2} {𝓢 : S} : EmptyCollection (FiniteContext F 𝓢)

Equations

• LO.Entailment.FiniteContext.instEmptyCollection = { emptyCollection := { ctx := [] } }

@[implicit_reducible]

instance LO.Entailment.FiniteContext.instMembership {F : Type u_1} {S : Sort u_2} {𝓢 : S} : Membership F (FiniteContext F 𝓢)

Equations

• LO.Entailment.FiniteContext.instMembership = { mem := fun (Γ : LO.Entailment.FiniteContext F 𝓢) (x : F) => x ∈ Γ.ctx }

@[implicit_reducible]

instance LO.Entailment.FiniteContext.instHasSubset {F : Type u_1} {S : Sort u_2} {𝓢 : S} : HasSubset (FiniteContext F 𝓢)

Equations

• LO.Entailment.FiniteContext.instHasSubset = { Subset := fun (x1 x2 : LO.Entailment.FiniteContext F 𝓢) => x1.ctx ⊆ x2.ctx }

@[implicit_reducible]

instance LO.Entailment.FiniteContext.instAdjoin {F : Type u_1} {S : Sort u_2} {𝓢 : S} : Adjoin F (FiniteContext F 𝓢)

Equations

• LO.Entailment.FiniteContext.instAdjoin = { adjoin := fun (x1 : F) (x2 : LO.Entailment.FiniteContext F 𝓢) => { ctx := x1 :: x2.ctx } }

theorem LO.Entailment.FiniteContext.mem_def {F : Type u_2} {S : Sort u_1} {𝓢 : S} {φ : F} {Γ : FiniteContext F 𝓢} : φ ∈ Γ ↔ φ ∈ Γ.ctx

@[simp]

theorem LO.Entailment.FiniteContext.coe_subset_coe_iff {F : Type u_1} {S : Sort u_2} {𝓢 : S} {Γ Δ : List F} : { ctx := Γ } ⊆ { ctx := Δ } ↔ Γ ⊆ Δ

@[simp]

theorem LO.Entailment.FiniteContext.mem_coe_iff {F : Type u_1} {S : Sort u_2} {𝓢 : S} {φ : F} {Γ : List F} : φ ∈ { ctx := Γ } ↔ φ ∈ Γ

@[simp]

theorem LO.Entailment.FiniteContext.not_mem_empty {F : Type u_1} {S : Sort u_2} {𝓢 : S} (φ : F) : φ ∉ ∅

@[implicit_reducible]

instance LO.Entailment.FiniteContext.instAdjunctiveSet {F : Type u_1} {S : Sort u_2} {𝓢 : S} : AdjunctiveSet F (FiniteContext F 𝓢)

Equations

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

@[implicit_reducible]

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

Equations

• LO.Entailment.FiniteContext.inst 𝓢 = { Prf := fun (x1 : LO.Entailment.FiniteContext F 𝓢) (x2 : F) => 𝓢 ⊢! x1.conj 🡒 x2 }

@[reducible, inline]

abbrev LO.Entailment.FiniteContext.Prf {F : Type u_1} {S : Type u_2} [Entailment S F] [LogicalConnective F] (𝓢 : S) (Γ : List F) (φ : F) : Type u_3

Equations

• (Γ ⊢[𝓢]! φ) = ({ ctx := Γ } ⊢! φ)

@[reducible, inline]

abbrev LO.Entailment.FiniteContext.Provable {F : Type u_1} {S : Type u_2} [Entailment S F] [LogicalConnective F] (𝓢 : S) (Γ : List F) (φ : F) : Prop

Equations

• (Γ ⊢[𝓢] φ) = ({ ctx := Γ } ⊢ φ)

@[reducible, inline]

abbrev LO.Entailment.FiniteContext.Unprovable {F : Type u_1} {S : Type u_2} [Entailment S F] [LogicalConnective F] (𝓢 : S) (Γ : List F) (φ : F) : Prop

Equations

• (Γ ⊬[𝓢] φ) = ({ ctx := Γ } ⊬ φ)

@[reducible, inline]

abbrev LO.Entailment.FiniteContext.PrfSet {F : Type u_1} {S : Type u_2} [Entailment S F] [LogicalConnective F] (𝓢 : S) (Γ : List F) (s : Set F) : Type (max u_3 u_1)

Equations

• (Γ ⊢[𝓢]!* s) = ({ ctx := Γ } ⊢!* s)

@[reducible, inline]

abbrev LO.Entailment.FiniteContext.ProvableSet {F : Type u_1} {S : Type u_2} [Entailment S F] [LogicalConnective F] (𝓢 : S) (Γ : List F) (s : Set F) : Prop

Equations

• (Γ ⊢[𝓢]* s) = ({ ctx := Γ } ⊢* s)

def LO.Entailment.FiniteContext.«term_⊢[_]!_» : Lean.TrailingParserDescr

Equations

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

def LO.Entailment.FiniteContext.«term_⊢[_]_» : Lean.TrailingParserDescr

Equations

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

def LO.Entailment.FiniteContext.«term_⊬[_]_» : Lean.TrailingParserDescr

Equations

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

def LO.Entailment.FiniteContext.«term_⊢[_]!*_» : Lean.TrailingParserDescr

Equations

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

def LO.Entailment.FiniteContext.«term_⊢[_]*_» : Lean.TrailingParserDescr

Equations

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

theorem LO.Entailment.FiniteContext.entailment_def {F : Type u_2} {S : Type u_1} {𝓢 : S} [Entailment S F] [LogicalConnective F] (Γ : FiniteContext F 𝓢) (φ : F) : (Γ ⊢! φ) = (𝓢 ⊢! Γ.conj 🡒 φ)

def LO.Entailment.FiniteContext.ofDef {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] {Γ : List F} {φ : F} (b : 𝓢 ⊢! ⋀Γ 🡒 φ) : Γ ⊢[𝓢]! φ

Equations

• LO.Entailment.FiniteContext.ofDef b = b

def LO.Entailment.FiniteContext.toDef {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] {Γ : List F} {φ : F} (b : Γ ⊢[𝓢]! φ) : 𝓢 ⊢! ⋀Γ 🡒 φ

Equations

• LO.Entailment.FiniteContext.toDef b = b

theorem LO.Entailment.FiniteContext.toₛ! {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] {Γ : List F} {φ : F} (b : Γ ⊢[𝓢] φ) : 𝓢 ⊢ ⋀Γ 🡒 φ

theorem LO.Entailment.FiniteContext.provable_iff {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] {Γ : List F} {φ : F} : Γ ⊢[𝓢] φ ↔ 𝓢 ⊢ ⋀Γ 🡒 φ

def LO.Entailment.FiniteContext.cast {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] {Γ' : List F} {φ' : F} {Γ : List F} {φ : F} (d : Γ ⊢[𝓢]! φ) (eΓ : Γ = Γ') (eφ : φ = φ') : Γ' ⊢[𝓢]! φ'

Equations

• LO.Entailment.FiniteContext.cast d eΓ eφ = eΓ ▸ eφ ▸ d

@[implicit_reducible]

instance LO.Entailment.FiniteContext.instAxiomatizedOfDecidableEq {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [Entailment.Minimal 𝓢] [DecidableEq F] : Axiomatized (FiniteContext F 𝓢)

Equations

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

@[implicit_reducible]

instance LO.Entailment.FiniteContext.instCompact {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] : Compact (FiniteContext F 𝓢)

Equations

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

def LO.Entailment.FiniteContext.nthAxm {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [Entailment.Minimal 𝓢] {Γ : List F} (n : ℕ) (h : n < Γ.length := by simp) : Γ ⊢[𝓢]! Γ[n]

Equations

• LO.Entailment.FiniteContext.nthAxm n h = LO.Entailment.conj₂Nth Γ n h

theorem LO.Entailment.FiniteContext.nth_axm! {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [Entailment.Minimal 𝓢] {Γ : List F} (n : ℕ) (h : n < Γ.length := by simp) : Γ ⊢[𝓢] Γ[n]

def LO.Entailment.FiniteContext.byAxm {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] {Γ : List F} [Entailment.Minimal 𝓢] [DecidableEq F] {φ : F} (h : φ ∈ Γ := by simp) : Γ ⊢[𝓢]! φ

Equations

• LO.Entailment.FiniteContext.byAxm h = LO.Entailment.Axiomatized.prfAxm ⋯

theorem LO.Entailment.FiniteContext.by_axm! {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] {Γ : List F} [Entailment.Minimal 𝓢] [DecidableEq F] {φ : F} (h : φ ∈ Γ := by simp) : Γ ⊢[𝓢] φ

def LO.Entailment.FiniteContext.weakening {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] {Γ Δ : List F} [Entailment.Minimal 𝓢] [DecidableEq F] (h : Γ ⊆ Δ) {φ : F} : Γ ⊢[𝓢]! φ → Δ ⊢[𝓢]! φ

Equations

• LO.Entailment.FiniteContext.weakening h = LO.Entailment.Axiomatized.weakening ⋯

theorem LO.Entailment.FiniteContext.weakening! {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] {Γ Δ : List F} [Entailment.Minimal 𝓢] [DecidableEq F] (h : Γ ⊆ Δ) {φ : F} : Γ ⊢[𝓢] φ → Δ ⊢[𝓢] φ

def LO.Entailment.FiniteContext.of {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] {Γ : List F} [Entailment.Minimal 𝓢] {φ : F} (b : 𝓢 ⊢! φ) : Γ ⊢[𝓢]! φ

Equations

• LO.Entailment.FiniteContext.of b = LO.Entailment.C_of_conseq b

def LO.Entailment.FiniteContext.emptyPrf {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [Entailment.Minimal 𝓢] {φ : F} : [] ⊢[𝓢]! φ → 𝓢 ⊢! φ

Equations

• LO.Entailment.FiniteContext.emptyPrf b = b⨀!LO.Entailment.verum

def LO.Entailment.FiniteContext.provable_iff_provable {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [Entailment.Minimal 𝓢] {φ : F} : 𝓢 ⊢ φ ↔ [] ⊢[𝓢] φ

Equations

• ⋯ = ⋯

theorem LO.Entailment.FiniteContext.of'! {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] {Γ : List F} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] (h : 𝓢 ⊢ φ) : Γ ⊢[𝓢] φ

def LO.Entailment.FiniteContext.id {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [Entailment.Minimal 𝓢] {φ : F} : [φ] ⊢[𝓢]! φ

Equations

• LO.Entailment.FiniteContext.id = LO.Entailment.FiniteContext.nthAxm 0 ⋯

@[simp]

theorem LO.Entailment.FiniteContext.id! {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [Entailment.Minimal 𝓢] {φ : F} : [φ] ⊢[𝓢] φ

def LO.Entailment.FiniteContext.byAxm₀ {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] {Γ : List F} [Entailment.Minimal 𝓢] {φ : F} : (φ :: Γ) ⊢[𝓢]! φ

Equations

• LO.Entailment.FiniteContext.byAxm₀ = LO.Entailment.FiniteContext.nthAxm 0 ⋯

theorem LO.Entailment.FiniteContext.by_axm₀! {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] {Γ : List F} [Entailment.Minimal 𝓢] {φ : F} : (φ :: Γ) ⊢[𝓢] φ

def LO.Entailment.FiniteContext.byAxm₁ {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] {Γ : List F} [Entailment.Minimal 𝓢] {φ ψ : F} : (φ :: ψ :: Γ) ⊢[𝓢]! ψ

Equations

• LO.Entailment.FiniteContext.byAxm₁ = LO.Entailment.FiniteContext.nthAxm 1 ⋯

theorem LO.Entailment.FiniteContext.by_axm₁! {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] {Γ : List F} [Entailment.Minimal 𝓢] {φ ψ : F} : (φ :: ψ :: Γ) ⊢[𝓢] ψ

def LO.Entailment.FiniteContext.byAxm₂ {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] {Γ : List F} [Entailment.Minimal 𝓢] {φ ψ χ : F} : (φ :: ψ :: χ :: Γ) ⊢[𝓢]! χ

Equations

• LO.Entailment.FiniteContext.byAxm₂ = LO.Entailment.FiniteContext.nthAxm 2 ⋯

theorem LO.Entailment.FiniteContext.by_axm₂! {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] {Γ : List F} [Entailment.Minimal 𝓢] {φ ψ χ : F} : (φ :: ψ :: χ :: Γ) ⊢[𝓢] χ

@[implicit_reducible]

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

Equations

• Γ.instModusPonens = { mdp := fun {φ ψ : F} => LO.Entailment.mdp₁ }

@[implicit_reducible]

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

Equations

• Γ.instHasAxiomVerum = { verum := LO.Entailment.FiniteContext.of LO.Entailment.verum }

@[implicit_reducible]

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

Equations

• Γ.instHasAxiomImplyK = { implyK := fun {φ ψ : F} => LO.Entailment.FiniteContext.of LO.Entailment.implyK }

@[implicit_reducible]

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

Equations

• Γ.instHasAxiomImplyS = { implyS := fun {φ ψ χ : F} => LO.Entailment.FiniteContext.of LO.Entailment.implyS }

@[implicit_reducible]

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

Equations

• Γ.instHasAxiomAndElim = { and₁ := fun {φ ψ : F} => LO.Entailment.FiniteContext.of LO.Entailment.and₁, and₂ := fun {φ ψ : F} => LO.Entailment.FiniteContext.of LO.Entailment.and₂ }

@[implicit_reducible]

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

Equations

• Γ.instHasAxiomAndInst = { and₃ := fun {φ ψ : F} => LO.Entailment.FiniteContext.of LO.Entailment.and₃ }

@[implicit_reducible]

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

Equations

• Γ.instHasAxiomOrInst = { or₁ := fun {φ ψ : F} => LO.Entailment.FiniteContext.of LO.Entailment.or₁, or₂ := fun {φ ψ : F} => LO.Entailment.FiniteContext.of LO.Entailment.or₂ }

@[implicit_reducible]

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

Equations

• Γ.instHasAxiomOrElim = { or₃ := fun {φ ψ χ : F} => LO.Entailment.FiniteContext.of LO.Entailment.or₃ }

@[implicit_reducible]

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

Equations

• Γ.instNegationEquiv = { negEquiv := fun {φ : F} => LO.Entailment.FiniteContext.of LO.Entailment.negEquiv }

@[implicit_reducible]

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

Equations

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

def LO.Entailment.FiniteContext.mdp' {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] {Γ Δ : List F} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] (bΓ : Γ ⊢[𝓢]! φ 🡒 ψ) (bΔ : Δ ⊢[𝓢]! φ) : (Γ ++ Δ) ⊢[𝓢]! ψ

Equations

• LO.Entailment.FiniteContext.mdp' bΓ bΔ = LO.Entailment.wk ⋯ bΓ⨀!LO.Entailment.wk ⋯ bΔ

def LO.Entailment.FiniteContext.deduct {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [Entailment.Minimal 𝓢] {φ ψ : F} {Γ : List F} : (φ :: Γ) ⊢[𝓢]! ψ → Γ ⊢[𝓢]! φ 🡒 ψ

Equations

• One or more equations did not get rendered due to their size.
• LO.Entailment.FiniteContext.deduct = fun (b : [φ] ⊢[𝓢]! ψ) => LO.Entailment.FiniteContext.ofDef (LO.Entailment.C_of_conseq (LO.Entailment.FiniteContext.toDef b))

theorem LO.Entailment.FiniteContext.deduct! {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] {Γ : List F} [Entailment.Minimal 𝓢] {φ ψ : F} (h : (φ :: Γ) ⊢[𝓢] ψ) : Γ ⊢[𝓢] φ 🡒 ψ

def LO.Entailment.FiniteContext.deductInv {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [Entailment.Minimal 𝓢] {φ ψ : F} {Γ : List F} : Γ ⊢[𝓢]! φ 🡒 ψ → (φ :: Γ) ⊢[𝓢]! ψ

Equations

• One or more equations did not get rendered due to their size.
• LO.Entailment.FiniteContext.deductInv = fun (b : [] ⊢[𝓢]! φ 🡒 ψ) => LO.Entailment.FiniteContext.ofDef (LO.Entailment.FiniteContext.toDef b⨀!LO.Entailment.verum)

theorem LO.Entailment.FiniteContext.deductInv! {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] {Γ : List F} [Entailment.Minimal 𝓢] {φ ψ : F} (h : Γ ⊢[𝓢] φ 🡒 ψ) : (φ :: Γ) ⊢[𝓢] ψ

theorem LO.Entailment.FiniteContext.deduct_iff {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [Entailment.Minimal 𝓢] {φ ψ : F} {Γ : List F} : Γ ⊢[𝓢] φ 🡒 ψ ↔ (φ :: Γ) ⊢[𝓢] ψ

def LO.Entailment.FiniteContext.deduct' {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [Entailment.Minimal 𝓢] {φ ψ : F} : [φ] ⊢[𝓢]! ψ → 𝓢 ⊢! φ 🡒 ψ

Equations

• LO.Entailment.FiniteContext.deduct' b = LO.Entailment.FiniteContext.emptyPrf (LO.Entailment.FiniteContext.deduct b)

theorem LO.Entailment.FiniteContext.deduct'! {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [Entailment.Minimal 𝓢] {φ ψ : F} (h : [φ] ⊢[𝓢] ψ) : 𝓢 ⊢ φ 🡒 ψ

def LO.Entailment.FiniteContext.deductInv' {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢! φ 🡒 ψ → [φ] ⊢[𝓢]! ψ

Equations

• LO.Entailment.FiniteContext.deductInv' b = LO.Entailment.FiniteContext.deductInv (LO.Entailment.FiniteContext.of b)

theorem LO.Entailment.FiniteContext.deductInv'! {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [Entailment.Minimal 𝓢] {φ ψ : F} (h : 𝓢 ⊢ φ 🡒 ψ) : [φ] ⊢[𝓢] ψ

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance LO.Entailment.FiniteContext.instStrongCutOfDecidableEq {F : Type u_1} {S : Type u_2} {𝓢 : S} [Entailment S F] [LogicalConnective F] [Entailment.Minimal 𝓢] [DecidableEq F] : StrongCut (FiniteContext F 𝓢) (FiniteContext F 𝓢)

Equations

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

structure LO.Entailment.Context (F : Type u_1) {S : Sort u_2} (𝓢 : S) : Type u_1

• ctx : Set F

@[implicit_reducible]

instance LO.Entailment.Context.instCoeSet {S : Sort u_1} {F : Type u_2} {𝓢 : S} : Coe (Set F) (Context F 𝓢)

Equations

• LO.Entailment.Context.instCoeSet = { coe := LO.Entailment.Context.mk }

@[implicit_reducible]

instance LO.Entailment.Context.instEmptyCollection {S : Sort u_1} {F : Type u_2} {𝓢 : S} : EmptyCollection (Context F 𝓢)

Equations

• LO.Entailment.Context.instEmptyCollection = { emptyCollection := { ctx := ∅ } }

@[implicit_reducible]

instance LO.Entailment.Context.instMembership {S : Sort u_1} {F : Type u_2} {𝓢 : S} : Membership F (Context F 𝓢)

Equations

• LO.Entailment.Context.instMembership = { mem := fun (Γ : LO.Entailment.Context F 𝓢) (x : F) => x ∈ Γ.ctx }

@[implicit_reducible]

instance LO.Entailment.Context.instHasSubset {S : Sort u_1} {F : Type u_2} {𝓢 : S} : HasSubset (Context F 𝓢)

Equations

• LO.Entailment.Context.instHasSubset = { Subset := fun (x1 x2 : LO.Entailment.Context F 𝓢) => x1.ctx ⊆ x2.ctx }

@[implicit_reducible]

instance LO.Entailment.Context.instAdjoin {S : Sort u_1} {F : Type u_2} {𝓢 : S} : Adjoin F (Context F 𝓢)

Equations

• LO.Entailment.Context.instAdjoin = { adjoin := fun (x1 : F) (x2 : LO.Entailment.Context F 𝓢) => { ctx := insert x1 x2.ctx } }

theorem LO.Entailment.Context.mem_def {S : Sort u_2} {F : Type u_1} {𝓢 : S} {φ : F} {Γ : Context F 𝓢} : φ ∈ Γ ↔ φ ∈ Γ.ctx

@[simp]

theorem LO.Entailment.Context.coe_subset_coe_iff {S : Sort u_2} {F : Type u_1} {𝓢 : S} {Γ Δ : Set F} : { ctx := Γ } ⊆ { ctx := Δ } ↔ Γ ⊆ Δ

@[simp]

theorem LO.Entailment.Context.mem_coe_iff {S : Sort u_2} {F : Type u_1} {𝓢 : S} {φ : F} {Γ : Set F} : φ ∈ { ctx := Γ } ↔ φ ∈ Γ

@[simp]

theorem LO.Entailment.Context.not_mem_empty {S : Sort u_2} {F : Type u_1} {𝓢 : S} (φ : F) : φ ∉ ∅

@[implicit_reducible]

instance LO.Entailment.Context.instAdjunctiveSet {S : Sort u_1} {F : Type u_2} {𝓢 : S} : AdjunctiveSet F (Context F 𝓢)

Equations

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

structure LO.Entailment.Context.Proof {S : Type u_1} {F : Type u_2} {𝓢 : S} [LogicalConnective F] [Entailment S F] (Γ : Context F 𝓢) (φ : F) : Type (max u_2 u_3)

• ctx : List F
• subset (ψ : F) : ψ ∈ self.ctx → ψ ∈ Γ
• prf : self.ctx ⊢[𝓢]! φ

@[implicit_reducible]

instance LO.Entailment.Context.inst {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] (𝓢 : S) : Entailment (Context F 𝓢) F

Equations

• LO.Entailment.Context.inst 𝓢 = { Prf := LO.Entailment.Context.Proof }

@[reducible, inline]

abbrev LO.Entailment.Context.Prf {S : Type u_1} {F : Type u_2} (𝓢 : S) [LogicalConnective F] [Entailment S F] (Γ : Set F) (φ : F) : Type (max u_2 u_3)

Equations

• (Γ *⊢[𝓢]! φ) = ({ ctx := Γ } ⊢! φ)

@[reducible, inline]

abbrev LO.Entailment.Context.Provable {S : Type u_1} {F : Type u_2} (𝓢 : S) [LogicalConnective F] [Entailment S F] (Γ : Set F) (φ : F) : Prop

Equations

• (Γ *⊢[𝓢] φ) = ({ ctx := Γ } ⊢ φ)

@[reducible, inline]

abbrev LO.Entailment.Context.Unprovable {S : Type u_1} {F : Type u_2} (𝓢 : S) [LogicalConnective F] [Entailment S F] (Γ : Set F) (φ : F) : Prop

Equations

• (Γ *⊬[𝓢] φ) = ({ ctx := Γ } ⊬ φ)

@[reducible, inline]

abbrev LO.Entailment.Context.PrfSet {S : Type u_1} {F : Type u_2} (𝓢 : S) [LogicalConnective F] [Entailment S F] (Γ s : Set F) : Type (max u_2 u_3)

Equations

• (Γ *⊢[𝓢]!* s) = ({ ctx := Γ } ⊢!* s)

@[reducible, inline]

abbrev LO.Entailment.Context.ProvableSet {S : Type u_1} {F : Type u_2} (𝓢 : S) [LogicalConnective F] [Entailment S F] (Γ s : Set F) : Prop

Equations

• (Γ *⊢[𝓢]* s) = ({ ctx := Γ } ⊢* s)

def LO.Entailment.Context.«term_*⊢[_]!_» : Lean.TrailingParserDescr

Equations

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

def LO.Entailment.Context.«term_*⊢[_]_» : Lean.TrailingParserDescr

Equations

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

def LO.Entailment.Context.«term_*⊬[_]_» : Lean.TrailingParserDescr

Equations

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

def LO.Entailment.Context.«term_*⊢[_]!*_» : Lean.TrailingParserDescr

Equations

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

def LO.Entailment.Context.«term_*⊢[_]*_» : Lean.TrailingParserDescr

Equations

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

theorem LO.Entailment.Context.provable_iff {S : Type u_2} {F : Type u_1} {𝓢 : S} [LogicalConnective F] [Entailment S F] {Γ : Set F} {φ : F} : Γ *⊢[𝓢] φ ↔ ∃ (Δ : List F), (∀ ψ ∈ Δ, ψ ∈ Γ) ∧ Δ ⊢[𝓢] φ

@[implicit_reducible]

instance LO.Entailment.Context.instAxiomatizedOfDecidableEq {S : Type u_1} {F : Type u_2} {𝓢 : S} [LogicalConnective F] [Entailment S F] [Entailment.Minimal 𝓢] [DecidableEq F] : Axiomatized (Context F 𝓢)

Equations

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

def LO.Entailment.Context.byAxm {S : Type u_1} {F : Type u_2} {𝓢 : S} [LogicalConnective F] [Entailment S F] [Entailment.Minimal 𝓢] [DecidableEq F] {Γ : Set F} {φ : F} (h : φ ∈ Γ) : Γ *⊢[𝓢]! φ

Equations

• LO.Entailment.Context.byAxm h = LO.Entailment.Axiomatized.prfAxm ⋯

theorem LO.Entailment.Context.by_axm {S : Type u_2} {F : Type u_1} {𝓢 : S} [LogicalConnective F] [Entailment S F] [Entailment.Minimal 𝓢] [DecidableEq F] {Γ : Set F} {φ : F} (h : φ ∈ Γ) : Γ *⊢[𝓢] φ

@[implicit_reducible]

instance LO.Entailment.Context.instCompact {S : Type u_1} {F : Type u_2} {𝓢 : S} [LogicalConnective F] [Entailment S F] : Compact (Context F 𝓢)

Equations

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

def LO.Entailment.Context.deduct {S : Type u_1} {F : Type u_2} {𝓢 : S} [LogicalConnective F] [Entailment S F] [Entailment.Minimal 𝓢] [DecidableEq F] {φ ψ : F} {Γ : Set F} : insert φ Γ *⊢[𝓢]! ψ → Γ *⊢[𝓢]! φ 🡒 ψ

Equations

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

theorem LO.Entailment.Context.deduct! {S : Type u_2} {F : Type u_1} {𝓢 : S} [LogicalConnective F] [Entailment S F] [Entailment.Minimal 𝓢] {φ : F} {Γ : Set F} {ψ : F} [DecidableEq F] (h : insert φ Γ *⊢[𝓢] ψ) : Γ *⊢[𝓢] φ 🡒 ψ

def LO.Entailment.Context.deductInv {S : Type u_1} {F : Type u_2} {𝓢 : S} [LogicalConnective F] [Entailment S F] [Entailment.Minimal 𝓢] {φ ψ : F} {Γ : Set F} : Γ *⊢[𝓢]! φ 🡒 ψ → insert φ Γ *⊢[𝓢]! ψ

Equations

• LO.Entailment.Context.deductInv { ctx := Δ, subset := h, prf := b } = { ctx := φ :: Δ, subset := ⋯, prf := LO.Entailment.FiniteContext.deductInv b }

theorem LO.Entailment.Context.deductInv! {S : Type u_2} {F : Type u_1} {𝓢 : S} [LogicalConnective F] [Entailment S F] [Entailment.Minimal 𝓢] {Γ : Set F} {φ ψ : F} [DecidableEq F] (h : Γ *⊢[𝓢] φ 🡒 ψ) : insert φ Γ *⊢[𝓢] ψ

@[implicit_reducible]

instance LO.Entailment.Context.deduction {S : Type u_1} {F : Type u_2} {𝓢 : S} [LogicalConnective F] [Entailment S F] [Entailment.Minimal 𝓢] [DecidableEq F] : Deduction (Context F 𝓢)

Equations

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

def LO.Entailment.Context.weakening {S : Type u_1} {F : Type u_2} {𝓢 : S} [LogicalConnective F] [Entailment S F] [Entailment.Minimal 𝓢] {Γ Δ : Set F} [DecidableEq F] (h : Γ ⊆ Δ) {φ : F} : Γ *⊢[𝓢]! φ → Δ *⊢[𝓢]! φ

Equations

• LO.Entailment.Context.weakening h = LO.Entailment.Axiomatized.weakening ⋯

theorem LO.Entailment.Context.weakening! {S : Type u_2} {F : Type u_1} {𝓢 : S} [LogicalConnective F] [Entailment S F] [Entailment.Minimal 𝓢] {Γ Δ : Set F} [DecidableEq F] (h : Γ ⊆ Δ) {φ : F} : Γ *⊢[𝓢] φ → Δ *⊢[𝓢] φ

def LO.Entailment.Context.of {S : Type u_1} {F : Type u_2} {𝓢 : S} [LogicalConnective F] [Entailment S F] [Entailment.Minimal 𝓢] {Γ : Set F} {φ : F} (b : 𝓢 ⊢! φ) : Γ *⊢[𝓢]! φ

Equations

• LO.Entailment.Context.of b = { ctx := [], subset := ⋯, prf := LO.Entailment.FiniteContext.of b }

theorem LO.Entailment.Context.of! {S : Type u_2} {F : Type u_1} {𝓢 : S} [LogicalConnective F] [Entailment S F] [Entailment.Minimal 𝓢] {φ : F} {Γ : Set F} (b : 𝓢 ⊢ φ) : Γ *⊢[𝓢] φ

def LO.Entailment.Context.mdp {S : Type u_1} {F : Type u_2} {𝓢 : S} [LogicalConnective F] [Entailment S F] [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] {Γ : Set F} (bpq : Γ *⊢[𝓢]! φ 🡒 ψ) (bp : Γ *⊢[𝓢]! φ) : Γ *⊢[𝓢]! ψ

Equations

• LO.Entailment.Context.mdp bpq bp = { ctx := bpq.ctx ++ bp.ctx, subset := ⋯, prf := LO.Entailment.FiniteContext.mdp' bpq.prf bp.prf }

theorem LO.Entailment.Context.by_axm! {S : Type u_2} {F : Type u_1} {𝓢 : S} [LogicalConnective F] [Entailment S F] [Entailment.Minimal 𝓢] {Γ : Set F} {φ : F} [DecidableEq F] (h : φ ∈ Γ) : Γ *⊢[𝓢] φ

def LO.Entailment.Context.emptyPrf {S : Type u_1} {F : Type u_2} {𝓢 : S} [LogicalConnective F] [Entailment S F] [Entailment.Minimal 𝓢] {φ : F} : ∅ *⊢[𝓢]! φ → 𝓢 ⊢! φ

Equations

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

theorem LO.Entailment.Context.emptyPrf! {S : Type u_1} {F : Type u_2} {𝓢 : S} [LogicalConnective F] [Entailment S F] [Entailment.Minimal 𝓢] {φ : F} : ∅ *⊢[𝓢] φ → 𝓢 ⊢ φ

theorem LO.Entailment.Context.provable_iff_provable {S : Type u_2} {F : Type u_1} {𝓢 : S} [LogicalConnective F] [Entailment S F] [Entailment.Minimal 𝓢] {φ : F} : 𝓢 ⊢ φ ↔ ∅ *⊢[𝓢] φ

theorem LO.Entailment.Context.iff_provable_context_provable_finiteContext_toList {S : Type u_2} {F : Type u_1} {𝓢 : S} [LogicalConnective F] [Entailment S F] [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] {Δ : Finset F} : ↑Δ *⊢[𝓢] φ ↔ Δ.toList ⊢[𝓢] φ

@[implicit_reducible]

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

Equations

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

@[simp]

theorem LO.Entailment.CONV! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] : 𝓢 ⊢ ⊤ 🡒 ∼⊥

def LO.Entailment.innerMDP {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] : 𝓢 ⊢! φ ⋏ (φ 🡒 ψ) 🡒 ψ

Equations

• LO.Entailment.innerMDP = LO.Entailment.FiniteContext.deduct' (have hp := LO.Entailment.FiniteContext.byAxm ⋯; have hpq := LO.Entailment.FiniteContext.byAxm ⋯; hpq⨀!hp)

theorem LO.Entailment.inner_mdp! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] : 𝓢 ⊢ φ ⋏ (φ 🡒 ψ) 🡒 ψ

def LO.Entailment.bot_of_mem_either {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} {Γ : List F} [DecidableEq F] (h₁ : φ ∈ Γ) (h₂ : ∼φ ∈ Γ) : Γ ⊢[𝓢]! ⊥

Equations

• LO.Entailment.bot_of_mem_either h₁ h₂ = LO.Entailment.CO_of_N (LO.Entailment.FiniteContext.byAxm h₂)⨀!LO.Entailment.FiniteContext.byAxm h₁

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

def LO.Entailment.negMDP {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} (hnp : 𝓢 ⊢! ∼φ) (hn : 𝓢 ⊢! φ) : 𝓢 ⊢! ⊥

Equations

• LO.Entailment.negMDP hnp hn = LO.Entailment.CO_of_N hnp⨀!hn

theorem LO.Entailment.neg_mdp {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} (hnp : 𝓢 ⊢ ∼φ) (hn : 𝓢 ⊢ φ) : 𝓢 ⊢ ⊥

def LO.Entailment.right_A_intro_left {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢! φ 🡒 χ) : 𝓢 ⊢! φ 🡒 χ ⋎ ψ

Equations

• LO.Entailment.right_A_intro_left h = LO.Entailment.FiniteContext.deduct' (LO.Entailment.A_intro_left (LO.Entailment.FiniteContext.deductInv (LO.Entailment.FiniteContext.of h)))

theorem LO.Entailment.right_A!_intro_left {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ φ 🡒 χ) : 𝓢 ⊢ φ 🡒 χ ⋎ ψ

def LO.Entailment.right_A_intro_right {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢! ψ 🡒 χ) : 𝓢 ⊢! ψ 🡒 φ ⋎ χ

Equations

• LO.Entailment.right_A_intro_right h = LO.Entailment.FiniteContext.deduct' (LO.Entailment.A_intro_right (LO.Entailment.FiniteContext.deductInv (LO.Entailment.FiniteContext.of h)))

theorem LO.Entailment.right_A!_intro_right {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ ψ 🡒 χ) : 𝓢 ⊢ ψ 🡒 φ ⋎ χ

def LO.Entailment.right_K_intro {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} [DecidableEq F] (hq : 𝓢 ⊢! φ 🡒 ψ) (hr : 𝓢 ⊢! φ 🡒 χ) : 𝓢 ⊢! φ 🡒 ψ ⋏ χ

Equations

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

theorem LO.Entailment.right_K!_intro {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} [DecidableEq F] (hq : 𝓢 ⊢ φ 🡒 ψ) (hr : 𝓢 ⊢ φ 🡒 χ) : 𝓢 ⊢ φ 🡒 ψ ⋏ χ

theorem LO.Entailment.left_K!_symm {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (d : 𝓢 ⊢ φ ⋏ ψ 🡒 χ) : 𝓢 ⊢ ψ ⋏ φ 🡒 χ

theorem LO.Entailment.left_K!_intro_right {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} [DecidableEq F] (h : 𝓢 ⊢ φ 🡒 χ) : 𝓢 ⊢ ψ ⋏ φ 🡒 χ

theorem LO.Entailment.left_K!_intro_left {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} [DecidableEq F] (h : 𝓢 ⊢ φ 🡒 χ) : 𝓢 ⊢ φ ⋏ ψ 🡒 χ

theorem LO.Entailment.cut! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ₁ φ₂ ψ₁ ψ₂ c : F} [DecidableEq F] (d₁ : 𝓢 ⊢ φ₁ ⋏ c 🡒 ψ₁) (d₂ : 𝓢 ⊢ φ₂ 🡒 c ⋎ ψ₂) : 𝓢 ⊢ φ₁ ⋏ φ₂ 🡒 ψ₁ ⋎ ψ₂

def LO.Entailment.inner_A_symm {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢! φ ⋎ ψ 🡒 ψ ⋎ φ

Equations

• LO.Entailment.inner_A_symm = LO.Entailment.FiniteContext.deduct' (LO.Entailment.of_C_of_C_of_A LO.Entailment.or₂ LO.Entailment.or₁ LO.Entailment.FiniteContext.id)

theorem LO.Entailment.or_comm! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢ φ ⋎ ψ 🡒 ψ ⋎ φ

def LO.Entailment.A_symm {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} (h : 𝓢 ⊢! φ ⋎ ψ) : 𝓢 ⊢! ψ ⋎ φ

Equations

• LO.Entailment.A_symm h = LO.Entailment.inner_A_symm⨀!h

theorem LO.Entailment.or_comm'! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} (h : 𝓢 ⊢ φ ⋎ ψ) : 𝓢 ⊢ ψ ⋎ φ

theorem LO.Entailment.A!_assoc {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} : 𝓢 ⊢ φ ⋎ ψ ⋎ χ ↔ 𝓢 ⊢ (φ ⋎ ψ) ⋎ χ

theorem LO.Entailment.K!_assoc {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} : 𝓢 ⊢ (φ ⋏ ψ) ⋏ χ 🡘 φ ⋏ ψ ⋏ χ

theorem LO.Entailment.K!_assoc_mp {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ (φ ⋏ ψ) ⋏ χ) : 𝓢 ⊢ φ ⋏ ψ ⋏ χ

theorem LO.Entailment.K!_assoc_mpr {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ φ ⋏ ψ ⋏ χ) : 𝓢 ⊢ (φ ⋏ ψ) ⋏ χ

def LO.Entailment.K_replace_left {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (hc : 𝓢 ⊢! φ ⋏ ψ) (h : 𝓢 ⊢! φ 🡒 χ) : 𝓢 ⊢! χ ⋏ ψ

Equations

• LO.Entailment.K_replace_left hc h = LO.Entailment.K_intro (h⨀!LO.Entailment.K_left hc) (LO.Entailment.K_right hc)

theorem LO.Entailment.K!_replace_left {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (hc : 𝓢 ⊢ φ ⋏ ψ) (h : 𝓢 ⊢ φ 🡒 χ) : 𝓢 ⊢ χ ⋏ ψ

def LO.Entailment.CKK_of_C {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢! φ 🡒 χ) : 𝓢 ⊢! φ ⋏ ψ 🡒 χ ⋏ ψ

Equations

• LO.Entailment.CKK_of_C h = LO.Entailment.FiniteContext.deduct' (LO.Entailment.K_replace_left LO.Entailment.FiniteContext.id (LO.Entailment.FiniteContext.of h))

theorem LO.Entailment.CKK!_of_C! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ φ 🡒 χ) : 𝓢 ⊢ φ ⋏ ψ 🡒 χ ⋏ ψ

def LO.Entailment.K_replace_right {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (hc : 𝓢 ⊢! φ ⋏ ψ) (h : 𝓢 ⊢! ψ 🡒 χ) : 𝓢 ⊢! φ ⋏ χ

Equations

• LO.Entailment.K_replace_right hc h = LO.Entailment.K_intro (LO.Entailment.K_left hc) (h⨀!LO.Entailment.K_right hc)

theorem LO.Entailment.K!_replace_right {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (hc : 𝓢 ⊢ φ ⋏ ψ) (h : 𝓢 ⊢ ψ 🡒 χ) : 𝓢 ⊢ φ ⋏ χ

def LO.Entailment.CKK_of_C' {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢! ψ 🡒 χ) : 𝓢 ⊢! φ ⋏ ψ 🡒 φ ⋏ χ

Equations

• LO.Entailment.CKK_of_C' h = LO.Entailment.FiniteContext.deduct' (LO.Entailment.K_replace_right LO.Entailment.FiniteContext.id (LO.Entailment.FiniteContext.of h))

theorem LO.Entailment.CKK!_of_C!' {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ ψ 🡒 χ) : 𝓢 ⊢ φ ⋏ ψ 🡒 φ ⋏ χ

def LO.Entailment.K_replace {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ ξ : F} (hc : 𝓢 ⊢! φ ⋏ ψ) (h₁ : 𝓢 ⊢! φ 🡒 χ) (h₂ : 𝓢 ⊢! ψ 🡒 ξ) : 𝓢 ⊢! χ ⋏ ξ

Equations

• LO.Entailment.K_replace hc h₁ h₂ = LO.Entailment.K_replace_right (LO.Entailment.K_replace_left hc h₁) h₂

theorem LO.Entailment.K!_replace {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ ξ : F} (hc : 𝓢 ⊢ φ ⋏ ψ) (h₁ : 𝓢 ⊢ φ 🡒 χ) (h₂ : 𝓢 ⊢ ψ 🡒 ξ) : 𝓢 ⊢ χ ⋏ ξ

def LO.Entailment.CKK_of_C_of_C {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ ξ : F} (h₁ : 𝓢 ⊢! φ 🡒 χ) (h₂ : 𝓢 ⊢! ψ 🡒 ξ) : 𝓢 ⊢! φ ⋏ ψ 🡒 χ ⋏ ξ

Equations

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

theorem LO.Entailment.CKK!_of_C!_of_C! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ ξ : F} (h₁ : 𝓢 ⊢ φ 🡒 χ) (h₂ : 𝓢 ⊢ ψ 🡒 ξ) : 𝓢 ⊢ φ ⋏ ψ 🡒 χ ⋏ ξ

def LO.Entailment.A_replace_left {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (hc : 𝓢 ⊢! φ ⋎ ψ) (hp : 𝓢 ⊢! φ 🡒 χ) : 𝓢 ⊢! χ ⋎ ψ

Equations

• LO.Entailment.A_replace_left hc hp = LO.Entailment.of_C_of_C_of_A (LO.Entailment.C_trans hp LO.Entailment.or₁) LO.Entailment.or₂ hc

theorem LO.Entailment.A!_replace_left {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (hc : 𝓢 ⊢ φ ⋎ ψ) (hp : 𝓢 ⊢ φ 🡒 χ) : 𝓢 ⊢ χ ⋎ ψ

def LO.Entailment.CAA_of_C_left {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (hp : 𝓢 ⊢! φ 🡒 χ) : 𝓢 ⊢! φ ⋎ ψ 🡒 χ ⋎ ψ

Equations

• LO.Entailment.CAA_of_C_left hp = LO.Entailment.FiniteContext.deduct' (LO.Entailment.A_replace_left LO.Entailment.FiniteContext.id (LO.Entailment.FiniteContext.of hp))

theorem LO.Entailment.A_replace_left! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (hp : 𝓢 ⊢ φ 🡒 χ) : 𝓢 ⊢ φ ⋎ ψ 🡒 χ ⋎ ψ

def LO.Entailment.A_replace_right {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (hc : 𝓢 ⊢! φ ⋎ ψ) (hq : 𝓢 ⊢! ψ 🡒 χ) : 𝓢 ⊢! φ ⋎ χ

Equations

• LO.Entailment.A_replace_right hc hq = LO.Entailment.of_C_of_C_of_A LO.Entailment.or₁ (LO.Entailment.C_trans hq LO.Entailment.or₂) hc

theorem LO.Entailment.A!_replace_right {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (hc : 𝓢 ⊢ φ ⋎ ψ) (hq : 𝓢 ⊢ ψ 🡒 χ) : 𝓢 ⊢ φ ⋎ χ

def LO.Entailment.CAA_of_C_right {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (hq : 𝓢 ⊢! ψ 🡒 χ) : 𝓢 ⊢! φ ⋎ ψ 🡒 φ ⋎ χ

Equations

• LO.Entailment.CAA_of_C_right hq = LO.Entailment.FiniteContext.deduct' (LO.Entailment.A_replace_right LO.Entailment.FiniteContext.id (LO.Entailment.FiniteContext.of hq))

theorem LO.Entailment.CAA!_of_C!_right {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (hq : 𝓢 ⊢ ψ 🡒 χ) : 𝓢 ⊢ φ ⋎ ψ 🡒 φ ⋎ χ

def LO.Entailment.A_replace {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ₁ φ₂ ψ₁ ψ₂ : F} (h : 𝓢 ⊢! φ₁ ⋎ ψ₁) (hp : 𝓢 ⊢! φ₁ 🡒 φ₂) (hq : 𝓢 ⊢! ψ₁ 🡒 ψ₂) : 𝓢 ⊢! φ₂ ⋎ ψ₂

Equations

• LO.Entailment.A_replace h hp hq = LO.Entailment.A_replace_right (LO.Entailment.A_replace_left h hp) hq

theorem LO.Entailment.A!_replace {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ₁ φ₂ ψ₁ ψ₂ : F} (h : 𝓢 ⊢ φ₁ ⋎ ψ₁) (hp : 𝓢 ⊢ φ₁ 🡒 φ₂) (hq : 𝓢 ⊢ ψ₁ 🡒 ψ₂) : 𝓢 ⊢ φ₂ ⋎ ψ₂

def LO.Entailment.CAA_of_C_of_C {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ₁ φ₂ ψ₁ ψ₂ : F} (hp : 𝓢 ⊢! φ₁ 🡒 φ₂) (hq : 𝓢 ⊢! ψ₁ 🡒 ψ₂) : 𝓢 ⊢! φ₁ ⋎ ψ₁ 🡒 φ₂ ⋎ ψ₂

Equations

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

theorem LO.Entailment.CAA!_of_C!_of_C! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ₁ φ₂ ψ₁ ψ₂ : F} (hp : 𝓢 ⊢ φ₁ 🡒 φ₂) (hq : 𝓢 ⊢ ψ₁ 🡒 ψ₂) : 𝓢 ⊢ φ₁ ⋎ ψ₁ 🡒 φ₂ ⋎ ψ₂

def LO.Entailment.EAA_of_E_of_E {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ₁ φ₂ ψ₁ ψ₂ : F} (hp : 𝓢 ⊢! φ₁ 🡘 φ₂) (hq : 𝓢 ⊢! ψ₁ 🡘 ψ₂) : 𝓢 ⊢! φ₁ ⋎ ψ₁ 🡘 φ₂ ⋎ ψ₂

Equations

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

theorem LO.Entailment.EAA!_of_E!_of_E! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ₁ φ₂ ψ₁ ψ₂ : F} (hp : 𝓢 ⊢ φ₁ 🡘 φ₂) (hq : 𝓢 ⊢ ψ₁ 🡘 ψ₂) : 𝓢 ⊢ φ₁ ⋎ ψ₁ 🡘 φ₂ ⋎ ψ₂

theorem LO.Entailment.EAAAA! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} : 𝓢 ⊢ φ ⋎ ψ ⋎ χ 🡘 (φ ⋎ ψ) ⋎ χ

theorem LO.Entailment.EAA!_of_E!_right {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (d : 𝓢 ⊢ ψ 🡘 χ) : 𝓢 ⊢ φ ⋎ ψ 🡘 φ ⋎ χ

theorem LO.Entailment.EAA!_of_E!_left {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (d : 𝓢 ⊢ φ 🡘 χ) : 𝓢 ⊢ φ ⋎ ψ 🡘 χ ⋎ ψ

def LO.Entailment.EKK_of_E_of_E {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ₁ φ₂ ψ₁ ψ₂ : F} (hp : 𝓢 ⊢! φ₁ 🡘 φ₂) (hq : 𝓢 ⊢! ψ₁ 🡘 ψ₂) : 𝓢 ⊢! φ₁ ⋏ ψ₁ 🡘 φ₂ ⋏ ψ₂

Equations

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

theorem LO.Entailment.EKK!_of_E!_of_E! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ₁ φ₂ ψ₁ ψ₂ : F} (hp : 𝓢 ⊢ φ₁ 🡘 φ₂) (hq : 𝓢 ⊢ ψ₁ 🡘 ψ₂) : 𝓢 ⊢ φ₁ ⋏ ψ₁ 🡘 φ₂ ⋏ ψ₂

def LO.Entailment.ECC_of_E_of_E {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ₁ φ₂ ψ₁ ψ₂ : F} (hp : 𝓢 ⊢! φ₁ 🡘 φ₂) (hq : 𝓢 ⊢! ψ₁ 🡘 ψ₂) : 𝓢 ⊢! (φ₁ 🡒 ψ₁) 🡘 (φ₂ 🡒 ψ₂)

Equations

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

theorem LO.Entailment.ECC!_of_E!_of_E! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ₁ φ₂ ψ₁ ψ₂ : F} (hp : 𝓢 ⊢ φ₁ 🡘 φ₂) (hq : 𝓢 ⊢ ψ₁ 🡘 ψ₂) : 𝓢 ⊢ (φ₁ 🡒 ψ₁) 🡘 (φ₂ 🡒 ψ₂)

theorem LO.Entailment.C!_repalce {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ₁ φ₂ ψ₁ ψ₂ : F} [DecidableEq F] (hp : 𝓢 ⊢ φ₁ 🡘 φ₂) (hq : 𝓢 ⊢ ψ₁ 🡘 ψ₂) : 𝓢 ⊢ φ₁ 🡒 ψ₁ ↔ 𝓢 ⊢ φ₂ 🡒 ψ₂

def LO.Entailment.dni {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] : 𝓢 ⊢! φ 🡒 ∼∼φ

Equations

• LO.Entailment.dni = LO.Entailment.FiniteContext.deduct' (LO.Entailment.N_of_CO (LO.Entailment.FiniteContext.deduct (LO.Entailment.bot_of_mem_either ⋯ ⋯)))

@[simp]

theorem LO.Entailment.dni! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] : 𝓢 ⊢ φ 🡒 ∼∼φ

def LO.Entailment.dni' {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] (b : 𝓢 ⊢! φ) : 𝓢 ⊢! ∼∼φ

Equations

• LO.Entailment.dni' b = LO.Entailment.dni⨀!b

theorem LO.Entailment.dni'! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] (b : 𝓢 ⊢ φ) : 𝓢 ⊢ ∼∼φ

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

Equations

• LO.Entailment.ANNNN_of_A d = LO.Entailment.of_C_of_C_of_A (LO.Entailment.C_trans LO.Entailment.dni LO.Entailment.or₁) (LO.Entailment.C_trans LO.Entailment.dni LO.Entailment.or₂) d

theorem LO.Entailment.ANNNN!_of_A! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] (d : 𝓢 ⊢ φ ⋎ ψ) : 𝓢 ⊢ ∼∼φ ⋎ ∼∼ψ

def LO.Entailment.KNNNN_of_K {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] (d : 𝓢 ⊢! φ ⋏ ψ) : 𝓢 ⊢! ∼∼φ ⋏ ∼∼ψ

Equations

• LO.Entailment.KNNNN_of_K d = LO.Entailment.K_intro (LO.Entailment.dni' (LO.Entailment.K_left d)) (LO.Entailment.dni' (LO.Entailment.K_right d))

theorem LO.Entailment.KNNNN!_of_K! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] (d : 𝓢 ⊢ φ ⋏ ψ) : 𝓢 ⊢ ∼∼φ ⋏ ∼∼ψ

def LO.Entailment.CNNOO {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] : 𝓢 ⊢! ∼∼⊥ 🡒 ⊥

Equations

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

def LO.Entailment.ENNOO {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] : 𝓢 ⊢! ∼∼⊥ 🡘 ⊥

Equations

• LO.Entailment.ENNOO = LO.Entailment.K_intro LO.Entailment.CNNOO LO.Entailment.dni

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

Equations

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

@[simp]

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

Equations

• ⋯ = ⋯

@[deprecated LO.Entailment.CCCNN "use `CCCNN`" (since := "2026-07-20")]

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

Alias of LO.Entailment.CCCNN.

Equations

• @LO.Entailment.contra₀ = @LO.Entailment.CCCNN

@[deprecated LO.Entailment.CCCNN! "use `CCCNN!`" (since := "2026-07-20")]

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

Alias of LO.Entailment.CCCNN!.

Equations

• @LO.Entailment.contra₀! = @LO.Entailment.CCCNN!

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

Equations

• LO.Entailment.contra b = LO.Entailment.CCCNN⨀!b

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

@[deprecated LO.Entailment.contra "use `contra`" (since := "2026-07-20")]

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

Alias of LO.Entailment.contra.

Equations

• @LO.Entailment.contra₀' = @LO.Entailment.contra

@[deprecated LO.Entailment.contra! "use `contra!`" (since := "2026-07-20")]

theorem LO.Entailment.contra₀'! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] (b : 𝓢 ⊢ φ 🡒 ψ) : 𝓢 ⊢ ∼ψ 🡒 ∼φ

Alias of LO.Entailment.contra!.

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

Equations

• LO.Entailment.CNNNN_of_C b = LO.Entailment.contra (LO.Entailment.contra b)

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

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

Equations

• LO.Entailment.CCCNNNN = LO.Entailment.FiniteContext.deduct' (LO.Entailment.CNNNN_of_C LO.Entailment.FiniteContext.id)

@[simp]

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

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

Equations

• LO.Entailment.CN_of_CN_right b = LO.Entailment.C_trans LO.Entailment.dni (LO.Entailment.contra b)

theorem LO.Entailment.CN!_of_CN!_right {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] (b : 𝓢 ⊢ φ 🡒 ∼ψ) : 𝓢 ⊢ ψ 🡒 ∼φ

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

Equations

• LO.Entailment.CCNCN = LO.Entailment.FiniteContext.deduct' (LO.Entailment.CN_of_CN_right LO.Entailment.FiniteContext.id)

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

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

Equations

• LO.Entailment.ENN_of_E b = LO.Entailment.E_intro (LO.Entailment.contra (LO.Entailment.K_right b)) (LO.Entailment.contra (LO.Entailment.K_left b))

theorem LO.Entailment.ENN!_of_E! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] (b : 𝓢 ⊢ φ 🡘 ψ) : 𝓢 ⊢ ∼φ 🡘 ∼ψ

def LO.Entailment.ENNCCOO {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] : 𝓢 ⊢! ∼∼φ 🡘 ((φ 🡒 ⊥) 🡒 ⊥)

Equations

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

@[simp]

theorem LO.Entailment.ENNCCOO! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] : 𝓢 ⊢ ∼∼φ 🡘 ((φ 🡒 ⊥) 🡒 ⊥)

def LO.Entailment.tne {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] : 𝓢 ⊢! ∼∼∼φ 🡒 ∼φ

Equations

• LO.Entailment.tne = LO.Entailment.contra LO.Entailment.dni

@[simp]

theorem LO.Entailment.tne! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] : 𝓢 ⊢ ∼∼∼φ 🡒 ∼φ

def LO.Entailment.tne' {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] (b : 𝓢 ⊢! ∼∼∼φ) : 𝓢 ⊢! ∼φ

Equations

• LO.Entailment.tne' b = LO.Entailment.tne⨀!b

theorem LO.Entailment.tne'! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] (b : 𝓢 ⊢ ∼∼∼φ) : 𝓢 ⊢ ∼φ

def LO.Entailment.tneIff {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] : 𝓢 ⊢! ∼∼∼φ 🡘 ∼φ

Equations

• LO.Entailment.tneIff = LO.Entailment.K_intro LO.Entailment.tne LO.Entailment.dni

def LO.Entailment.CCC_of_C_left {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢! ψ 🡒 φ) : 𝓢 ⊢! (φ 🡒 χ) 🡒 ψ 🡒 χ

Equations

• LO.Entailment.CCC_of_C_left h = LO.Entailment.FiniteContext.deduct' (LO.Entailment.C_trans (LO.Entailment.FiniteContext.of h) LO.Entailment.FiniteContext.id)

theorem LO.Entailment.CCC!_of_C!_left {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ ψ 🡒 φ) : 𝓢 ⊢ (φ 🡒 χ) 🡒 ψ 🡒 χ

@[deprecated LO.Entailment.CCC_of_C_left "use `CCC_of_C_left`" (since := "2026-07-20")]

def LO.Entailment.rev_dhyp_imp' {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢! ψ 🡒 φ) : 𝓢 ⊢! (φ 🡒 χ) 🡒 ψ 🡒 χ

Alias of LO.Entailment.CCC_of_C_left.

Equations

• @LO.Entailment.rev_dhyp_imp' = @LO.Entailment.CCC_of_C_left

@[deprecated LO.Entailment.CCC!_of_C!_left "use `CCC!_of_C!_left`" (since := "2026-07-20")]

theorem LO.Entailment.rev_dhyp_imp'! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ ψ 🡒 φ) : 𝓢 ⊢ (φ 🡒 χ) 🡒 ψ 🡒 χ

Alias of LO.Entailment.CCC!_of_C!_left.

theorem LO.Entailment.C!_iff_C!_of_iff_left {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ φ 🡘 ψ) : 𝓢 ⊢ φ 🡒 χ ↔ 𝓢 ⊢ ψ 🡒 χ

theorem LO.Entailment.C!_iff_C!_of_iff_right {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ φ 🡘 ψ) : 𝓢 ⊢ χ 🡒 φ ↔ 𝓢 ⊢ χ 🡒 ψ

def LO.Entailment.C_swap {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} [DecidableEq F] (h : 𝓢 ⊢! φ 🡒 ψ 🡒 χ) : 𝓢 ⊢! ψ 🡒 φ 🡒 χ

Equations

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

theorem LO.Entailment.C!_swap {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} [DecidableEq F] (h : 𝓢 ⊢ φ 🡒 ψ 🡒 χ) : 𝓢 ⊢ ψ 🡒 φ 🡒 χ

def LO.Entailment.CCCCC {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} [DecidableEq F] : 𝓢 ⊢! (φ 🡒 ψ 🡒 χ) 🡒 ψ 🡒 φ 🡒 χ

Equations

• LO.Entailment.CCCCC = LO.Entailment.FiniteContext.deduct' (LO.Entailment.C_swap LO.Entailment.FiniteContext.id)

@[simp]

theorem LO.Entailment.CCCCC! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} [DecidableEq F] : 𝓢 ⊢ (φ 🡒 ψ 🡒 χ) 🡒 ψ 🡒 φ 🡒 χ

def LO.Entailment.C_of_CC {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] (h : 𝓢 ⊢! φ 🡒 φ 🡒 ψ) : 𝓢 ⊢! φ 🡒 ψ

Equations

• LO.Entailment.C_of_CC h = LO.Entailment.FiniteContext.deduct' (have this := LO.Entailment.FiniteContext.of h; this⨀!LO.Entailment.FiniteContext.byAxm ⋯⨀!LO.Entailment.FiniteContext.byAxm ⋯)

theorem LO.Entailment.C!_of_CC! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] (h : 𝓢 ⊢ φ 🡒 φ 🡒 ψ) : 𝓢 ⊢ φ 🡒 ψ

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

Equations

• LO.Entailment.CCC = LO.Entailment.C_swap LO.Entailment.C_id

theorem LO.Entailment.CCC! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] : 𝓢 ⊢ φ 🡒 (φ 🡒 ψ) 🡒 ψ

def LO.Entailment.CCC_of_C_right {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢! φ 🡒 ψ) : 𝓢 ⊢! (χ 🡒 φ) 🡒 χ 🡒 ψ

Equations

• LO.Entailment.CCC_of_C_right h = LO.Entailment.implyS⨀!LO.Entailment.C_of_conseq h

theorem LO.Entailment.CCC!_of_C!_right {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ φ 🡒 ψ) : 𝓢 ⊢ (χ 🡒 φ) 🡒 χ 🡒 ψ

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

Equations

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

@[simp]

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

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

Equations

• LO.Entailment.CNNNN_of_NNC b = LO.Entailment.CNNCCNNNN⨀!b

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

def LO.Entailment.O_intro_of_KN {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} (h : 𝓢 ⊢! φ ⋏ ∼φ) : 𝓢 ⊢! ⊥

Equations

• LO.Entailment.O_intro_of_KN h = LO.Entailment.CO_of_N (LO.Entailment.K_right h)⨀!LO.Entailment.K_left h

theorem LO.Entailment.O!_intro_of_KN! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} (h : 𝓢 ⊢ φ ⋏ ∼φ) : 𝓢 ⊢ ⊥

theorem LO.Entailment.lac'! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} (h : 𝓢 ⊢ φ ⋏ ∼φ) : 𝓢 ⊢ ⊥

Law of contradiction

def LO.Entailment.CKNO {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} : 𝓢 ⊢! φ ⋏ ∼φ 🡒 ⊥

Equations

• LO.Entailment.CKNO = LO.Entailment.FiniteContext.deduct' (LO.Entailment.O_intro_of_KN LO.Entailment.FiniteContext.id)

@[simp]

theorem LO.Entailment.CKNO! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} : 𝓢 ⊢ φ ⋏ ∼φ 🡒 ⊥

theorem LO.Entailment.lac! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} : 𝓢 ⊢ φ ⋏ ∼φ 🡒 ⊥

Law of contradiction

def LO.Entailment.CANNNK {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] : 𝓢 ⊢! ∼φ ⋎ ∼ψ 🡒 ∼(φ ⋏ ψ)

Equations

• LO.Entailment.CANNNK = LO.Entailment.left_A_intro (LO.Entailment.contra LO.Entailment.and₁) (LO.Entailment.contra LO.Entailment.and₂)

@[simp]

theorem LO.Entailment.CANNNK! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] : 𝓢 ⊢ ∼φ ⋎ ∼ψ 🡒 ∼(φ ⋏ ψ)

def LO.Entailment.NK_of_ANN {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] (d : 𝓢 ⊢! ∼φ ⋎ ∼ψ) : 𝓢 ⊢! ∼(φ ⋏ ψ)

Equations

• LO.Entailment.NK_of_ANN d = LO.Entailment.CANNNK⨀!d

theorem LO.Entailment.NK!_of_ANN! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] (d : 𝓢 ⊢ ∼φ ⋎ ∼ψ) : 𝓢 ⊢ ∼(φ ⋏ ψ)

def LO.Entailment.CKNNNA {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] : 𝓢 ⊢! ∼φ ⋏ ∼ψ 🡒 ∼(φ ⋎ ψ)

Equations

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

@[simp]

theorem LO.Entailment.CKNNNA! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] : 𝓢 ⊢ ∼φ ⋏ ∼ψ 🡒 ∼(φ ⋎ ψ)

def LO.Entailment.NA_of_KNN {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] (d : 𝓢 ⊢! ∼φ ⋏ ∼ψ) : 𝓢 ⊢! ∼(φ ⋎ ψ)

Equations

• LO.Entailment.NA_of_KNN d = LO.Entailment.CKNNNA⨀!d

theorem LO.Entailment.NA!_of_KNN! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] (d : 𝓢 ⊢ ∼φ ⋏ ∼ψ) : 𝓢 ⊢ ∼(φ ⋎ ψ)

def LO.Entailment.CNAKNN {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] : 𝓢 ⊢! ∼(φ ⋎ ψ) 🡒 ∼φ ⋏ ∼ψ

Equations

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

@[simp]

theorem LO.Entailment.CNAKNN! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] : 𝓢 ⊢ ∼(φ ⋎ ψ) 🡒 ∼φ ⋏ ∼ψ

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

Equations

• LO.Entailment.KNN_of_NA b = LO.Entailment.CNAKNN⨀!b

theorem LO.Entailment.KNN!_of_NA! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] (b : 𝓢 ⊢ ∼(φ ⋎ ψ)) : 𝓢 ⊢ ∼φ ⋏ ∼ψ

def LO.Entailment.EConj₂Conj {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] (Γ : List F) : 𝓢 ⊢! ⋀Γ 🡘 Γ.conj

Equations

• LO.Entailment.EConj₂Conj [] = LO.Entailment.E_Id
• LO.Entailment.EConj₂Conj [head] = LO.Entailment.E_intro (LO.Entailment.FiniteContext.deduct' (LO.Entailment.K_intro LO.Entailment.FiniteContext.id LO.Entailment.verum)) LO.Entailment.and₁
• LO.Entailment.EConj₂Conj (head :: ψ :: Γ) = LO.Entailment.EKK_of_E_of_E LO.Entailment.E_Id (LO.Entailment.EConj₂Conj (ψ :: Γ))

@[simp]

theorem LO.Entailment.EConj₂Conj! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {Γ : List F} : 𝓢 ⊢ ⋀Γ 🡘 Γ.conj

theorem LO.Entailment.CConj!_iff_CConj₂ {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} {Γ : List F} : 𝓢 ⊢ Γ.conj 🡒 φ ↔ 𝓢 ⊢ ⋀Γ 🡒 φ

def LO.Entailment.right_Conj'_intro {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {ι : Type u_4} [DecidableEq F] (φ : F) (l : List ι) (ψ : ι → F) (b : (i : ι) → i ∈ l → 𝓢 ⊢! φ 🡒 ψ i) : 𝓢 ⊢! φ 🡒 List.conj' ψ l

! note: It may be easier to handle define List.conj based on List.conj' (?)

Equations

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

theorem LO.Entailment.right_Conj'!_intro {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {ι : Type u_3} [DecidableEq F] (φ : F) (l : List ι) (ψ : ι → F) (b : ∀ i ∈ l, 𝓢 ⊢ φ 🡒 ψ i) : 𝓢 ⊢ φ 🡒 List.conj' ψ l

def LO.Entailment.left_Conj'_intro {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {ι : Type u_4} {i : ι} [DecidableEq F] {l : List ι} (h : i ∈ l) (φ : ι → F) : 𝓢 ⊢! List.conj' φ l 🡒 φ i

Equations

• LO.Entailment.left_Conj'_intro h φ = LO.Entailment.left_Conj₂_intro ⋯

theorem LO.Entailment.left_Conj'!_intro {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {ι : Type u_3} {i : ι} [DecidableEq F] {l : List ι} (h : i ∈ l) (φ : ι → F) : 𝓢 ⊢ List.conj' φ l 🡒 φ i

theorem LO.Entailment.right_Fconj!_intro {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] (φ : F) (s : Finset F) (b : ∀ ψ ∈ s, 𝓢 ⊢ φ 🡒 ψ) : 𝓢 ⊢ φ 🡒 s.conj

theorem LO.Entailment.left_Fconj!_intro {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] {s : Finset F} (h : φ ∈ s) : 𝓢 ⊢ s.conj 🡒 φ

theorem LO.Entailment.right_Fconj'!_intro {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {ι : Type u_3} [DecidableEq F] (φ : F) (s : Finset ι) (ψ : ι → F) (b : ∀ i ∈ s, 𝓢 ⊢ φ 🡒 ψ i) : 𝓢 ⊢ φ 🡒 ⩕ (i : ι) ∈ s, ψ i

theorem LO.Entailment.left_Fconj'!_intro {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {ι : Type u_3} [DecidableEq F] {s : Finset ι} (φ : ι → F) {i : ι} (hi : i ∈ s) : 𝓢 ⊢ (⩕ (i : ι) ∈ s, φ i) 🡒 φ i

theorem LO.Entailment.right_Uconj!_intro {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {ι : Type u_3} [DecidableEq F] [Fintype ι] (φ : F) (ψ : ι → F) (b : ∀ (i : ι), 𝓢 ⊢ φ 🡒 ψ i) : 𝓢 ⊢ φ 🡒 ⩕ (i : ι), ψ i

theorem LO.Entailment.left_Uconj!_intro {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {ι : Type u_3} [DecidableEq F] [Fintype ι] (φ : ι → F) (i : ι) : 𝓢 ⊢ (⩕ (i : ι), φ i) 🡒 φ i

theorem LO.Entailment.Conj₂!_iff_forall_provable {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] {Γ : List F} : 𝓢 ⊢ ⋀Γ ↔ ∀ φ ∈ Γ, 𝓢 ⊢ φ

theorem LO.Entailment.CConj₂Conj₂!_of_subset {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {Γ Δ : List F} [DecidableEq F] (h : ∀ φ ∈ Γ, φ ∈ Δ) : 𝓢 ⊢ ⋀Δ 🡒 ⋀Γ

theorem LO.Entailment.CConj₂Conj₂!_of_provable {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {Γ Δ : List F} [DecidableEq F] (h : ∀ φ ∈ Γ, Δ ⊢[𝓢] φ) : 𝓢 ⊢ ⋀Δ 🡒 ⋀Γ

theorem LO.Entailment.CConj₂!_of_forall_provable {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {Γ Δ : List F} [DecidableEq F] (h : ∀ φ ∈ Γ, Δ ⊢[𝓢] φ) : Δ ⊢[𝓢] ⋀Γ

theorem LO.Entailment.CConj₂!_of_unique {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} {Γ : List F} [DecidableEq F] (he : ∀ g ∈ Γ, g = φ) : 𝓢 ⊢ φ 🡒 ⋀Γ

theorem LO.Entailment.C!_of_CConj₂!_of_unique {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} {Γ : List F} [DecidableEq F] (he : ∀ g ∈ Γ, g = φ) (hd : 𝓢 ⊢ ⋀Γ 🡒 ψ) : 𝓢 ⊢ φ 🡒 ψ

theorem LO.Entailment.CConj₂!_iff_CKConj₂! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} {Γ : List F} [DecidableEq F] : 𝓢 ⊢ ⋀(φ :: Γ) 🡒 ψ ↔ 𝓢 ⊢ φ ⋏ ⋀Γ 🡒 ψ

@[simp]

theorem LO.Entailment.CConj₂AppendKConj₂Conj₂! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {Γ Δ : List F} [DecidableEq F] : 𝓢 ⊢ ⋀(Γ ++ Δ) 🡒 ⋀Γ ⋏ ⋀Δ

@[simp]

theorem LO.Entailment.CKConj₂RemoveConj₂! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} {Γ : List F} [DecidableEq F] : 𝓢 ⊢ ⋀List.remove φ Γ ⋏ φ 🡒 ⋀Γ

theorem LO.Entailment.CKConj₂Remove!_of_CConj₂! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} {Γ : List F} [DecidableEq F] (b : 𝓢 ⊢ ⋀Γ 🡒 ψ) : 𝓢 ⊢ ⋀List.remove φ Γ ⋏ φ 🡒 ψ

theorem LO.Entailment.Conj₂Append!_iff_KConj₂Conj₂! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {Γ Δ : List F} [DecidableEq F] : 𝓢 ⊢ ⋀(Γ ++ Δ) ↔ 𝓢 ⊢ ⋀Γ ⋏ ⋀Δ

@[simp]

theorem LO.Entailment.EConj₂AppendKConj₂Conj₂! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {Γ Δ : List F} [DecidableEq F] : 𝓢 ⊢ ⋀(Γ ++ Δ) 🡘 ⋀Γ ⋏ ⋀Δ

theorem LO.Entailment.CConj₂Append!_iff_CKConj₂Conj₂! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} {Γ Δ : List F} [DecidableEq F] : 𝓢 ⊢ ⋀(Γ ++ Δ) 🡒 φ ↔ 𝓢 ⊢ ⋀Γ ⋏ ⋀Δ 🡒 φ

@[simp]

theorem LO.Entailment.CFConjConj₂ {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] {Γ : Finset F} : 𝓢 ⊢ ⋀Γ.toList 🡒 Γ.conj

@[simp]

theorem LO.Entailment.CConj₂Conj_list {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] {Γ : List F} : 𝓢 ⊢ ⋀Γ 🡒 Γ.toFinset.conj

@[simp]

theorem LO.Entailment.CConj₂FConj {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] {Γ : Finset F} : 𝓢 ⊢ Γ.conj 🡒 ⋀Γ.toList

@[simp]

theorem LO.Entailment.CConj₂FConj_list {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] {Γ : List F} : 𝓢 ⊢ Γ.toFinset.conj 🡒 ⋀Γ

theorem LO.Entailment.FConj_DT {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] {Γ : Finset F} : 𝓢 ⊢ Γ.conj 🡒 φ ↔ ↑Γ *⊢[𝓢] φ

theorem LO.Entailment.FConj!_iff_forall_provable {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] {Γ : Finset F} : 𝓢 ⊢ Γ.conj ↔ ∀ φ ∈ Γ, 𝓢 ⊢ φ

theorem LO.Entailment.FConj_of_FConj!_of_subset {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] {Γ Δ : Finset F} (h : Δ ⊆ Γ) (hΓ : 𝓢 ⊢ Γ.conj) : 𝓢 ⊢ Δ.conj

theorem LO.Entailment.CFConj_FConj!_of_subset {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] {Γ Δ : Finset F} (h : Δ ⊆ Γ) : 𝓢 ⊢ Γ.conj 🡒 Δ.conj

@[simp]

theorem LO.Entailment.CFconjUnionKFconj! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] {Γ Δ : Finset F} : 𝓢 ⊢ (Γ ∪ Δ).conj 🡒 Γ.conj ⋏ Δ.conj

@[simp]

theorem LO.Entailment.CinsertFConjKFConj! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] {Γ : Finset F} : 𝓢 ⊢ (insert φ Γ).conj 🡒 φ ⋏ Γ.conj

@[simp]

theorem LO.Entailment.CKFconjFconjUnion! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] {Γ Δ : Finset F} : 𝓢 ⊢ Γ.conj ⋏ Δ.conj 🡒 (Γ ∪ Δ).conj

@[simp]

theorem LO.Entailment.CKFConjinsertFConj! {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] {Γ : Finset F} : 𝓢 ⊢ φ ⋏ Γ.conj 🡒 (insert φ Γ).conj

theorem LO.Entailment.FConj_DT' {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] {Γ Δ : Finset F} : ↑Γ *⊢[𝓢] Δ.conj 🡒 φ ↔ ↑(Γ ∪ Δ) *⊢[𝓢] φ

theorem LO.Entailment.CFconjFconj!_of_provable {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] {Γ Δ : Finset F} (h : ∀ φ ∈ Γ, ↑Δ *⊢[𝓢] φ) : 𝓢 ⊢ Δ.conj 🡒 Γ.conj

def LO.Entailment.right_Disj_intro {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] (Γ : List F) (h : φ ∈ Γ) : 𝓢 ⊢! φ 🡒 Γ.disj

Equations

• One or more equations did not get rendered due to their size.
• LO.Entailment.right_Disj_intro [] h_2 = ⋯.elim

def LO.Entailment.right_Disj!_intro {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] (Γ : List F) (h : φ ∈ Γ) : 𝓢 ⊢ φ 🡒 Γ.disj

Equations

• ⋯ = ⋯

def LO.Entailment.right_Disj_intro' {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] (Γ : List F) (h : φ ∈ Γ) (hψ : 𝓢 ⊢! ψ 🡒 φ) : 𝓢 ⊢! ψ 🡒 Γ.disj

Equations

• LO.Entailment.right_Disj_intro' Γ h hψ = LO.Entailment.C_trans hψ (LO.Entailment.right_Disj_intro Γ h)

def LO.Entailment.right_Disj!_intro' {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] (Γ : List F) (h : φ ∈ Γ) (hψ : 𝓢 ⊢ ψ 🡒 φ) : 𝓢 ⊢ ψ 🡒 Γ.disj

Equations

• ⋯ = ⋯

def LO.Entailment.right_Disj₂_intro {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] (Γ : List F) (h : φ ∈ Γ) : 𝓢 ⊢! φ 🡒 ⋁Γ

Equations

• One or more equations did not get rendered due to their size.
• LO.Entailment.right_Disj₂_intro [] h_2 = ⋯.elim
• LO.Entailment.right_Disj₂_intro [ψ] h_2 = ⋯ ▸ LO.Entailment.C_id

def LO.Entailment.right_Disj₂!_intro {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] (Γ : List F) (h : φ ∈ Γ) : 𝓢 ⊢ φ 🡒 ⋁Γ

Equations

• ⋯ = ⋯

def LO.Entailment.right_Disj'_intro {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {ι : Type u_4} {i : ι} [DecidableEq F] (φ : ι → F) (l : List ι) (h : i ∈ l) : 𝓢 ⊢! φ i 🡒 List.disj' φ l

Equations

• LO.Entailment.right_Disj'_intro φ l h = LO.Entailment.right_Disj₂_intro (List.map φ l) ⋯

theorem LO.Entailment.right_Disj'!_intro {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {ι : Type u_3} {i : ι} [DecidableEq F] (φ : ι → F) (l : List ι) (h : i ∈ l) : 𝓢 ⊢ φ i 🡒 List.disj' φ l

theorem LO.Entailment.right_Fdisj!_intro {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] (s : Finset F) (h : φ ∈ s) : 𝓢 ⊢ φ 🡒 s.disj

theorem LO.Entailment.right_Fdisj'!_intro {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {ι : Type u_3} [DecidableEq F] (s : Finset ι) (φ : ι → F) {i : ι} (hi : i ∈ s) : 𝓢 ⊢ φ i 🡒 ⩖ (j : ι) ∈ s, φ j

theorem LO.Entailment.right_Udisj!_intro {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {ι : Type u_3} {i : ι} [DecidableEq F] [Fintype ι] (φ : ι → F) : 𝓢 ⊢ φ i 🡒 ⩖ (j : ι), φ j

theorem LO.Entailment.CFConj_CDisj!_of_K_intro {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} {Γ Δ : Finset F} [DecidableEq F] (hp : φ ∈ Γ) (hpq : ψ ∈ Γ) (hψ : φ ⋏ ψ ∈ Δ) : 𝓢 ⊢ Γ.conj 🡒 Δ.disj

theorem LO.Entailment.CFConj_CDisj!_of_innerMDP {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} {Γ Δ : Finset F} [DecidableEq F] (hp : φ ∈ Γ) (hpq : φ 🡒 ψ ∈ Γ) (hψ : ψ ∈ Δ) : 𝓢 ⊢ Γ.conj 🡒 Δ.disj

theorem LO.Entailment.iff_FiniteContext_Context {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] {Γ : List F} : Γ ⊢[𝓢] φ ↔ ↑Γ.toFinset *⊢[𝓢] φ

theorem LO.Entailment.FConj'_iff_forall_provable {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {α : Type u_3} [DecidableEq F] {s : Finset α} {ι : α → F} : (𝓢 ⊢ ⩕ (i : α) ∈ s, ι i) ↔ ∀ i ∈ s, 𝓢 ⊢ ι i

theorem LO.Entailment.Context.provable_iff_finset {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] {Γ : Set F} {φ : F} : Γ *⊢[𝓢] φ ↔ ∃ (Δ : Finset F), ↑Δ ⊆ Γ ∧ ↑Δ *⊢[𝓢] φ

theorem LO.Entailment.Context.bot_of_mem_neg {F : Type u_1} [LogicalConnective F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] {Γ : Set F} (h₁ : φ ∈ Γ) (h₂ : ∼φ ∈ Γ) : Γ *⊢[𝓢] ⊥