How much induction does a p-adic valuation need?

Question

Recently I learned a nice constructive proof of the irrationality of $\sqrt{2}$, which uses the 2-adic valuation of an integer: the count of how many times a number is divisible by 2. The valuation requires some induction to construct, and this nice answer by François Dorais talks about how Robinson's Arithmetic $Q$ isn't strong enough to prove $\sqrt{2}$ irrational.

By the question "how much induction...?" I mean what is the complexity of the statement that is used in the application of induction to prove the existence of the valuation (I think the particular case $p=2$ is not special here). Further, I think the only property really needed in this irrationality proof is that the parity of the valuation is well-defined, so in principle it is this specific property that I need to know the strength of:

there is a well-defined multiplicative function $p_2\colon \mathbb{N}\to \{\pm 1\}$ encoding the parity of the 2-adic valuation.

I can easily think of a recursion (say in some dependent type theory, or a proof assistent) that defines this function, but I don't know how to classify the precise strength of the induction principle needed, in the usual arithmetic hierarchy.

[As an aside, I really like this proof, not just because it gives a constructive lower bound on how far a rational is from $\sqrt{2}$, but also because it doesn't rely on more extensive factorisation properties of integers, like one of the most common proofs relying on fractions in 'lowest terms', or on the beautiful, but more subtle, use of infinite descent]

Answer 1

If you want to stick to theories in the basic language of arithmetic $\langle0,1,+,\cdot,<\rangle$, the irrationality of $\sqrt2$ can be easily proved in the theory $IE_1$ (i.e., using induction for bounded existential formulas), since it proves the $\gcd$ property; or even more directly, you can just prove $$\forall a,b<x\,(a^2=2b^2\to b=0)$$ by induction on $x$ (this is a bounded universal formula rather than existential, but $IE_1=IU_1$).

$IE_1$ also proves that any number $x$ can be written uniquely as $yz$ where $y$ is odd and $z$ a power of two (meaning $z$ has no odd divisor apart from $1$), and you can define the parity of $v_2(x)$ by saying that $v_2(x)$ is even iff $z$ is a square. This will be multiplicative as required in the question. Alternatively (but leading to an equivalent definition), $IE_1$ proves that any $x$ can be uniquely written as $y^2z$ with $z$ square-free, and then we can define that $v_2(x)$ is even iff $z$ is odd.

Some larger fragment of $I\Delta_0$ has a $\Delta_0$-definition of the graph of exponentiation, which will enable to define $v_2(x)$ itself.

However, even $IE_1$ is essentially overkill. People usually study bounded arithmetic in languages that are in various ways more suitable than the basic language of arithmetic, and then the 2-adic valuation is definable in very weak fragments; usually not because of some clever trick, but since it more or less belongs to the language. E.g., whenever you have a well-defined bit predicate $$\DeclareMathOperator\bit{bit}\bit(i,X)=\lfloor X2^{-i}\rfloor\bmod2,$$ you can define $$v_2(X)=i\iff\bit(i,X)=1\land\forall j<i\:\bit(j,X)=0.$$ In particular, you can do just that (with a $\Sigma^B_0$ formula) for binary integers $X$ in the basic theory $V^0$ (see [1]), which cannot even define general multiplication, hence it has no meaningful way of stating (let alone proving) the irrationality of $\sqrt2$. The latter can be done in the extension $\mathrm{VTC}^0$ of $\mathrm V^0$ (see [1] again for the definition).

In the realm of one-sorted theories of arithmetic, which is perhaps more in line with the spirit of the question, you can do all this using $\Sigma^b_0$ length-induction (i.e., in the theory $\Sigma^b_0$-LIND as defined e.g. in [2]).

[1] Stephen A. Cook, Phuong Nguyen: Logical foundations of proof complexity, Cambridge University Press, 2010. https://doi.org/10.1017/CBO9780511676277

[2] Chris Pollett: A propositional proof system for $R^i_2$. In: Proof complexity and feasible arithmetics (P. Beame, S. Buss, eds.), DIMACS Series in Discrete Mathematics and Theoretical Computer Science 39 39, AMS, 1997, pp. 253–278.

Answer 2

This is not intended as an answer but rather as a long-winded explanation of what having a 2-adic valuation means for really weak theories such as Q and open induction, which is much too long for a comment.

First and foremost there is a big difference between having a 2-adic valuation term versus a 2-adic valuation relation. A term is always total and single valued, whereas a relation is much more flexible since it neither has to be total nor single valued. So I will prefer the relation symbol for greater generality.

Let's introduce the notation $V_2(x,y)$ to mean that $2^y \mid x$, equivalently $\nu_2(x) \geq y$, where $\nu_2$ is the usual 2-adic valuation. What are the axioms for $V_2$? Here are a three obvious ones: $$V_2(0,y)$$ $$V_2(1,y) \iff y = 0$$ $$V_2(x,y) \iff V_2(x+x,y+1)$$ and two more to reflect the "ultrametric" inequalities $$\min(\nu_2(x),\nu_2(y)) \leq \nu_2(x+y) \leq \max(\nu_2(x),\nu_2(y))+1,$$ namely: $$V_2(x,y_1) \land V_2(x,y_2) \to V_2(x,y_1+y_2)$$ $$V_2(x+1,y_1+y_2) \to V_2(x,y_1) \lor V_2(x,y_2)$$ Interestingly, these already capture all the properties of $V_2$ with respect to the standard model, but to handle multiplication properly we should add the two axioms: $$V_2(x_1,y_1) \land V_2(x_2,y_2) \to V_2(x_1x_2,y_1 + y_2)$$ $$V_2(x_1x_1,y_1+y_2) \to V_2(x_1,y_1) \lor V_2(x_2,y_2)$$ It follows from these axioms that for every $x$ there can be only one $y$ with the property that $V(x,y) \land \lnot V(x,y+1)$. For nonzero standard numbers, this unique $y$ is exactly $\nu_2(x)$. But to ensure that $\nu_2(x)$ is well defined for any $x\neq 0$ we need to add the totality axiom: $$\forall x(x \neq 0 \to \exists y \lnot V_2(x,y))$$

In the language of arithmetic augmented with a symbol for the relation $V_2(x,y)$, open induction and the above axioms ensure that for every $x \neq 0$ there is a unique $y$ such that $V_2(x,y) \land \lnot V_2(x,y+1)$ and we can now conservatively extend this language with a function symbol $\nu_2(x)$ that denotes this $y$ such that $V_2(x,y) \land \lnot V_2(x,y+1)$ when $x \neq 0$. (It doesn't matter much exactly how $\nu_2(0)$ is defined but this is another reason to prefer the relation $V_2$ over 2-adic valuation term.)

With such a $V_2$ and open induction it is easy to prove that $\sqrt{2}$ is irrational, i.e., $2x^2 = y^2$ has no nontrivial solutions. So the precise question is how much induction is needed to have a definable predicate $V_2(x,y)$ that satisfies the above axioms?

Trivially, if $2^y$ is total then we can define $V_2(x,y) \equiv 2^y \mid x$ but this is clearly overkill. On the other hand, it is not obvious how one could define $V_2(x,y)$ without mentioning exponentiation at all.