Is open induction as strong as bounded induction without free bounds? As was established in my question here, one reason that $Q$ + induction on formulas with bounded quantifiers is stronger than $Q$ + induction on quantifier-free formulas is that the variable that we're doing induction on could be the bound of one of the bounded quantifiers.  ($Q$ denotes Robinson arithmetic.)  My question, is that the only reason for the difference in strength?  Would the have equal strength if this possibility were disallowed?  In other words, is $Q$ + induction on quantifier-free formulas just as strong as $Q$ + induction on formulas with bounded quantifiers, with the bounds being either numerals or bound variables?
To me, the answer is pretty obviously yes, since a formula with bounded quantifiers with the bounds being either numerals or bound variables can very easily be written as a formula without quantifiers, and we can apply induction to the latter formula, and then derive a formula of the former type.
Any help would be greatly appreciated.
Thank You in Advance.  
 A: Your thinking is correct. A formula in the language of natural number arithmetic in which all quantifiers are bound by a constant or a bound variable is equivalent to a quantifier-free formula. To see this work down from the top of formula, transforming existential quantifiers into disjunctions and universal quantifiers into conjunctions. E.g., transform $\exists x < 2\cdot\phi$ into $\phi[0/x] \lor \phi[1/x] \lor \phi[2/x]$, where $\phi[i/x]$ means the result of substituting $i$ for $x$ in $\phi$. These transformations preserve the property that all quantifiers are bounded by either constants or bound variables and reduce the number of quantifiers. When no more transformations are possible, you have a quantifier-free formula equivalent to the original. This equivalence holds in any theory that can prove all instances of:
$$x < S^n(0) \implies x = 0 \lor x = S(0) \lor x = S^2(0) \lor \ldots \lor x = S^{n-1}(0)$$
(when $n = 0$, the empty disjunction should be read as a false statement, e.g. $0 \not= 0$).
In particular, I claim the equivalence holds in Robinson's system $Q$. In $Q$ one defines $x < y$ to mean $\exists b\cdot x + S(b) = y$. It is easy to prove (by induction in the metalanguage) that the axioms of $Q$ imply all instances of:
$$ x + S(b) = S^n(0) \implies x = 0 \lor x = S(0) \lor x = S^2(0) \lor \ldots \lor x = S^{n-1}(0)$$
Hence the claimed equivalence does indeed hold in $Q$.
