Proof of Predicative Formulas for the Derivative Condition and for Powers

Auxiliary formulas. By Predicative Substitution of Values of Functions and Binary Operations, and Predicative Formulas for Negatives, Differences, Absolute Values, Distances, Reciprocals and Quotients in an Ordered Field (iv), Predicative Substitution of Values of Functions and Binary Operations, and Predicative Formulas for Negatives, Differences, Absolute Values, Distances, Reciprocals and Quotients in an Ordered Field (viii) and Predicative Substitution of Values of Functions and Binary Operations, and Predicative Formulas for Negatives, Differences, Absolute Values, Distances, Reciprocals and Quotients in an Ordered Field (v), applied to the ordered field $\mathbb{R}$ (The Real Numbers, with the Natural Numbers, Integers and Rationals Identified with Subsets of the Reals, and Completeness (ii)), with its variables $t_{1},\dots,t_{6}$ taken as set variables and renamed to the parameters $\mathbb{R}$, $+$, $\cdot$, $0$, $1$ and $\le$ and its displayed variables renamed as needed, by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (i), there are predicative formulas $D(u,v,w)$, $Q(u,v,w)$ and $A(u,w)$, for distinct set variables $u$, $v$ and $w$, whose free variables are among $u$, $v$, $w$ and these parameters, such that for all sets $u$, $v$ and $w$: $D(u,v,w)$ holds if and only if $u,v\in\mathbb{R}$ and $w=u-v$; $Q(u,v,w)$ holds if and only if $u,v\in\mathbb{R}$, $v\neq0$ and $w=u/v$; and $A(u,w)$ holds if and only if $u\in\mathbb{R}$ and $w=|u|$. Below they are used with other set variables put for $u$, $v$ and $w$, again by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (i).

Proof of (i). The formula. Let $\varepsilon$, $\delta$, $t$, $a$, $b$, $c$, $e$, $n$, $q$, $r$ and $w$ be distinct set variables, other than $h$, $x$, $L$ and the parameters. Let $\beta(x,t,\delta)$ be the formula

$$t\in I\wedge\exists e\,\exists n\,\bigl(D(t,x,e)\wedge A(e,n)\wedge0<n\wedge n<\delta\bigr),$$

let $\kappa(h,x,L,t,\varepsilon)$ be the formula

$$\exists a\,\exists b\,\exists c\,\exists e\,\exists q\,\exists r\,\exists w\,\bigl((t,a)\in h\wedge(x,b)\in h\wedge D(a,b,c)\wedge D(t,x,e)\wedge Q(c,e,q)\wedge D(q,L,r)\wedge A(r,w)\wedge w<\varepsilon\bigr),$$

and let $\Delta(h,x,L)$ be the formula

$$\gamma(h,x,L)\wedge\forall\varepsilon\,\Bigl((\varepsilon\in\mathbb{R}\wedge0<\varepsilon)\Rightarrow\exists\delta\,\bigl(\delta\in\mathbb{R}\wedge0<\delta\wedge\forall t\,(\beta(x,t,\delta)\Rightarrow\kappa(h,x,L,t,\varepsilon))\bigr)\Bigr).$$

Here $(t,a)\in h$ and $(x,b)\in h$ are the formulas of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iii), and $0<n$, $n<\delta$, $0<\varepsilon$, $0<\delta$ and $w<\varepsilon$ are, in the relation notation of Partial and Total Orders on a Set and the Associated Strict Relation (iii), memberships of ordered pairs in the parameter $<$, formulas of the same clause. The free variables of $\Delta$ are among $h$, $x$, $L$ and the parameters.

Predicativity. $\gamma$ is predicative by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (vii), the pair memberships by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iii), and $D$, $Q$ and $A$ by the auxiliary formulas above. $\Delta$ is built from these and from the memberships $t\in I$, $\varepsilon\in\mathbb{R}$ and $\delta\in\mathbb{R}$ by connectives and by quantifiers over the set variables $\varepsilon$, $\delta$, $t$, $a$, $b$, $c$, $e$, $n$, $q$, $r$ and $w$ only. The subformulas $\gamma$, the pair memberships, $D$, $Q$ and $A$, being predicative, contain no quantifier over a class variable. So no quantifier of $\Delta$ is applied to a class variable, and $\Delta$ is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i).

Meaning. Fix an assignment of sets to $h$, $x$ and $L$. If $\gamma(h,x,L)$ fails, then $\Delta(h,x,L)$ fails by its first conjunct, and so does the condition. Let now $\gamma(h,x,L)$ hold: $h:I\to\mathbb{R}$ is a map, $x\in I$ and $L\in\mathbb{R}$, and $I\subseteq\mathbb{R}$ (Intervals of the Real Line (i)). Let $\delta,\varepsilon\in\mathbb{R}$, and let $t$ be a set.

First, $\beta(x,t,\delta)$ holds if and only if $t\in I$ and $0<|t-x|<\delta$: for $t\in I$, $t,x\in\mathbb{R}$, so $D(t,x,e)$ holds exactly for $e=t-x$, and then $A(e,n)$ exactly for $n=|t-x|$.

Second, let $t\in I$ with $0<|t-x|$. Then $t-x\neq0$, as $|0|=0$ (Rules of Arithmetic and Order in an Ordered Field (x)). For every set $a$, $(t,a)\in h$ if and only if $a=h(t)$, and $(x,b)\in h$ if and only if $b=h(x)$, by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (iii) and Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (i), so that the quantifiers $\exists a$ and $\exists b$ with these conjuncts substitute the values $h(t)$ and $h(x)$, as in Predicative Substitution of Values of Functions and Binary Operations, and Predicative Formulas for Negatives, Differences, Absolute Values, Distances, Reciprocals and Quotients in an Ordered Field (i) for the function $h$ with domain $I$; and $h(t),h(x)\in\mathbb{R}$ (Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (ii)). So, in $\kappa(h,x,L,t,\varepsilon)$, the conjuncts before $w<\varepsilon$ hold exactly for $a=h(t)$, $b=h(x)$, $c=h(t)-h(x)$, $e=t-x$, $q=\bigl(h(t)-h(x)\bigr)/(t-x)$, $r=q-L$ and $w=|r|$, by the meanings of $D$, $Q$ and $A$, and $\kappa(h,x,L,t,\varepsilon)$ holds if and only if

$$\Bigl|\frac{h(t)-h(x)}{t-x}-L\Bigr|<\varepsilon .$$

Hence $\Delta(h,x,L)$ holds if and only if for every real $\varepsilon>0$ there is a real $\delta>0$ such that every $t\in I$ with $0<|t-x|<\delta$ satisfies the last inequality, that is, by Derivative of a Real Function on an Interval (i), if and only if $L$ is a derivative of $h$ at $x$. So under every assignment, $\Delta(h,x,L)$ holds if and only if $\gamma(h,x,L)$ holds and $L$ is a derivative of $h$ at $x$: $\Delta$ expresses this condition, as in Conditions Expressed by a Predicative Formula, and Guards (ii), with $h$, $x$ and $L$ for $x_{1}$, $x_{2}$ and $x_{3}$.

Proof of (ii). The formula. Let $a$, $p$ and $k$ be distinct set variables, other than $t$, $m$, $z$ and the parameters. Let $\mathrm{it}(z,m,a)$ be the predicative formula of Iterated Operations Are Given by a Predicative Formula (i), with $z$, $m$ and $a$ for its $w$, $n$ and $a$, and with the parameters $\mathbb{R}$, $\cdot$, $\mathbb{N}$, and the order $\le$ and the addition $+$ of $\mathbb{N}_{0}$ put for its class variables $X$, $F$, $Y$, $R$ and $P$. Let $\chi(t,a)$ be the formula $\forall p\,(p\in a\Leftrightarrow\exists k\,(k\in\mathbb{N}_{0}\wedge p=(k,t)))$, with $p=(k,t)$ the formula of Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (ii), and let $\pi(t,m,z)$ be the formula

$$t\in\mathbb{R}\wedge m\in\mathbb{N}_{0}\wedge\Bigl((m=0\wedge z=1)\vee\bigl(m\in\mathbb{N}\wedge\exists a\,(\chi(t,a)\wedge\mathrm{it}(z,m,a))\bigr)\Bigr).$$

Its free variables are among $t$, $m$, $z$ and the parameters.

Predicativity. $\mathrm{it}$ is predicative by Iterated Operations Are Given by a Predicative Formula (i), and $p=(k,t)$ by Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (ii); $\pi$ is built from these and from memberships and equations by connectives and by quantifiers over the set variables $a$, $p$ and $k$. The subformulas $\mathrm{it}$ and $p=(k,t)$, being predicative, contain no quantifier over a class variable, so no quantifier of $\pi$ is applied to a class variable, and $\pi$ is predicative by Predicativity of Expressions with Abbreviations, and Symbol-Free Forms of the Basic Defined Set Symbols (i).

Meaning. Let $t$, $m$ and $z$ be sets. If $t\notin\mathbb{R}$ or $m\notin\mathbb{N}_{0}$, both $\pi(t,m,z)$ and the condition fail. Let $t\in\mathbb{R}$ and $m\in\mathbb{N}_{0}$. As $\mathbb{N}=\mathbb{N}_{0}\setminus\{0\}$ (The Natural Numbers and the Natural Numbers with Zero: Arithmetic, Order, Induction and Recursion (ii)), exactly one of $m=0$ and $m\in\mathbb{N}$ holds.

If $m=0$, then $\pi(t,m,z)$ holds if and only if $z=1$; and $t^{0}=1$, the neutral element of the multiplication of the commutative ring $\mathbb{R}$, by Maps Given by Iterated Operations: Partial Iterates, Images of Natural Numbers, Powers and Operations over a Finite Set (iv). So $\pi(t,m,z)$ holds if and only if $z=t^{m}$.

Let $m\in\mathbb{N}$. Let $c_{t}:\mathbb{N}_{0}\to\mathbb{R}$ be the map $k\mapsto t$ (Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (v)). For every set $p$: if $p\in c_{t}$, then $p=(k,v)$ with $k\in\mathbb{N}_{0}$ and $v=c_{t}(k)=t$; and $(k,t)=(k,c_{t}(k))\in c_{t}$ for every $k\in\mathbb{N}_{0}$; both by Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (i) and Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (ii), $c_{t}$ being a relation with domain $\mathbb{N}_{0}$ (Functions, Values of a Function, and Functions from One Class to Another (iii)). With Predicativity under Renaming of Set Variables by Variables, of Formulas with Ordered Pairs, and of Formulas for Relations, Functions, Maps, Injectivity, Surjectivity and Bijectivity (ii), $\chi(t,c_{t})$ holds, and a set $a$ satisfies $\chi(t,a)$ if and only if $a$ and $c_{t}$ have the same elements, that is, $a=c_{t}$. So $\exists a\,(\chi(t,a)\wedge\mathrm{it}(z,m,a))$ holds if and only if $\mathrm{it}(z,m,c_{t})$. The map $c_{t}$ is a map from the set $\mathbb{N}_{0}$, which contains $[m]$ (The Segments [n]: Each Is a Set, and 1 Lies in [n] for n ∈ ℕ (i)), to $\mathbb{R}$; so by Iterated Operations Are Given by a Predicative Formula (i), $\mathrm{it}(z,m,c_{t})$ holds if and only if $z=\prod_{k=1}^{m}(c_{t})_{k}$, which by Iterated Operations: Finite Sums and Finite Products (ii) is the iterated product of the restriction $c_{t}|_{[m]}$. That restriction is a map $[m]\to\mathbb{R}$ with value $t$ at every $k\in[m]$ (Domains and Restrictions of Maps (iii)), so it is the map $k\mapsto t$ on $[m]$ (Values, Restriction and Equality of a Map, and the Map $u\mapsto t(u)$ as a Defined Set Symbol (iv)), whose iterated product is $\prod_{k=1}^{m}t$ by Iterated Operations: Finite Sums and Finite Products (i), and this is $t^{m}$ by Powers with Exponents in the Natural Numbers with Zero (i). So $\pi(t,m,z)$ holds if and only if $z=t^{m}$.

Hence, under every assignment, $\pi(t,m,z)$ holds if and only if $t\in\mathbb{R}$, $m\in\mathbb{N}_{0}$ and $z=t^{m}$: $\pi$ expresses this condition, as in Conditions Expressed by a Predicative Formula, and Guards (ii), with $t$, $m$ and $z$ for $x_{1}$, $x_{2}$ and $x_{3}$.