The Functions f ↦ f⁺ and f ↦ f⁻ on the Real-Valued Functions on a Set, and a Predicative Form of g = f⁺ and g = f⁻

In the setting of Routine Facts Used Without Citation: Arithmetic, Maps, Predicativity and Indices, functions and their values are as in Sets and Maps: Ordinary Notation (v). The order $\le$ of $\mathbb{R}$ is total (Arithmetic and Order Rules in the Real Numbers, Stated for ℝ (viii)), and for $a\in\mathbb{R}$, $\max\{a,0\}$ is the greatest element of $\{a,0\}$ (The Maximum and Minimum of Two Elements of a Total Order (i)). Let $X$ be a set and let $\mathbb{R}^{X}$ be the class of functions from $X$ to $\mathbb{R}$; it is a set (The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (ii)) whose elements are exactly the functions $X\to\mathbb{R}$ (The Elements of the Class of Functions from a Set to a Set, and This Class Is a Set (i)). For $f\in\mathbb{R}^{X}$, its positive part $f^{+}$ and negative part $f^{-}$ are functions $X\to\mathbb{R}$, so elements of $\mathbb{R}^{X}$.

(i) The maximum with $0$. For all $a,z\in\mathbb{R}$,

$$z=\max\{a,0\}\iff(z=a\ \text{or}\ z=0),\quad a\le z\quad\text{and}\quad 0\le z.$$

(ii) Predicative form. This clause is a statement of the metatheory; conditions expressed by a predicative formula, parameters and their fixed values are as in Conditions Expressed by a Predicative Formula, and Guards (i). Let $f$ and $g$ be distinct set variables, and take $X$, $\mathbb{R}$, the addition $+$ and the order $\le$ of $\mathbb{R}$, and its element $0$ as parameters. Then each of the two conditions

$$f\in\mathbb{R}^{X}\ \text{and}\ g=f^{+},\qquad\qquad f\in\mathbb{R}^{X}\ \text{and}\ g=f^{-}$$

on $f$ and $g$ is expressed by a predicative formula.

(iii) The functions $f\mapsto f^{+}$ and $f\mapsto f^{-}$. There is exactly one function $P:\mathbb{R}^{X}\to\mathbb{R}^{X}$, and exactly one function $N:\mathbb{R}^{X}\to\mathbb{R}^{X}$, such that

$$P(f)=f^{+}\quad\text{and}\quad N(f)=f^{-}\qquad(f\in\mathbb{R}^{X}).$$

Moreover, for every $f\in\mathbb{R}^{X}$ and every set $g$: $g=f^{+}$ if and only if $(f,g)\in P$, and $g=f^{-}$ if and only if $(f,g)\in N$.