| 22 |
22 |
|
| 23 |
23 |
The $\basic$ axioms of bounded arithmetic give the inductive definitions and interrelationships of the various function and predicate symbols.
|
| 24 |
24 |
It also states fundamental algebraic properties, e.g.\ $(0,\succ{ } )$ is a free algebra, and, for us, it will also give us certain `typing' information for our function symbols based on their $\bc$ specification, with safe inputs ranging over $\safe$ and normal ones over $\normal$.
|
| 25 |
|
For instance, we include the following axioms:\footnote{Later some of these will be redundant, for instance $\safe (u \times x) $ and $\safe (u \smsh v)$ are consequences of $\Sigma^\safe_i$-$\pind$, but $\safe (x + y)$ is not since both inputs are safe and so we cannot induct.}
|
| 26 |
|
\[
|
| 27 |
|
\begin{array}{l}
|
| 28 |
|
\forall u^\normal. \safe(u) \\
|
| 29 |
|
\safe (0) \\
|
| 30 |
|
\forall x^\safe . \safe (\succ{} x) \\
|
| 31 |
|
\end{array}
|
| 32 |
|
\qquad
|
| 33 |
|
\begin{array}{l}
|
| 34 |
|
\forall x^\safe, y^\safe . \safe(x+y)\\
|
| 35 |
|
\forall u^\normal, x^\safe . \safe(u\times x) \\
|
| 36 |
|
\forall u^\normal , v^\normal . \safe (u \smsh v)\\
|
| 37 |
|
\forall u^\safe .\safe(\hlf{u})\\
|
| 38 |
|
\forall u^\normal .\safe(|x|)
|
| 39 |
|
\end{array}
|
| 40 |
|
\]
|
| 41 |
|
Notice that we have $\normal \subseteq \safe$.
|
| 42 |
25 |
|
|
26 |
|
|
27 |
Namely, in addition to usual axioms, our $\basic$ includes the following:\footnote{Later some of these will be redundant, for instance $\safe (u \times x) $ and $\safe (u \smsh v)$ are consequences of $\Sigma^\safe_i$-$\pind$, but $\safe (x + y)$ is not since both inputs are safe and so we cannot induct.}
|
|
28 |
\begin{enumerate}[(a)]
|
|
29 |
\item $\forall u^\normal. \safe(u) $
|
|
30 |
\item $\safe (0) $
|
|
31 |
\item $\forall x^\safe . \safe (\succ{} x) $
|
|
32 |
\item $\forall u^\safe .\safe(\hlf{u})$
|
|
33 |
\item $\forall x^\safe, y^\safe . \safe(x+y)$
|
|
34 |
\item $\forall u^\normal, x^\safe . \safe(u\times x) $
|
|
35 |
\item $\forall u^\normal , v^\normal . \safe (u \smsh v)$
|
|
36 |
\item $\forall u^\normal .\safe(|x|)$
|
|
37 |
\end{enumerate}
|
|
38 |
%\[
|
|
39 |
%\begin{array}{l}
|
|
40 |
%\forall u^\normal. \safe(u) \\
|
|
41 |
%\safe (0) \\
|
|
42 |
%\forall x^\safe . \safe (\succ{} x) \\
|
|
43 |
%\forall u^\safe .\safe(\hlf{u})
|
|
44 |
%\end{array}
|
|
45 |
%\qquad
|
|
46 |
%\begin{array}{l}
|
|
47 |
%\forall x^\safe, y^\safe . \safe(x+y)\\
|
|
48 |
%\forall u^\normal, x^\safe . \safe(u\times x) \\
|
|
49 |
%\forall u^\normal , v^\normal . \safe (u \smsh v)\\
|
|
50 |
%\forall u^\normal .\safe(|x|)
|
|
51 |
%\end{array}
|
|
52 |
%\]
|
|
53 |
Notice in particular that we have $\normal \subseteq \safe$.
|
|
54 |
%
|
| 43 |
55 |
Apart from these, the remaining $\basic$ axioms mimic those of Buss in \cite{Buss86book}:
|
|
56 |
\begin{enumerate}[(1)]
|
|
57 |
\item $\forall x^{\safe}, y^{\safe}. (y\leq x\cimp y \leq \succ{} x) $
|
|
58 |
\item $\forall x^{\safe}. x \neq \succ{} x$
|
|
59 |
\item $\forall x^{\safe}.0 \leq x$
|
|
60 |
\item $\forall x^{\safe}, y^{\safe}. ((x\leq y \cand x \neq y) \ciff \succ{} x \leq y) $
|
|
61 |
\item $\forall x^{\safe}. (x\neq 0 \cimp \succ{0}x \neq 0)$
|
|
62 |
\item $\forall x^{\safe}, y^{\safe}. (y\leq x \cor x \leq y)$
|
|
63 |
\item $\forall x^{\safe}, y^{\safe}. ((x\leq y \cand y\leq x )\cimp x=y)$
|
|
64 |
\item $\forall x^{\safe}, y^{\safe}, z^{\safe}. ((x\leq y \cand y\leq z) \cimp x\leq z)$
|
|
65 |
\item $|0|=0$
|
|
66 |
\item $\forall x^{\safe}, y^{\safe}.( x\neq 0 \cimp (|\succ{0}x|=\succ{}( |x|) \cand |\succ{1}x|= \succ{}(|x|))) $
|
|
67 |
\item $|\succ{}0|=\succ{} 0$
|
|
68 |
\item $\forall x^{\safe}, y^{\safe}. (x\leq y \cimp |x|\leq |y|)$
|
|
69 |
\item $\forall x^{\normal}, y^{\normal}. |x\smsh y|=\succ{}( |x|\cdot |y|)$
|
|
70 |
\item $\forall y^{\normal}. 0 \smsh y=\succ{} 0$
|
|
71 |
\item $\forall x^{\normal}. (x\neq 0 \cimp (1 \smsh(\succ{0}x)=\succ{0}(1\smsh x) \cand 1 \smsh(\succ{1}x)=\succ{0}(1\smsh x)))$
|
|
72 |
\item $\forall x^{\normal}, y^{\normal}. x \smsh y = y \smsh x$
|
|
73 |
\item $\forall x^{\normal}, y^{\normal}, z^{\normal}. ( |x|= |y| \cimp x\smsh z = y\smsh z)$
|
|
74 |
\item $\forall x^{\normal}, u^{\normal}, v^{\normal}, y^{\normal}. (|x|= |u|+ |v| \cimp x\smsh y=(u\smsh y)\cdot (v\smsh y))$
|
|
75 |
\item $\forall x^{\safe}, y^{\safe}. x\leq x+y$
|
|
76 |
\item $\forall x^{\safe}, y^{\safe}. ( ( x\leq y \cand x\neq y) \cimp( \succ{}(\succ{0}x) \leq \succ{0}y \cand \succ{}(\succ{0}x) \neq \succ{0}y))$
|
|
77 |
\item $\forall x^{\safe}, y^{\safe}. x+y=y+x$
|
|
78 |
\item $\forall x^{\safe}. x+0=x$
|
|
79 |
\item $\forall x^{\safe}, y^{\safe}. x+\succ{}y=\succ{}(x+y)$
|
|
80 |
\item $\forall x^{\safe}, y^{\safe}, z^{\safe}. (x+y)+z=x+(y+z)$
|
|
81 |
\item $\forall x^{\safe}, y^{\safe}, z^{\safe}. ( x+y \leq x+z \ciff y\leq z)$
|
|
82 |
\item $\forall x^{\safe} 0\cdot x =0$
|
|
83 |
\item $\forall x^{\safe}, y^{\normal}. x\cdot(\succ{}y)=(x\cdot y)+x$
|
|
84 |
\item $\forall x^{\normal}, y^{\normal}. x\cdot y=y\cdot x$
|
|
85 |
\item $\forall x^{\normal}, y^{\safe}, z^{\safe}. x\cdot(y+z)=(x\cdot y)+(x\cdot z)$
|
|
86 |
\item $\forall x^{\normal}, y^{\safe}, z^{\safe}. (x\geq \succ{} 0 \cimp (x\cdot y \leq x\cdot z \ciff y\leq z))$
|
|
87 |
\item $\forall x^{\normal} . (x\neq 0 \cimp |x|=\succ{}(\hlf{x}))$
|
|
88 |
\item $\forall x^{\safe}, y^{\safe}. ( x= \hlf{y} \ciff (\succ{0}x=y \cor \succ{}(\succ{0}x)=y))$
|
|
89 |
\end{enumerate}
|
| 44 |
90 |
|
| 45 |
|
$$
|
| 46 |
|
%\begin{equation}
|
| 47 |
|
\begin{array}{l}
|
| 48 |
|
\forall x^{\safe}, y^{\safe}. (y\leq x\cimp y \leq \succ{} x) \\
|
| 49 |
|
\forall x^{\safe}. x \neq \succ{} x\\
|
| 50 |
|
\forall x^{\safe}.0 \leq x\\
|
| 51 |
|
\forall x^{\safe}, y^{\safe}. ((x\leq y \cand x \neq y) \ciff \succ{} x \leq y) \\
|
| 52 |
|
\forall x^{\safe}. (x\neq 0 \cimp \succ{0}x \neq 0)\\
|
| 53 |
|
\forall x^{\safe}, y^{\safe}. (y\leq x \cor x \leq y)\\
|
| 54 |
|
\forall x^{\safe}, y^{\safe}. ((x\leq y \cand y\leq x )\cimp x=y)\\
|
| 55 |
|
\forall x^{\safe}, y^{\safe}, z^{\safe}. ((x\leq y \cand y\leq z) \cimp x\leq z)\\
|
| 56 |
|
|0|=0\\
|
| 57 |
|
\forall x^{\safe}, y^{\safe}.( x\neq 0 \cimp (|\succ{0}x|=\succ{}( |x|) \cand |\succ{1}x|= \succ{}(|x|))) \\
|
| 58 |
|
|\succ{}0|=\succ{} 0\\
|
| 59 |
|
\forall x^{\safe}, y^{\safe}. (x\leq y \cimp |x|\leq |y|)\\
|
| 60 |
|
\forall x^{\normal}, y^{\normal}. |x\smsh y|=\succ{}( |x|\cdot |y|)\\
|
| 61 |
|
\forall y^{\normal}. 0 \smsh y=\succ{} 0\\
|
| 62 |
|
\forall x^{\normal}. (x\neq 0 \cimp (1 \smsh(\succ{0}x)=\succ{0}(1\smsh x) \cand 1 \smsh(\succ{1}x)=\succ{0}(1\smsh x)))\\
|
| 63 |
|
\forall x^{\normal}, y^{\normal}. x \smsh y = y \smsh x\\
|
| 64 |
|
\forall x^{\normal}, y^{\normal}, z^{\normal}. ( |x|= |y| \cimp x\smsh z = y\smsh z)\\
|
| 65 |
|
\forall x^{\normal}, u^{\normal}, v^{\normal}, y^{\normal}. (|x|= |u|+ |v| \cimp x\smsh y=(u\smsh y)\cdot (v\smsh y))\\
|
| 66 |
|
\forall x^{\safe}, y^{\safe}. x\leq x+y\\
|
| 67 |
|
\forall x^{\safe}, y^{\safe}. ( ( x\leq y \cand x\neq y) \cimp( \succ{}(\succ{0}x) \leq \succ{0}y \cand \succ{}(\succ{0}x) \neq \succ{0}y))\\
|
| 68 |
|
\forall x^{\safe}, y^{\safe}. x+y=y+x\\
|
| 69 |
|
\forall x^{\safe}. x+0=x\\
|
| 70 |
|
\forall x^{\safe}, y^{\safe}. x+\succ{}y=\succ{}(x+y)\\
|
| 71 |
|
\forall x^{\safe}, y^{\safe}, z^{\safe}. (x+y)+z=x+(y+z)\\
|
| 72 |
|
\forall x^{\safe}, y^{\safe}, z^{\safe}. ( x+y \leq x+z \ciff y\leq z)\\
|
| 73 |
|
\forall x^{\safe} 0\cdot x =0\\
|
| 74 |
|
\forall x^{\safe}, y^{\normal}. x\cdot(\succ{}y)=(x\cdot y)+x\\
|
| 75 |
|
%\text{\anupam{check above normal/safe! Pretty sure should be other way around.}}\\
|
| 76 |
|
\forall x^{\normal}, y^{\normal}. x\cdot y=y\cdot x\\
|
| 77 |
|
\forall x^{\normal}, y^{\safe}, z^{\safe}. x\cdot(y+z)=(x\cdot y)+(x\cdot z)\\
|
| 78 |
|
\forall x^{\normal}, y^{\safe}, z^{\safe}. (x\geq \succ{} 0 \cimp (x\cdot y \leq x\cdot z \ciff y\leq z))\\
|
| 79 |
|
\forall x^{\normal} . (x\neq 0 \cimp |x|=\succ{}(\hlf{x}))\\
|
| 80 |
|
\forall x^{\safe}, y^{\safe}. ( x= \hlf{y} \ciff (\succ{0}x=y \cor \succ{}(\succ{0}x)=y))
|
| 81 |
|
\end{array}
|
| 82 |
|
%\end{equation}
|
| 83 |
|
$$
|
| 84 |
91 |
|
|
92 |
%$$
|
|
93 |
%%\begin{equation}
|
|
94 |
%\begin{array}{l}
|
|
95 |
%\forall x^{\safe}, y^{\safe}. (y\leq x\cimp y \leq \succ{} x) \\
|
|
96 |
%\forall x^{\safe}. x \neq \succ{} x\\
|
|
97 |
%\forall x^{\safe}.0 \leq x\\
|
|
98 |
%\forall x^{\safe}, y^{\safe}. ((x\leq y \cand x \neq y) \ciff \succ{} x \leq y) \\
|
|
99 |
%\forall x^{\safe}. (x\neq 0 \cimp \succ{0}x \neq 0)\\
|
|
100 |
%\forall x^{\safe}, y^{\safe}. (y\leq x \cor x \leq y)\\
|
|
101 |
%\forall x^{\safe}, y^{\safe}. ((x\leq y \cand y\leq x )\cimp x=y)\\
|
|
102 |
%\forall x^{\safe}, y^{\safe}, z^{\safe}. ((x\leq y \cand y\leq z) \cimp x\leq z)\\
|
|
103 |
%|0|=0\\
|
|
104 |
%\forall x^{\safe}, y^{\safe}.( x\neq 0 \cimp (|\succ{0}x|=\succ{}( |x|) \cand |\succ{1}x|= \succ{}(|x|))) \\
|
|
105 |
%|\succ{}0|=\succ{} 0\\
|
|
106 |
%\forall x^{\safe}, y^{\safe}. (x\leq y \cimp |x|\leq |y|)\\
|
|
107 |
%\forall x^{\normal}, y^{\normal}. |x\smsh y|=\succ{}( |x|\cdot |y|)\\
|
|
108 |
%\forall y^{\normal}. 0 \smsh y=\succ{} 0\\
|
|
109 |
%\forall x^{\normal}. (x\neq 0 \cimp (1 \smsh(\succ{0}x)=\succ{0}(1\smsh x) \cand 1 \smsh(\succ{1}x)=\succ{0}(1\smsh x)))\\
|
|
110 |
%\forall x^{\normal}, y^{\normal}. x \smsh y = y \smsh x\\
|
|
111 |
%\forall x^{\normal}, y^{\normal}, z^{\normal}. ( |x|= |y| \cimp x\smsh z = y\smsh z)\\
|
|
112 |
%\forall x^{\normal}, u^{\normal}, v^{\normal}, y^{\normal}. (|x|= |u|+ |v| \cimp x\smsh y=(u\smsh y)\cdot (v\smsh y))\\
|
|
113 |
%\forall x^{\safe}, y^{\safe}. x\leq x+y\\
|
|
114 |
%\forall x^{\safe}, y^{\safe}. ( ( x\leq y \cand x\neq y) \cimp( \succ{}(\succ{0}x) \leq \succ{0}y \cand \succ{}(\succ{0}x) \neq \succ{0}y))\\
|
|
115 |
%\forall x^{\safe}, y^{\safe}. x+y=y+x\\
|
|
116 |
%\forall x^{\safe}. x+0=x\\
|
|
117 |
%\forall x^{\safe}, y^{\safe}. x+\succ{}y=\succ{}(x+y)\\
|
|
118 |
%\forall x^{\safe}, y^{\safe}, z^{\safe}. (x+y)+z=x+(y+z)\\
|
|
119 |
%\forall x^{\safe}, y^{\safe}, z^{\safe}. ( x+y \leq x+z \ciff y\leq z)\\
|
|
120 |
%\forall x^{\safe} 0\cdot x =0\\
|
|
121 |
%\forall x^{\safe}, y^{\normal}. x\cdot(\succ{}y)=(x\cdot y)+x\\
|
|
122 |
%%\text{\anupam{check above normal/safe! Pretty sure should be other way around.}}\\
|
|
123 |
%\forall x^{\normal}, y^{\normal}. x\cdot y=y\cdot x\\
|
|
124 |
%\forall x^{\normal}, y^{\safe}, z^{\safe}. x\cdot(y+z)=(x\cdot y)+(x\cdot z)\\
|
|
125 |
%\forall x^{\normal}, y^{\safe}, z^{\safe}. (x\geq \succ{} 0 \cimp (x\cdot y \leq x\cdot z \ciff y\leq z))\\
|
|
126 |
%\forall x^{\normal} . (x\neq 0 \cimp |x|=\succ{}(\hlf{x}))\\
|
|
127 |
%\forall x^{\safe}, y^{\safe}. ( x= \hlf{y} \ciff (\succ{0}x=y \cor \succ{}(\succ{0}x)=y))
|
|
128 |
%\end{array}
|
|
129 |
%%\end{equation}
|
|
130 |
%$$
|
|
131 |
%
|
| 85 |
132 |
|
| 86 |
133 |
|
| 87 |
134 |
|
| 88 |
135 |
|
| 89 |
136 |
|
| 90 |
|
It is often useful for us to work with \emph{length-induction}, which is equivalent to polynomial induction and well known from bounded arithmetic:
|
| 91 |
|
\begin{proposition}
|
| 92 |
|
[Length induction]
|
| 93 |
|
The axiom schema of formulae,
|
| 94 |
|
\begin{equation}
|
| 95 |
|
\label{eqn:lind}
|
| 96 |
|
( A(0) \cand \forall x^\normal . (A(x) \cimp A(\succ{} x)) ) \cimp \forall x^\safe. A(|x|)
|
| 97 |
|
\end{equation}
|
| 98 |
|
for formulae $A \in \Sigma^\safe_i$
|
| 99 |
|
is equivalent to $\cpind{\Sigma^\safe_i}$.
|
| 100 |
|
\end{proposition}
|
| 101 |
|
\begin{proof}
|
| 102 |
|
Suppose we have $A(0)$ and $A(a) \cimp A(\succ{} a)$ for each $a \in \normal$.
|
| 103 |
|
Then, by $\basic$, we have that $A(|a|) \cimp A(|2a|)$ and $A(|a|) \cimp A(|2a+1|)$ for each $a \in \normal$, whence we may conclude $\forall x. A(|x|)$ by polynomial induction on $A(|x|)$.
|
| 104 |
|
\end{proof}
|
| 105 |
137 |
|
| 106 |
|
Let us refer to the axiom schema in \eqref{eqn:lind} as $\clind{\Xi}$, when $A \in \mathcal \Xi$.
|
| 107 |
|
We will freely use this in place of polynomial induction whenever it is convenient.
|
| 108 |
138 |
|
| 109 |
139 |
%\begin{definition}
|
| 110 |
140 |
% [Basic theory]
|
| ... | ... | |
| 126 |
156 |
%
|
| 127 |
157 |
%Use base theory + sharply bounded quantifiers.
|
| 128 |
158 |
|
|
159 |
In addition to these axioms, our theories will contain forms of induction, defined below.
|
| 129 |
160 |
|
| 130 |
|
\begin{definition}
|
| 131 |
|
[Quantifier hierarchy]
|
| 132 |
|
$\Sigma^\safe_0 = \Pi^\safe_0 $ is the set of formulae whose only quantifiers are sharply bounded and where $\safe , \normal$ do not occur free.
|
| 133 |
|
We define $\Sigma^\safe_{i+1}$ as the closure of $\Pi^\safe_i $ under $\cor, \cand $, safe existentials and sharply bounded quantifiers.
|
| 134 |
|
We define $\Pi^\safe_{i+1}$ as the closure of $\Sigma^\safe_i $ under $\cor, \cand $, safe universals and sharply bounded quantifiers.
|
| 135 |
|
\end{definition}
|
| 136 |
|
|
| 137 |
|
|
| 138 |
|
Notice that the criterion that $\safe$ does not occur free is not a real restriction, since we can write $\safe (x)$ as $\exists y^\safe . y=x$.
|
| 139 |
|
The criterion is purely to give an appropriate definition of the hierarchy above.
|
| 140 |
|
|
| 141 |
161 |
%\anupam{Collection principles for prenexing? Otherwise need to add closure under sharply bounded quantifiers.}
|
| 142 |
162 |
|
| 143 |
163 |
|
| ... | ... | |
| 158 |
178 |
%We write $I\Xi$ to denote the theory consisting of $\basic$ and $\cax{\Xi}{\ind}$.
|
| 159 |
179 |
\end{definition}
|
| 160 |
180 |
|
|
181 |
We will introduce in fact a hierarchy of theories calibrated by the complexity of induction formulae, so we now introduce the appropriate quantifier hierarchy.
|
| 161 |
182 |
|
|
183 |
\begin{definition}
|
|
184 |
[Quantifier hierarchy]
|
|
185 |
$\Sigma^\safe_0 = \Pi^\safe_0 $ is the set of formulae whose only quantifiers are sharply bounded and where $\safe , \normal$ do not occur free.
|
|
186 |
We define $\Sigma^\safe_{i+1}$ as the closure of $\Pi^\safe_i $ under $\cor, \cand $, safe existentials and sharply bounded quantifiers.
|
|
187 |
We define $\Pi^\safe_{i+1}$ as the closure of $\Sigma^\safe_i $ under $\cor, \cand $, safe universals and sharply bounded quantifiers.
|
|
188 |
\end{definition}
|
|
189 |
|
|
190 |
|
|
191 |
Notice that the criterion that $\safe$ does not occur free is not a real restriction, since we can write $\safe (x)$ as $\exists y^\safe . y=x$.
|
|
192 |
The criterion is purely to give an appropriate definition of the hierarchy above.
|
|
193 |
|
|
194 |
|
| 162 |
195 |
\begin{definition}\label{def:ariththeory}
|
| 163 |
196 |
Define the theory $\arith^i$ consisting of the $\basic$ axioms, $\cpind{\Sigma^\safe_i } $,
|
| 164 |
197 |
%\begin{itemize}
|
| ... | ... | |
| 195 |
228 |
\todo{Proof: Patrick? The final two should require PIND.}
|
| 196 |
229 |
\end{example}
|
| 197 |
230 |
|
|
231 |
It is often useful for us to work with \emph{length-induction}, which is equivalent to polynomial induction and well known from bounded arithmetic:
|
|
232 |
\begin{proposition}
|
|
233 |
[Length induction]
|
|
234 |
The axiom schema of formulae,
|
|
235 |
\begin{equation}
|
|
236 |
\label{eqn:lind}
|
|
237 |
( A(0) \cand \forall x^\normal . (A(x) \cimp A(\succ{} x)) ) \cimp \forall x^\safe. A(|x|)
|
|
238 |
\end{equation}
|
|
239 |
for formulae $A \in \Sigma^\safe_i$
|
|
240 |
is equivalent to $\cpind{\Sigma^\safe_i}$.
|
|
241 |
\end{proposition}
|
|
242 |
\begin{proof}
|
|
243 |
Suppose we have $A(0)$ and $A(a) \cimp A(\succ{} a)$ for each $a \in \normal$.
|
|
244 |
Then, by $\basic$, we have that $A(|a|) \cimp A(|2a|)$ and $A(|a|) \cimp A(|2a+1|)$ for each $a \in \normal$, whence we may conclude $\forall x. A(|x|)$ by polynomial induction on $A(|x|)$.
|
|
245 |
\end{proof}
|
| 198 |
246 |
|
|
247 |
Let us refer to the axiom schema in \eqref{eqn:lind} as $\clind{\Xi}$, when $A \in \Xi$.
|
|
248 |
We will freely use this in place of polynomial induction whenever it is convenient.
|
|
249 |
|
|
250 |
|
| 199 |
251 |
\subsection{Graphs of some basic functions}\label{sect:graphsbasicfunctions}
|
| 200 |
252 |
|
| 201 |
|
We say that a function $f$ is \emph{represented} by a formula $A_f$ in a theory if we can prove a formula of the form $\forall \vec u^{\normal} , \forall \vec x^{\safe}, \exists! y^{\safe}. A_f$. The variables $\vec u$ and $\vec x$ can respectively be thought of as normal and safe arguments of $f$, and $y$ is the output of $f(\vec u; \vec x)$.
|
|
253 |
We say that a function $f$ is \emph{represented} by a formula $A_f$ in a theory if we can prove a formula of the form $\forall \vec u^{\normal} , \forall \vec x^{\safe}, \exists! y^{\safe}. A_f (\vec u , \vec x , y)$, such that $\Nat \models A_f (\vec u , \vec x , f(\vec u , \vec x))$. The variables $\vec u$ and $\vec x$ can respectively be thought of as normal and safe arguments of $f$, and $y$ is the output of $f(\vec u; \vec x)$.
|
|
254 |
We sometimes explicitly delimit variables as such when it is helpful, writing $A_f (\vec u ; \vec x , y)$.
|
| 202 |
255 |
|
| 203 |
256 |
Let us give a few examples for basic functions representable in $\arith^1$, wherein proofs of totality are routine:
|
| 204 |
257 |
\begin{itemize}
|
| ... | ... | |
| 206 |
259 |
%\item Successor $\succ{}$: $\forall x^{\safe} , \exists^{\safe} y. y=x+1.$. The formulas for the binary successors $\succ{0}$, $\succ{1}$ and the constant functions $\epsilon^k$ are defined in a similar way.
|
| 207 |
260 |
%\item Predecessor $p$: $\forall^{\safe} x, \exists^{\safe} y. (x=\succ{0} y \cor x=\succ{1} y \cor (x=\epsilon \cand y= \epsilon)) .$
|
| 208 |
261 |
\item Conditional $C$:
|
| 209 |
|
$$\begin{array}{ll}
|
| 210 |
|
\forall x^{\safe} , y_0^{\safe}, y_1^{\safe}, \exists y^{\safe}. & ((x=0)\cand (y=y_0)\\
|
| 211 |
|
& \cor( \exists z^{\safe}.(x=\succ{0}z) \cand (y=y_0))\\
|
| 212 |
|
& \cor( \exists z^{\safe}.(x=\succ{1}z) \cand (y=y_1)))\
|
|
262 |
$$
|
|
263 |
\forall x^{\safe} , y_0^{\safe}, y_1^{\safe}, \exists y^{\safe}.
|
|
264 |
\left(
|
|
265 |
\begin{array}{rl}
|
|
266 |
&\exists z^{\safe}.x=\succ{0}z \cand y=y_0 \\
|
|
267 |
\cor& \exists z^{\safe}.x=\succ{1}z \cand y=y_1
|
| 213 |
268 |
\end{array}
|
|
269 |
\right)
|
| 214 |
270 |
$$
|
|
271 |
%$$\begin{array}{ll}
|
|
272 |
%\forall x^{\safe} , y_0^{\safe}, y_1^{\safe}, \exists y^{\safe}. & ((x=0)\cand (y=y_0)\\
|
|
273 |
% & \cor( \exists z^{\safe}.(x=\succ{0}z) \cand (y=y_0))\\
|
|
274 |
% & \cor( \exists z^{\safe}.(x=\succ{1}z) \cand (y=y_1)))\
|
|
275 |
%\end{array}
|
|
276 |
%$$
|
| 215 |
277 |
%\item Addition:
|
| 216 |
278 |
%$\forall^{\safe} x, y, \exists^{\safe} z. z=x+y$.
|
| 217 |
279 |
\item Prefix:
|