Vorspiel

instance instNonemptyOfZero_leanPool {α : Type u_1} [Zero α] : Nonempty α

def termExp_ : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• termExp_ = Lean.ParserDescr.node `termExp_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "exp ") (Lean.ParserDescr.cat `term 90))

theorem Matrix.forall_vecCons_iff {α : Type u_1} {n : ℕ} (φ : (Fin (n + 1) → α) → Prop) : (∀ (v : Fin (n + 1) → α), φ v) ↔ ∀ (a : α) (v : Fin n → α), φ (a :> v)

theorem Matrix.comp_vecCons₂' {β : Sort u_1} {γ : Type u_2} {α : Type u_3} {n : ℕ} (g : β → γ) (f : α → β) (a : α) (s : Fin n → α) : (fun (x : Fin n.succ) => g (f ((a :> s) x))) = g (f a) :> fun (i : Fin n) => g (f (s i))

@[simp]

theorem Set.subset_union_three₁ {α : Type u_1} (s t u : Set α) : s ⊆ s ∪ t ∪ u

@[simp]

theorem Set.subset_union_three₂ {α : Type u_1} (s t u : Set α) : t ⊆ s ∪ t ∪ u

@[simp]

theorem Set.subset_union_three₃ {α : Type u_1} (s t u : Set α) : u ⊆ s ∪ t ∪ u

theorem Matrix.fun_eq_vec₃ {α : Type u_1} {v : Fin 3 → α} : v = ![v 0, v 1, v 2]

theorem Matrix.fun_eq_vec₄ {α : Type u_1} {v : Fin 4 → α} : v = ![v 0, v 1, v 2, v 3]

@[simp]

theorem Matrix.cons_app_four {α : Type u_1} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ → α) : (a :> s) 4 = s 3

@[simp]

theorem Matrix.cons_app_five {α : Type u_1} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ.succ → α) : (a :> s) 5 = s 4

@[simp]

theorem Matrix.cons_app_six {α : Type u_1} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ.succ.succ → α) : (a :> s) 6 = s 5

@[simp]

theorem Matrix.cons_app_seven {α : Type u_1} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ.succ.succ.succ → α) : (a :> s) 7 = s 6

@[simp]

theorem Matrix.cons_app_eight {α : Type u_1} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ.succ.succ.succ.succ → α) : (a :> s) 8 = s 7

theorem Matrix.eq_vecCons' {n : ℕ} {C : Type u_1} (s : Fin (n + 1) → C) : (s 0 :> fun (x : Fin n) => s x.succ) = s

theorem forall_fin_iff_zero_and_forall_succ {k : ℕ} {P : Fin (k + 1) → Prop} : (∀ (i : Fin (k + 1)), P i) ↔ P 0 ∧ ∀ (i : Fin k), P i.succ

theorem exists_fin_iff_zero_or_exists_succ {k : ℕ} {P : Fin (k + 1) → Prop} : (∃ (i : Fin (k + 1)), P i) ↔ P 0 ∨ ∃ (i : Fin k), P i.succ

theorem forall_vec_iff_forall_forall_vec {k : ℕ} {α : Type u_1} {P : (Fin (k + 1) → α) → Prop} : (∀ (v : Fin (k + 1) → α), P v) ↔ ∀ (x : α) (v : Fin k → α), P (x :> v)

theorem exists_vec_iff_exists_exists_vec {k : ℕ} {α : Type u_1} {P : (Fin (k + 1) → α) → Prop} : (∃ (v : Fin (k + 1) → α), P v) ↔ ∃ (x : α) (v : Fin k → α), P (x :> v)

theorem exists_le_vec_iff_exists_le_exists_vec {α : Type u_1} {k : ℕ} [LE α] {P : (Fin (k + 1) → α) → Prop} {f : Fin (k + 1) → α} : (∃ v ≤ f, P v) ↔ ∃ x ≤ f 0, ∃ v ≤ fun (x : Fin k) => f x.succ, P (x :> v)

theorem forall_le_vec_iff_forall_le_forall_vec {α : Type u_1} {k : ℕ} [LE α] {P : (Fin (k + 1) → α) → Prop} {f : Fin (k + 1) → α} : (∀ v ≤ f, P v) ↔ ∀ x ≤ f 0, ∀ v ≤ fun (x : Fin k) => f x.succ, P (x :> v)

@[implicit_reducible]

instance instToStringEmptyOfVorspiel : ToString Empty

Equations

• instToStringEmptyOfVorspiel = { toString := Empty.elim }

class Hash (α : Type u_1) : Type u_1

Imported declaration from the Incompleteness formalization.

• hash : α → α → α

  Imported declaration from the Incompleteness formalization.

def «term_#_» : Lean.TrailingParserDescr

Imported declaration from the Incompleteness formalization.

Equations

• «term_#_» = Lean.ParserDescr.trailingNode `«term_#_» 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " # ") (Lean.ParserDescr.cat `term 81))

class Length (α : Type u_1) : Type u_1

Imported declaration from the Incompleteness formalization.

• length : α → α

  Imported declaration from the Incompleteness formalization.

def Length.«term‖_‖» : Lean.ParserDescr

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.Polarity.coe {α : Type u_1} [SigmaSymbol α] [PiSymbol α] : Polarity → α

Imported declaration from the Incompleteness formalization.

Equations

• LO.Polarity.sigma.coe = Sg
• LO.Polarity.pi.coe = Pg

@[implicit_reducible]

instance LO.Polarity.instCoe {α : Type u_1} [SigmaSymbol α] [PiSymbol α] : Coe Polarity α

Equations

• LO.Polarity.instCoe = { coe := LO.Polarity.coe }

@[simp]

theorem LO.Polarity.coe_sigma {α : Type u_1} [SigmaSymbol α] [PiSymbol α] : Sg.coe = Sg

@[simp]

theorem LO.Polarity.coe_pi {α : Type u_1} [SigmaSymbol α] [PiSymbol α] : Pg.coe = Pg

@[simp]

theorem LO.SigmaPiDelta.alt_coe (Γ : Polarity) : Γ.coe.alt = Γ.alt.coe

def LO.FirstOrder.Semiterm.fvarList {L : Language} {ξ : Type u_2} {n : ℕ} : Semiterm L ξ n → List ξ

Imported declaration from the Incompleteness formalization.

Equations

• (LO.FirstOrder.Semiterm.bvar a).fvarList = []
• (LO.FirstOrder.Semiterm.fvar x_1).fvarList = [x_1]
• (LO.FirstOrder.Semiterm.func a v).fvarList = (Matrix.toList fun (i : Fin arity) => (v i).fvarList).flatten

def LO.FirstOrder.Semiterm.fvarEnum {ξ : Type u_1} {L : Language} {n : ℕ} [DecidableEq ξ] (t : Semiterm L ξ n) : ξ → ℕ

Imported declaration from the Incompleteness formalization.

Equations

• t.fvarEnum a = List.idxOf a t.fvarList

def LO.FirstOrder.Semiterm.fvarEnumInv {ξ : Type u_1} {L : Language} {n : ℕ} [Inhabited ξ] (t : Semiterm L ξ n) : ℕ → ξ

Imported declaration from the Incompleteness formalization.

Equations

• t.fvarEnumInv i = if hi : i < t.fvarList.length then t.fvarList.get ⟨i, hi⟩ else default

theorem LO.FirstOrder.Semiterm.fvarEnumInv_fvarEnum {ξ : Type u_1} {L : Language} {n : ℕ} [DecidableEq ξ] [Inhabited ξ] {t : Semiterm L ξ n} {x : ξ} (hx : x ∈ t.fvarList) : t.fvarEnumInv (t.fvarEnum x) = x

theorem LO.FirstOrder.Semiterm.mem_fvarList_iff_fvar? {ξ : Type u_1} {L : Language} {n : ℕ} {x : ξ} [DecidableEq ξ] {t : Semiterm L ξ n} : x ∈ t.fvarList ↔ t.FVar? x

def LO.FirstOrder.Semiformula.fvarList {L : Language} {ξ : Type u_2} {n : ℕ} : Semiformula L ξ n → List ξ

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Semiformula.verum.fvarList = []
• LO.FirstOrder.Semiformula.falsum.fvarList = []
• (LO.FirstOrder.Semiformula.rel a v).fvarList = (Matrix.toList fun (i : Fin arity) => (v i).fvarList).flatten
• (LO.FirstOrder.Semiformula.nrel a v).fvarList = (Matrix.toList fun (i : Fin arity) => (v i).fvarList).flatten
• (p.and q).fvarList = p.fvarList ++ q.fvarList
• (p.or q).fvarList = p.fvarList ++ q.fvarList
• p.all.fvarList = p.fvarList
• p.ex.fvarList = p.fvarList

def LO.FirstOrder.Semiformula.fvarEnum {ξ : Type u_1} {L : Language} {n : ℕ} [DecidableEq ξ] (φ : Semiformula L ξ n) : ξ → ℕ

Imported declaration from the Incompleteness formalization.

Equations

• φ.fvarEnum a = List.idxOf a φ.fvarList

def LO.FirstOrder.Semiformula.fvarEnumInv {ξ : Type u_1} {L : Language} {n : ℕ} [Inhabited ξ] (φ : Semiformula L ξ n) : ℕ → ξ

Imported declaration from the Incompleteness formalization.

Equations

• φ.fvarEnumInv i = if hi : i < φ.fvarList.length then φ.fvarList.get ⟨i, hi⟩ else default

theorem LO.FirstOrder.Semiformula.fvarEnumInv_fvarEnum {ξ : Type u_1} {L : Language} {n : ℕ} [DecidableEq ξ] [Inhabited ξ] {φ : Semiformula L ξ n} {x : ξ} (hx : x ∈ φ.fvarList) : φ.fvarEnumInv (φ.fvarEnum x) = x

theorem LO.FirstOrder.Semiformula.mem_fvarList_iff_fvar? {ξ : Type u_1} {L : Language} {n : ℕ} {x : ξ} [DecidableEq ξ] {φ : Semiformula L ξ n} : x ∈ φ.fvarList ↔ φ.FVar? x

def LO.FirstOrder.Arith.termToStr {μ : Type u_1} [ToString μ] {n : ℕ} : Semiterm ℒₒᵣ μ n → String

Imported declaration from the Incompleteness formalization.

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.Arith.termToStr (LO.FirstOrder.Semiterm.bvar x_1) = "x_{" ++ toString (n - 1 - ↑x_1) ++ "}"
• LO.FirstOrder.Arith.termToStr (LO.FirstOrder.Semiterm.fvar x_1) = "a_{" ++ toString x_1 ++ "}"
• LO.FirstOrder.Arith.termToStr (LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.ORing.Func.zero a) = "0"
• LO.FirstOrder.Arith.termToStr (LO.FirstOrder.Semiterm.func LO.FirstOrder.Language.ORing.Func.one a) = "1"

@[implicit_reducible]

instance LO.FirstOrder.Arith.instReprSemitermORing {μ : Type u_1} [ToString μ] {n : ℕ} : Repr (Semiterm ℒₒᵣ μ n)

Equations

• LO.FirstOrder.Arith.instReprSemitermORing = { reprPrec := fun (t : LO.FirstOrder.Semiterm ℒₒᵣ μ n) (x : ℕ) => Std.Format.text (LO.FirstOrder.Arith.termToStr t) }

@[implicit_reducible]

instance LO.FirstOrder.Arith.instToStringSemitermORing {μ : Type u_1} [ToString μ] {n : ℕ} : ToString (Semiterm ℒₒᵣ μ n)

Equations

• LO.FirstOrder.Arith.instToStringSemitermORing = { toString := LO.FirstOrder.Arith.termToStr }

def LO.FirstOrder.Arith.formulaToStr {μ : Type u_1} [ToString μ] {n : ℕ} : Semiformula ℒₒᵣ μ n → String

Imported declaration from the Incompleteness formalization.

Equations

• One or more equations did not get rendered due to their size.
• LO.FirstOrder.Arith.formulaToStr LO.FirstOrder.Semiformula.verum = "\\top"
• LO.FirstOrder.Arith.formulaToStr LO.FirstOrder.Semiformula.falsum = "\\bot"
• LO.FirstOrder.Arith.formulaToStr (LO.FirstOrder.Semiformula.rel LO.FirstOrder.Language.ORing.Rel.eq v) = LO.FirstOrder.Arith.termToStr (v 0) ++ " = " ++ LO.FirstOrder.Arith.termToStr (v 1)
• LO.FirstOrder.Arith.formulaToStr (LO.FirstOrder.Semiformula.rel LO.FirstOrder.Language.ORing.Rel.lt v) = LO.FirstOrder.Arith.termToStr (v 0) ++ " < " ++ LO.FirstOrder.Arith.termToStr (v 1)
• LO.FirstOrder.Arith.formulaToStr (LO.FirstOrder.Semiformula.nrel LO.FirstOrder.Language.ORing.Rel.eq v) = LO.FirstOrder.Arith.termToStr (v 0) ++ " \\not = " ++ LO.FirstOrder.Arith.termToStr (v 1)
• LO.FirstOrder.Arith.formulaToStr (LO.FirstOrder.Semiformula.nrel LO.FirstOrder.Language.ORing.Rel.lt v) = LO.FirstOrder.Arith.termToStr (v 0) ++ " \\not < " ++ LO.FirstOrder.Arith.termToStr (v 1)
• LO.FirstOrder.Arith.formulaToStr (φ.and ψ) = "[" ++ LO.FirstOrder.Arith.formulaToStr φ ++ "]" ++ " \\land " ++ "[" ++ LO.FirstOrder.Arith.formulaToStr ψ ++ "]"
• LO.FirstOrder.Arith.formulaToStr (φ.or ψ) = "[" ++ LO.FirstOrder.Arith.formulaToStr φ ++ "]" ++ " \\lor " ++ "[" ++ LO.FirstOrder.Arith.formulaToStr ψ ++ "]"
• LO.FirstOrder.Arith.formulaToStr φ.all = "(\\forall x_{" ++ toString x✝ ++ "}) " ++ "[" ++ LO.FirstOrder.Arith.formulaToStr φ ++ "]"
• LO.FirstOrder.Arith.formulaToStr φ.ex = "(\\exists x_{" ++ toString x✝ ++ "}) " ++ "[" ++ LO.FirstOrder.Arith.formulaToStr φ ++ "]"

@[implicit_reducible]

instance LO.FirstOrder.Arith.instReprSemiformulaORing {μ : Type u_1} [ToString μ] {n : ℕ} : Repr (Semiformula ℒₒᵣ μ n)

Equations

• LO.FirstOrder.Arith.instReprSemiformulaORing = { reprPrec := fun (t : LO.FirstOrder.Semiformula ℒₒᵣ μ n) (x : ℕ) => Std.Format.text (LO.FirstOrder.Arith.formulaToStr t) }

@[implicit_reducible]

instance LO.FirstOrder.Arith.instToStringSemiformulaORing {μ : Type u_1} [ToString μ] {n : ℕ} : ToString (Semiformula ℒₒᵣ μ n)

Equations

• LO.FirstOrder.Arith.instToStringSemiformulaORing = { toString := LO.FirstOrder.Arith.formulaToStr }

instance LO.FirstOrder.Arith.indScheme_of_indH (M : Type u_1) [ORingStruc M] (Γ : Polarity) (n : ℕ) [M ⊧ₘ* 𝐈𝐍𝐃Γ n] : M ⊧ₘ* Theory.indScheme ℒₒᵣ (Hierarchy Γ n)

@[simp]

theorem LO.FirstOrder.Semiformula.eval_operator₃ {ξ : Type u_3} {L : Language} {M : Type u_1} {s : Structure L M} {n : ℕ} {ε : ξ → M} {e : Fin n → M} {o : Operator L 3} {t₁ t₂ t₃ : Semiterm L ξ n} : (Eval s e ε) (o.operator ![t₁, t₂, t₃]) ↔ o.val ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂, Semiterm.val s e ε t₃]

@[simp]

theorem LO.FirstOrder.Semiformula.eval_operator₄ {ξ : Type u_3} {L : Language} {M : Type u_1} {s : Structure L M} {n : ℕ} {ε : ξ → M} {e : Fin n → M} {o : Operator L 4} {t₁ t₂ t₃ t₄ : Semiterm L ξ n} : (Eval s e ε) (o.operator ![t₁, t₂, t₃, t₄]) ↔ o.val ![Semiterm.val s e ε t₁, Semiterm.val s e ε t₂, Semiterm.val s e ε t₃, Semiterm.val s e ε t₄]

@[reducible, inline]

abbrev LO.FirstOrder.Semiterm.Rlz {L : Language} {M : Type u_1} [Structure L M] {n : ℕ} (t : Semiterm L M n) (e : Fin n → M) : M

Imported declaration from the Incompleteness formalization.

Equations

• t.Rlz e = LO.FirstOrder.Semiterm.valm M e id t

@[reducible, inline]

abbrev LO.FirstOrder.Semiformula.Rlz {L : Language} {M : Type u_1} [Structure L M] {n : ℕ} (φ : Semiformula L M n) (e : Fin n → M) : Prop

Imported declaration from the Incompleteness formalization.

Equations

• φ.Rlz e = (LO.FirstOrder.Semiformula.Evalm M e id) φ

@[simp]

theorem LO.FirstOrder.models₀_not_iff {L : Language} {M : Type u_1} [Nonempty M] [Structure L M] (σ : Sentence L) : M ⊧ₘ₀ ∼σ ↔ ¬M ⊧ₘ₀ σ

@[simp]

theorem LO.FirstOrder.models₀_or_iff {L : Language} {M : Type u_1} [Nonempty M] [Structure L M] (σ π : Sentence L) : M ⊧ₘ₀ σ ⋎ π ↔ M ⊧ₘ₀ σ ∨ M ⊧ₘ₀ π

@[simp]

theorem LO.FirstOrder.models₀_imply_iff {L : Language} {M : Type u_1} [Nonempty M] [Structure L M] (σ π : Sentence L) : M ⊧ₘ₀ σ ==> π ↔ M ⊧ₘ₀ σ → M ⊧ₘ₀ π

@[simp]

theorem LO.FirstOrder.Arith.Hierarchy.exItr {L : Language} [L.LT] {μ : Type v} {s n k : ℕ} {φ : Semiformula L μ (n + k)} : Hierarchy Sg (s + 1) (∃^[k] φ) ↔ Hierarchy Sg (s + 1) φ

@[simp]

theorem LO.FirstOrder.Arith.Hierarchy.univItr {L : Language} [L.LT] {μ : Type v} {s n k : ℕ} {φ : Semiformula L μ (n + k)} : Hierarchy Pg (s + 1) (∀^[k] φ) ↔ Hierarchy Pg (s + 1) φ

instance LO.FirstOrder.Arith.instModelsTheoryCobhamR0 (M : Type u_1) [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] : M ⊧ₘ* 𝐑₀

theorem LO.FirstOrder.Arith.nat_extention_sigmaOne (M : Type u_1) [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {σ : Sentence ℒₒᵣ} (hσ : Hierarchy Sg 1 σ) : ℕ ⊧ₘ₀ σ → M ⊧ₘ₀ σ

theorem LO.FirstOrder.Arith.nat_extention_piOne (M : Type u_1) [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {σ : Sentence ℒₒᵣ} (hσ : Hierarchy Pg 1 σ) : M ⊧ₘ₀ σ → ℕ ⊧ₘ₀ σ

theorem LO.Arith.bold_sigma_one_completeness' {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐑₀] {n : ℕ} {σ : FirstOrder.Semisentence ℒₒᵣ n} (hσ : FirstOrder.Arith.Hierarchy Sg 1 σ) {e : Fin n → ℕ} : ℕ ⊧/e σ → (M ⊧/fun (x : Fin n) => ORingStruc.numeral (e x)) σ

@[simp]

theorem List.Vector.nil_get {α : Type u_1} (v : Vector α 0) : v.get = ![]