@[reducible, inline]

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

Equations

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

@[reducible, inline]

abbrev FFL.Axioms.Verum {F : Type u_1} [LogicalNeutral F] : F

Equations

• FFL.Axioms.Verum = ⊤

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

class FFL.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 FFL.Entailment.mdp! {S : Type u_1} {F : Type u_2} {inst✝ : LogicalConnective F} {inst✝¹ : Entailment S F} {𝓢 : S} [self : ModusPonens 𝓢] {φ ψ : F} : 𝓢 ⊢! φ 🡒 ψ → 𝓢 ⊢! φ → 𝓢 ⊢! ψ

Alias of FFL.Entailment.ModusPonens.mdp!.

Equations

• @FFL.Entailment.mdp! = @FFL.Entailment.ModusPonens.mdp!

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

Equations

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

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

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

Equations

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

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

Equations

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

class FFL.Entailment.NegationEquiv {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] [LogicalNeutral 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 FFL.Entailment.neg_equiv {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ : F} [LogicalNeutral F] [NegationEquiv 𝓢] : 𝓢 ⊢ ∼φ 🡘 (φ 🡒 ⊥)

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

• verum! : 𝓢 ⊢! Axioms.Verum

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

Equations

• FFL.Entailment.verum! = FFL.Entailment.HasAxiomVerum.verum!

@[simp]

theorem FFL.Entailment.verum {S : Type u_1} {F : Type u_2} [Entailment S F] {𝓢 : S} [LogicalNeutral F] [HasAxiomVerum 𝓢] : 𝓢 ⊢ ⊤

class FFL.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 FFL.Entailment.implyK {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [HasAxiomImplyK 𝓢] : 𝓢 ⊢ φ 🡒 ψ 🡒 φ

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

Equations

• FFL.Entailment.C!_of_conseq! h = FFL.Entailment.implyK!⨀!h

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

Alias of FFL.Entailment.C!_of_conseq!.

Equations

• @FFL.Entailment.dhyp! = @FFL.Entailment.C!_of_conseq!

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

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

Alias of FFL.Entailment.C_of_conseq.

class FFL.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 FFL.Entailment.implyS {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ χ : F} [HasAxiomImplyS 𝓢] : 𝓢 ⊢ (φ 🡒 ψ 🡒 χ) 🡒 (φ 🡒 ψ) 🡒 φ 🡒 χ

class FFL.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 FFL.Entailment.and₁ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [HasAxiomAndElim 𝓢] : 𝓢 ⊢ φ ⋏ ψ 🡒 φ

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

Equations

• FFL.Entailment.K!_left d = FFL.Entailment.and₁!⨀!d

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

@[simp]

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

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

Equations

• FFL.Entailment.K!_right d = FFL.Entailment.and₂!⨀!d

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

class FFL.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 FFL.Entailment.and₃ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [HasAxiomAndInst 𝓢] : 𝓢 ⊢ φ 🡒 ψ 🡒 φ ⋏ ψ

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

Equations

• FFL.Entailment.K!_intro d₁ d₂ = FFL.Entailment.and₃!⨀!d₁⨀!d₂

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

class FFL.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 FFL.Entailment.or₁ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ : F} [HasAxiomOrInst 𝓢] : 𝓢 ⊢ φ 🡒 φ ⋎ ψ

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

Equations

• FFL.Entailment.A!_intro_left d = FFL.Entailment.or₁!⨀!d

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

@[simp]

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

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

Equations

• FFL.Entailment.A!_intro_right d = FFL.Entailment.or₂!⨀!d

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

class FFL.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 FFL.Entailment.or₃ {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} {φ ψ χ : F} [HasAxiomOrElim 𝓢] : 𝓢 ⊢ (φ 🡒 χ) 🡒 (ψ 🡒 χ) 🡒 φ ⋎ ψ 🡒 χ

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

Equations

• FFL.Entailment.left_A!_intro d₁ d₂ = FFL.Entailment.or₃!⨀!d₁⨀!d₂

def FFL.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 FFL.Entailment.left_A!_intro.

Equations

• @FFL.Entailment.CA!_of_C!_of_C! = @FFL.Entailment.left_A!_intro

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

theorem FFL.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 FFL.Entailment.left_A_intro.

def FFL.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

• FFL.Entailment.of_C!_of_C!_of_A! d₁ d₂ d₃ = FFL.Entailment.or₃!⨀!d₁⨀!d₂⨀!d₃

def FFL.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 FFL.Entailment.of_C!_of_C!_of_A!.

Equations

• @FFL.Entailment.A!_cases = @FFL.Entailment.of_C!_of_C!_of_A!

theorem FFL.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 FFL.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 FFL.Entailment.of_C_of_C_of_A.

class FFL.Entailment.Minimal {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] [LogicalNeutral F] (𝓢 : S) extends FFL.Entailment.ModusPonens 𝓢, FFL.Entailment.NegationEquiv 𝓢, FFL.Entailment.HasAxiomVerum 𝓢, FFL.Entailment.HasAxiomImplyK 𝓢, FFL.Entailment.HasAxiomImplyS 𝓢, FFL.Entailment.HasAxiomAndElim 𝓢, FFL.Entailment.HasAxiomAndInst 𝓢, FFL.Entailment.HasAxiomOrInst 𝓢, FFL.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 FFL.Entailment.CO!_of_N! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ : F} [LogicalNeutral F] [HasAxiomAndElim 𝓢] [NegationEquiv 𝓢] : 𝓢 ⊢! ∼φ → 𝓢 ⊢! φ 🡒 ⊥

Equations

• FFL.Entailment.CO!_of_N! h = FFL.Entailment.K!_left FFL.Entailment.negEquiv!⨀!h

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

Equations

• FFL.Entailment.N!_of_CO! h = FFL.Entailment.K!_right FFL.Entailment.negEquiv!⨀!h

theorem FFL.Entailment.N_iff_CO {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ : F} [LogicalNeutral F] [HasAxiomAndElim 𝓢] [NegationEquiv 𝓢] : 𝓢 ⊢ ∼φ ↔ 𝓢 ⊢ φ 🡒 ⊥

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

Equations

• FFL.Entailment.E!_intro b₁ b₂ = FFL.Entailment.K!_intro b₁ b₂

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

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

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

def FFL.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

• FFL.Entailment.C!_of_E!_mp h = FFL.Entailment.K!_left h

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

def FFL.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

• FFL.Entailment.C!_of_E!_mpr h = FFL.Entailment.K!_right h

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

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

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

Equations

• FFL.Entailment.C!_id = FFL.Entailment.implyS!⨀!FFL.Entailment.implyK!⨀!FFL.Entailment.implyK!

@[simp]

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

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

Equations

• FFL.Entailment.E!_id = FFL.Entailment.K!_intro FFL.Entailment.C!_id FFL.Entailment.C!_id

@[simp]

theorem FFL.Entailment.E_id {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ : F} [HasAxiomAndInst 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] : 𝓢 ⊢ φ 🡘 φ

@[instance_reducible]

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

Equations

• FFL.Entailment.instNegationEquivOfNegAbbrevOfHasAxiomImplyKOfHasAxiomImplySOfHasAxiomAndInst = { negEquiv! := fun {φ : F} => have this := FFL.Entailment.E!_id; ⋯.mpr this }

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

Equations

• FFL.Entailment.NO! = FFL.Entailment.N!_of_CO! FFL.Entailment.C!_id

@[simp]

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

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

Equations

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

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

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

Equations

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

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

Equations

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

def FFL.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 = FFL.Entailment.C!_of_conseq! FFL.Entailment.implyS!⨀₁bqr⨀₁bq

theorem FFL.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 FFL.Entailment.«term_⨀₂_» : Lean.TrailingParserDescr

Equations

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

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

Equations

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

def FFL.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 = FFL.Entailment.C!_of_conseq! (FFL.Entailment.C!_of_conseq! FFL.Entailment.implyS!)⨀₂bqr⨀₂bq

theorem FFL.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 FFL.Entailment.«term_⨀₃_» : Lean.TrailingParserDescr

Equations

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

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

Equations

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

def FFL.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 = FFL.Entailment.C!_of_conseq! (FFL.Entailment.C!_of_conseq! (FFL.Entailment.C!_of_conseq! FFL.Entailment.implyS!))⨀₃bqr⨀₃bq

theorem FFL.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 FFL.Entailment.«term_⨀₄_» : Lean.TrailingParserDescr

Equations

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

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

Equations

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

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

Equations

• FFL.Entailment.C!_trans bpq bqr = FFL.Entailment.implyS!⨀!FFL.Entailment.C!_of_conseq! bqr⨀!bpq

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

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

Equations

• FFL.Entailment.C!_replace h₁ h₂ h = FFL.Entailment.C!_trans h₁ (FFL.Entailment.C!_trans h h₂)

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

def FFL.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 FFL.Entailment.E_replace {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ₁ ψ₁ φ₂ ψ₂ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] : 𝓢 ⊢ φ₁ 🡘 ψ₁ → 𝓢 ⊢ φ₂ 🡘 ψ₂ → 𝓢 ⊢ φ₁ 🡘 φ₂ → 𝓢 ⊢ ψ₁ 🡘 ψ₂

def FFL.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 FFL.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 FFL.Entailment.CCCC! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ : F} [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] : 𝓢 ⊢! φ 🡒 ψ 🡒 χ 🡒 φ

Equations

• FFL.Entailment.CCCC! = FFL.Entailment.C!_trans FFL.Entailment.implyK! FFL.Entailment.implyK!

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

def FFL.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

• FFL.Entailment.CK!_of_C!_of_C! bq br = FFL.Entailment.C!_of_conseq! FFL.Entailment.and₃!⨀₁bq⨀₁br

theorem FFL.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 FFL.Entailment.CKK! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] : 𝓢 ⊢! φ ⋏ ψ 🡒 ψ ⋏ φ

Equations

• FFL.Entailment.CKK! = FFL.Entailment.CK!_of_C!_of_C! FFL.Entailment.and₂! FFL.Entailment.and₁!

@[simp]

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

def FFL.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

• FFL.Entailment.K!_symm h = FFL.Entailment.CKK!⨀!h

theorem FFL.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 FFL.Entailment.CEE! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] : 𝓢 ⊢! φ 🡘 ψ 🡒 ψ 🡘 φ

Equations

• FFL.Entailment.CEE! = FFL.Entailment.CKK!

@[simp]

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

def FFL.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

• FFL.Entailment.E!_symm h = FFL.Entailment.CEE!⨀!h

theorem FFL.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 FFL.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 FFL.Entailment.ECKCC {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ ψ χ : F} [HasAxiomAndInst 𝓢] [HasAxiomAndElim 𝓢] [HasAxiomImplyK 𝓢] [HasAxiomImplyS 𝓢] : 𝓢 ⊢ (φ ⋏ ψ 🡒 χ) 🡘 (φ 🡒 ψ 🡒 χ)

def FFL.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

• FFL.Entailment.CC!_of_CK! d = FFL.Entailment.K!_left FFL.Entailment.ECKCC!⨀!d

def FFL.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

• FFL.Entailment.CK!_of_CC! d = FFL.Entailment.K!_right FFL.Entailment.ECKCC!⨀!d

theorem FFL.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 FFL.Entailment.CV! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [Entailment S F] {𝓢 : S} [ModusPonens 𝓢] {φ : F} [LogicalNeutral F] [HasAxiomVerum 𝓢] [HasAxiomImplyK 𝓢] : 𝓢 ⊢! φ 🡒 ⊤

Equations

• FFL.Entailment.CV! = FFL.Entailment.C!_of_conseq! FFL.Entailment.verum!

@[simp]

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

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

theorem FFL.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 FFL.Entailment.conj₂Nth! {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] (Γ : List F) (n : ℕ) (hn : n < Γ.length) : 𝓢 ⊢! ⋀Γ 🡒 Γ[n]

Equations

• FFL.Entailment.conj₂Nth! [] x x_1 = ⋯.elim
• FFL.Entailment.conj₂Nth! [ψ] 0 x_3 = FFL.Entailment.C!_id
• FFL.Entailment.conj₂Nth! (φ :: ψ :: Γ) 0 x_3 = FFL.Entailment.and₁!
• FFL.Entailment.conj₂Nth! (φ :: ψ :: Γ) n.succ hn = FFL.Entailment.C!_trans FFL.Entailment.and₂! (FFL.Entailment.conj₂Nth! (ψ :: Γ) n ⋯)

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

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

Equations

• FFL.Entailment.left_Conj!_intro h_2 = ⋯.elim
• FFL.Entailment.left_Conj!_intro h_2 = if e : φ = ψ then e ▸ FFL.Entailment.and₁! else have this := ⋯; FFL.Entailment.C!_trans FFL.Entailment.and₂! (FFL.Entailment.left_Conj!_intro this)

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

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

Equations

• FFL.Entailment.Conj!_intro [] b_2 = FFL.Entailment.verum!
• FFL.Entailment.Conj!_intro (ψ :: Γ_2) b_2 = FFL.Entailment.K!_intro (b_2 ψ ⋯) (FFL.Entailment.Conj!_intro Γ_2 fun (ψ_1 : F) (hq : ψ_1 ∈ Γ_2) => b_2 ψ_1 ⋯)

theorem FFL.Entailment.Conj_intro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {Γ : List F} (b : ∀ φ ∈ Γ, 𝓢 ⊢ φ) : 𝓢 ⊢ Γ.conj

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

Equations

• FFL.Entailment.right_Conj!_intro φ [] b_2 = FFL.Entailment.C!_of_conseq! FFL.Entailment.verum!
• FFL.Entailment.right_Conj!_intro φ (ψ :: Γ_2) b_2 = FFL.Entailment.CK!_of_C!_of_C! (b_2 ψ ⋯) (FFL.Entailment.right_Conj!_intro φ Γ_2 fun (ψ_1 : F) (hq : ψ_1 ∈ Γ_2) => b_2 ψ_1 ⋯)

theorem FFL.Entailment.right_Conj_intro {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] (φ : F) (Γ : List F) (b : ∀ ψ ∈ Γ, 𝓢 ⊢ φ 🡒 ψ) : 𝓢 ⊢ φ 🡒 Γ.conj

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

Equations

• FFL.Entailment.CConjConj! h = FFL.Entailment.right_Conj!_intro Γ.conj Δ fun (x : F) (hq : x ∈ Δ) => FFL.Entailment.left_Conj!_intro ⋯

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

Equations

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

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

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

Equations

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

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

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

Equations

• One or more equations did not get rendered due to their size.
• FFL.Entailment.right_Conj₂!_intro φ [] b_2 = FFL.Entailment.C!_of_conseq! FFL.Entailment.verum!
• FFL.Entailment.right_Conj₂!_intro φ [ψ] b_2 = b_2 (⋀[ψ]) ⋯

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

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

Equations

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

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

@[reducible, inline]

abbrev FFL.Entailment.Minimal.ofEquiv {S : Type u_1} {F : Type u_2} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] {G : Type u_3} {T : Type u_4} [Entailment T G] [LogicalConnective G] [LogicalNeutral 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 FFL.Entailment.FiniteContext {S : Sort u_1} (F : Type u_2) (𝓢 : S) : Type u_2

• ctx : List F

@[instance_reducible]

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

Equations

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

@[reducible, inline]

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

Equations

• Γ.conj = ⋀Γ.ctx

@[reducible, inline]

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

Equations

• Γ.disj = ⋁Γ.ctx

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[instance_reducible]

instance FFL.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.

@[instance_reducible]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

• FFL.Entailment.FiniteContext.ofDef! b = b

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

Equations

• FFL.Entailment.FiniteContext.toDef! b = b

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

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

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

Equations

• FFL.Entailment.FiniteContext.cast! d eΓ eφ = eΓ ▸ eφ ▸ d

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

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

Equations

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

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

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

Equations

• FFL.Entailment.FiniteContext.byAxm! h = FFL.Entailment.Axiomatized.prfAxm ⋯

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

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

Equations

• FFL.Entailment.FiniteContext.weakening! h = FFL.Entailment.Axiomatized.weakening ⋯

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

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

Equations

• FFL.Entailment.FiniteContext.of! b = FFL.Entailment.C!_of_conseq! b

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

Equations

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

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

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

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

Equations

• FFL.Entailment.FiniteContext.id! = FFL.Entailment.FiniteContext.nthAxm! 0 ⋯

@[simp]

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

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

Equations

• FFL.Entailment.FiniteContext.byAxm₀! = FFL.Entailment.FiniteContext.nthAxm! 0 ⋯

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

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

Equations

• FFL.Entailment.FiniteContext.byAxm₁! = FFL.Entailment.FiniteContext.nthAxm! 1 ⋯

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

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

Equations

• FFL.Entailment.FiniteContext.byAxm₂! = FFL.Entailment.FiniteContext.nthAxm! 2 ⋯

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

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

Equations

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

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

Equations

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

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

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

Equations

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

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

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

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

Equations

• FFL.Entailment.FiniteContext.deduct'! b = FFL.Entailment.FiniteContext.emptyPrf! (FFL.Entailment.FiniteContext.deduct! b)

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

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

Equations

• FFL.Entailment.FiniteContext.deductInv'! b = FFL.Entailment.FiniteContext.deductInv! (FFL.Entailment.FiniteContext.of! b)

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

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

• ctx : Set F

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[instance_reducible]

instance FFL.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 FFL.Entailment.Context.Proof {S : Type u_1} {F : Type u_2} {𝓢 : S} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] (Γ : Context F 𝓢) (φ : F) : Type (max u_2 u_3)

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

@[instance_reducible]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

@[reducible, inline]

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

@[instance_reducible]

instance FFL.Entailment.Context.instAxiomatizedOfDecidableEq {S : Type u_1} {F : Type u_2} {𝓢 : S} [LogicalConnective F] [LogicalNeutral 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 FFL.Entailment.Context.byAxm! {S : Type u_1} {F : Type u_2} {𝓢 : S} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] [Entailment.Minimal 𝓢] [DecidableEq F] {Γ : Set F} {φ : F} (h : φ ∈ Γ) : Γ *⊢[𝓢]! φ

Equations

• FFL.Entailment.Context.byAxm! h = FFL.Entailment.Axiomatized.prfAxm ⋯

@[instance_reducible]

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

Equations

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

def FFL.Entailment.Context.deduct! {S : Type u_1} {F : Type u_2} {𝓢 : S} [LogicalConnective F] [LogicalNeutral 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 FFL.Entailment.Context.deduct {S : Type u_2} {F : Type u_1} {𝓢 : S} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] [Entailment.Minimal 𝓢] {φ : F} {Γ : Set F} {ψ : F} [DecidableEq F] (h : insert φ Γ *⊢[𝓢] ψ) : Γ *⊢[𝓢] φ 🡒 ψ

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

Equations

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

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

@[instance_reducible]

instance FFL.Entailment.Context.deduction {S : Type u_1} {F : Type u_2} {𝓢 : S} [LogicalConnective F] [LogicalNeutral 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 FFL.Entailment.Context.weakening! {S : Type u_1} {F : Type u_2} {𝓢 : S} [LogicalConnective F] [LogicalNeutral F] [Entailment S F] [Entailment.Minimal 𝓢] {Γ Δ : Set F} [DecidableEq F] (h : Γ ⊆ Δ) {φ : F} : Γ *⊢[𝓢]! φ → Δ *⊢[𝓢]! φ

Equations

• FFL.Entailment.Context.weakening! h = FFL.Entailment.Axiomatized.weakening ⋯

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

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

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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

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

@[instance_reducible]

instance FFL.Entailment.Context.minimal {S : Type u_1} {F : Type u_2} {𝓢 : S} [LogicalConnective F] [LogicalNeutral 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 FFL.Entailment.CVNO {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] : 𝓢 ⊢ ⊤ 🡒 ∼⊥

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

Equations

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

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

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

Equations

• FFL.Entailment.bot_of_mem_either! h₁ h₂ = FFL.Entailment.CO!_of_N! (FFL.Entailment.FiniteContext.byAxm! h₂)⨀!FFL.Entailment.FiniteContext.byAxm! h₁

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

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

Equations

• FFL.Entailment.negMDP! hnp hn = FFL.Entailment.CO!_of_N! hnp⨀!hn

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

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

Equations

• FFL.Entailment.right_A!_intro_left h = FFL.Entailment.FiniteContext.deduct'! (FFL.Entailment.A!_intro_left (FFL.Entailment.FiniteContext.deductInv! (FFL.Entailment.FiniteContext.of! h)))

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

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

Equations

• FFL.Entailment.right_A!_intro_right h = FFL.Entailment.FiniteContext.deduct'! (FFL.Entailment.A!_intro_right (FFL.Entailment.FiniteContext.deductInv! (FFL.Entailment.FiniteContext.of! h)))

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

def FFL.Entailment.right_K!_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral 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 FFL.Entailment.right_K_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} [DecidableEq F] (hq : 𝓢 ⊢ φ 🡒 ψ) (hr : 𝓢 ⊢ φ 🡒 χ) : 𝓢 ⊢ φ 🡒 ψ ⋏ χ

theorem FFL.Entailment.left_K_symm {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (d : 𝓢 ⊢ φ ⋏ ψ 🡒 χ) : 𝓢 ⊢ ψ ⋏ φ 🡒 χ

theorem FFL.Entailment.left_K_intro_right {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} [DecidableEq F] (h : 𝓢 ⊢ φ 🡒 χ) : 𝓢 ⊢ ψ ⋏ φ 🡒 χ

theorem FFL.Entailment.left_K_intro_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} [DecidableEq F] (h : 𝓢 ⊢ φ 🡒 χ) : 𝓢 ⊢ φ ⋏ ψ 🡒 χ

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

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

Equations

• FFL.Entailment.CAA! = FFL.Entailment.FiniteContext.deduct'! (FFL.Entailment.of_C!_of_C!_of_A! FFL.Entailment.or₂! FFL.Entailment.or₁! FFL.Entailment.FiniteContext.id!)

theorem FFL.Entailment.CAA {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} : 𝓢 ⊢ φ ⋎ ψ 🡒 ψ ⋎ φ

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

Equations

• FFL.Entailment.A!_symm h = FFL.Entailment.CAA!⨀!h

theorem FFL.Entailment.A_symm {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} (h : 𝓢 ⊢ φ ⋎ ψ) : 𝓢 ⊢ ψ ⋎ φ

theorem FFL.Entailment.A_assoc {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} : 𝓢 ⊢ φ ⋎ ψ ⋎ χ ↔ 𝓢 ⊢ (φ ⋎ ψ) ⋎ χ

theorem FFL.Entailment.K_assoc {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} : 𝓢 ⊢ (φ ⋏ ψ) ⋏ χ 🡘 φ ⋏ ψ ⋏ χ

theorem FFL.Entailment.K_assoc_mp {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ (φ ⋏ ψ) ⋏ χ) : 𝓢 ⊢ φ ⋏ ψ ⋏ χ

theorem FFL.Entailment.K_assoc_mpr {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ φ ⋏ ψ ⋏ χ) : 𝓢 ⊢ (φ ⋏ ψ) ⋏ χ

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

Equations

• FFL.Entailment.K!_replace_left hc h = FFL.Entailment.K!_intro (h⨀!FFL.Entailment.K!_left hc) (FFL.Entailment.K!_right hc)

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

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

Equations

• FFL.Entailment.CKK!_of_C! h = FFL.Entailment.FiniteContext.deduct'! (FFL.Entailment.K!_replace_left FFL.Entailment.FiniteContext.id! (FFL.Entailment.FiniteContext.of! h))

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

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

Equations

• FFL.Entailment.K!_replace_right hc h = FFL.Entailment.K!_intro (FFL.Entailment.K!_left hc) (h⨀!FFL.Entailment.K!_right hc)

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

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

Equations

• FFL.Entailment.CKK!_of_C!' h = FFL.Entailment.FiniteContext.deduct'! (FFL.Entailment.K!_replace_right FFL.Entailment.FiniteContext.id! (FFL.Entailment.FiniteContext.of! h))

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

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

Equations

• FFL.Entailment.K!_replace hc h₁ h₂ = FFL.Entailment.K!_replace_right (FFL.Entailment.K!_replace_left hc h₁) h₂

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

def FFL.Entailment.CKK!_of_C!_of_C! {F : Type u_1} [LogicalConnective F] [LogicalNeutral 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 FFL.Entailment.CKK_of_C_of_C {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ ξ : F} (h₁ : 𝓢 ⊢ φ 🡒 χ) (h₂ : 𝓢 ⊢ ψ 🡒 ξ) : 𝓢 ⊢ φ ⋏ ψ 🡒 χ ⋏ ξ

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

Equations

• FFL.Entailment.A!_replace_left hc hp = FFL.Entailment.of_C!_of_C!_of_A! (FFL.Entailment.C!_trans hp FFL.Entailment.or₁!) FFL.Entailment.or₂! hc

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

def FFL.Entailment.CAA!_of_C!_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (hp : 𝓢 ⊢! φ 🡒 χ) : 𝓢 ⊢! φ ⋎ ψ 🡒 χ ⋎ ψ

Equations

• FFL.Entailment.CAA!_of_C!_left hp = FFL.Entailment.FiniteContext.deduct'! (FFL.Entailment.A!_replace_left FFL.Entailment.FiniteContext.id! (FFL.Entailment.FiniteContext.of! hp))

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

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

Equations

• FFL.Entailment.A!_replace_right hc hq = FFL.Entailment.of_C!_of_C!_of_A! FFL.Entailment.or₁! (FFL.Entailment.C!_trans hq FFL.Entailment.or₂!) hc

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

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

Equations

• FFL.Entailment.CAA!_of_C!_right hq = FFL.Entailment.FiniteContext.deduct'! (FFL.Entailment.A!_replace_right FFL.Entailment.FiniteContext.id! (FFL.Entailment.FiniteContext.of! hq))

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

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

Equations

• FFL.Entailment.A!_replace h hp hq = FFL.Entailment.A!_replace_right (FFL.Entailment.A!_replace_left h hp) hq

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

def FFL.Entailment.CAA!_of_C!_of_C! {F : Type u_1} [LogicalConnective F] [LogicalNeutral 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 FFL.Entailment.CAA_of_C_of_C {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ₁ φ₂ ψ₁ ψ₂ : F} (hp : 𝓢 ⊢ φ₁ 🡒 φ₂) (hq : 𝓢 ⊢ ψ₁ 🡒 ψ₂) : 𝓢 ⊢ φ₁ ⋎ ψ₁ 🡒 φ₂ ⋎ ψ₂

def FFL.Entailment.EAA!_of_E!_of_E! {F : Type u_1} [LogicalConnective F] [LogicalNeutral 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 FFL.Entailment.EAA_of_E_of_E {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ₁ φ₂ ψ₁ ψ₂ : F} (hp : 𝓢 ⊢ φ₁ 🡘 φ₂) (hq : 𝓢 ⊢ ψ₁ 🡘 ψ₂) : 𝓢 ⊢ φ₁ ⋎ ψ₁ 🡘 φ₂ ⋎ ψ₂

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

theorem FFL.Entailment.EAA_of_E_right {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (d : 𝓢 ⊢ ψ 🡘 χ) : 𝓢 ⊢ φ ⋎ ψ 🡘 φ ⋎ χ

theorem FFL.Entailment.EAA_of_E_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (d : 𝓢 ⊢ φ 🡘 χ) : 𝓢 ⊢ φ ⋎ ψ 🡘 χ ⋎ ψ

def FFL.Entailment.EKK!_of_E!_of_E! {F : Type u_1} [LogicalConnective F] [LogicalNeutral 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 FFL.Entailment.EKK_of_E_of_E {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ₁ φ₂ ψ₁ ψ₂ : F} (hp : 𝓢 ⊢ φ₁ 🡘 φ₂) (hq : 𝓢 ⊢ ψ₁ 🡘 ψ₂) : 𝓢 ⊢ φ₁ ⋏ ψ₁ 🡘 φ₂ ⋏ ψ₂

def FFL.Entailment.ECC!_of_E!_of_E! {F : Type u_1} [LogicalConnective F] [LogicalNeutral 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 FFL.Entailment.ECC_of_E_of_E {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ₁ φ₂ ψ₁ ψ₂ : F} (hp : 𝓢 ⊢ φ₁ 🡘 φ₂) (hq : 𝓢 ⊢ ψ₁ 🡘 ψ₂) : 𝓢 ⊢ (φ₁ 🡒 ψ₁) 🡘 (φ₂ 🡒 ψ₂)

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

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

Equations

• FFL.Entailment.dni! = FFL.Entailment.FiniteContext.deduct'! (FFL.Entailment.N!_of_CO! (FFL.Entailment.FiniteContext.deduct! (FFL.Entailment.bot_of_mem_either! ⋯ ⋯)))

@[simp]

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

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

Equations

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

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

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

Equations

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

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

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

Equations

• FFL.Entailment.KNNNN!_of_K! d = FFL.Entailment.K!_intro (FFL.Entailment.dni'! (FFL.Entailment.K!_left d)) (FFL.Entailment.dni'! (FFL.Entailment.K!_right d))

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

def FFL.Entailment.CNNOO! {F : Type u_1} [LogicalConnective F] [LogicalNeutral 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 FFL.Entailment.ENNOO! {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] : 𝓢 ⊢! ∼∼⊥ 🡘 ⊥

Equations

• FFL.Entailment.ENNOO! = FFL.Entailment.K!_intro FFL.Entailment.CNNOO! FFL.Entailment.dni!

def FFL.Entailment.CCCNN! {F : Type u_1} [LogicalConnective F] [LogicalNeutral 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 FFL.Entailment.CCCNN {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] : 𝓢 ⊢ (φ 🡒 ψ) 🡒 ∼ψ 🡒 ∼φ

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

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

Alias of FFL.Entailment.CCCNN!.

Equations

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

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

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

Alias of FFL.Entailment.CCCNN.

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

Equations

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

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

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

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

Alias of FFL.Entailment.contra!.

Equations

• @FFL.Entailment.contra₀'! = @FFL.Entailment.contra!

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

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

Alias of FFL.Entailment.contra.

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

Equations

• FFL.Entailment.CNNNN!_of_C! b = FFL.Entailment.contra! (FFL.Entailment.contra! b)

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

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

Equations

• FFL.Entailment.CCCNNNN! = FFL.Entailment.FiniteContext.deduct'! (FFL.Entailment.CNNNN!_of_C! FFL.Entailment.FiniteContext.id!)

@[simp]

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

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

Equations

• FFL.Entailment.CN!_of_CN!_right b = FFL.Entailment.C!_trans FFL.Entailment.dni! (FFL.Entailment.contra! b)

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

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

Equations

• FFL.Entailment.CCNCN! = FFL.Entailment.FiniteContext.deduct'! (FFL.Entailment.CN!_of_CN!_right FFL.Entailment.FiniteContext.id!)

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

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

Equations

• FFL.Entailment.ENN!_of_E! b = FFL.Entailment.E!_intro (FFL.Entailment.contra! (FFL.Entailment.K!_right b)) (FFL.Entailment.contra! (FFL.Entailment.K!_left b))

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

def FFL.Entailment.ENNCCOO! {F : Type u_1} [LogicalConnective F] [LogicalNeutral 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 FFL.Entailment.ENNCCOO {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] : 𝓢 ⊢ ∼∼φ 🡘 ((φ 🡒 ⊥) 🡒 ⊥)

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

Equations

• FFL.Entailment.tne! = FFL.Entailment.contra! FFL.Entailment.dni!

@[simp]

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

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

Equations

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

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

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

Equations

• FFL.Entailment.tneIff! = FFL.Entailment.K!_intro FFL.Entailment.tne! FFL.Entailment.dni!

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

Equations

• FFL.Entailment.CCC!_of_C!_left h = FFL.Entailment.FiniteContext.deduct'! (FFL.Entailment.C!_trans (FFL.Entailment.FiniteContext.of! h) FFL.Entailment.FiniteContext.id!)

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

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

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

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

Equations

• @FFL.Entailment.rev_dhyp_imp'! = @FFL.Entailment.CCC!_of_C!_left

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

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

Alias of FFL.Entailment.CCC_of_C_left.

theorem FFL.Entailment.C_iff_C_of_iff_left {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ φ 🡘 ψ) : 𝓢 ⊢ φ 🡒 χ ↔ 𝓢 ⊢ ψ 🡒 χ

theorem FFL.Entailment.C_iff_C_of_iff_right {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} (h : 𝓢 ⊢ φ 🡘 ψ) : 𝓢 ⊢ χ 🡒 φ ↔ 𝓢 ⊢ χ 🡒 ψ

def FFL.Entailment.C!_swap {F : Type u_1} [LogicalConnective F] [LogicalNeutral 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 FFL.Entailment.C_swap {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ χ : F} [DecidableEq F] (h : 𝓢 ⊢ φ 🡒 ψ 🡒 χ) : 𝓢 ⊢ ψ 🡒 φ 🡒 χ

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

Equations

• FFL.Entailment.CCCCC! = FFL.Entailment.FiniteContext.deduct'! (FFL.Entailment.C!_swap FFL.Entailment.FiniteContext.id!)

@[simp]

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

def FFL.Entailment.C!_of_CC! {F : Type u_1} [LogicalConnective F] [LogicalNeutral 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 FFL.Entailment.C_of_CC {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] (h : 𝓢 ⊢ φ 🡒 φ 🡒 ψ) : 𝓢 ⊢ φ 🡒 ψ

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

Equations

• FFL.Entailment.CCC! = FFL.Entailment.C!_swap FFL.Entailment.C!_id

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

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

Equations

• FFL.Entailment.CCC!_of_C!_right h = FFL.Entailment.implyS!⨀!FFL.Entailment.C!_of_conseq! h

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

def FFL.Entailment.CNNCCNNNN! {F : Type u_1} [LogicalConnective F] [LogicalNeutral 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 FFL.Entailment.CNNCCNNNN {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] : 𝓢 ⊢ ∼∼(φ 🡒 ψ) 🡒 ∼∼φ 🡒 ∼∼ψ

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

Equations

• FFL.Entailment.CNNNN!_of_NNC! b = FFL.Entailment.CNNCCNNNN!⨀!b

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

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

Equations

• FFL.Entailment.O!_intro_of_KN! h = FFL.Entailment.CO!_of_N! (FFL.Entailment.K!_right h)⨀!FFL.Entailment.K!_left h

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

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

Law of contradiction

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

Equations

• FFL.Entailment.CKNO! = FFL.Entailment.FiniteContext.deduct'! (FFL.Entailment.O!_intro_of_KN! FFL.Entailment.FiniteContext.id!)

@[simp]

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

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

Law of contradiction

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

Equations

• FFL.Entailment.CANNNK! = FFL.Entailment.left_A!_intro (FFL.Entailment.contra! FFL.Entailment.and₁!) (FFL.Entailment.contra! FFL.Entailment.and₂!)

@[simp]

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

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

Equations

• FFL.Entailment.NK!_of_ANN! d = FFL.Entailment.CANNNK!⨀!d

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

def FFL.Entailment.CKNNNA! {F : Type u_1} [LogicalConnective F] [LogicalNeutral 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 FFL.Entailment.CKNNNA {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] : 𝓢 ⊢ ∼φ ⋏ ∼ψ 🡒 ∼(φ ⋎ ψ)

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

Equations

• FFL.Entailment.NA!_of_KNN! d = FFL.Entailment.CKNNNA!⨀!d

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

def FFL.Entailment.CNAKNN! {F : Type u_1} [LogicalConnective F] [LogicalNeutral 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 FFL.Entailment.CNAKNN {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ ψ : F} [DecidableEq F] : 𝓢 ⊢ ∼(φ ⋎ ψ) 🡒 ∼φ ⋏ ∼ψ

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

Equations

• FFL.Entailment.KNN!_of_NA! b = FFL.Entailment.CNAKNN!⨀!b

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

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

Equations

• One or more equations did not get rendered due to their size.
• FFL.Entailment.EConj₂Conj! [] = FFL.Entailment.E!_id
• FFL.Entailment.EConj₂Conj! (head :: ψ :: Γ) = FFL.Entailment.EKK!_of_E!_of_E! FFL.Entailment.E!_id (FFL.Entailment.EConj₂Conj! (ψ :: Γ))

@[simp]

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

theorem FFL.Entailment.CConj_iff_CConj₂ {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} {Γ : List F} : 𝓢 ⊢ Γ.conj 🡒 φ ↔ 𝓢 ⊢ ⋀Γ 🡒 φ

def FFL.Entailment.right_Conj'!_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral 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 FFL.Entailment.right_Conj'_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral 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 FFL.Entailment.left_Conj'!_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral 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

• FFL.Entailment.left_Conj'!_intro h φ = FFL.Entailment.left_Conj₂!_intro ⋯

theorem FFL.Entailment.left_Conj'_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral 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 FFL.Entailment.right_Fconj_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] (φ : F) (s : Finset F) (b : ∀ ψ ∈ s, 𝓢 ⊢ φ 🡒 ψ) : 𝓢 ⊢ φ 🡒 s.conj

theorem FFL.Entailment.left_Fconj_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] {s : Finset F} (h : φ ∈ s) : 𝓢 ⊢ s.conj 🡒 φ

theorem FFL.Entailment.right_Fconj'_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral 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 FFL.Entailment.left_Fconj'_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral 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 FFL.Entailment.right_Uconj_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral 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 FFL.Entailment.left_Uconj_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {ι : Type u_3} [DecidableEq F] [Fintype ι] (φ : ι → F) (i : ι) : 𝓢 ⊢ (⩕ (i : ι), φ i) 🡒 φ i

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem FFL.Entailment.CFConjConj₂_list {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] {Γ : List F} : 𝓢 ⊢ Γ.toFinset.conj 🡒 ⋀Γ

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

theorem FFL.Entailment.FConj_iff_forall_provable {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] {Γ : Finset F} : 𝓢 ⊢ Γ.conj ↔ ∀ φ ∈ Γ, 𝓢 ⊢ φ

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

theorem FFL.Entailment.CFConjFConj_of_subset {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] {Γ Δ : Finset F} (h : Δ ⊆ Γ) : 𝓢 ⊢ Γ.conj 🡒 Δ.conj

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

def FFL.Entailment.right_Disj!_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral 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.
• FFL.Entailment.right_Disj!_intro [] h_2 = ⋯.elim

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

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

Equations

• FFL.Entailment.right_Disj!_intro' Γ h hψ = FFL.Entailment.C!_trans hψ (FFL.Entailment.right_Disj!_intro Γ h)

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

def FFL.Entailment.right_Disj₂!_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral 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.
• FFL.Entailment.right_Disj₂!_intro [] h_2 = ⋯.elim
• FFL.Entailment.right_Disj₂!_intro [ψ] h_2 = ⋯ ▸ FFL.Entailment.C!_id

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

def FFL.Entailment.right_Disj'!_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral 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

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

theorem FFL.Entailment.right_Disj'_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral 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 FFL.Entailment.right_Fdisj_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {φ : F} [DecidableEq F] (s : Finset F) (h : φ ∈ s) : 𝓢 ⊢ φ 🡒 s.disj

theorem FFL.Entailment.right_Fdisj'_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral 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 FFL.Entailment.right_Udisj_intro {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] {ι : Type u_3} {i : ι} [DecidableEq F] [Fintype ι] (φ : ι → F) : 𝓢 ⊢ φ i 🡒 ⩖ (j : ι), φ j

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

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

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

theorem FFL.Entailment.FConj'_iff_forall_provable {F : Type u_1} [LogicalConnective F] [LogicalNeutral 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 FFL.Entailment.Context.provable_iff_finset {F : Type u_1} [LogicalConnective F] [LogicalNeutral F] {S : Type u_2} [Entailment S F] {𝓢 : S} [Entailment.Minimal 𝓢] [DecidableEq F] {Γ : Set F} {φ : F} : Γ *⊢[𝓢] φ ↔ ∃ (Δ : Finset F), ↑Δ ⊆ Γ ∧ ↑Δ *⊢[𝓢] φ

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