Documentation

Arithmetization.Vorspiel.Vorspiel

source
instance instNonemptyOfZero_arithmetization {α : Type u_1} [Zero α] :
Nonempty α
source
def termExp_ :
Lean.ParserDescr
Equations
source
theorem Matrix.forall_iff {α : Type u_1} {n : ℕ} (φ : (Fin (n + 1) → α) → Prop) :
(∀ (v : Fin (n + 1) → α), φ v) ↔ ∀ (a : α) (v : Fin n → α), φ (a :> v)
source
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))
source
@[simp]
theorem Set.subset_union_three₁ {α : Type u_1} (s t u : Set α) :
s ⊆ s ∪ t ∪ u
source
@[simp]
theorem Set.subset_union_three₂ {α : Type u_1} (s t u : Set α) :
t ⊆ s ∪ t ∪ u
source
@[simp]
theorem Set.subset_union_three₃ {α : Type u_1} (s t u : Set α) :
u ⊆ s ∪ t ∪ u
source
theorem Matrix.fun_eq_vec₃ {α : Type u_1} {v : Fin 3 → α} :
v = ![v 0, v 1, v 2]
source
theorem Matrix.fun_eq_vec₄ {α : Type u_1} {v : Fin 4 → α} :
v = ![v 0, v 1, v 2, v 3]
source
@[simp]
theorem Matrix.cons_app_four {α : Type u_1} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ → α) :
(a :> s) 4 = s 3
source
@[simp]
theorem Matrix.cons_app_five {α : Type u_1} {n : ℕ} (a : α) (s : Fin n.succ.succ.succ.succ.succ → α) :
(a :> s) 5 = s 4
source
@[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
source
@[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
source
@[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
source
theorem Matrix.eq_vecCons' {n : ℕ} {C : Type u_1} (s : Fin (n + 1) → C) :
(s 0 :> fun (x : Fin n) => s x.succ) = s
source
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
source
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
source
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)
source
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)
source
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)
source
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)
source
instance instToStringEmpty_arithmetization :
ToString Empty
Equations
source
class Hash (α : Type u_1) :
Type u_1
  • hash : α → α → α
Instances
source
def «term_#_» :
Lean.TrailingParserDescr
Equations
source
class Length (α : Type u_1) :
Type u_1
  • length : α → α
Instances
    source
    def «term‖_‖» :
    Lean.ParserDescr
    Equations
    • One or more equations did not get rendered due to their size.
    source
    def LO.Polarity.coe {α : Type u_1} [SigmaSymbol α] [PiSymbol α] :
    Polarity → α
    Equations
    source
    instance LO.Polarity.instCoe_arithmetization {α : Type u_1} [SigmaSymbol α] [PiSymbol α] :
    Coe Polarity α
    Equations
    source
    @[simp]
    theorem LO.Polarity.coe_sigma {α : Type u_1} [SigmaSymbol α] [PiSymbol α] :
    𝚺.coe = 𝚺
    source
    @[simp]
    theorem LO.Polarity.coe_pi {α : Type u_1} [SigmaSymbol α] [PiSymbol α] :
    𝚷.coe = 𝚷
    source
    @[simp]
    theorem LO.SigmaPiDelta.alt_coe (Γ : Polarity) :
    Γ.coe.alt = Γ.alt.coe
    source
    def LO.FirstOrder.Semiterm.fvarList {L : Language} {ξ : Type u_2} {n : ℕ} :
    Semiterm L ξ n → List ξ
    Equations
    source
    def LO.FirstOrder.Semiterm.fvarEnum {ξ : Type u_1} {L : Language} {n : ℕ} [DecidableEq ξ] (t : Semiterm L ξ n) :
    ξ → ℕ
    Equations
    source
    def LO.FirstOrder.Semiterm.fvarEnumInv {ξ : Type u_1} {L : Language} {n : ℕ} [Inhabited ξ] (t : Semiterm L ξ n) :
    ℕ → ξ
    Equations
    • t.fvarEnumInv i = if hi : i < t.fvarList.length then t.fvarList.get ⟨i, hi⟩ else default
    source
    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
    source
    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
    source
    def LO.FirstOrder.Semiformula.fvarList {L : Language} {ξ : Type u_2} {n : ℕ} :
    Semiformula L ξ n → List ξ
    Equations
    source
    def LO.FirstOrder.Semiformula.fvarEnum {ξ : Type u_1} {L : Language} {n : ℕ} [DecidableEq ξ] (φ : Semiformula L ξ n) :
    ξ → ℕ
    Equations
    source
    def LO.FirstOrder.Semiformula.fvarEnumInv {ξ : Type u_1} {L : Language} {n : ℕ} [Inhabited ξ] (φ : Semiformula L ξ n) :
    ℕ → ξ
    Equations
    • φ.fvarEnumInv i = if hi : i < φ.fvarList.length then φ.fvarList.get ⟨i, hi⟩ else default
    source
    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
    source
    theorem LO.FirstOrder.Semiformula.mem_fvarList_iff_fvar? {ξ : Type u_1} {L : Language} {n : ℕ} {x : ξ} [DecidableEq ξ] {φ : Semiformula L ξ n} :
    x ∈ φ.fvarList ↔ φ.FVar? x
    source
    def LO.FirstOrder.Arith.termToStr {μ : Type u_1} [ToString μ] {n : ℕ} :
    Semiterm ℒₒᵣ μ n → String
    Equations
    source
    instance LO.FirstOrder.Arith.instReprSemitermORing_arithmetization {μ : Type u_1} [ToString μ] {n : ℕ} :
    Repr (Semiterm ℒₒᵣ μ n)
    Equations
    source
    instance LO.FirstOrder.Arith.instToStringSemitermORing_arithmetization {μ : Type u_1} [ToString μ] {n : ℕ} :
    ToString (Semiterm ℒₒᵣ μ n)
    Equations
    source
    def LO.FirstOrder.Arith.formulaToStr {μ : Type u_1} [ToString μ] {n : ℕ} :
    Semiformula ℒₒᵣ μ n → String
    source
    instance LO.FirstOrder.Arith.instReprSemiformulaORing_arithmetization {μ : Type u_1} [ToString μ] {n : ℕ} :
    Repr (Semiformula ℒₒᵣ μ n)
    Equations
    source
    instance LO.FirstOrder.Arith.instToStringSemiformulaORing_arithmetization {μ : Type u_1} [ToString μ] {n : ℕ} :
    ToString (Semiformula ℒₒᵣ μ n)
    Equations
    source
    instance LO.FirstOrder.Arith.indScheme_of_indH (M : Type u_1) [ORingStruc M] (Γ : Polarity) (n : ℕ) [M ⊧ₘ* 𝐈𝐍𝐃Γ n] :
    M ⊧ₘ* Theory.indScheme ℒₒᵣ (Hierarchy Γ n)
    source
    @[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₃]
    source
    @[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₄]
    source
    @[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
    Equations
    source
    @[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
    Equations
    source
    @[simp]
    theorem LO.FirstOrder.models₀_not_iff {L : Language} {M : Type u_1} [Nonempty M] [Structure L M] (σ : Sentence L) :
    M ⊧ₘ₀ ∼σ ↔ ¬M ⊧ₘ₀ σ
    source
    @[simp]
    theorem LO.FirstOrder.models₀_or_iff {L : Language} {M : Type u_1} [Nonempty M] [Structure L M] (σ π : Sentence L) :
    M ⊧ₘ₀ σ ⋎ π ↔ M ⊧ₘ₀ σ ∨ M ⊧ₘ₀ π
    source
    @[simp]
    theorem LO.FirstOrder.models₀_imply_iff {L : Language} {M : Type u_1} [Nonempty M] [Structure L M] (σ π : Sentence L) :
    M ⊧ₘ₀ σ ➝ π ↔ M ⊧ₘ₀ σ → M ⊧ₘ₀ π
    source
    @[simp]
    theorem LO.FirstOrder.Arith.Hierarchy.exItr {L : Language} [L.LT] {μ : Type v} {s n k : ℕ} {φ : Semiformula L μ (n + k)} :
    Hierarchy 𝚺 (s + 1) (∃^[k] φ) ↔ Hierarchy 𝚺 (s + 1) φ
    source
    @[simp]
    theorem LO.FirstOrder.Arith.Hierarchy.univItr {L : Language} [L.LT] {μ : Type v} {s n k : ℕ} {φ : Semiformula L μ (n + k)} :
    Hierarchy 𝚷 (s + 1) (∀^[k] φ) ↔ Hierarchy 𝚷 (s + 1) φ
    source
    instance LO.FirstOrder.Arith.instModelsTheoryCobhamR0_arithmetization (M : Type u_1) [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] :
    M ⊧ₘ* 𝐑₀
    source
    theorem LO.FirstOrder.Arith.nat_extention_sigmaOne (M : Type u_1) [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {σ : Sentence ℒₒᵣ} (hσ : Hierarchy 𝚺 1 σ) :
    ℕ ⊧ₘ₀ σ → M ⊧ₘ₀ σ
    source
    theorem LO.FirstOrder.Arith.nat_extention_piOne (M : Type u_1) [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻] {σ : Sentence ℒₒᵣ} (hσ : Hierarchy 𝚷 1 σ) :
    M ⊧ₘ₀ σ → ℕ ⊧ₘ₀ σ
    source
    theorem LO.Arith.bold_sigma_one_completeness' {M : Type u_1} [ORingStruc M] [M ⊧ₘ* 𝐑₀] {n : ℕ} {σ : FirstOrder.Semisentence ℒₒᵣ n} (hσ : FirstOrder.Arith.Hierarchy 𝚺 1 σ) {e : Fin n → ℕ} :
    ℕ ⊧/e σ → (M ⊧/fun (x : Fin n) => ORingStruc.numeral (e x)) σ
    source
    @[simp]
    theorem List.Vector.nil_get {α : Type u_1} (v : Vector α 0) :
    v.get = ![]