#Algebraic Proofs of Cut Elimination

Main reference: Jeremy Avigad, Algebraic proofs of cut elimination, The Journal of Logic and Algebraic Programming, Volume 49, Issues 1–2, 2001, Pages 15-30

inductive LO.FirstOrder.Derivation.IsCutFree {L : Language} {Γ : Sequent L} : ⊢ᵀ Γ → Prop

• axL {L : Language} (Γ : List (SyntacticFormula L)) {k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ℕ 0) : IsCutFree (Derivation.axL Γ r v)
• verum {L : Language} (Γ : List (SyntacticFormula L)) : IsCutFree (Derivation.verum Γ)
• or {L : Language} {Γ : List (SyntacticFormula L)} {φ ψ : SyntacticFormula L} {d : ⊢ᵀ φ :: ψ :: Γ} : IsCutFree d → IsCutFree (Derivation.or d)
• and {L : Language} {Γ : List (SyntacticFormula L)} {φ ψ : SyntacticFormula L} {dφ : ⊢ᵀ φ :: Γ} {dψ : ⊢ᵀ ψ :: Γ} : IsCutFree dφ → IsCutFree dψ → IsCutFree (Derivation.and dφ dψ)
• all {L : Language} {Γ : List (SyntacticSemiformula L 0)} {φ : SyntacticSemiformula L (0 + 1)} {d : ⊢ᵀ Rewriting.free φ :: Rewriting.shifts Γ} : IsCutFree d → IsCutFree (Derivation.all d)
• ex {L : Language} {Γ : List (SyntacticFormula L)} {φ : SyntacticSemiformula L (Nat.succ 0)} (t : Semiterm L ℕ 0) {d : ⊢ᵀ φ/[t] :: Γ} : IsCutFree d → IsCutFree (Derivation.ex t d)
• wk {L : Language} {Δ Γ : Sequent L} {d : ⊢ᵀ Δ} (ss : Δ ⊆ Γ) : IsCutFree d → IsCutFree (Derivation.wk d ss)

@[simp]

theorem LO.FirstOrder.Derivation.isCutFree_or_iff {L : Language} {Γ : Sequent L} {φ ψ : SyntacticFormula L} {d : ⊢ᵀ φ :: ψ :: Γ} : IsCutFree (or d) ↔ IsCutFree d

@[simp]

theorem LO.FirstOrder.Derivation.isCutFree_and_iff {L : Language} {Γ : Sequent L} {φ ψ : SyntacticFormula L} {dφ : ⊢ᵀ φ :: Γ} {dψ : ⊢ᵀ ψ :: Γ} : IsCutFree (and dφ dψ) ↔ IsCutFree dφ ∧ IsCutFree dψ

@[simp]

theorem LO.FirstOrder.Derivation.isCutFree_all_iff {L : Language} {Γ : Sequent L} {φ : SyntacticSemiformula L (0 + 1)} {d : ⊢ᵀ Rewriting.free φ :: Rewriting.shifts Γ} : IsCutFree (all d) ↔ IsCutFree d

@[simp]

theorem LO.FirstOrder.Derivation.isCutFree_ex_iff {L : Language} {Γ : Sequent L} {φ : SyntacticSemiformula L (Nat.succ 0)} {t : Semiterm L ℕ 0} {d : ⊢ᵀ φ/[t] :: Γ} : IsCutFree (ex t d) ↔ IsCutFree d

@[simp]

theorem LO.FirstOrder.Derivation.isCutFree_wk_iff {L : Language} {Γ Δ : Sequent L} {d : ⊢ᵀ Δ} {ss : Δ ⊆ Γ} : IsCutFree (wk d ss) ↔ IsCutFree d

@[simp]

theorem LO.FirstOrder.Derivation.IsCutFree.cast {L : Language} {Γ Δ : Sequent L} {d : ⊢ᵀ Γ} {e : Γ = Δ} : IsCutFree (Derivation.cast d e) ↔ IsCutFree d

@[simp]

theorem LO.FirstOrder.Derivation.IsCutFree.not_cut {L : Language} {Γ : Sequent L} {φ : SyntacticFormula L} (dp : ⊢ᵀ φ :: Γ) (dn : ⊢ᵀ ∼φ :: Γ) : ¬IsCutFree (cut dp dn)

@[simp]

theorem LO.FirstOrder.Derivation.isCutFree_rewrite_iff_isCutFree {L : Language} {Γ : Sequent L} {f : ℕ → SyntacticTerm L} {d : ⊢ᵀ Γ} : IsCutFree (rewrite d f) ↔ IsCutFree d

@[simp]

theorem LO.FirstOrder.Derivation.isCutFree_map_iff_isCutFree {L : Language} {Γ : Sequent L} {f : ℕ → ℕ} {d : ⊢ᵀ Γ} : IsCutFree (Derivation.map d f) ↔ IsCutFree d

@[simp]

theorem LO.FirstOrder.Derivation.IsCutFree.genelalizeByNewver_isCutFree {L : Language} {Δ : Sequent L} {m : ℕ} {φ : SyntacticSemiformula L 1} (hp : ¬Semiformula.FVar? φ m) (hΔ : ∀ ψ ∈ Δ, ¬Semiformula.FVar? ψ m) (d : ⊢ᵀ φ/[Semiterm.fvar m] :: Δ) : IsCutFree (genelalizeByNewver hp hΔ d) ↔ IsCutFree d

inductive LO.FirstOrder.PositiveDerivationFrom {L : Language} (Ξ : Sequent L) : Sequent L → Type u

• verum {L : Language} {Ξ : Sequent L} (Γ : List (SyntacticFormula L)) : Ξ ⟶⁺ ⊤ :: Γ
• or {L : Language} {Ξ : Sequent L} {Γ : List (SyntacticFormula L)} {φ ψ : SyntacticFormula L} : Ξ ⟶⁺ φ :: ψ :: Γ → Ξ ⟶⁺ φ ⋎ ψ :: Γ
• ex {L : Language} {Ξ : Sequent L} {Γ : List (SyntacticFormula L)} {φ : SyntacticSemiformula L (Nat.succ 0)} (t : Semiterm L ℕ 0) : Ξ ⟶⁺ φ/[t] :: Γ → Ξ ⟶⁺ (∃' φ) :: Γ
• wk {L : Language} {Ξ Γ Δ : Sequent L} : Ξ ⟶⁺ Δ → Δ ⊆ Γ → Ξ ⟶⁺ Γ
• id {L : Language} {Ξ : Sequent L} : Ξ ⟶⁺ Ξ

def LO.FirstOrder.«term_⟶⁺_» : Lean.TrailingParserDescr

Equations

• LO.FirstOrder.«term_⟶⁺_» = Lean.ParserDescr.trailingNode `LO.FirstOrder.«term_⟶⁺_» 45 46 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⟶⁺ ") (Lean.ParserDescr.cat `term 46))

def LO.FirstOrder.PositiveDerivationFrom.ofSubset {L : Language} {Ξ Γ : Sequent L} (ss : Ξ ⊆ Γ) : Ξ ⟶⁺ Γ

Equations

• LO.FirstOrder.PositiveDerivationFrom.ofSubset ss = LO.FirstOrder.PositiveDerivationFrom.id.wk ss

def LO.FirstOrder.PositiveDerivationFrom.trans {L : Language} {Ξ Γ Δ : Sequent L} : Ξ ⟶⁺ Γ → Γ ⟶⁺ Δ → Ξ ⟶⁺ Δ

Equations

• x✝.trans (LO.FirstOrder.PositiveDerivationFrom.verum Γ_1) = LO.FirstOrder.PositiveDerivationFrom.verum Γ_1
• x✝.trans d.or = (x✝.trans d).or
• x✝.trans (LO.FirstOrder.PositiveDerivationFrom.ex t d) = LO.FirstOrder.PositiveDerivationFrom.ex t (x✝.trans d)
• x✝.trans (d.wk h) = (x✝.trans d).wk h
• x✝.trans LO.FirstOrder.PositiveDerivationFrom.id = x✝

def LO.FirstOrder.PositiveDerivationFrom.cons {L : Language} {Ξ Γ : Sequent L} (φ : SyntacticFormula L) : Ξ ⟶⁺ Γ → φ :: Ξ ⟶⁺ φ :: Γ

Equations

• LO.FirstOrder.PositiveDerivationFrom.cons φ (LO.FirstOrder.PositiveDerivationFrom.verum Γ_2) = (LO.FirstOrder.PositiveDerivationFrom.verum Γ_2).wk ⋯
• LO.FirstOrder.PositiveDerivationFrom.cons φ d.or = ((LO.FirstOrder.PositiveDerivationFrom.cons φ d).wk ⋯).or.wk ⋯
• LO.FirstOrder.PositiveDerivationFrom.cons φ (LO.FirstOrder.PositiveDerivationFrom.ex t d) = (LO.FirstOrder.PositiveDerivationFrom.ex t ((LO.FirstOrder.PositiveDerivationFrom.cons φ d).wk ⋯)).wk ⋯
• LO.FirstOrder.PositiveDerivationFrom.cons φ (d.wk h) = (LO.FirstOrder.PositiveDerivationFrom.cons φ d).wk ⋯
• LO.FirstOrder.PositiveDerivationFrom.cons φ LO.FirstOrder.PositiveDerivationFrom.id = LO.FirstOrder.PositiveDerivationFrom.id

def LO.FirstOrder.PositiveDerivationFrom.append {L : Language} {Ξ Γ : Sequent L} (Δ : Sequent L) : Ξ ⟶⁺ Γ → Δ ++ Ξ ⟶⁺ Δ ++ Γ

Equations

• LO.FirstOrder.PositiveDerivationFrom.append [] x✝ = x✝
• LO.FirstOrder.PositiveDerivationFrom.append (φ :: Δ) x✝ = LO.FirstOrder.PositiveDerivationFrom.cons φ (LO.FirstOrder.PositiveDerivationFrom.append Δ x✝)

def LO.FirstOrder.PositiveDerivationFrom.add {L : Language} {Γ Δ Ξ Θ : Sequent L} : Γ ⟶⁺ Δ → Ξ ⟶⁺ Θ → Γ ++ Ξ ⟶⁺ Δ ++ Θ

Equations

• (LO.FirstOrder.PositiveDerivationFrom.verum Δ_2).add x✝ = LO.FirstOrder.PositiveDerivationFrom.verum (Δ_2.append Θ)
• d.or.add x✝ = (d.add x✝).or
• (LO.FirstOrder.PositiveDerivationFrom.ex t d).add x✝ = LO.FirstOrder.PositiveDerivationFrom.ex t (d.add x✝)
• (d.wk h).add x✝ = (d.add x✝).wk ⋯
• LO.FirstOrder.PositiveDerivationFrom.id.add x✝ = LO.FirstOrder.PositiveDerivationFrom.append Γ x✝

def LO.FirstOrder.PositiveDerivationFrom.graft {L : Language} {Ξ Γ : Sequent L} (b : ⊢ᵀ Ξ) : Ξ ⟶⁺ Γ → ⊢ᵀ Γ

Equations

• LO.FirstOrder.PositiveDerivationFrom.graft b (LO.FirstOrder.PositiveDerivationFrom.verum Γ_2) = LO.FirstOrder.Derivation.verum Γ_2
• LO.FirstOrder.PositiveDerivationFrom.graft b d.or = LO.FirstOrder.Derivation.or (LO.FirstOrder.PositiveDerivationFrom.graft b d)
• LO.FirstOrder.PositiveDerivationFrom.graft b (LO.FirstOrder.PositiveDerivationFrom.ex t d) = LO.FirstOrder.Derivation.ex t (LO.FirstOrder.PositiveDerivationFrom.graft b d)
• LO.FirstOrder.PositiveDerivationFrom.graft b (d.wk h) = LO.FirstOrder.Derivation.wk (LO.FirstOrder.PositiveDerivationFrom.graft b d) h
• LO.FirstOrder.PositiveDerivationFrom.graft b LO.FirstOrder.PositiveDerivationFrom.id = b

theorem LO.FirstOrder.PositiveDerivationFrom.graft_isCutFree_of_isCutFree {L : Language} {Ξ Γ : Sequent L} {b : ⊢ᵀ Ξ} {d : Ξ ⟶⁺ Γ} (hb : Derivation.IsCutFree b) : Derivation.IsCutFree (graft b d)

structure LO.FirstOrder.Hauptsatz.StrongerThan {L : Language} (q p : Sequent L) : Type u

• val : ∼p ⟶⁺ ∼q

def LO.FirstOrder.Hauptsatz.«term_≼_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Hauptsatz.instMinSequent {L : Language} : Min (Sequent L)

Equations

• LO.FirstOrder.Hauptsatz.instMinSequent = { min := fun (p q : LO.FirstOrder.Sequent L) => p ++ q }

theorem LO.FirstOrder.Hauptsatz.inf_def {L : Language} (p q : Sequent L) : p ⊓ q = p ++ q

@[simp]

theorem LO.FirstOrder.Hauptsatz.neg_inf_p_eq {L : Language} (p q : Sequent L) : ∼(p ⊓ q) = ∼p ⊓ ∼q

def LO.FirstOrder.Hauptsatz.StrongerThan.refl {L : Language} (p : Sequent L) : StrongerThan p p

Equations

• LO.FirstOrder.Hauptsatz.StrongerThan.refl p = { val := LO.FirstOrder.PositiveDerivationFrom.id }

def LO.FirstOrder.Hauptsatz.StrongerThan.trans {L : Language} {r q p : Sequent L} (srq : StrongerThan r q) (sqp : StrongerThan q p) : StrongerThan r p

Equations

• srq.trans sqp = { val := sqp.val.trans srq.val }

def LO.FirstOrder.Hauptsatz.StrongerThan.ofSubset {L : Language} {q p : Sequent L} (h : q ⊇ p) : StrongerThan q p

Equations

• LO.FirstOrder.Hauptsatz.StrongerThan.ofSubset h = { val := LO.FirstOrder.PositiveDerivationFrom.ofSubset ⋯ }

def LO.FirstOrder.Hauptsatz.StrongerThan.and {L : Language} {p : Sequent L} (φ ψ : SyntacticFormula L) : StrongerThan (φ ⋏ ψ :: p) (φ :: ψ :: p)

Equations

• LO.FirstOrder.Hauptsatz.StrongerThan.and φ ψ = { val := LO.FirstOrder.PositiveDerivationFrom.id.or }

def LO.FirstOrder.Hauptsatz.StrongerThan.andLeft {L : Language} {p : Sequent L} (φ ψ : SyntacticFormula L) : StrongerThan (φ ⋏ ψ :: p) (φ :: p)

Equations

• LO.FirstOrder.Hauptsatz.StrongerThan.andLeft φ ψ = (LO.FirstOrder.Hauptsatz.StrongerThan.and φ ψ).trans (LO.FirstOrder.Hauptsatz.StrongerThan.ofSubset ⋯)

def LO.FirstOrder.Hauptsatz.StrongerThan.andRight {L : Language} {p : Sequent L} (φ ψ : SyntacticFormula L) : StrongerThan (φ ⋏ ψ :: p) (ψ :: p)

Equations

• LO.FirstOrder.Hauptsatz.StrongerThan.andRight φ ψ = (LO.FirstOrder.Hauptsatz.StrongerThan.and φ ψ).trans (LO.FirstOrder.Hauptsatz.StrongerThan.ofSubset ⋯)

def LO.FirstOrder.Hauptsatz.StrongerThan.all {L : Language} {p : Sequent L} (φ : SyntacticSemiformula L 1) (t : Semiterm L ℕ 0) : StrongerThan ((∀' φ) :: p) (φ/[t] :: p)

Equations

• LO.FirstOrder.Hauptsatz.StrongerThan.all φ t = { val := LO.FirstOrder.PositiveDerivationFrom.ex t (⋯.mpr LO.FirstOrder.PositiveDerivationFrom.id) }

def LO.FirstOrder.Hauptsatz.StrongerThan.minLeLeft {L : Language} (p q : Sequent L) : StrongerThan (p ⊓ q) p

Equations

• LO.FirstOrder.Hauptsatz.StrongerThan.minLeLeft p q = LO.FirstOrder.Hauptsatz.StrongerThan.ofSubset ⋯

def LO.FirstOrder.Hauptsatz.StrongerThan.minLeRight {L : Language} (p q : Sequent L) : StrongerThan (p ⊓ q) q

Equations

• LO.FirstOrder.Hauptsatz.StrongerThan.minLeRight p q = LO.FirstOrder.Hauptsatz.StrongerThan.ofSubset ⋯

def LO.FirstOrder.Hauptsatz.StrongerThan.leMinOfle {L✝ : Language} {r p q : Sequent L✝} (srp : StrongerThan r p) (srq : StrongerThan r q) : StrongerThan r (p ⊓ q)

Equations

• srp.leMinOfle srq = { val := let d := (srp.val.add srq.val).wk ⋯; ⋯ ▸ d }

def LO.FirstOrder.Hauptsatz.StrongerThan.leMinRightOfLe {L✝ : Language} {q p : Sequent L✝} (s : StrongerThan q p) : StrongerThan q (p ⊓ q)

Equations

• s.leMinRightOfLe = s.leMinOfle (LO.FirstOrder.Hauptsatz.StrongerThan.refl q)

@[reducible, inline]

abbrev LO.FirstOrder.Hauptsatz.Forces {L : Language} (p : Sequent L) : SyntacticFormulaᵢ L → Type u

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.Hauptsatz.Forces p LO.FirstOrder.Semiformulaᵢ.verum = PUnit.{?u.1352 + 1}
• LO.FirstOrder.Hauptsatz.Forces p LO.FirstOrder.Semiformulaᵢ.falsum = { b : ⊢ᵀ ∼p // LO.FirstOrder.Derivation.IsCutFree b }
• LO.FirstOrder.Hauptsatz.Forces p (LO.FirstOrder.Semiformulaᵢ.rel R v) = { b : ⊢ᵀ LO.FirstOrder.Semiformula.rel R v :: ∼p // LO.FirstOrder.Derivation.IsCutFree b }
• LO.FirstOrder.Hauptsatz.Forces p (LO.FirstOrder.Semiformulaᵢ.and φ ψ) = (LO.FirstOrder.Hauptsatz.Forces p φ × LO.FirstOrder.Hauptsatz.Forces p ψ)
• LO.FirstOrder.Hauptsatz.Forces p (LO.FirstOrder.Semiformulaᵢ.or φ ψ) = (LO.FirstOrder.Hauptsatz.Forces p φ ⊕ LO.FirstOrder.Hauptsatz.Forces p ψ)
• LO.FirstOrder.Hauptsatz.Forces p (LO.FirstOrder.Semiformulaᵢ.all φ) = ((t : LO.FirstOrder.SyntacticTerm L) → LO.FirstOrder.Hauptsatz.Forces p (φ/[t]))
• LO.FirstOrder.Hauptsatz.Forces p (LO.FirstOrder.Semiformulaᵢ.ex φ) = ((t : LO.FirstOrder.SyntacticTerm L) × LO.FirstOrder.Hauptsatz.Forces p (φ/[t]))

def LO.FirstOrder.Hauptsatz.«term_⊩_» : Lean.TrailingParserDescr

Equations

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

@[reducible, inline]

abbrev LO.FirstOrder.Hauptsatz.allForces {L : Language} (φ : SyntacticFormulaᵢ L) : Type u

Equations

• LO.FirstOrder.Hauptsatz.allForces φ = ((p : LO.FirstOrder.Sequent L) → LO.FirstOrder.Hauptsatz.Forces p φ)

def LO.FirstOrder.Hauptsatz.«term⊩_» : Lean.ParserDescr

Equations

• LO.FirstOrder.Hauptsatz.«term⊩_» = Lean.ParserDescr.node `LO.FirstOrder.Hauptsatz.«term⊩_» 45 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "⊩ ") (Lean.ParserDescr.cat `term 45))

def LO.FirstOrder.Hauptsatz.Forces.verumEquiv {L✝ : Language} {p : Sequent L✝} : Forces p ⊤ ≃ PUnit.{u_1 + 1}

Equations

• LO.FirstOrder.Hauptsatz.Forces.verumEquiv = Equiv.refl (LO.FirstOrder.Hauptsatz.Forces p ⊤)

def LO.FirstOrder.Hauptsatz.Forces.falsumEquiv {L✝ : Language} {p : Sequent L✝} : Forces p ⊥ ≃ { b : ⊢ᵀ ∼p // Derivation.IsCutFree b }

Equations

• LO.FirstOrder.Hauptsatz.Forces.falsumEquiv = Equiv.refl (LO.FirstOrder.Hauptsatz.Forces p ⊥)

def LO.FirstOrder.Hauptsatz.Forces.relEquiv {L : Language} {p : Sequent L} {k : ℕ} {R : L.Rel k} {v : Fin k → Semiterm L ℕ 0} : Forces p (Semiformulaᵢ.rel R v) ≃ { b : ⊢ᵀ Semiformula.rel R v :: ∼p // Derivation.IsCutFree b }

Equations

• LO.FirstOrder.Hauptsatz.Forces.relEquiv = Equiv.refl (LO.FirstOrder.Hauptsatz.Forces p (LO.FirstOrder.Semiformulaᵢ.rel R v))

def LO.FirstOrder.Hauptsatz.Forces.andEquiv {L : Language} {p : Sequent L} {φ ψ : SyntacticFormulaᵢ L} : Forces p (φ ⋏ ψ) ≃ Forces p φ × Forces p ψ

Equations

• LO.FirstOrder.Hauptsatz.Forces.andEquiv = Equiv.refl (LO.FirstOrder.Hauptsatz.Forces p (φ ⋏ ψ))

def LO.FirstOrder.Hauptsatz.Forces.orEquiv {L : Language} {p : Sequent L} {φ ψ : SyntacticFormulaᵢ L} : Forces p (φ ⋎ ψ) ≃ Forces p φ ⊕ Forces p ψ

Equations

• LO.FirstOrder.Hauptsatz.Forces.orEquiv = Equiv.refl (LO.FirstOrder.Hauptsatz.Forces p (φ ⋎ ψ))

def LO.FirstOrder.Hauptsatz.Forces.implyEquiv {L : Language} {p : Sequent L} {φ ψ : SyntacticFormulaᵢ L} : Forces p (φ ➝ ψ) ≃ ((q : Sequent L) → StrongerThan q p → Forces q φ → Forces q ψ)

Equations

• LO.FirstOrder.Hauptsatz.Forces.implyEquiv = Equiv.refl (LO.FirstOrder.Hauptsatz.Forces p (φ ➝ ψ))

def LO.FirstOrder.Hauptsatz.Forces.allEquiv {L : Language} {p : Sequent L} {φ : SyntacticSemiformulaᵢ L (0 + 1)} : Forces p (∀' φ) ≃ ((t : SyntacticTerm L) → Forces p (φ/[t]))

Equations

• LO.FirstOrder.Hauptsatz.Forces.allEquiv = Equiv.refl (LO.FirstOrder.Hauptsatz.Forces p (∀' φ))

def LO.FirstOrder.Hauptsatz.Forces.exEquiv {L : Language} {p : Sequent L} {φ : SyntacticSemiformulaᵢ L (0 + 1)} : Forces p (∃' φ) ≃ (t : SyntacticTerm L) × Forces p (φ/[t])

Equations

• LO.FirstOrder.Hauptsatz.Forces.exEquiv = Equiv.refl (LO.FirstOrder.Hauptsatz.Forces p (∃' φ))

@[irreducible]

def LO.FirstOrder.Hauptsatz.Forces.monotone {L : Language} {q p : Sequent L} (s : StrongerThan q p) {φ : SyntacticFormulaᵢ L} : Forces p φ → Forces q φ

@[irreducible]

def LO.FirstOrder.Hauptsatz.Forces.explosion {L : Language} {p : Sequent L} (b : Forces p ⊥) (φ : SyntacticFormulaᵢ L) : Forces p φ

Equations

• One or more equations did not get rendered due to their size.
• b.explosion LO.FirstOrder.Semiformulaᵢ.verum = PUnit.unit
• b.explosion LO.FirstOrder.Semiformulaᵢ.falsum = b
• b.explosion (LO.FirstOrder.Semiformulaᵢ.and φ ψ) = LO.FirstOrder.Hauptsatz.Forces.andEquiv.symm (b.explosion φ, b.explosion ψ)
• b.explosion (LO.FirstOrder.Semiformulaᵢ.or φ ψ) = LO.FirstOrder.Hauptsatz.Forces.orEquiv.symm (Sum.inl (b.explosion φ))
• b.explosion (LO.FirstOrder.Semiformulaᵢ.all φ) = LO.FirstOrder.Hauptsatz.Forces.allEquiv.symm fun (t : LO.FirstOrder.SyntacticTerm L) => b.explosion (φ/[t])
• b.explosion (LO.FirstOrder.Semiformulaᵢ.ex φ) = LO.FirstOrder.Hauptsatz.Forces.exEquiv.symm ⟨default, b.explosion (φ/[default])⟩

def LO.FirstOrder.Hauptsatz.Forces.efq {L : Language} (φ : SyntacticFormulaᵢ L) : allForces (⊥ ➝ φ)

Equations

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

def LO.FirstOrder.Hauptsatz.Forces.implyOf {L : Language} {p : Sequent L} {φ ψ : SyntacticFormulaᵢ L} (b : (q : Sequent L) → Forces q φ → Forces (p ⊓ q) ψ) : Forces p (φ ➝ ψ)

Equations

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

def LO.FirstOrder.Hauptsatz.Forces.modusPonens {L : Language} {p : Sequent L} {φ ψ : SyntacticFormulaᵢ L} (f : Forces p (φ ➝ ψ)) (g : Forces p φ) : Forces p ψ

Equations

• f.modusPonens g = LO.FirstOrder.Hauptsatz.Forces.implyEquiv f p (LO.FirstOrder.Hauptsatz.StrongerThan.refl p) g

@[irreducible]

noncomputable def LO.FirstOrder.Hauptsatz.Forces.ofMinimalProof {L : Language} {φ : SyntacticFormulaᵢ L} : 𝐌𝐢𝐧¹ ⊢ φ → allForces φ

def LO.FirstOrder.Hauptsatz.Forces.relRefl {L : Language} {k : ℕ} (R : L.Rel k) (v : Fin k → SyntacticTerm L) : Forces [Semiformula.rel R v] (Semiformulaᵢ.rel R v)

Equations

• LO.FirstOrder.Hauptsatz.Forces.relRefl R v = LO.FirstOrder.Hauptsatz.Forces.relEquiv.symm ⟨LO.FirstOrder.Derivation.axL (List.map (fun (x : LO.FirstOrder.Semiformula L ℕ 0) => ∼x) []) R v, ⋯⟩

@[irreducible]

def LO.FirstOrder.Hauptsatz.Forces.refl {L : Language} (φ : SyntacticFormula L) : Forces [φ] (Semiformula.doubleNegation φ)

def LO.FirstOrder.Hauptsatz.Forces.conj {L : Language} {p : Sequent L} {Γ : Sequentᵢ L} (b : (φ : SyntacticFormulaᵢ L) → φ ∈ Γ → Forces p φ) : Forces p (⋀Γ)

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.Hauptsatz.Forces.conj x_2 = PUnit.unit
• LO.FirstOrder.Hauptsatz.Forces.conj b = b φ ⋯

def LO.FirstOrder.Hauptsatz.Forces.conj' {L : Language} {p Γ : Sequent L} (b : (φ : SyntacticFormula L) → φ ∈ Γ → Forces p (Semiformula.doubleNegation φ)) : Forces p (⋀Sequent.doubleNegation Γ)

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.Hauptsatz.Forces.conj' x_2 = PUnit.unit
• LO.FirstOrder.Hauptsatz.Forces.conj' b = b φ ⋯

noncomputable def LO.FirstOrder.Hauptsatz.main {L : Language} [L.DecidableEq] {Γ : Sequent L} : ⊢ᵀ Γ → { d : ⊢ᵀ Γ // Derivation.IsCutFree d }

Equations

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

def LO.FirstOrder.hauptsatz {L : Language} [L.DecidableEq] {Γ : Sequent L} : ⊢ᵀ Γ → { d : ⊢ᵀ Γ // Derivation.IsCutFree d }

Alias of LO.FirstOrder.Hauptsatz.main.

Equations

• @LO.FirstOrder.hauptsatz = @LO.FirstOrder.Hauptsatz.main