870: Structural Proof Theory/2
Harvey Friedman
hmflogic at gmail.com
Sun Feb 28 01:18:30 EST 2021
Continues from https://cs.nyu.edu/pipermail/fom/2021-February/022496.html
***I AM OFFICIALLY ASKING FOM CONTRIBUTORS TO STOP CONFLATING PROOF
VERIFICATION ACTIVITIES WITH PROOF FINDING ACTIVITIES. OTHERWISE I
WILL CONSIDER FILING A COMPLAINT WITH THE EDITORIAL BOARD ABOUT THIS
MISREPRESENTATION***
It seems like I want to take this topic in many different directions.
But the unifying theme is
NEW KINDS OF INVESTIGATIONS INTO PROOFS OF ACTUAL MATHEMATICAL THEOREMS
In other words, typically
SUPPOSE WE LOOK AT A FUNDAMENTAL MATHEMATICAL THEOREM. ALL KNOWN
PROOFS HAVE CERTAIN INTERESTING PROPERTIES. **PROVE** THAT ALL PROOFS
HAVE THESE CERTAIN INTERESTING PROPERTIES.
More specifically, I am thinking of a specific BELOVED formal system T
and a specific BELOVED theorem A of T. We know that there is a proof
of A from T, and we even KNOW this with a level of CERTAINTY that we
never had before proof assistants. This is because A has actually been
formally verified by them from T. BUT WHAT can we say about all
possible proofs of A from T?
Even this seems like an incredibly rich source of NEW DEEP PROBLEMS.
In many directions.
In this posting, I am going to restrain myself by focusing on one
beloved T and one beloved A.
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.
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?
Now let's talk about ways to formalized this Conjecture. First of all,
let's back and clarify things. To know where we are going, to orient
ourselves, we need to address at least some:
WHAT KINDS OF A's FROM T CAN BE PROVED **WITH NO IDEA**? And
presumably although needs to be checked, from the proof technologies.
In COMPARISON with NO SQRT(2) there is are the far easier
*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.
PROOF OF NO 1/2: By induction. 0 is not a solution. Suppose n is not a
solution. Then n+1 is not a solution. Why? Suppose 2(n+1) = 1. Then
2n+2 = 1. 2n+1 = 0. But 0 is not a successor. Looks like we only need
2(n+1) = 2n+2. That looks like a SELF PROVING INDUCTION. Where the
statement is used as the induction hypothesis!
It seems n+m = m+n is at a new level from NO 1/2.
PROBLEM. Work out just how and what would be going on UNDER THE HOOD
if we put proof technology on the above six.
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.
WELL, I expect to go into this kind of thing in more detail in later
installments. But first let me try to jump the gun some and formulate
some specific questions.
If I remember correctly, this GROUP OF SIX can all be proved using
quantifier free induction in the primitive language of PA without
primitive recursion. 0,S,+,x. There is the question of throwing in <
and for finer investigations, whether we also want <=, not=. This is
important if we are interested in having no and limiting the use of,
connectives.
QUESTION. Can NO SQRT(2) be proved in this quantifier free induction?
Now I think this question was answered by I think Shepherdson many
years ago, in the negative.
QUESTION. Can NO SQRT(2) be proved using induction for existential
formulas or for universal formulas? Here we allow a block of
existential quantifiers, or a block of universal quantifiers in the
front. I just don't remember if this was addressed. I think many years
ago Lou Van den Dries might have looked into something like this - and
Alex Willkie.
AND even if you can do this for E...E and/or A...A, to test whether
you are using an "idea" or just doing complicated coding, one can ask
HOW MANY QUANTIFIERS ARE YOU USING?
QUESTION. Is there any small set of small formulas even with
alternating quantifiers, in the 0,S,+,x primitives, where induction
with respect to them suffices to prove NO SQRT(2)?
NOW REVISIT these questions with PA using more. Add EXPONENTIATION to
PA. Restart all of this investigation there. Start with the
fundamental defining axiom for exponentiation. Then develop all of the
usual standard quantifier free information involving 0,S,+,x,exp. With
n^m, not just 2^n. Interesting question is showing that doing stuff
with 2^n will not get you the stuff for n^m without more "ideas" of
some sort.
QUESTION. Armed with all of the basic quantifier free stuff with
0,S,+,x,exp, now what is the status of NO SQRT(2)? How simple now can
we make the proof of NO SQRT(2) now? Does NO SQRT(2) need an IDEA? Or
is this exactly the kind of thing that can be done with proof
technology as soon as you tell it to work with exponentiation, or give
it the library for exponentiation?
##########################################
My website is at https://u.osu.edu/friedman.8/ and my youtube site is at
https://www.youtube.com/channel/UCdRdeExwKiWndBl4YOxBTEQ
This is the 870th in a series of self contained numbered
postings to FOM covering a wide range of topics in f.o.m. The list of
previous numbered postings #1-799 can be found at
http://u.osu.edu/friedman.8/foundational-adventures/fom-email-list/
800: Beyond Perfectly Natural/6 4/3/18 8:37PM
801: Big Foundational Issues/1 4/4/18 12:15AM
802: Systematic f.o.m./1 4/4/18 1:06AM
803: Perfectly Natural/7 4/11/18 1:02AM
804: Beyond Perfectly Natural/8 4/12/18 11:23PM
805: Beyond Perfectly Natural/9 4/20/18 10:47PM
806: Beyond Perfectly Natural/10 4/22/18 9:06PM
807: Beyond Perfectly Natural/11 4/29/18 9:19PM
808: Big Foundational Issues/2 5/1/18 12:24AM
809: Goedel's Second Reworked/1 5/20/18 3:47PM
810: Goedel's Second Reworked/2 5/23/18 10:59AM
811: Big Foundational Issues/3 5/23/18 10:06PM
812: Goedel's Second Reworked/3 5/24/18 9:57AM
813: Beyond Perfectly Natural/12 05/29/18 6:22AM
814: Beyond Perfectly Natural/13 6/3/18 2:05PM
815: Beyond Perfectly Natural/14 6/5/18 9:41PM
816: Beyond Perfectly Natural/15 6/8/18 1:20AM
817: Beyond Perfectly Natural/16 Jun 13 01:08:40
818: Beyond Perfectly Natural/17 6/13/18 4:16PM
819: Sugared ZFC Formalization/1 6/13/18 6:42PM
820: Sugared ZFC Formalization/2 6/14/18 6:45PM
821: Beyond Perfectly Natural/18 6/17/18 1:11AM
822: Tangible Incompleteness/1 7/14/18 10:56PM
823: Tangible Incompleteness/2 7/17/18 10:54PM
824: Tangible Incompleteness/3 7/18/18 11:13PM
825: Tangible Incompleteness/4 7/20/18 12:37AM
826: Tangible Incompleteness/5 7/26/18 11:37PM
827: Tangible Incompleteness Restarted/1 9/23/19 11:19PM
828: Tangible Incompleteness Restarted/2 9/23/19 11:19PM
829: Tangible Incompleteness Restarted/3 9/23/19 11:20PM
830: Tangible Incompleteness Restarted/4 9/26/19 1:17 PM
831: Tangible Incompleteness Restarted/5 9/29/19 2:54AM
832: Tangible Incompleteness Restarted/6 10/2/19 1:15PM
833: Tangible Incompleteness Restarted/7 10/5/19 2:34PM
834: Tangible Incompleteness Restarted/8 10/10/19 5:02PM
835: Tangible Incompleteness Restarted/9 10/13/19 4:50AM
836: Tangible Incompleteness Restarted/10 10/14/19 12:34PM
837: Tangible Incompleteness Restarted/11 10/18/20 02:58AM
838: New Tangible Incompleteness/1 1/11/20 1:04PM
839: New Tangible Incompleteness/2 1/13/20 1:10 PM
840: New Tangible Incompleteness/3 1/14/20 4:50PM
841: New Tangible Incompleteness/4 1/15/20 1:58PM
842: Gromov's "most powerful language" and set theory 2/8/20 2:53AM
843: Brand New Tangible Incompleteness/1 3/22/20 10:50PM
844: Brand New Tangible Incompleteness/2 3/24/20 12:37AM
845: Brand New Tangible Incompleteness/3 3/28/20 7:25AM
846: Brand New Tangible Incompleteness/4 4/1/20 12:32 AM
847: Brand New Tangible Incompleteness/5 4/9/20 1 34AM
848. Set Equation Theory/1 4/15 11:45PM
849. Set Equation Theory/2 4/16/20 4:50PM
850: Set Equation Theory/3 4/26/20 12:06AM
851: Product Inequality Theory/1 4/29/20 12:08AM
852: Order Theoretic Maximality/1 4/30/20 7:17PM
853: Embedded Maximality (revisited)/1 5/3/20 10:19PM
854: Lower R Invariant Maximal Sets/1: 5/14/20 11:32PM
855: Lower Equivalent and Stable Maximal Sets/1 5/17/20 4:25PM
856: Finite Increasing reducers/1 6/18/20 4 17PM :
857: Finite Increasing reducers/2 6/16/20 6:30PM
858: Mathematical Representations of Ordinals/1 6/18/20 3:30AM
859. Incompleteness by Effectivization/1 6/19/20 1132PM :
860: Unary Regressive Growth/1 8/120 9:50PM
861: Simplified Axioms for Class Theory 9/16/20 9:17PM
862: Symmetric Semigroups 2/2/21 9:11 PM
863: Structural Mapping Theory/1 2/4/21 11:36PM
864: Structural Mapping Theory/2 2/7/21 1:07AM
865: Structural Mapping Theory/3 2/10/21 11:57PM
866: Structural Mapping Theory/4 2/13/21 12:47AM
867: Structural Mapping Theory/5 2/14/21 11:27PM
868: Structural Mapping Theory/6 2/15/21 9:45PM
869: Structural Proof Theory/1 2/13/21,,10:44AM
Harvey Friedman
More information about the FOM
mailing list