## On foundations ## The natural numbers are characterized by their induction principle (in second-order logic/in a higher universe/as an inductive type). If one only has a first order theory, then one cannot have an induction principle, and instead one has a entire category of models. Thus, the first order models of arithmetic typically found in classical logic and model theory do not define the natural numbers, and this is true even of first-order Peano arithmetic. ## Euclidean semirings ## Given a additively cancellative commutative semiring $R$, a term $e:R$ is *left cancellative* if for all $a:R$ and $b:R$, $e \cdot a = e \cdot b$ implies $a = b$. $$\mathrm{isLeftCancellative}(e) \coloneqq \prod_{a:R} \prod_{b :R}(e \cdot a = e \cdot b) \to (a = b)$$ A term $e:R$ is *right cancellative* if for all $a:R$ and $b:R$, $a \cdot e = b \cdot e$ implies $a = b$. $$\mathrm{isRightCancellative}(e) \coloneqq \prod_{a:R} \prod_{b :R}(a \cdot e = b \cdot e) \to (a = b)$$ An term $e:R$ is *cancellative* if it is both left cancellative and right cancellative. $$\mathrm{isCancellative}(e) \coloneqq \mathrm{isLeftCancellative}(e) \times \mathrm{isRightCancellative}(e)$$ The **multiplicative submonoid of cancellative elements in $R$** is the subset of all cancellative elements in $R$ $$\mathrm{Can}(R) \coloneqq \sum_{e:R} \mathrm{isCancellative}(e)$$ A **Euclidean semiring** is a additively cancellative commutative semiring $R$ for which there exists a function $d \colon \mathrm{Can}(R) \to \mathbb{N}$ from the multiplicative submonoid of cancellative elements in $R$ to the [[natural numbers]], often called a *degree function*, a function $(-)\div(-):R \times \mathrm{Can}(R) \to R$ called the *division function*, and a function $(-)\ \%\ (-):R \times \mathrm{Can}(R) \to R$ called the remainder function, such that for all $a \in R$ and $b \in \mathrm{Can}(R)$, $a = (a \div b) \cdot b + (a\ \%\ b)$ and either $a\ \%\ b = 0$ or $d(a\ \%\ b) \lt d(g)$.