[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] Primitive recursive arithmetic means that I am entirely wrong about the nature of the natural numbers. The natural numbers can be defined predicatively without universal quantifiers. * Wikipedia, [Primitive recursive arithmetic](https://en.wikipedia.org/wiki/Primitive_recursive_arithmetic) Primitive recursive arithmetic to define the natural numbers finitely without logic, then define the universe hierarchy of book HoTT using the numbers in primitive recursive arithmetic. There is no need to define a separate proposition judgment, only universe level judgments and typing judgments. Every type is an element of a Russell universe. The end of strong predicativity. The natural numbers come first, and then types/sets/whatever come afterwards. ---- There is a hierarchy of ordered field structures Rational numbers -> Archimedean ordered fields -> Archimedean Euclidean fields -> Archimedean analytic Euclidean fields -> Cauchy complete Archimedean ordered fields -> the terminal Archimedean ordered field ---- We need Archimedean ordered fields which has all analytic functions... ## Entire functions What is an entire function? * Wikipedia, [Entire function](https://en.wikipedia.org/wiki/Entire_function) Given real number $a$, an entire function is a function $f:\mathbb{R} \to \mathbb{R}$ with a sequence $c:\mathbb{N} \to \mathbb{R}$ such that for all real numbers $x$, $f(x)$ is the limit of the power series $$\sum_{i = 0}^{\infty} c(n) \frac{(x - a)^n}{n!}$$ What is the limit of the power series? It is the limit of the sequence of partial sums $g:\mathbb{R} \times \mathbb{N} \to \mathbb{R}$ defined as $$g(x, m) = \sum_{i = 0}^{m} c(n) \frac{(x - a)^n}{n!}$$ Now we need to express it in $\epsilon$-$\delta$ terms. However, in order to do that we additionally need to assume a modulus of convergence for the series. $$\prod_{x:\mathbb{R}} \prod_{\epsilon:\mathbb{Q}_+} \sum_{N:\mathbb{N}} \prod_{m:\mathbb{N}} \prod_{m:\mathbb{N}} (m \geq N) \times (n \geq N) \to (-\epsilon \lt g(x, m) - g(x, n) \lt \epsilon)$$ $$\sum_{M:\mathbb{R} \times \mathbb{Q}_+ \to \mathbb{N}} \prod_{x:\mathbb{R}} \prod_{\epsilon:\mathbb{Q}_+} \prod_{m:\mathbb{N}} \prod_{m:\mathbb{N}} (m \geq M(x, \epsilon)) \times (n \geq M(x, \epsilon)) \to (-\epsilon \lt g(x, m) - g(x, n) \lt \epsilon)$$ Then to say that $f$ is the limit of the sequence we have $$\prod_{x:\mathbb{R}} \prod_{\epsilon:\mathbb{Q}_+} \sum_{N:\mathbb{N}} \prod_{m:\mathbb{N}} (m \geq N) \to (-\epsilon \lt g(x, m) - f(x) \lt \epsilon)$$ We talk about convergent power series. Every convergent power series has a limit function on the real numbers. ## Analytic functions What is an analytic function? * Wikipedia, [Analytic function](https://en.wikipedia.org/wiki/Analytic_function) Given real number $a$ and positive real number $\epsilon$, let $(a - \epsilon, a + \epsilon) \subseteq \mathbb{R}$ denote the open interval with endpoints $a$ and $b$. An analytic function is a function $f:(a - \epsilon, a + \epsilon) \to \mathbb{R}$ with a sequence $c:\mathbb{N} \to \mathbb{R}$ such that for all real numbers $x$ such that $a - \epsilon \lt x \lt a + \epsilon$, $f(x)$ is the limit of the power series $$\sum_{i = 0}^{\infty} c(n) \frac{(x - a)^n}{n!}$$ What is the limit of the power series? It is the limit of the sequence of partial sums $f:(a - \epsilon, a + \epsilon) \times \mathbb{N} \to \mathbb{R}$ defined as $$f(x, m) = \sum_{i = 0}^{m} c(n) \frac{(x - a)^n}{n!}$$ Now we need to express it in $\epsilon$-$\delta$ terms. However, in order to do that we additionally need to assume a modulus of convergence for the series. ## Analytic continuation We just add to the Archimedean ordered field the axiom that it has all analytic functions. We need analytic continuations to continue the functions to the unbounded situation. * Wikipedia, [Analytic continuation](https://en.wikipedia.org/wiki/Analytic_continuation) which is necessary for defining the commonly used analytic functions, such as the exponential, logarithm, trigonometric functions and their inverses. category: redirected to nlab