Hauptsatz of classical first-order logic

Main reference: Jeremy Avigad, Algebraic proofs of cut elimination [Avi01]

inductive LO.FirstOrder.Derivation.Positive {L : Language} (Ξ : Sequent L) : Sequent L → Type u_1

• or {L : Language} {Ξ : Sequent L} {φ ψ : Proposition L} {Γ : List (Proposition L)} : Ξ ⟶⁺ φ :: ψ :: Γ → Ξ ⟶⁺ φ ⋎ ψ :: Γ
• exs {L : Language} {Ξ : Sequent L} {φ : Semiproposition L (Nat.succ 0)} {t : Semiterm L ℕ 0} {Γ : List (Proposition L)} : Ξ ⟶⁺ φ/[t] :: Γ → Ξ ⟶⁺ (∃¹ φ) :: Γ
• contraction {L : Language} {Ξ Δ Γ : Sequent L} : Ξ ⟶⁺ Δ → Δ ⊆ Γ → Ξ ⟶⁺ Γ
• id {L : Language} {Ξ : Sequent L} : Ξ ⟶⁺ Ξ

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

Equations

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

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

Equations

• LO.FirstOrder.Derivation.Positive.ofSubset ss = LO.FirstOrder.Derivation.Positive.id.contraction ss

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

Equations

• x✝.trans d.or = (x✝.trans d).or
• x✝.trans d.exs = (x✝.trans d).exs
• x✝.trans (d.contraction h) = (x✝.trans d).contraction h
• x✝.trans LO.FirstOrder.Derivation.Positive.id = x✝

def LO.FirstOrder.Derivation.Positive.cons {L : Language} {Ξ Γ : Sequent L} (φ : Proposition L) : Ξ ⟶⁺ Γ → φ :: Ξ ⟶⁺ φ :: Γ

Equations

• LO.FirstOrder.Derivation.Positive.cons φ d.or = ((LO.FirstOrder.Derivation.Positive.cons φ d).contraction ⋯).or.contraction ⋯
• LO.FirstOrder.Derivation.Positive.cons φ d.exs = ((LO.FirstOrder.Derivation.Positive.cons φ d).contraction ⋯).exs.contraction ⋯
• LO.FirstOrder.Derivation.Positive.cons φ (d.contraction h) = (LO.FirstOrder.Derivation.Positive.cons φ d).contraction ⋯
• LO.FirstOrder.Derivation.Positive.cons φ LO.FirstOrder.Derivation.Positive.id = LO.FirstOrder.Derivation.Positive.id

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

Equations

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

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

Equations

• d.or.add x✝ = (d.add x✝).or
• d.exs.add x✝ = (d.add x✝).exs
• (d.contraction h).add x✝ = (d.add x✝).contraction ⋯
• LO.FirstOrder.Derivation.Positive.id.add x✝ = LO.FirstOrder.Derivation.Positive.append Γ x✝

def LO.FirstOrder.Derivation.Positive.graft {L : Language} {Ξ Γ : Sequent L} (b : ⊢ᴸᴷ¹ Ξ) : Ξ ⟶⁺ Γ → ⊢ᴸᴷ¹ Γ

Equations

• LO.FirstOrder.Derivation.Positive.graft b d.or = (LO.FirstOrder.Derivation.Positive.graft b d).or
• LO.FirstOrder.Derivation.Positive.graft b d.exs = (LO.FirstOrder.Derivation.Positive.graft b d).exs
• LO.FirstOrder.Derivation.Positive.graft b (d.contraction h) = (LO.FirstOrder.Derivation.Positive.graft b d).contraction h
• LO.FirstOrder.Derivation.Positive.graft b LO.FirstOrder.Derivation.Positive.id = b

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

structure LO.FirstOrder.Derivation.Canonical.StrongerThan {L : Language} (q p : Sequent L) : Type u_1

• val : ∼p ⟶⁺ ∼q

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

Equations

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

@[implicit_reducible]

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

Equations

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

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

@[simp]

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

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

Equations

• LO.FirstOrder.Derivation.Canonical.StrongerThan.refl p = { val := LO.FirstOrder.Derivation.Positive.id }

def LO.FirstOrder.Derivation.Canonical.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.Derivation.Canonical.StrongerThan.ofSubset {L : Language} {q p : Sequent L} (h : q ⊇ p) : StrongerThan q p

Equations

• LO.FirstOrder.Derivation.Canonical.StrongerThan.ofSubset h = { val := LO.FirstOrder.Derivation.Positive.ofSubset ⋯ }

def LO.FirstOrder.Derivation.Canonical.StrongerThan.and {L : Language} {p : Sequent L} (φ ψ : Proposition L) : StrongerThan (φ ⋏ ψ :: p) (φ :: ψ :: p)

Equations

• LO.FirstOrder.Derivation.Canonical.StrongerThan.and φ ψ = { val := LO.FirstOrder.Derivation.Positive.id.or }

def LO.FirstOrder.Derivation.Canonical.StrongerThan.K_left {L : Language} {p : Sequent L} (φ ψ : Proposition L) : StrongerThan (φ ⋏ ψ :: p) (φ :: p)

Equations

• LO.FirstOrder.Derivation.Canonical.StrongerThan.K_left φ ψ = (LO.FirstOrder.Derivation.Canonical.StrongerThan.and φ ψ).trans (LO.FirstOrder.Derivation.Canonical.StrongerThan.ofSubset ⋯)

def LO.FirstOrder.Derivation.Canonical.StrongerThan.K_right {L : Language} {p : Sequent L} (φ ψ : Proposition L) : StrongerThan (φ ⋏ ψ :: p) (ψ :: p)

Equations

• LO.FirstOrder.Derivation.Canonical.StrongerThan.K_right φ ψ = (LO.FirstOrder.Derivation.Canonical.StrongerThan.and φ ψ).trans (LO.FirstOrder.Derivation.Canonical.StrongerThan.ofSubset ⋯)

def LO.FirstOrder.Derivation.Canonical.StrongerThan.all {L : Language} {p : Sequent L} (φ : Semiproposition L 1) (t : Semiterm L ℕ 0) : StrongerThan ((∀¹ φ) :: p) (φ/[t] :: p)

Equations

• LO.FirstOrder.Derivation.Canonical.StrongerThan.all φ t = { val := (⋯.mpr LO.FirstOrder.Derivation.Positive.id).exs }

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

Equations

• LO.FirstOrder.Derivation.Canonical.StrongerThan.minLeLeft p q = LO.FirstOrder.Derivation.Canonical.StrongerThan.ofSubset ⋯

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

Equations

• LO.FirstOrder.Derivation.Canonical.StrongerThan.minLeRight p q = LO.FirstOrder.Derivation.Canonical.StrongerThan.ofSubset ⋯

def LO.FirstOrder.Derivation.Canonical.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 := have d := (srp.val.add srq.val).contraction ⋯; ⋯ ▸ d }

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

Equations

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

@[irreducible]

def LO.FirstOrder.Derivation.Canonical.Forces {L : Language} (p : Sequent L) : Propositionᵢ L → Type u

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.Derivation.Canonical.Forces p LO.FirstOrder.Semiformulaᵢ.falsum = { b : ⊢ᴸᴷ¹ ∼p // b.IsCutFree }
• LO.FirstOrder.Derivation.Canonical.Forces p (LO.FirstOrder.Semiformulaᵢ.rel R v) = { b : ⊢ᴸᴷ¹ LO.FirstOrder.Semiformula.rel R v :: ∼p // b.IsCutFree }
• LO.FirstOrder.Derivation.Canonical.Forces p (LO.FirstOrder.Semiformulaᵢ.and φ ψ) = (LO.FirstOrder.Derivation.Canonical.Forces p φ × LO.FirstOrder.Derivation.Canonical.Forces p ψ)
• LO.FirstOrder.Derivation.Canonical.Forces p (LO.FirstOrder.Semiformulaᵢ.or φ ψ) = (LO.FirstOrder.Derivation.Canonical.Forces p φ ⊕ LO.FirstOrder.Derivation.Canonical.Forces p ψ)
• LO.FirstOrder.Derivation.Canonical.Forces p (LO.FirstOrder.Semiformulaᵢ.all φ) = ((t : LO.FirstOrder.SyntacticTerm L) → LO.FirstOrder.Derivation.Canonical.Forces p (φ/[t]))
• LO.FirstOrder.Derivation.Canonical.Forces p (LO.FirstOrder.Semiformulaᵢ.exs φ) = ((t : LO.FirstOrder.SyntacticTerm L) × LO.FirstOrder.Derivation.Canonical.Forces p (φ/[t]))

@[reducible, inline]

abbrev LO.FirstOrder.Derivation.Canonical.allForces {L : Language} (φ : Propositionᵢ L) : Type u_1

Equations

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

def LO.FirstOrder.Derivation.Canonical.Forces.«term_⊩_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Derivation.Canonical.Forces.«term⊩_» : Lean.ParserDescr

Equations

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

def LO.FirstOrder.Derivation.Canonical.Forces.falsumEquiv {L✝ : Language} {p : Sequent L✝} : Forces p ⊥ ≃ { b : ⊢ᴸᴷ¹ ∼p // b.IsCutFree }

Equations

• LO.FirstOrder.Derivation.Canonical.Forces.falsumEquiv = ⋯.mpr (Equiv.refl { b : ⊢ᴸᴷ¹ ∼p // b.IsCutFree })

def LO.FirstOrder.Derivation.Canonical.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 // b.IsCutFree }

Equations

• LO.FirstOrder.Derivation.Canonical.Forces.relEquiv = ⋯.mpr (Equiv.refl { b : ⊢ᴸᴷ¹ LO.FirstOrder.Semiformula.rel R v :: ∼p // b.IsCutFree })

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

Equations

• LO.FirstOrder.Derivation.Canonical.Forces.andEquiv = ⋯.mpr (Equiv.refl (LO.FirstOrder.Derivation.Canonical.Forces p φ × LO.FirstOrder.Derivation.Canonical.Forces p ψ))

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

Equations

• LO.FirstOrder.Derivation.Canonical.Forces.orEquiv = ⋯.mpr (Equiv.refl (LO.FirstOrder.Derivation.Canonical.Forces p φ ⊕ LO.FirstOrder.Derivation.Canonical.Forces p ψ))

def LO.FirstOrder.Derivation.Canonical.Forces.implyEquiv {L : Language} {p : Sequent L} {φ ψ : Propositionᵢ L} : Forces p (φ 🡒 ψ) ≃ ((q : Sequent L) → StrongerThan q p → Forces q φ → Forces q ψ)

Equations

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

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

Equations

• LO.FirstOrder.Derivation.Canonical.Forces.allEquiv = ⋯.mpr (Equiv.refl ((t : LO.FirstOrder.SyntacticTerm L) → LO.FirstOrder.Derivation.Canonical.Forces p (φ/[t])))

def LO.FirstOrder.Derivation.Canonical.Forces.exsEquiv {L : Language} {p : Sequent L} {φ : Semipropositionᵢ L (0 + 1)} : Forces p (∃¹ φ) ≃ (t : SyntacticTerm L) × Forces p (φ/[t])

Equations

• LO.FirstOrder.Derivation.Canonical.Forces.exsEquiv = ⋯.mpr (Equiv.refl ((t : LO.FirstOrder.SyntacticTerm L) × LO.FirstOrder.Derivation.Canonical.Forces p (φ/[t])))

def LO.FirstOrder.Derivation.Canonical.Forces.cast {L : Language} {φ ψ : Propositionᵢ L} {p : Sequent L} (f : Forces p φ) (s : φ = ψ) : Forces p ψ

Equations

• f.cast s = s ▸ f

@[irreducible]

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

Equations

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

@[irreducible]

def LO.FirstOrder.Derivation.Canonical.Forces.explosion {L : Language} {p : Sequent L} (b : Forces p ⊥) (φ : Propositionᵢ L) : Forces p φ

Equations

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

def LO.FirstOrder.Derivation.Canonical.Forces.efq {L : Language} (φ : Propositionᵢ L) : allForces (⊥ 🡒 φ)

Equations

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

def LO.FirstOrder.Derivation.Canonical.Forces.implyOf {L : Language} {p : Sequent L} {φ ψ : Propositionᵢ 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.Derivation.Canonical.Forces.modusPonens {L : Language} {p : Sequent L} {φ ψ : Propositionᵢ L} (f : Forces p (φ 🡒 ψ)) (g : Forces p φ) : Forces p ψ

Equations

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

@[irreducible]

def LO.FirstOrder.Derivation.Canonical.Forces.sound {L : Language} {φ : Propositionᵢ L} : 𝗠𝗶𝗻¹ ⊢! φ → allForces φ

Equations

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

def LO.FirstOrder.Derivation.Canonical.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.Derivation.Canonical.Forces.relRefl R v = LO.FirstOrder.Derivation.Canonical.Forces.relEquiv.symm ⟨LO.FirstOrder.Derivation.identity R v, ⋯⟩

def LO.FirstOrder.Derivation.Canonical.Forces.refl.or {L✝ : Language} {φ ψ : Proposition L✝} (ihφ : Forces [φ] (Semiformula.doubleNegation φ)) (ihψ : Forces [ψ] (Semiformula.doubleNegation ψ)) : Forces [φ ⋎ ψ] (φ ⋎ ψ).doubleNegation

Equations

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

def LO.FirstOrder.Derivation.Canonical.Forces.refl.exs {L✝ : Language} {φ : Semiproposition L✝ (Nat.succ 0)} (d : (x : ℕ) → Forces [φ/[Semiterm.fvar x]] φ/[Semiterm.fvar x].doubleNegation) : Forces [∃¹ φ] (∃¹ φ).doubleNegation

Equations

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

@[irreducible]

def LO.FirstOrder.Derivation.Canonical.Forces.refl {L : Language} (φ : Proposition L) : Forces [φ] (Semiformula.doubleNegation φ)

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.Derivation.Canonical.Forces.refl LO.FirstOrder.Semiformula.falsum = LO.FirstOrder.Derivation.Canonical.Forces.falsumEquiv.symm ⟨LO.FirstOrder.Derivation.verum, ⋯⟩

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

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.Derivation.Canonical.Forces.conj b = b φ ⋯

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

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.Derivation.Canonical.Forces.conj' b = b φ ⋯

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

Cut elimination theorem of $\mathbf{LK}$.

Equations

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