Routine Facts, Continued: Typed Arithmetic, Maps and Predicativity

(i) Base. This setting extends Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices: its conventions and notation are in force.

(ii) Types. Real numbers may be read as elements of the type $\mathrm{Real}$ of The Real Numbers as a Type (i), with differences, quotients, absolute values and the order in the extended real line read back as in Differences, Quotients and Absolute Values of Real Numbers, and Their Order in the Extended Real Line, Read in the Type Real (i), Differences, Quotients and Absolute Values of Real Numbers, and Their Order in the Extended Real Line, Read in the Type Real (ii), Differences, Quotients and Absolute Values of Real Numbers, and Their Order in the Extended Real Line, Read in the Type Real (iii) and Differences, Quotients and Absolute Values of Real Numbers, and Their Order in the Extended Real Line, Read in the Type Real (iv), and Differences, Quotients and Absolute Values of Real Numbers, and Their Order in the Extended Real Line, Read in the Type Real (v); elements of $\mathbb{N}_{0}$ may be read as elements of the type $\mathrm{Natural}$ of The Natural Numbers with Zero as a Type (i); further order and arithmetic facts of $\mathbb{R}$, stated on classes, are as in Order and Arithmetic of ℝ on Classes, Continued; and the reciprocal of a nonzero element of $\mathrm{Real}$ is as in The Reciprocal on the Type of Real Numbers (i).

(iii) Maps. Values, pairs, extensionality, restrictions, constant maps and preimages of maps between classes are as in Maps between Classes: Values, Pairs, Extensionality, Restrictions, Constant Maps and Preimages; inverse relations, preimages, images and enlarged codomains as in Membership in Inverse Relations, Preimages and Images of Classes, and Enlarging the Codomain of a Map; maps given by functional predicative relations, and families of sections, as in Maps from Functional Predicative Relations, and Families of Sections; agreement of the values of two maps as in Maps between Classes, Continued: Agreement of Values; composite maps $x\mapsto W(f(x),g(x))$ into classes, images of singletons, and agreement of maps by induction as in Composite Maps into Classes, Images of Singletons, and Agreement of Maps by Induction.

(iv) Natural numbers. The order and arithmetic of $\mathbb{N}_{0}$, of the natural numbers and of the segments $[n]$ are as in Order and Arithmetic of ℕ₀ in Flat Form, and the law packages of the operations of $\mathbb{N}_{0}$ and of a commutative ring as in Law Packages for the Operations of ℕ₀ and of a Commutative Ring. Induction over $\mathbb{N}$ for predicative conditions, and the order below $1$ and below $n+1$, are as in Induction for Predicative Formulas, and the Order of ℕ below 1 and below n+1; elements of segments are natural numbers and the order is transitive across $<$ and $\le$, by Elements of a Segment Are Natural Numbers, and Mixed Transitivity of the Order on the Natural Numbers; not $m<n$ gives $n\le m$ and $m<n+1$ gives $m\le n$, by Order Facts for Natural Numbers: Not Less Than Gives Greater or Equal, and Below n+1 Gives at Most n; and $n\in[n]$ for $n\in\mathbb{N}$, with membership in the addition class on $\mathbb{N}_{0}$, by The Number n Lies in the Segment [n], and Membership in the Addition Class on ω; intervals of $\mathbb{N}_{0}$ are sets, and a class containing $A\cup\{b\}$ contains $A$ and $b$, by Sethood and Subclasses: Bookkeeping; $\le$ on $\mathbb{N}_{0}$ as membership or equality, and the order against $+1$, as in Further Order Facts for ℕ₀ in Flat Form: ≤ as Membership or Equality, Transitivity for Sets, and the Order against +1; and multiplication on $\mathbb{N}_{0}$ as a recursion, as in Multiplication on ℕ₀ as a Recursion.

(v) Predicativity. Predicative formulas stay predicative under renaming, weakening and substitution of variables, and their meaning is invariant, as in Renaming and Substituting Variables in Predicative Formulas; formulas built from the vocabulary of finite combinatorics are predicative at any variable positions, as in Predicative Formulas for the Vocabulary of Finite Combinatorics, at Any Variable Positions; so are equality with unordered pairs, singletons and successors, as in Atomic Predicative Formulas: Equality with Unordered Pairs, Singletons and Successors; the true condition and agreement of two classes at a pair, as in The True Condition and Agreement of Two Classes at a Pair Are Predicative; differences, quotients, absolute values, distances and the strict order of the real numbers, as in Predicative Formulas for Differences, Quotients, Absolute Values, Distances and the Strict Order of the Real Numbers, at Any Variable Positions; the graph of multiplication on $\mathbb{N}_{0}$, as in The Graph of Multiplication on ℕ₀ Is Given by a Predicative Formula; and injectivity of a map, as in Injectivity of a Map between Set Variables Is Predicative; class comprehension in two and three set variables is stated with ordered pairs as in Class Comprehension in Two and Three Set Variables, Stated with Ordered Pairs, and values of variables and set parameters are sets, with a predicative monotonicity condition, as in Values of Variables and Set Parameters Are Sets; a Predicative Monotonicity Condition; formula trees with named values, as in The Graph Reading of a Formula Tree Is Predicative and Agrees with Its Reading, So the Reading Is Predicative.

(vi) Use. The facts carried by (ii), (iii), (iv) and (v), and their elementary consequences, are used without further citation.