Derivation2

Different characterizations of proof.

inductive LO.FirstOrder.Derivation2 {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] (T : Theory L) : Finset (SyntacticFormula L) → Type u_1

Imported declaration from the Incompleteness formalization.

• closed {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] {T : Theory L} (Δ : Finset (SyntacticFormula L)) (φ : SyntacticFormula L) : φ ∈ Δ → ∼φ ∈ Δ → Derivation2 T Δ
• root {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] {T : Theory L} {Δ : Finset (SyntacticFormula L)} (φ : SyntacticFormula L) : φ ∈ T → φ ∈ Δ → Derivation2 T Δ
• verum {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] {T : Theory L} {Δ : Finset (SyntacticFormula L)} : ⊤ ∈ Δ → Derivation2 T Δ
• and {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] {T : Theory L} {Δ : Finset (SyntacticFormula L)} {φ ψ : SyntacticFormula L} : φ ⋏ ψ ∈ Δ → Derivation2 T (insert φ Δ) → Derivation2 T (insert ψ Δ) → Derivation2 T Δ
• or {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] {T : Theory L} {Δ : Finset (SyntacticFormula L)} {φ ψ : SyntacticFormula L} : φ ⋎ ψ ∈ Δ → Derivation2 T (insert φ (insert ψ Δ)) → Derivation2 T Δ
• all {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] {T : Theory L} {Δ : Finset (SyntacticFormula L)} {φ : SyntacticSemiformula L 1} : ∀' φ ∈ Δ → Derivation2 T (insert (Rewriting.free φ) (Finset.image Rewriting.shift Δ)) → Derivation2 T Δ
• ex {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] {T : Theory L} {Δ : Finset (SyntacticFormula L)} {φ : SyntacticSemiformula L 1} : ∃' φ ∈ Δ → (t : SyntacticTerm L) → Derivation2 T (insert (φ/[t]) Δ) → Derivation2 T Δ
• wk {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] {T : Theory L} {Δ Γ : Finset (SyntacticFormula L)} : Derivation2 T Δ → Δ ⊆ Γ → Derivation2 T Γ
• shift {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] {T : Theory L} {Δ : Finset (SyntacticFormula L)} : Derivation2 T Δ → Derivation2 T (Finset.image Rewriting.shift Δ)
• cut {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] {T : Theory L} {Δ : Finset (SyntacticFormula L)} {φ : SyntacticFormula L} : Derivation2 T (insert φ Δ) → Derivation2 T (insert (∼φ) Δ) → Derivation2 T Δ

def LO.FirstOrder.«term_⊢₂_» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

abbrev LO.FirstOrder.Derivable2 {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] (T : Theory L) (Γ : Finset (SyntacticFormula L)) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Derivable2 T Γ = Nonempty (LO.FirstOrder.Derivation2 T Γ)

def LO.FirstOrder.«term_⊢₂!_» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

@[reducible, inline]

abbrev LO.FirstOrder.Derivable2SingleConseq {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] (T : Theory L) (φ : SyntacticFormula L) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Derivable2SingleConseq T φ = LO.FirstOrder.Derivable2 T {φ}

def LO.FirstOrder.«term_⊢₂.!_» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.FirstOrder.shifts_toFinset_eq_image_shift {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] (Δ : Sequent L) : (Rewriting.shifts Δ).toFinset = Finset.image Rewriting.shift (List.toFinset Δ)

def LO.FirstOrder.Derivation.toDerivation2 {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] (T : Theory L) {Γ : Sequent L} : T ⟹ Γ → Derivation2 T (List.toFinset Γ)

Imported declaration from the Incompleteness formalization.

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.Derivation.toDerivation2 T (LO.FirstOrder.Derivation.root h) = LO.FirstOrder.Derivation2.root φ h ⋯
• LO.FirstOrder.Derivation.toDerivation2 T (LO.FirstOrder.Derivation.verum Δ) = LO.FirstOrder.Derivation2.verum ⋯
• LO.FirstOrder.Derivation.toDerivation2 T (dp.and dq) = LO.FirstOrder.Derivation2.and ⋯ ((LO.FirstOrder.Derivation.toDerivation2 T dp).wk ⋯) ((LO.FirstOrder.Derivation.toDerivation2 T dq).wk ⋯)
• LO.FirstOrder.Derivation.toDerivation2 T dpq.or = LO.FirstOrder.Derivation2.or ⋯ ((LO.FirstOrder.Derivation.toDerivation2 T dpq).wk ⋯)
• LO.FirstOrder.Derivation.toDerivation2 T dp.all = LO.FirstOrder.Derivation2.all ⋯ ((LO.FirstOrder.Derivation.toDerivation2 T dp).wk ⋯)
• LO.FirstOrder.Derivation.toDerivation2 T (LO.FirstOrder.Derivation.ex t dp) = LO.FirstOrder.Derivation2.ex ⋯ t ((LO.FirstOrder.Derivation.toDerivation2 T dp).wk ⋯)
• LO.FirstOrder.Derivation.toDerivation2 T (d.wk h) = (LO.FirstOrder.Derivation.toDerivation2 T d).wk ⋯
• LO.FirstOrder.Derivation.toDerivation2 T (d₁.cut d₂) = ((LO.FirstOrder.Derivation.toDerivation2 T d₁).wk ⋯).cut ((LO.FirstOrder.Derivation.toDerivation2 T d₂).wk ⋯)

noncomputable def LO.FirstOrder.Derivation2.toDerivation {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] {T : Theory L} {Γ : Finset (SyntacticFormula L)} : Derivation2 T Γ → T ⟹ Γ.toList

Imported declaration from the Incompleteness formalization.

Equations

• (LO.FirstOrder.Derivation2.closed x✝ φ hp hn).toDerivation = LO.FirstOrder.Derivation.em ⋯ ⋯
• (LO.FirstOrder.Derivation2.root φ hp h).toDerivation = LO.Tait.wk (LO.FirstOrder.Derivation.root hp) ⋯
• (LO.FirstOrder.Derivation2.verum h).toDerivation = LO.Tait.verum' ⋯
• (LO.FirstOrder.Derivation2.and h dp dq).toDerivation = LO.Tait.and' ⋯ (LO.Tait.wk dp.toDerivation ⋯) (LO.Tait.wk dq.toDerivation ⋯)
• (LO.FirstOrder.Derivation2.or h dpq).toDerivation = LO.Tait.or' ⋯ (LO.Tait.wk dpq.toDerivation ⋯)
• (LO.FirstOrder.Derivation2.all h d).toDerivation = LO.FirstOrder.Derivation.all' ⋯ (LO.Tait.wk d.toDerivation ⋯)
• (LO.FirstOrder.Derivation2.ex h t d).toDerivation = LO.FirstOrder.Derivation.ex' ⋯ t (LO.Tait.wk d.toDerivation ⋯)
• (d.wk h).toDerivation = LO.Tait.wk d.toDerivation ⋯
• d.shift.toDerivation = LO.Tait.wk (LO.FirstOrder.Derivation.shift d.toDerivation) ⋯
• (d.cut dn).toDerivation = LO.Tait.cut (LO.Tait.wk d.toDerivation ⋯) (LO.Tait.wk dn.toDerivation ⋯)

theorem LO.FirstOrder.derivable_iff_derivable2 {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] {T : Theory L} {Γ : List (SyntacticFormula L)} : T ⟹! Γ ↔ Derivable2 T Γ.toFinset

theorem LO.FirstOrder.provable_iff_derivable2 {L : Language} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] {T : Theory L} {φ : SyntacticFormula L} : T ⊢! φ ↔ Derivable2SingleConseq T φ

Imported declaration from the Incompleteness formalization.