Quantifier-free induction and comparison with $\sqrt{2}$ I am trying to understand quantifier-free induction in the system called PRA - primitive recursive arithmetic which states the following:
$$ \frac{ \varphi[0] \quad \varphi[n] \implies \varphi[Sn]}{\varphi[m]} $$
Now, suppose we are given a rational approximation of $\sqrt{2}$ as follows (I will work with the naturals together with zero):
$$ \textrm{Let } x_0:=1 \\ \textrm{Set } x_{n+1}:=\frac{1}{2} \left( x_n + \frac{2}{x_n} \right) \textrm{for } n=0,1,2,...$$
I want to construct the following term:
$$ c(a) = \left\{\begin{matrix}
0, a < \sqrt{2}\\ 
1, a \geq \sqrt{2}
\end{matrix}\right. $$
for any given rational number $a$. I will use the following definitions for comparison:
$$ \begin{matrix}
\sqrt{2} > a \triangleq \exists n \geq 0 . x_n > a + 2^{-n} \\
\sqrt{2} \leq a \triangleq \forall n \geq 0 . x_n \leq a + 2^{-n}
\end{matrix} $$
Denote $\varphi[n] := x_n \leq a + 2^{-n} $ and $ \psi[n] := x_n > a + 2^{-n}$. Then,
$$ c(a) = \left\{\begin{matrix}
0,  \exists n \geq 0 . \psi[n] := x_n > a + 2^{-n} \\ 
1, \forall n \geq 0 . \varphi[n] := x_n \leq a + 2^{-n} 
\end{matrix}\right. $$
I will assume that the quantifiers can be eliminated in the final claims. For example, $\exists n \geq 0 . \psi[n] := x_n > a + 2^{-n}$ means that a relevant $n$ has been constructed.
Questions:
Can we use induction to show $c(a)=0$?
Is the following true in PRA about these two particular formulas?


*

*$\forall n \geq 0 . \varphi[n] \Longleftrightarrow \varphi[m]$ assuming $m$ is free in $\varphi[m]$. In other words, does $\forall n \geq 0 . \varphi[n]$ admit quantifier elimination?

*Is $c(a)$ decidable?
Update: after an insightful answer, I have started wondering how to define $c(a)$ for a transcendent number, such as $\pi$, which is still definable as a Cauchy sequence though.
Update: as seen in here, comparison of transcendental numbers with arbitrary rationals is much more subtle.
 A: So what you're really doing here is create an auxiliary sequence $y_n=x_n-2^{-n}$. I suppose (but haven't verified it in detail) that the $y_n$s approach $\sqrt 2$ monotonically from below, and $y_n$ is certainly primitive recursive as a function of $n$.
You then define $a > \sqrt2$ to mean that $a\ge y_n$ for all $n$. After the changes discussed in comments, it looks like this actually agrees with the common meaning of when a rational number is greater than $\sqrt2$.

Can we use induction to show that $c(a)=0$?

For any given $a$ you don't even use induction to show this. Just pull an  $n$ such that $y_n>a$ out of a hat, and show what the value of $y_n$ is, and that it is more than $a$. In PRA you don't need induction to show that such-and-such function has such-and-such value at such-and-such input -- simply applying the recursion equations sufficiently many times is enough.

Is the following true in PRA about these two particular formulas?
  
  
*
  
*$\forall n \geq 0 . \varphi[n] \Longleftrightarrow \varphi[m]$ assuming $m$ is free in $\varphi[m]$.
  

Definitely not for an arbitrary $a$ -- say, for $a=\frac12$ we have that $\varphi(0)$ is true (since $\frac12\ge y_0=0$) but $\varphi(1)$ is false because $1\not\ge y_1 = 1$.
It is unclear what you're trying to express by "assuming $m$ is free in $\varphi[m]$", since you have an explicit definition of $\varphi$, and $m$ is certainly free in $x_m>a+2^{-m}$.
On the other hand, if you fix an $a$ that is actually larger than $\sqrt2$, then it feels like you should be able to prove in PRA for that fixed $a$ that $\neg\varphi(n)$ for all $n$. This proof will use induction somewhere, though not necessary on the formula $\neg\varphi(n)$ itself. I haven't worked out the details.
Once you know $\forall n\,\neg\varphi(n)$ it follows easily that $\forall n,m\,(\varphi(n)\leftrightarrow \varphi(m))$.


  
*Is $c(a)$ decidable?
  

Yes, of course. It is decided by the following algorithm
input a
if a < 0
then output 0
else if a*a < 2
     then output 0
     else output 1

Remember that whether a function is computable depends on on what its values are, and not how you have defined the values to be what they are.
