11
$\begingroup$

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]

$\endgroup$
8
  • 2
    $\begingroup$ I don't think the wikipedia editor "wants" a constructive proof, but the proof gives an explicit bound on how badly a given rational approximates $\sqrt{2}$, which is something a proof by contradiction doesn't do. Note also that proof by contradiction and proof of negation are two different things. The usual proof by infinite descent is a constructive proof, in the sense it doesn't use the law of the excluded middle, but, again, it's not explicit. My question is: how small a fragment of induction is needed to make this proof go through. $\endgroup$
    – David Roberts
    Commented Mar 5, 2022 at 3:47
  • $\begingroup$ Is the problem with Q that the 2-adic valuation can't be defined or that one can't prove it has the properties it has? For example multiplication can be defined in Q but one can't prove it is commutative. In some sense (maybe not he one you are using) all computable functions can be defined in Q. $\endgroup$
    – Will Sawin
    Commented Mar 5, 2022 at 3:47
  • $\begingroup$ @WillSawin I don't know. I'm not a logician. Maybe Q can't show that the 2-adic valuation is multiplicative? I don't know. As stated, I am just considering "there is a well-defined multiplicative function $p_2$...." $\endgroup$
    – David Roberts
    Commented Mar 5, 2022 at 3:50
  • 2
    $\begingroup$ I got that, I was just reacting to your comment that a non-constructive proof does not give a bound. $\endgroup$ Commented Mar 5, 2022 at 5:42
  • 2
    $\begingroup$ Common proofs of the irrationality of $\sqrt{2}$ are almost all (secretly!) constructive. This is because irrationality is a negative statement and they are proofs of a negative rather than a proof by contradiction. $\endgroup$ Commented Mar 5, 2022 at 5:47

2 Answers 2

9
$\begingroup$

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.

$\endgroup$
4
  • $\begingroup$ Can you say briefly what $\Sigma^B$ and $\Sigma^b$ denote? I guess the b is meant to denote 'bounded'? EDIT: oh, I see the $\Sigma^b$ family is in section 2 of your reference [2]. But the $\Sigma^B$? $\endgroup$
    – David Roberts
    Commented Mar 5, 2022 at 8:17
  • $\begingroup$ $\Sigma^B_i$ formuals are define in chapter IV of [1]. I’m not sure how to explain it without defining the language of the theory in detail, which I was trying to avoid. But anyway, B also standsfor bounded. The language of $V^0$ is two-sorted, with first sort for natural numbers and second sort for finite sets of natural numbers. The second sort is the main one; its elements can also be interpreted as finite strings, or as integers written in binary, whichever is more useful in a given context. The integers of the first sort are only auxiliary, mainly for indexing the second-sort objects; ... $\endgroup$ Commented Mar 5, 2022 at 8:43
  • $\begingroup$ ... they are logarithmically small compared to the second-sort integers. There is a kind of translation between the one-sorted and two-sorted languages of bounded arithmetic, where the objects of the one-sorted theories correspond to the second-sort objects of the two-sorted theories. Now, $\Sigma^B_0$ formulas are formulas using bounded first-sort quantifiers, and no second-sort quantifiers (but they may use second-sort free variables). They are basically the analogue of $\Sigma^b_0$ under the outlined translation, but it does not quite match. $\endgroup$ Commented Mar 5, 2022 at 8:47
  • $\begingroup$ Ok, thanks! If I need the gory details I can check the reference. $\endgroup$
    – David Roberts
    Commented Mar 5, 2022 at 10:12
8
$\begingroup$

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.

$\endgroup$
1
  • 1
    $\begingroup$ I think you have a small typo in your axioms for $V_2$ — $V_2(x,y)\Longleftrightarrow V_2(x+1, y+y)$ should be the other way around; the RHS should be $V_2(x+x, y+1)$... $\endgroup$ Commented Mar 6, 2022 at 4:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.