Calculus

@[reducible, inline]

abbrev LO.FirstOrder.Sequent (L : Language) : Type u_1

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Sequent L = List (LO.FirstOrder.SyntacticFormula L)

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

Imported declaration from the Incompleteness formalization.

• axL {L : Language} {T : Theory L} (Γ : List (SyntacticFormula L)) {k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ℕ 0) : Derivation T (Semiformula.rel r v :: Semiformula.nrel r v :: Γ)
• verum {L : Language} {T : Theory L} (Γ : List (SyntacticFormula L)) : Derivation T (⊤ :: Γ)
• or {L : Language} {T : Theory L} {Γ : List (SyntacticFormula L)} {φ ψ : SyntacticFormula L} : Derivation T (φ :: ψ :: Γ) → Derivation T (φ ⋎ ψ :: Γ)
• and {L : Language} {T : Theory L} {Γ : List (SyntacticFormula L)} {φ ψ : SyntacticFormula L} : Derivation T (φ :: Γ) → Derivation T (ψ :: Γ) → Derivation T (φ ⋏ ψ :: Γ)
• all {L : Language} {T : Theory L} {Γ : List (SyntacticSemiformula L 0)} {φ : SyntacticSemiformula L (0 + 1)} : Derivation T (Rewriting.free φ :: Rewriting.shifts Γ) → Derivation T ((∀' φ) :: Γ)
• ex {L : Language} {T : Theory L} {Γ : List (SyntacticFormula L)} {φ : SyntacticSemiformula L (Nat.succ 0)} (t : Semiterm L ℕ 0) : Derivation T (φ/[t] :: Γ) → Derivation T ((∃' φ) :: Γ)
• wk {L : Language} {T : Theory L} {Γ Δ : Sequent L} : Derivation T Δ → Δ ⊆ Γ → Derivation T Γ
• cut {L : Language} {T : Theory L} {Γ : List (SyntacticFormula L)} {φ : SyntacticFormula L} : Derivation T (φ :: Γ) → Derivation T (∼φ :: Γ) → Derivation T Γ
• root {L : Language} {T : Theory L} {φ : SyntacticFormula L} : φ ∈ T → Derivation T [φ]

@[implicit_reducible]

instance LO.FirstOrder.instOneSidedSyntacticFormulaTheory {L : Language} : OneSided (SyntacticFormula L) (Theory L)

Equations

• LO.FirstOrder.instOneSidedSyntacticFormulaTheory = { Derivation := LO.FirstOrder.Derivation }

@[reducible, inline]

abbrev LO.FirstOrder.Derivation₀ {L : Language} (Γ : Sequent L) : Type u_1

Imported declaration from the Incompleteness formalization.

Equations

• (⊢ᵀ Γ) = (∅ ⟹ Γ)

@[reducible, inline]

abbrev LO.FirstOrder.Derivable₀ {L : Language} (Γ : Sequent L) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• (⊢ᵀ! Γ) = (∅ ⟹! Γ)

def LO.FirstOrder.«term⊢ᵀ_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.«term⊢ᵀ!_» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.Derivation.length {L : Language} {T : Theory L} {Δ : Sequent L} : T ⟹ Δ → ℕ

Imported declaration from the Incompleteness formalization.

Equations

• (LO.FirstOrder.Derivation.axL Γ r v).length = 0
• (LO.FirstOrder.Derivation.verum Γ).length = 0
• d.or.length = d.length.succ
• (dp.and dq).length = (max dp.length dq.length).succ
• d.all.length = d.length.succ
• (LO.FirstOrder.Derivation.ex t d).length = d.length.succ
• (d.wk a).length = d.length.succ
• (dp.cut dn).length = (max dp.length dn.length).succ
• (LO.FirstOrder.Derivation.root a).length = 0

@[simp]

theorem LO.FirstOrder.Derivation.length_axL {L : Language} {T : Theory L} {Δ : Sequent L} {k : ℕ} {r : L.Rel k} {v : Fin k → Semiterm L ℕ 0} : (axL Δ r v).length = 0

@[simp]

theorem LO.FirstOrder.Derivation.length_verum {L : Language} {T : Theory L} {Δ : Sequent L} : (verum Δ).length = 0

@[simp]

theorem LO.FirstOrder.Derivation.length_and {L : Language} {T : Theory L} {Δ : Sequent L} {φ ψ : SyntacticFormula L} (dp : T ⟹ φ :: Δ) (dq : T ⟹ ψ :: Δ) : (and dp dq).length = (max (length dp) (length dq)).succ

@[simp]

theorem LO.FirstOrder.Derivation.length_or {L : Language} {T : Theory L} {Δ : Sequent L} {φ ψ : SyntacticFormula L} (d : T ⟹ φ :: ψ :: Δ) : (or d).length = (length d).succ

@[simp]

theorem LO.FirstOrder.Derivation.length_all {L : Language} {T : Theory L} {Δ : Sequent L} {φ : SyntacticSemiformula L (0 + 1)} (d : T ⟹ Rewriting.free φ :: Rewriting.shifts Δ) : (all d).length = (length d).succ

@[simp]

theorem LO.FirstOrder.Derivation.length_ex {L : Language} {T : Theory L} {Δ : Sequent L} {t : Semiterm L ℕ 0} {φ : SyntacticSemiformula L (Nat.succ 0)} (d : T ⟹ φ/[t] :: Δ) : (ex t d).length = (length d).succ

@[simp]

theorem LO.FirstOrder.Derivation.length_wk {L : Language} {T : Theory L} {Δ Γ : Sequent L} (d : T ⟹ Δ) (h : Δ ⊆ Γ) : (wk d h).length = (length d).succ

@[simp]

theorem LO.FirstOrder.Derivation.length_cut {L : Language} {T : Theory L} {Δ : Sequent L} {φ : SyntacticFormula L} (dp : T ⟹ φ :: Δ) (dn : T ⟹ ∼φ :: Δ) : (cut dp dn).length = (max (length dp) (length dn)).succ

def LO.FirstOrder.Derivation.repr {L : Language} {T : Theory L} [(k : ℕ) → ToString (L.Func k)] [(k : ℕ) → ToString (L.Rel k)] {Δ : Sequent L} : T ⟹ Δ → String

Imported declaration from the Incompleteness formalization.

Equations

• (LO.FirstOrder.Derivation.axL Γ r v).repr = "\\AxiomC{}\n" ++ "\\RightLabel{\\scriptsize(axL)}\n" ++ "\\UnaryInfC{$" ++ reprStr Γ ++ "$}\n\n"
• (LO.FirstOrder.Derivation.verum Γ).repr = "\\AxiomC{}\n" ++ "\\RightLabel{\\scriptsize($\\top$)}\n" ++ "\\UnaryInfC{$" ++ reprStr Γ ++ "$}\n\n"
• d.or.repr = d.repr ++ "\\RightLabel{\\scriptsize($\\lor$)}\n" ++ "\\UnaryInfC{$" ++ reprStr (φ ⋎ ψ :: Γ) ++ "$}\n\n"
• (dp.and dq).repr = dp.repr ++ dq.repr ++ "\\RightLabel{\\scriptsize($\\land$)}\n" ++ "\\BinaryInfC{$" ++ reprStr (φ ⋏ ψ :: Γ) ++ "$}\n\n"
• d.all.repr = d.repr ++ "\\RightLabel{\\scriptsize($\\forall$)}\n" ++ "\\UnaryInfC{$" ++ reprStr ((∀' φ) :: Γ) ++ "$}\n\n"
• (LO.FirstOrder.Derivation.ex t d).repr = d.repr ++ "\\RightLabel{\\scriptsize($\\exists$)}\n" ++ "\\UnaryInfC{$" ++ reprStr ((∃' φ) :: Γ) ++ "$}\n\n"
• (d.wk a).repr = d.repr ++ "\\RightLabel{\\scriptsize(wk)}\n" ++ "\\UnaryInfC{$" ++ reprStr Δ_3 ++ "$}\n\n"
• (dp.cut dn).repr = dp.repr ++ dn.repr ++ "\\RightLabel{\\scriptsize(Cut)}\n" ++ "\\BinaryInfC{$" ++ reprStr Δ ++ "$}\n\n"
• (LO.FirstOrder.Derivation.root a).repr = "\\AxiomC{}\n" ++ "\\RightLabel{\\scriptsize(ROOT)}\n" ++ "\\UnaryInfC{$" ++ reprStr φ ++ ", " ++ reprStr (∼φ) ++ "$}\n\n"

@[implicit_reducible]

instance LO.FirstOrder.Derivation.instReprDerivationSyntacticFormulaTheory {L : Language} {T : Theory L} {Δ : Sequent L} [(k : ℕ) → ToString (L.Func k)] [(k : ℕ) → ToString (L.Rel k)] : Repr (T ⟹ Δ)

Equations

• LO.FirstOrder.Derivation.instReprDerivationSyntacticFormulaTheory = { reprPrec := fun (d : T ⟹ Δ) (x : ℕ) => Std.Format.text (LO.FirstOrder.Derivation.repr d) }

@[reducible, inline]

abbrev LO.FirstOrder.Derivation.cast {L : Language} {T : Theory L} {Δ Γ : Sequent L} (d : T ⟹ Δ) (e : Δ = Γ) : T ⟹ Γ

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Derivation.cast d e = e ▸ d

theorem LO.FirstOrder.Derivation.cast_eq {L : Language} {T : Theory L} {Δ : Sequent L} (d : T ⟹ Δ) (e : Δ = Δ) : Derivation.cast d e = d

@[simp]

theorem LO.FirstOrder.Derivation.length_cast {L : Language} {T : Theory L} {Δ Γ : Sequent L} (d : T ⟹ Δ) (e : Δ = Γ) : length (Derivation.cast d e) = length d

theorem LO.FirstOrder.Derivation.length_cast' {L : Language} {T : Theory L} {Δ Γ : Sequent L} (d : T ⟹ Δ) (e : Δ = Γ) : length (e ▸ d) = length d

def LO.FirstOrder.Derivation.weakening {L : Language} {T : Theory L} {Γ Δ : Sequent L} : Derivation T Δ → Δ ⊆ Γ → Derivation T Γ

Alias of LO.FirstOrder.Derivation.wk.

Equations

• @LO.FirstOrder.Derivation.weakening = @LO.FirstOrder.Derivation.wk

def LO.FirstOrder.Derivation.verum' {L : Language} {T : Theory L} {Δ : Sequent L} (h : ⊤ ∈ Δ) : T ⟹ Δ

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Derivation.verum' h = (LO.FirstOrder.Derivation.verum Δ).wk ⋯

def LO.FirstOrder.Derivation.axL' {L : Language} {T : Theory L} {Δ : Sequent L} {k : ℕ} (r : L.Rel k) (v : Fin k → Semiterm L ℕ 0) (h : Semiformula.rel r v ∈ Δ) (hn : Semiformula.nrel r v ∈ Δ) : T ⟹ Δ

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Derivation.axL' r v h hn = (LO.FirstOrder.Derivation.axL Δ r v).wk ⋯

def LO.FirstOrder.Derivation.all' {L : Language} {T : Theory L} {Δ : Sequent L} {φ : SyntacticSemiformula L (0 + 1)} (h : ∀' φ ∈ Δ) (d : T ⟹ Rewriting.free φ :: Rewriting.shifts Δ) : T ⟹ Δ

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Derivation.all' h d = (LO.FirstOrder.Derivation.all d).wk ⋯

def LO.FirstOrder.Derivation.ex' {L : Language} {T : Theory L} {Δ : Sequent L} {φ : SyntacticSemiformula L (0 + 1)} (h : ∃' φ ∈ Δ) (t : Semiterm L ℕ 0) (d : T ⟹ φ/[t] :: Δ) : T ⟹ Δ

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Derivation.ex' h t d = (LO.FirstOrder.Derivation.ex t d).wk ⋯

theorem LO.FirstOrder.Derivation.ne_step_max (n m : ℕ) : n ≠ max n m + 1

@[simp]

theorem LO.FirstOrder.Derivation.ne_step_max' (n m : ℕ) : n ≠ max m n + 1

@[irreducible]

def LO.FirstOrder.Derivation.em {L : Language} {T : Theory L} {Δ : Sequent L} {φ : SyntacticFormula L} (hpos : φ ∈ Δ) (hneg : ∼φ ∈ Δ) : T ⟹ Δ

Imported declaration from the Incompleteness formalization.

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.Derivation.em hpos hneg = LO.FirstOrder.Derivation.verum' hpos
• LO.FirstOrder.Derivation.em hpos hneg = LO.FirstOrder.Derivation.verum' hneg
• LO.FirstOrder.Derivation.em hpos hneg = LO.FirstOrder.Derivation.axL' R v hpos hneg
• LO.FirstOrder.Derivation.em hpos hneg = LO.FirstOrder.Derivation.axL' R v hneg hpos
• LO.FirstOrder.Derivation.em hpos hneg = ((LO.FirstOrder.Derivation.and (LO.FirstOrder.Derivation.em ⋯ ⋯) (LO.FirstOrder.Derivation.em ⋯ ⋯)).wk ⋯).or.wk ⋯
• LO.FirstOrder.Derivation.em hpos hneg = ((LO.FirstOrder.Derivation.and (LO.FirstOrder.Derivation.em ⋯ ⋯) (LO.FirstOrder.Derivation.em ⋯ ⋯)).wk ⋯).or.wk ⋯

@[implicit_reducible]

instance LO.FirstOrder.Derivation.instTaitSyntacticFormulaTheory {L : Language} : Tait (SyntacticFormula L) (Theory L)

Equations

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

@[implicit_reducible]

instance LO.FirstOrder.Derivation.instCutSyntacticFormulaTheory {L : Language} : Tait.Cut (SyntacticFormula L) (Theory L)

Equations

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

def LO.FirstOrder.Derivation.provableOfDerivable {L : Language} {T : Theory L} {φ : SyntacticFormula L} (b : T ⟹. φ) : T ⊢ φ

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Derivation.provableOfDerivable b = b

def LO.FirstOrder.Derivation.specialize {L : Language} {T : Theory L} {Γ : Sequent L} {φ : SyntacticSemiformula L 1} (t : SyntacticTerm L) : T ⟹ (∀' φ) :: Γ → T ⟹ φ/[t] :: Γ

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Derivation.specialize t d = (LO.FirstOrder.Derivation.wk d ⋯).cut (id (LO.FirstOrder.Derivation.ex t (⋯.mpr (LO.Tait.em ⋯ ⋯))))

def LO.FirstOrder.Derivation.specializes {L : Language} {T : Theory L} {k : ℕ} {φ : SyntacticSemiformula L k} {Γ : Sequent L} (v : Fin k → SyntacticTerm L) : T ⟹ (∀* φ) :: Γ → T ⟹ φ <~ v :: Γ

Imported declaration from the Incompleteness formalization.

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.Derivation.specializes x_5 x✝ = LO.FirstOrder.Derivation.cast x✝ ⋯

def LO.FirstOrder.Derivation.instances {L : Language} {T : Theory L} {k : ℕ} {φ : SyntacticSemiformula L k} {Γ : Sequent L} {v : Fin k → SyntacticTerm L} : T ⟹ φ <~ v :: Γ → T ⟹ (∃* φ) :: Γ

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Derivation.instances b = LO.FirstOrder.Derivation.cast b ⋯
• LO.FirstOrder.Derivation.instances b = LO.FirstOrder.Derivation.instances ((LO.FirstOrder.Derivation.ex (v 0) (LO.FirstOrder.Derivation.cast b ⋯)).cast ⋯)

def LO.FirstOrder.Derivation.allClosureFixitr {L : Language} {T : Theory L} {φ : SyntacticFormula L} (dp : T ⊢ φ) (m : ℕ) : T ⊢ ∀* (Rewriting.app (Rew.fixitr 0 m)) φ

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Derivation.allClosureFixitr dp 0 = ⋯.mpr dp
• LO.FirstOrder.Derivation.allClosureFixitr dp m.succ = ⋯.mpr (⋯.mpr (LO.FirstOrder.Derivation.allClosureFixitr dp m)).all

def LO.FirstOrder.Derivation.toClose {L : Language} {T : Theory L} {φ : SyntacticFormula L} (b : T ⊢ φ) : T ⊢ Semiformula.close φ

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Derivation.toClose b = LO.FirstOrder.Derivation.allClosureFixitr b (LO.FirstOrder.Semiformula.fvSup φ)

theorem LO.FirstOrder.Derivation.toClose! {L : Language} {T : Theory L} {φ : SyntacticFormula L} (b : T ⊢! φ) : T ⊢! Semiformula.close φ

Imported declaration from the Incompleteness formalization.

def LO.FirstOrder.Derivation.rewrite₁ {L : Language} {T : Theory L} {φ : SyntacticFormula L} (b : T ⊢ φ) (f : ℕ → SyntacticTerm L) : T ⊢ (Rewriting.app (Rew.rewrite f)) φ

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.Derivation.rewrite {L : Language} {T : Theory L} {Δ : List (SyntacticFormula L)} : T ⟹ Δ → (f : ℕ → SyntacticTerm L) → T ⟹ List.map (fun (φ : SyntacticSemiformula L 0) => (Rewriting.app (Rew.rewrite f)) φ) Δ

Imported declaration from the Incompleteness formalization.

Equations

• One or more equations did not get rendered due to their size.
• d.or.rewrite x✝ = (LO.FirstOrder.Derivation.or (LO.FirstOrder.Derivation.cast (d.rewrite x✝) ⋯)).cast ⋯
• (dp.and dq).rewrite x✝ = (LO.FirstOrder.Derivation.and (LO.FirstOrder.Derivation.cast (dp.rewrite x✝) ⋯) (LO.FirstOrder.Derivation.cast (dq.rewrite x✝) ⋯)).cast ⋯
• (LO.FirstOrder.Derivation.ex t d).rewrite x✝ = (LO.FirstOrder.Derivation.ex ((LO.FirstOrder.Rew.rewrite x✝) t) (LO.FirstOrder.Derivation.cast (d.rewrite x✝) ⋯)).cast ⋯
• (d.wk ss).rewrite x✝ = LO.FirstOrder.Derivation.wk (d.rewrite x✝) ⋯
• (d.cut dn).rewrite x✝ = (LO.FirstOrder.Derivation.cut (LO.FirstOrder.Derivation.cast (d.rewrite x✝) ⋯) (LO.FirstOrder.Derivation.cast (dn.rewrite x✝) ⋯)).cast ⋯
• (LO.FirstOrder.Derivation.root h).rewrite x✝ = (LO.FirstOrder.Derivation.root h).rewrite₁ x✝

def LO.FirstOrder.Derivation.map {L : Language} {T : Theory L} {Δ : Sequent L} (d : T ⟹ Δ) (f : ℕ → ℕ) : T ⟹ List.map (fun (φ : SyntacticSemiformula L 0) => (Rewriting.app (Rew.rewriteMap f)) φ) Δ

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Derivation.map d f = LO.FirstOrder.Derivation.rewrite d fun (x : ℕ) => LO.FirstOrder.Semiterm.fvar (f x)

def LO.FirstOrder.Derivation.shift {L : Language} {T : Theory L} {Δ : Sequent L} (d : T ⟹ Δ) : T ⟹ Rewriting.shifts Δ

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Derivation.shift d = LO.FirstOrder.Derivation.cast (LO.FirstOrder.Derivation.map d Nat.succ) ⋯

def LO.FirstOrder.Derivation.trans {L : Language} {T U : Theory L} (F : U ⊢* T) {Γ : Sequent L} : T ⟹ Γ → U ⟹ Γ

Imported declaration from the Incompleteness formalization.

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.Derivation.trans F (LO.FirstOrder.Derivation.axL Γ_2 R v) = LO.FirstOrder.Derivation.axL Γ_2 R v
• LO.FirstOrder.Derivation.trans F (LO.FirstOrder.Derivation.verum Γ_2) = LO.FirstOrder.Derivation.verum Γ_2
• LO.FirstOrder.Derivation.trans F d.or = LO.FirstOrder.Derivation.or (LO.FirstOrder.Derivation.trans (fun {f : LO.FirstOrder.SyntacticFormula L} => F) d)
• LO.FirstOrder.Derivation.trans F d.all = LO.FirstOrder.Derivation.all (LO.FirstOrder.Derivation.trans (fun {f : LO.FirstOrder.SyntacticFormula L} => F) d)
• LO.FirstOrder.Derivation.trans F (LO.FirstOrder.Derivation.ex t d) = LO.FirstOrder.Derivation.ex t (LO.FirstOrder.Derivation.trans (fun {f : LO.FirstOrder.SyntacticFormula L} => F) d)
• LO.FirstOrder.Derivation.trans F (d.wk ss) = LO.FirstOrder.Derivation.wk (LO.FirstOrder.Derivation.trans (fun {f : LO.FirstOrder.SyntacticFormula L} => F) d) ss
• LO.FirstOrder.Derivation.trans F (LO.FirstOrder.Derivation.root h) = F h

@[implicit_reducible]

instance LO.FirstOrder.Derivation.instAxiomatizedSyntacticFormulaTheory {L : Language} : Tait.Axiomatized (SyntacticFormula L) (Theory L)

Equations

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

def LO.FirstOrder.Derivation.invClose {L : Language} {T : Theory L} {φ : SyntacticFormula L} (b : T ⊢ Semiformula.close φ) : T ⊢ φ

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Derivation.invClose b = (LO.FirstOrder.Derivation.wk b ⋯).cut (LO.FirstOrder.Derivation.not_close'✝ φ)

theorem LO.FirstOrder.Derivation.invClose! {L : Language} {T : Theory L} {φ : SyntacticFormula L} (b : T ⊢! Semiformula.close φ) : T ⊢! φ

Imported declaration from the Incompleteness formalization.

def LO.FirstOrder.Derivation.deduction {L : Language} {T : Theory L} {Γ : Sequent L} {φ : SyntacticFormula L} [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → DecidableEq (L.Rel k)] (d : insert φ T ⟹ Γ) : T ⟹ ∼Semiformula.close φ :: Γ

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Derivation.deduction d = LO.Tait.ofAxiomSubset ⋯ (LO.FirstOrder.Derivation.deductionAux✝ d)

theorem LO.FirstOrder.Derivation.provable_iff_inconsistent {L : Language} {T : Theory L} {φ : SyntacticFormula L} : T ⊢! φ ↔ Entailment.Inconsistent (insert (∼Semiformula.close φ) T)

Imported declaration from the Incompleteness formalization.

theorem LO.FirstOrder.Derivation.unprovable_iff_consistent {L : Language} {T : Theory L} {φ : SyntacticFormula L} : T ⊬ φ ↔ Entailment.Consistent (insert (∼Semiformula.close φ) T)

Imported declaration from the Incompleteness formalization.

theorem LO.FirstOrder.Derivation.shifts_image {L₁ : Language} {L₂ : Language} (Φ : L₁.Hom L₂) {Δ : List (SyntacticFormula L₁)} : Rewriting.shifts (List.map (⇑(Semiformula.lMap Φ)) Δ) = List.map (⇑(Semiformula.lMap Φ)) (Rewriting.shifts Δ)

def LO.FirstOrder.Derivation.lMap {L₁ : Language} {L₂ : Language} {T₁ : Theory L₁} (Φ : L₁.Hom L₂) {Δ : List (SyntacticFormula L₁)} : T₁ ⟹ Δ → Theory.lMap Φ T₁ ⟹ List.map (⇑(Semiformula.lMap Φ)) Δ

Imported declaration from the Incompleteness formalization.

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.Derivation.lMap Φ (LO.FirstOrder.Derivation.verum Δ_2) = LO.FirstOrder.Derivation.verum (List.map (⇑(LO.FirstOrder.Semiformula.lMap Φ)) Δ_2)
• LO.FirstOrder.Derivation.lMap Φ d.or = (LO.FirstOrder.Derivation.or (LO.FirstOrder.Derivation.lMap Φ d)).cast ⋯
• LO.FirstOrder.Derivation.lMap Φ d.all = (LO.FirstOrder.Derivation.all (LO.FirstOrder.Derivation.cast (LO.FirstOrder.Derivation.lMap Φ d) ⋯)).cast ⋯
• LO.FirstOrder.Derivation.lMap Φ (d.wk ss) = LO.FirstOrder.Derivation.wk (LO.FirstOrder.Derivation.lMap Φ d) ⋯
• LO.FirstOrder.Derivation.lMap Φ (LO.FirstOrder.Derivation.root h) = LO.FirstOrder.Derivation.root ⋯

theorem LO.FirstOrder.Derivation.inconsistent_lMap {L₁ : Language} {L₂ : Language} {T₁ : Theory L₁} (Φ : L₁.Hom L₂) : Entailment.Inconsistent T₁ → Entailment.Inconsistent (Theory.lMap Φ T₁)

def LO.FirstOrder.Derivation.genelalizeByNewver {L : Language} {T : Theory L} {Δ : Sequent L} {m : ℕ} {φ : SyntacticSemiformula L 1} (hp : ¬Semiformula.FVar? φ m) (hΔ : ∀ ψ ∈ Δ, ¬Semiformula.FVar? ψ m) (d : T ⟹ φ/[Semiterm.fvar m] :: Δ) : T ⟹ (∀' φ) :: Δ

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Derivation.genelalizeByNewver hp hΔ d = LO.FirstOrder.Derivation.all (LO.FirstOrder.Derivation.cast (LO.FirstOrder.Derivation.map d fun (x : ℕ) => if x = m then 0 else x + 1) ⋯)

def LO.FirstOrder.Derivation.exOfInstances {L : Language} {T : Theory L} {Γ : Sequent L} (v : List (SyntacticTerm L)) (φ : SyntacticSemiformula L 1) (h : T ⟹ List.map (fun (x : Semiterm L ℕ 0) => φ/[x]) v ++ Γ) : T ⟹ (∃' φ) :: Γ

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.Derivation.exOfInstances' {L : Language} {T : Theory L} {Γ : Sequent L} (v : List (SyntacticTerm L)) (φ : SyntacticSemiformula L 1) (h : T ⟹ (∃' φ) :: List.map (fun (x : Semiterm L ℕ 0) => φ/[x]) v ++ Γ) : T ⟹ (∃' φ) :: Γ

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Derivation.exOfInstances' v φ h = LO.FirstOrder.Derivation.wk (LO.FirstOrder.Derivation.exOfInstances v φ (LO.FirstOrder.Derivation.wk h ⋯)) ⋯

def LO.FirstOrder.newVar {L : Language} (Γ : Sequent L) : ℕ

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.newVar Γ = List.foldr max 0 (List.map LO.FirstOrder.Semiformula.fvSup Γ)

theorem LO.FirstOrder.not_fvar?_newVar {L : Language} {φ : SyntacticFormula L} {Γ : Sequent L} (h : φ ∈ Γ) : ¬Semiformula.FVar? φ (newVar Γ)

def LO.FirstOrder.Derivation.allNvar {L : Language} {T : Theory L} {Δ : Sequent L} {φ : SyntacticSemiformula L (0 + 1)} (h : ∀' φ ∈ Δ) : T ⟹ φ/[Semiterm.fvar (newVar Δ)] :: Δ → T ⟹ Δ

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Derivation.allNvar h b = LO.Tait.wk (LO.FirstOrder.Derivation.genelalizeByNewver ⋯ ⋯ b) ⋯

def LO.FirstOrder.Derivation.id {L : Language} {T : Theory L} {Δ : Sequent L} {φ : SyntacticFormula L} (hp : φ ∈ T) : T ⟹ ∼Semiformula.close φ :: Δ → T ⟹ Δ

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Derivation.id hp b = LO.Tait.cut (LO.Tait.wk (LO.FirstOrder.Derivation.root hp).toClose ⋯) b

instance LO.FirstOrder.Theory.instWeakerThanSyntacticFormulaHAdd {L : Language} {T U : Theory L} : T wkn T + U

instance LO.FirstOrder.Theory.instWeakerThanSyntacticFormulaHAdd_1 {L : Language} {T U : Theory L} : U wkn T + U

structure LO.FirstOrder.Theory.Alt (L : Language) : Type u_1

An auxiliary structure to provide systems of provability of sentence.

• thy : Theory L

  Imported declaration from the Incompleteness formalization.

def LO.FirstOrder.Theory.alt {L : Language} (thy : Theory L) : Alt L

Alias of LO.FirstOrder.Theory.Alt.mk.

Equations

• @LO.FirstOrder.Theory.alt = @LO.FirstOrder.Theory.Alt.mk

@[implicit_reducible]

instance LO.FirstOrder.instEntailmentSentenceAlt {L : Language} : Entailment (Sentence L) (Theory.Alt L)

Equations

• LO.FirstOrder.instEntailmentSentenceAlt = { Prf := fun (T : LO.FirstOrder.Theory.Alt L) (σ : LO.FirstOrder.Sentence L) => T.thy ⊢ ↑σ }

@[simp]

theorem LO.FirstOrder.Theory.alt_thy {L : Language} (T : Theory L) : T.alt.thy = T

@[reducible, inline]

abbrev LO.FirstOrder.Provable₀ {L : Language} (T : Theory L) (σ : Sentence L) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• (T ⊢!. σ) = (T.alt ⊢! σ)

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.Unprovable₀ {L : Language} (T : Theory L) (σ : Sentence L) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• (T ⊬. σ) = (T.alt ⊬ σ)

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))

@[implicit_reducible]

instance LO.FirstOrder.instClassicalAltSentence {L : Language} (T : Theory.Alt L) : Entailment.Classical T

Equations

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

theorem LO.FirstOrder.provable₀_iff {L : Language} {T : Theory L} {σ : Sentence L} : T ⊢!. σ ↔ T ⊢! ↑σ

theorem LO.FirstOrder.unprovable₀_iff {L : Language} {T : Theory L} {σ : Sentence L} : T ⊬. σ ↔ T ⊬ ↑σ