870: Structural Proof Theory/2

[Harvey Friedman]

Interesting relevant point, Arnon! You are saying CORRECTLY, that in
the case of NO SQRT(2), instead of introducing HALF(2n) = n as a
function symbol, and going after an ordinary equational induction, we
can instead not introduce it, and use instead a more complicated
course of values induction involving a quantifier - without even
getting involved with functions or encodings of them.

Both ways are good if we are talking about USER controlled proofs
where you tell the program what to be doing.

However, I was trying to see if there is a realistic JUMP here for the
program, to do this without user direction. So there are really two
different paths here for that, which may or may not be completely out
of the question. One is for the program to come up with your induction
statement, and the other is to come up with the right HALF function,
with the obvious equational ordinary induction.

There is another advantage to the HALF function. It naturally occurs
when taking the functional approach to the earlier easier challenges
of working out things in PRESBURGER. Like the even/odd dichotomy.

So there may be a greater chance of something new here regarding JUMPS
if we take the Function Introduction approach. Like primitive
recursion and its obvious variants.

On Tue, Mar 2, 2021 at 3:05 AM Arnon Avron <aa at tauex.tau.ac.il> wrote:
>
>
> Harvey presents in this message two relatively complicated proofs,
> both requiring `idea's, in an enriched version of PA that
>  "2n^2 = m^2 has no solutions in n,m > 0". However,
> This claim is easily equivalent in PA to:
> "For every m>0 there is no n<m such that 2n^2 = m^2".
> To me it seems that the most natural way to prove the latter easy claim
> in PA is by course-of-values induction, based on the observation
> that if m^2=2n^2 for some n<m, then for that n we have
> that n^2=2k^2 for some k<n. (Obviously, this is just a straightforward
> formalization in PA of the classical proof that NO SQRT(2)).
>
> What am I missing here?
>
> Arnon