870: Structural Proof Theory/2

[Timothy Y. Chow]

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