870: Structural Proof Theory/2

[Buzzard, Kevin M]

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.

HF:

CONJECTURE. A cannot be proved from T (with or without PR function
symbols) without an "idea".

QUESTION. Can this idea or any sufficiently powerful idea to prove A
from T be discovered by proof technology?

Me: I totally agree that an idea is needed. I would say that the tech
again right now is in a situation where this question is kind of meaningless
or inappropriate :-( The ATPs will have a real problem finding this
because they don't know which induction principle to use, the ITPs
will all just say "oh yeah, this is a proof in the library". Again whilst
I completely understand that this looks like a natural "how to start
to understand all this" question, it's like giving a neural network
which could be trained to distinguish cats from dogs given some data,
a picture of a cat, but no data other than some formal definition of a cat.

HF:

*GROUP OF SIX*

NO 1/2. I.e., 2n = 1 has no solutions.
n+m = m+n
(n+m)+r = n+(m+r).
nm = nm
(nm)r = n(mr)
n(m+r) = nm+nr.

Me:

whilst I'm certainly not an expert in machine learning, it would not surprise
me if you could say to a machine "try proving these by induction" and then
wait a couple of minutes and it might well find the 5 last proofs (axioms
of a commutative semiring). For example associativity of addition is
very straightforward to prove if you try induction on all three of the variables
and then just follow your nose -- assuming a + 0 := a and a+Sb := S(a+b) then induction on r
makes this stuff drop out. Commutativity is harder because it involves
discovering an idea which you don't mention: Sa + b = S(a+b). To get
a feeling as to how hard these things are you can work through the proofs
in the natural number game and you will find that a lot of the time you are
just "following your nose". These are precisely the proofs that the computer
can find. But there's a trick -- in the natural number game I carefully arrange
the proofs so that they're in just the right order. Furthermore it is certainly
not the case that following your nose gets you everywhere -- for example
proving that if a>0 and ab=ac then b=c is quite tough. I wouldn't fancy
the computer's chances here.

HF:

PROBLEM. Work out just how and what would be going on UNDER THE HOOD
if we put proof technology on the above six.

Me: this is almost certainly easy and already-done.

HF:

CONJECTURE. There is a clear sense in which all of these (not NO
SQRT(2)) require NO IDEA. And can be eaten up by proof technology. BUT
I AM NOT QUITE SURE ABOUT THIS and want to see this gone into
carefully.

Me: I would say that commutativity of addition requires an idea.
Try proving it by induction yourself -- you run into an issue.
The art is to build up the right theorems in the right order.


-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20210321/bf62c37b/attachment-0001.html>