[[!redirects Sandbox > history]] [[!redirects Sandbox]] < [[nlab:Sandbox]] \section{First order logic with apartness} Our sets have apartness in them, and our functions are strongly extensional. Thus, constructively, they behave as weakly predicative mathematics, because if there is a set of propositions, then excluded middle holds. We call a 0-truncated type simply a 0-type, rather than an h-set. \section{Smooth real numbers} Let $\mathbb{R}[X]$ be the real polynomial ring generated by the natural numbers, with sequence of indeterminants $X:\mathbb{N} \to \mathbb{R}[X]$. We define the smooth real numbers to be the quotient ring $$\mathcal{R} \coloneqq \frac{\mathbb{R}[X]}{X(n)^{n + 2} \sim 0}$$ This implies that the smooth real numbers are a local ring, where the non-invertible elements are those whose real component is zero, and thus are called **purely infinitesimal real number**. Given a list of pairs of natural numbers $p:(\mathbb{N} \times \mathbb{N})^*$ let $r$ be a finite product of powers of infintesimals $$r \coloneqq \prod_{i = 0}^{\mathrm{len}(p) - 1} X(\pi_1(p(i)))^{\pi_2(p(i))}$$ The order to which the finite product of powers of infintesimals vanishes is the least common multiple of the natural numbers $(\pi_1(p(i)) + 2) \div \pi_2(p(i))$ $$\mathrm{Order}(r) \coloneqq \lcm_{i:\mathrm{Fin}(n)} (\pi_1(p(i)) + 2) \div \pi_2(p(i))$$ Every purely infinitesimal real number can be expressed as a linear combination of a finite product of powers of infintesimals. The order to which purely infinitesimal real number vanishes is at most the least common multiple of the order of all the finite product of powers of infintesimals used to express the purely infinitesimal real number. By definition, $\mathbb{R}$ is the reduced part of $\mathcal{R}$. category: redirected to nlab