2.2. ISigma1🔗

2.2.1. Exponential

It is proved that the graph of exponential is definable by \Sigma_0-formula, and their inductive properties are provable in \mathsf{I}\Sigma_0. In \mathsf{I}\Sigma_1, we can further prove their entireness.

2.2.2. Theory of Hereditary Finite Sets

Weak theory of sets in \mathbf V_\omega (Hereditary Finite Sets) can be developed inside \mathsf{I}\Sigma_1 using Ackermann coding and BIT predicate. Hereafter, we will use the notation i \in a in the sense of BIT predicate:

theorem

LO.FirstOrder.Arithmetic.mem_iff_bit.{u_1} {V : Type u_1}
  [LO.ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {i a : V} :
  i ∈ a ↔ LO.FirstOrder.Arithmetic.Bit i a
LO.FirstOrder.Arithmetic.mem_iff_bit.{u_1}
  {V : Type u_1} [LO.ORingStructure V]
  [V ⊧ₘ* 𝗜𝚺₁] {i a : V} :
  i ∈ a ↔ LO.FirstOrder.Arithmetic.Bit i a

The following comprehension holds.

theorem

LO.FirstOrder.Arithmetic.finset_comprehension₁.{u_1} {V : Type u_1}
  [LO.ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {Γ : LO.SigmaPiDelta} {P : V → Prop}
  (hP : { Γ := Γ, rank := 1 }-Predicate P) (a : V) :
  ∃ s < Exp.exp a, ∀ i < a, i ∈ s ↔ P i
LO.FirstOrder.Arithmetic.finset_comprehension₁.{u_1}
  {V : Type u_1} [LO.ORingStructure V]
  [V ⊧ₘ* 𝗜𝚺₁] {Γ : LO.SigmaPiDelta}
  {P : V → Prop}
  (hP : { Γ := Γ, rank := 1 }-Predicate P)
  (a : V) :
  ∃ s < Exp.exp a, ∀ i < a, i ∈ s ↔ P i

The basic concepts of set theory, such as union, inter, cartesian product, and mapping, etc. are defined.

2.2.2.1. Seq

\mathrm{Seq}(s) iff s is a mapping and its domain is [0, l) for some l.

def

LO.FirstOrder.Arithmetic.Seq.{u_1} {V : Type u_1} [LO.ORingStructure V]
  [V ⊧ₘ* 𝗜𝚺₁] (s : V) : Prop
LO.FirstOrder.Arithmetic.Seq.{u_1}
  {V : Type u_1} [LO.ORingStructure V]
  [V ⊧ₘ* 𝗜𝚺₁] (s : V) : Prop

2.2.3. Primitive Recursion

Let f(\vec v), g(\vec{v}, x, z) be a \Sigma_1-function. There is a \Sigma_1-function \mathsf{PR}_{f,g}(\vec{v}, u) such that:

\begin{align*} \mathsf{PR}_{f,g}(\vec{v}, 0) &= f(\vec{v}) \\ \mathsf{PR}_{f,g}(\vec{v}, u + 1) &= g(\vec{v}, u, \mathsf{PR}_{f,g}(\vec{v}, u)) \end{align*}

structure

LO.FirstOrder.Arithmetic.PR.Blueprint (k : ℕ) : Type
LO.FirstOrder.Arithmetic.PR.Blueprint
  (k : ℕ) : Type

Constructor

LO.FirstOrder.Arithmetic.PR.Blueprint.mk

Fields

zero : 𝚺₁.Semisentence (k + 1)

succ : 𝚺₁.Semisentence (k + 3)

structure

LO.FirstOrder.Arithmetic.PR.Construction.{u_1} (V : Type u_1)
  [LO.ORingStructure V] {k : ℕ}
  (p : LO.FirstOrder.Arithmetic.PR.Blueprint k) : Type u_1
LO.FirstOrder.Arithmetic.PR.Construction.{u_1}
  (V : Type u_1) [LO.ORingStructure V]
  {k : ℕ}
  (p :
    LO.FirstOrder.Arithmetic.PR.Blueprint
      k) :
  Type u_1

Constructor

LO.FirstOrder.Arithmetic.PR.Construction.mk.{u_1}

Fields

zero : (Fin k → V) → V

succ : (Fin k → V) → V → V → V

zero_defined : LO.FirstOrder.Arithmetic.HierarchySymbol.DefinedFunction self.zero p.zero

succ_defined : LO.FirstOrder.Arithmetic.HierarchySymbol.DefinedFunction (fun v ↦ self.succ (fun x ↦ v x.succ.succ) (v 1) (v 0)) p.succ

def

LO.FirstOrder.Arithmetic.PR.Construction.result.{u_1} {V : Type u_1}
  [LO.ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {k : ℕ}
  {p : LO.FirstOrder.Arithmetic.PR.Blueprint k}
  (c : LO.FirstOrder.Arithmetic.PR.Construction V p) (v : Fin k → V)
  (u : V) : V
LO.FirstOrder.Arithmetic.PR.Construction.result.{u_1}
  {V : Type u_1} [LO.ORingStructure V]
  [V ⊧ₘ* 𝗜𝚺₁] {k : ℕ}
  {p :
    LO.FirstOrder.Arithmetic.PR.Blueprint
      k}
  (c :
    LO.FirstOrder.Arithmetic.PR.Construction
      V p)
  (v : Fin k → V) (u : V) : V

theorem

LO.FirstOrder.Arithmetic.PR.Construction.result_zero.{u_1}
  {V : Type u_1} [LO.ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {k : ℕ}
  {p : LO.FirstOrder.Arithmetic.PR.Blueprint k}
  (c : LO.FirstOrder.Arithmetic.PR.Construction V p) (v : Fin k → V) :
  c.result v 0 = c.zero v
LO.FirstOrder.Arithmetic.PR.Construction.result_zero.{u_1}
  {V : Type u_1} [LO.ORingStructure V]
  [V ⊧ₘ* 𝗜𝚺₁] {k : ℕ}
  {p :
    LO.FirstOrder.Arithmetic.PR.Blueprint
      k}
  (c :
    LO.FirstOrder.Arithmetic.PR.Construction
      V p)
  (v : Fin k → V) :
  c.result v 0 = c.zero v

theorem

LO.FirstOrder.Arithmetic.PR.Construction.result_succ.{u_1}
  {V : Type u_1} [LO.ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {k : ℕ}
  {p : LO.FirstOrder.Arithmetic.PR.Blueprint k}
  (c : LO.FirstOrder.Arithmetic.PR.Construction V p) (v : Fin k → V)
  (u : V) : c.result v (u + 1) = c.succ v u (c.result v u)
LO.FirstOrder.Arithmetic.PR.Construction.result_succ.{u_1}
  {V : Type u_1} [LO.ORingStructure V]
  [V ⊧ₘ* 𝗜𝚺₁] {k : ℕ}
  {p :
    LO.FirstOrder.Arithmetic.PR.Blueprint
      k}
  (c :
    LO.FirstOrder.Arithmetic.PR.Construction
      V p)
  (v : Fin k → V) (u : V) :
  c.result v (u + 1) =
    c.succ v u (c.result v u)

2.2.4. Fixed-point

Let \Phi_C(\vec{v}, x) be a predicate, which takes a class C as a parameter. Then there is a \Sigma_1-predicate \mathsf{Fix}_{\Phi}(\vec{v}, x) such that

\mathsf{Fix}_\Phi(\vec{v}, x) \iff \Phi_{\{z \mid \mathsf{Fix}_\Phi(\vec{v}, z)\}} (\vec{v}, x)

if \Phi satisfies following conditions:

1 \Phi is \Delta_1-definable if C is a set. i.e., a predicate (c, \vec{v}, x) \mapsto \Phi_{\{z \mid \mathrm{Bit}(z, c)\}}(\vec{v}, x) is \Delta_1-definable. 2 Monotone: C \subseteq C' and \Phi_C(\vec{v}, x) implies \Phi_{C'}(\vec{v}, x). 3 Finite: \Phi_C (\vec{v}, x) implies the existence of a m s.t. \Phi_{\{z \in C \mid z < m\}} (\vec{v}, x).

structure

LO.FirstOrder.Arithmetic.Fixpoint.Blueprint (k : ℕ) : Type
LO.FirstOrder.Arithmetic.Fixpoint.Blueprint
  (k : ℕ) : Type

Constructor

LO.FirstOrder.Arithmetic.Fixpoint.Blueprint.mk

Fields

core : 𝚫₁.Semisentence (k + 2)

structure

LO.FirstOrder.Arithmetic.Fixpoint.Construction.{u_1} (V : Type u_1)
  [LO.ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {k : ℕ}
  (φ : LO.FirstOrder.Arithmetic.Fixpoint.Blueprint k) : Type u_1
LO.FirstOrder.Arithmetic.Fixpoint.Construction.{u_1}
  (V : Type u_1) [LO.ORingStructure V]
  [V ⊧ₘ* 𝗜𝚺₁] {k : ℕ}
  (φ :
    LO.FirstOrder.Arithmetic.Fixpoint.Blueprint
      k) :
  Type u_1

Constructor

LO.FirstOrder.Arithmetic.Fixpoint.Construction.mk.{u_1}

Fields

Φ : (Fin k → V) → Set V → V → Prop

defined : LO.FirstOrder.Arithmetic.HierarchySymbol.Defined (fun v ↦ self.Φ (fun x ↦ v x.succ.succ) {x | x ∈ v 1} (v 0)) φ.core

monotone : ∀ {C C' : Set V}, C ⊆ C' → ∀ {v : Fin k → V} {x : V}, self.Φ v C x → self.Φ v C' x

type class

LO.FirstOrder.Arithmetic.Fixpoint.Construction.Finite.{u_1}
  (V : Type u_1) [LO.ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {k : ℕ}
  {φ : LO.FirstOrder.Arithmetic.Fixpoint.Blueprint k}
  (c : LO.FirstOrder.Arithmetic.Fixpoint.Construction V φ) : Prop
LO.FirstOrder.Arithmetic.Fixpoint.Construction.Finite.{u_1}
  (V : Type u_1) [LO.ORingStructure V]
  [V ⊧ₘ* 𝗜𝚺₁] {k : ℕ}
  {φ :
    LO.FirstOrder.Arithmetic.Fixpoint.Blueprint
      k}
  (c :
    LO.FirstOrder.Arithmetic.Fixpoint.Construction
      V φ) :
  Prop

Instance Constructor

LO.FirstOrder.Arithmetic.Fixpoint.Construction.Finite.mk.{u_1}

Methods

finite : ∀ {C : Set V} {v : Fin k → V} {x : V}, c.Φ v C x → ∃ m, c.Φ v {y | y ∈ C ∧ y < m} x

def

LO.FirstOrder.Arithmetic.Fixpoint.Construction.Fixpoint.{u_1}
  {V : Type u_1} [LO.ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {k : ℕ}
  {φ : LO.FirstOrder.Arithmetic.Fixpoint.Blueprint k}
  (c : LO.FirstOrder.Arithmetic.Fixpoint.Construction V φ)
  (v : Fin k → V) (x : V) : Prop
LO.FirstOrder.Arithmetic.Fixpoint.Construction.Fixpoint.{u_1}
  {V : Type u_1} [LO.ORingStructure V]
  [V ⊧ₘ* 𝗜𝚺₁] {k : ℕ}
  {φ :
    LO.FirstOrder.Arithmetic.Fixpoint.Blueprint
      k}
  (c :
    LO.FirstOrder.Arithmetic.Fixpoint.Construction
      V φ)
  (v : Fin k → V) (x : V) : Prop

theorem

LO.FirstOrder.Arithmetic.Fixpoint.Construction.case.{u_1} {V : Type u_1}
  [LO.ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {k : ℕ}
  {φ : LO.FirstOrder.Arithmetic.Fixpoint.Blueprint k}
  (c : LO.FirstOrder.Arithmetic.Fixpoint.Construction V φ)
  {v : Fin k → V} {x : V}
  [LO.FirstOrder.Arithmetic.Fixpoint.Construction.Finite V c] :
  c.Fixpoint v x ↔ c.Φ v {z | c.Fixpoint v z} x
LO.FirstOrder.Arithmetic.Fixpoint.Construction.case.{u_1}
  {V : Type u_1} [LO.ORingStructure V]
  [V ⊧ₘ* 𝗜𝚺₁] {k : ℕ}
  {φ :
    LO.FirstOrder.Arithmetic.Fixpoint.Blueprint
      k}
  (c :
    LO.FirstOrder.Arithmetic.Fixpoint.Construction
      V φ)
  {v : Fin k → V} {x : V}
  [LO.FirstOrder.Arithmetic.Fixpoint.Construction.Finite
      V c] :
  c.Fixpoint v x ↔
    c.Φ v {z | c.Fixpoint v z} x

\mathsf{Fix}_\Phi(\vec v, x) is \Delta_1 if \Phi satisfies strong finiteness:

type class

LO.FirstOrder.Arithmetic.Fixpoint.Construction.StrongFinite.{u_1}
  (V : Type u_1) [LO.ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {k : ℕ}
  {φ : LO.FirstOrder.Arithmetic.Fixpoint.Blueprint k}
  (c : LO.FirstOrder.Arithmetic.Fixpoint.Construction V φ) : Prop
LO.FirstOrder.Arithmetic.Fixpoint.Construction.StrongFinite.{u_1}
  (V : Type u_1) [LO.ORingStructure V]
  [V ⊧ₘ* 𝗜𝚺₁] {k : ℕ}
  {φ :
    LO.FirstOrder.Arithmetic.Fixpoint.Blueprint
      k}
  (c :
    LO.FirstOrder.Arithmetic.Fixpoint.Construction
      V φ) :
  Prop

Instance Constructor

LO.FirstOrder.Arithmetic.Fixpoint.Construction.StrongFinite.mk.{u_1}

Methods

strong_finite : ∀ {C : Set V} {v : Fin k → V} {x : V}, c.Φ v C x → c.Φ v {y | y ∈ C ∧ y < x} x

Also structural induction holds.

theorem

LO.FirstOrder.Arithmetic.Fixpoint.Construction.induction.{u_1}
  {V : Type u_1} [LO.ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] {k : ℕ}
  {φ : LO.FirstOrder.Arithmetic.Fixpoint.Blueprint k}
  (c : LO.FirstOrder.Arithmetic.Fixpoint.Construction V φ)
  {v : Fin k → V} {Γ : LO.SigmaPiDelta}
  [LO.FirstOrder.Arithmetic.Fixpoint.Construction.StrongFinite V c]
  {P : V → Prop} (hP : { Γ := Γ, rank := 1 }-Predicate P)
  (H :
    ∀ (C : Set V),
      (∀ x ∈ C, c.Fixpoint v x ∧ P x) → ∀ (x : V), c.Φ v C x → P x)
  (x : V) : c.Fixpoint v x → P x
LO.FirstOrder.Arithmetic.Fixpoint.Construction.induction.{u_1}
  {V : Type u_1} [LO.ORingStructure V]
  [V ⊧ₘ* 𝗜𝚺₁] {k : ℕ}
  {φ :
    LO.FirstOrder.Arithmetic.Fixpoint.Blueprint
      k}
  (c :
    LO.FirstOrder.Arithmetic.Fixpoint.Construction
      V φ)
  {v : Fin k → V} {Γ : LO.SigmaPiDelta}
  [LO.FirstOrder.Arithmetic.Fixpoint.Construction.StrongFinite
      V c]
  {P : V → Prop}
  (hP : { Γ := Γ, rank := 1 }-Predicate P)
  (H :
    ∀ (C : Set V),
      (∀ x ∈ C, c.Fixpoint v x ∧ P x) →
        ∀ (x : V), c.Φ v C x → P x)
  (x : V) : c.Fixpoint v x → P x