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]
Best Answer
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.