Documentation

Foundation.FirstOrder.Hauptsatz

#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

source
inductive LO.FirstOrder.Derivation.IsCutFree {L : Language} {Γ : Sequent L} :
⊢ᵀ Γ → Prop
source
@[simp]
theorem LO.FirstOrder.Derivation.isCutFree_or_iff {L : Language} {Γ : Sequent L} {φ ψ : SyntacticFormula L} {d : ⊢ᵀ φ :: ψ :: Γ} :
IsCutFree (or d) ↔ IsCutFree d
source
@[simp]
theorem LO.FirstOrder.Derivation.isCutFree_and_iff {L : Language} {Γ : Sequent L} {φ ψ : SyntacticFormula L} {dφ : ⊢ᵀ φ :: Γ} {dψ : ⊢ᵀ ψ :: Γ} :
IsCutFree (and dφ dψ) ↔ IsCutFree dφ ∧ IsCutFree dψ
source
@[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
source
@[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
source
@[simp]
theorem LO.FirstOrder.Derivation.isCutFree_wk_iff {L : Language} {Γ Δ : Sequent L} {d : ⊢ᵀ Δ} {ss : Δ ⊆ Γ} :
IsCutFree (wk d ss) ↔ IsCutFree d
source
@[simp]
theorem LO.FirstOrder.Derivation.IsCutFree.cast {L : Language} {Γ Δ : Sequent L} {d : ⊢ᵀ Γ} {e : Γ = Δ} :
IsCutFree (Derivation.cast d e) ↔ IsCutFree d
source
@[simp]
theorem LO.FirstOrder.Derivation.IsCutFree.not_cut {L : Language} {Γ : Sequent L} {φ : SyntacticFormula L} (dp : ⊢ᵀ φ :: Γ) (dn : ⊢ᵀ ∼φ :: Γ) :
¬IsCutFree (cut dp dn)
source
@[simp]
theorem LO.FirstOrder.Derivation.isCutFree_rewrite_iff_isCutFree {L : Language} {Γ : Sequent L} {f : ℕ → SyntacticTerm L} {d : ⊢ᵀ Γ} :
IsCutFree (rewrite d f) ↔ IsCutFree d
source
@[simp]
theorem LO.FirstOrder.Derivation.isCutFree_map_iff_isCutFree {L : Language} {Γ : Sequent L} {f : ℕ → ℕ} {d : ⊢ᵀ Γ} :
IsCutFree (Derivation.map d f) ↔ IsCutFree d
source
@[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
source
inductive LO.FirstOrder.PositiveDerivationFrom {L : Language} (Ξ : Sequent L) :
Sequent L → Type u
source
def LO.FirstOrder.«term_⟶⁺_» :
Lean.TrailingParserDescr
Equations
source
def LO.FirstOrder.PositiveDerivationFrom.ofSubset {L : Language} {Ξ Γ : Sequent L} (ss : Ξ ⊆ Γ) :
Ξ ⟶⁺ Γ
Equations
source
def LO.FirstOrder.PositiveDerivationFrom.trans {L : Language} {Ξ Γ Δ : Sequent L} :
Ξ ⟶⁺ Γ → Γ ⟶⁺ Δ → Ξ ⟶⁺ Δ
Equations
source
def LO.FirstOrder.PositiveDerivationFrom.cons {L : Language} {Ξ Γ : Sequent L} (φ : SyntacticFormula L) :
Ξ ⟶⁺ Γ → φ :: Ξ ⟶⁺ φ :: Γ
Equations
source
def LO.FirstOrder.PositiveDerivationFrom.append {L : Language} {Ξ Γ : Sequent L} (Δ : Sequent L) :
Ξ ⟶⁺ Γ → Δ ++ Ξ ⟶⁺ Δ ++ Γ
Equations
source
def LO.FirstOrder.PositiveDerivationFrom.add {L : Language} {Γ Δ Ξ Θ : Sequent L} :
Γ ⟶⁺ Δ → Ξ ⟶⁺ Θ → Γ ++ Ξ ⟶⁺ Δ ++ Θ
Equations
source
def LO.FirstOrder.PositiveDerivationFrom.graft {L : Language} {Ξ Γ : Sequent L} (b : ⊢ᵀ Ξ) :
Ξ ⟶⁺ Γ → ⊢ᵀ Γ
Equations
source
theorem LO.FirstOrder.PositiveDerivationFrom.graft_isCutFree_of_isCutFree {L : Language} {Ξ Γ : Sequent L} {b : ⊢ᵀ Ξ} {d : Ξ ⟶⁺ Γ} (hb : Derivation.IsCutFree b) :
Derivation.IsCutFree (graft b d)
source
structure LO.FirstOrder.Hauptsatz.StrongerThan {L : Language} (q p : Sequent L) :
Type u
source
def LO.FirstOrder.Hauptsatz.«term_≼_» :
Lean.TrailingParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
def LO.FirstOrder.Hauptsatz.instMinSequent {L : Language} :
Min (Sequent L)
Equations
source
theorem LO.FirstOrder.Hauptsatz.inf_def {L : Language} (p q : Sequent L) :
p ⊓ q = p ++ q
source
@[simp]
theorem LO.FirstOrder.Hauptsatz.neg_inf_p_eq {L : Language} (p q : Sequent L) :
∼(p ⊓ q) = ∼p ⊓ ∼q
source
def LO.FirstOrder.Hauptsatz.StrongerThan.refl {L : Language} (p : Sequent L) :
StrongerThan p p
Equations
source
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 }
source
def LO.FirstOrder.Hauptsatz.StrongerThan.ofSubset {L : Language} {q p : Sequent L} (h : q ⊇ p) :
StrongerThan q p
Equations
source
def LO.FirstOrder.Hauptsatz.StrongerThan.and {L : Language} {p : Sequent L} (φ ψ : SyntacticFormula L) :
StrongerThan (φ ⋏ ψ :: p) (φ :: ψ :: p)
Equations
source
def LO.FirstOrder.Hauptsatz.StrongerThan.andLeft {L : Language} {p : Sequent L} (φ ψ : SyntacticFormula L) :
StrongerThan (φ ⋏ ψ :: p) (φ :: p)
Equations
source
def LO.FirstOrder.Hauptsatz.StrongerThan.andRight {L : Language} {p : Sequent L} (φ ψ : SyntacticFormula L) :
StrongerThan (φ ⋏ ψ :: p) (ψ :: p)
Equations
source
def LO.FirstOrder.Hauptsatz.StrongerThan.all {L : Language} {p : Sequent L} (φ : SyntacticSemiformula L 1) (t : Semiterm L ℕ 0) :
StrongerThan ((∀' φ) :: p) (φ/[t] :: p)
Equations
source
def LO.FirstOrder.Hauptsatz.StrongerThan.minLeLeft {L : Language} (p q : Sequent L) :
StrongerThan (p ⊓ q) p
Equations
source
def LO.FirstOrder.Hauptsatz.StrongerThan.minLeRight {L : Language} (p q : Sequent L) :
StrongerThan (p ⊓ q) q
Equations
source
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 }
source
def LO.FirstOrder.Hauptsatz.StrongerThan.leMinRightOfLe {L✝ : Language} {q p : Sequent L✝} (s : StrongerThan q p) :
StrongerThan q (p ⊓ q)
Equations
source
@[reducible, inline]
abbrev LO.FirstOrder.Hauptsatz.Forces {L : Language} (p : Sequent L) :
SyntacticFormulaᵢ L → Type u
Equations
source
def LO.FirstOrder.Hauptsatz.«term_⊩_» :
Lean.TrailingParserDescr
Equations
  • One or more equations did not get rendered due to their size.
source
@[reducible, inline]
abbrev LO.FirstOrder.Hauptsatz.allForces {L : Language} (φ : SyntacticFormulaᵢ L) :
Type u
Equations
source
def LO.FirstOrder.Hauptsatz.«term⊩_» :
Lean.ParserDescr
Equations
source
def LO.FirstOrder.Hauptsatz.Forces.verumEquiv {L✝ : Language} {p : Sequent L✝} :
Forces p ⊤ ≃ PUnit.{u_1 + 1}
Equations
source
def LO.FirstOrder.Hauptsatz.Forces.falsumEquiv {L✝ : Language} {p : Sequent L✝} :
Forces p ⊥ ≃ { b : ⊢ᵀ ∼p // Derivation.IsCutFree b }
Equations
source
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
source
def LO.FirstOrder.Hauptsatz.Forces.andEquiv {L : Language} {p : Sequent L} {φ ψ : SyntacticFormulaᵢ L} :
Forces p (φ ⋏ ψ) ≃ Forces p φ × Forces p ψ
Equations
source
def LO.FirstOrder.Hauptsatz.Forces.orEquiv {L : Language} {p : Sequent L} {φ ψ : SyntacticFormulaᵢ L} :
Forces p (φ ⋎ ψ) ≃ Forces p φ ⊕ Forces p ψ
Equations
source
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
source
def LO.FirstOrder.Hauptsatz.Forces.allEquiv {L : Language} {p : Sequent L} {φ : SyntacticSemiformulaᵢ L (0 + 1)} :
Forces p (∀' φ) ≃ ((t : SyntacticTerm L) → Forces p (φ/[t]))
Equations
source
def LO.FirstOrder.Hauptsatz.Forces.exEquiv {L : Language} {p : Sequent L} {φ : SyntacticSemiformulaᵢ L (0 + 1)} :
Forces p (∃' φ) ≃ (t : SyntacticTerm L) × Forces p (φ/[t])
Equations
source
@[irreducible]
def LO.FirstOrder.Hauptsatz.Forces.monotone {L : Language} {q p : Sequent L} (s : StrongerThan q p) {φ : SyntacticFormulaᵢ L} :
Forces p φ → Forces q φ
source
@[irreducible]
def LO.FirstOrder.Hauptsatz.Forces.explosion {L : Language} {p : Sequent L} (b : Forces p ⊥) (φ : SyntacticFormulaᵢ L) :
Forces p φ
Equations
source
def LO.FirstOrder.Hauptsatz.Forces.efq {L : Language} (φ : SyntacticFormulaᵢ L) :
allForces (⊥ ➝ φ)
Equations
  • One or more equations did not get rendered due to their size.
source
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.
source
def LO.FirstOrder.Hauptsatz.Forces.modusPonens {L : Language} {p : Sequent L} {φ ψ : SyntacticFormulaᵢ L} (f : Forces p (φ ➝ ψ)) (g : Forces p φ) :
Forces p ψ
Equations
source
@[irreducible]
noncomputable def LO.FirstOrder.Hauptsatz.Forces.ofMinimalProof {L : Language} {φ : SyntacticFormulaᵢ L} :
𝐌𝐢𝐧¹ ⊢ φ → allForces φ
source
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
source
@[irreducible]
def LO.FirstOrder.Hauptsatz.Forces.refl {L : Language} (φ : SyntacticFormula L) :
Forces [φ] (Semiformula.doubleNegation φ)
source
def LO.FirstOrder.Hauptsatz.Forces.conj {L : Language} {p : Sequent L} {Γ : Sequentᵢ L} (b : (φ : SyntacticFormulaᵢ L) → φ ∈ Γ → Forces p φ) :
Forces p (⋀Γ)
Equations
source
def LO.FirstOrder.Hauptsatz.Forces.conj' {L : Language} {p Γ : Sequent L} (b : (φ : SyntacticFormula L) → φ ∈ Γ → Forces p (Semiformula.doubleNegation φ)) :
Forces p (⋀Sequent.doubleNegation Γ)
Equations
source
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.
source
def LO.FirstOrder.hauptsatz {L : Language} [L.DecidableEq] {Γ : Sequent L} :
⊢ᵀ Γ → { d : ⊢ᵀ Γ // Derivation.IsCutFree d }

Alias of LO.FirstOrder.Hauptsatz.main.

Equations