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]

3more comments