# 870: Structural Proof Theory/2

Timothy Y. Chow tchow at math.princeton.edu
Mon Mar 22 20:43:28 EDT 2021

```Kevin Buzzard wrote:

> HF:
>
> BELOVED T. T is Peano arithmetic with primitive recursive function symbols.
> BELOVED A. NO SQRT(2). I.e., A is "2n^2 = m^2 has no solutions in n,m > 0".
>
> The "ONLY" proof I know of for this gem in T or anywhere else goes
> like this take essentially two forms.
>
> FIRST PROOF. There is something called the "the number of times 2
> divides n", call it F(n). Now F(nm) = F(n)+F(m) and F(2) = 1.
>
> Suppose 2n^2 = m^2, n,m > 0. Then F(2n^2)  = F(2) + F(n) + F(n) =
> F(m^2) = F(m) + F(m). So 1 + F(n) + F(n) = F(m) + F(m). Invoke the
> even/odd dichotomy for the contradiction.
>
> SECOND PROOF. Use the exponential 2^n. We know 2^0 = 1 and 2^(n+1) =
> 2^n + 2^n. Can define this using the primitive recursive function
> symbol capabilities put in beloved T. Now our previous function F can
> be reasonably defined in terms of 2^n. F(n) is the greatest m such
> that 2^n divides n. And then repeat the proof.
>
> SO IT APPEARS THAT AN "IDEA" IS NEEDED TO PROVE A FROM T.
>
> Me:
>
> The usual proof is strong induction, which I'm surprised you don't mention.
> If m is odd then m^2 is odd (multiply out) so if m^2 is even then m is even
> (this uses that everything is odd or even) and 2n^2=m^2 =4l^2 so 2l^2=n^2
> is a smaller solution.

I have no disagreement with the main point that an "idea" seems to be
needed.  But I wonder if the following proof is really the same as one of
the above?  It feels different to me because it generalizes easily to
showing that sqrt(n) is either an integer or irrational.

Let q be the smallest positive integer such that q*sqrt(2) is an integer.
Then q*(sqrt(2) - 1) is a smaller one, contradiction.

(In a bit more detail: Because q*sqrt(2) is an integer, so are
q*(sqrt(2) - 1) and q*(sqrt(2) - 1)*sqrt(2) = 2q - q*sqrt(2).  The
other thing to check is that 0 < sqrt(2) - 1 < 1.  To generalize to
sqrt(n) we just replace "sqrt(2) - 1" with "sqrt(n) - floor(sqrt(n))".)

Tim
```