874: Structural Proof Theory/6
Harvey Friedman
hmflogic at gmail.com
Mon Mar 1 18:52:28 EST 2021
So some general categories of research projects in and around proof
technology are crystallizing.
1. Of course, ways to make the tech more powerful for verification.
One of the great tools that I think has not been exploited anywhere
near enough is DECISION PROCEDURES. These can be very fragmentary,
like deciding all particularly simple statements in a specific
language. I think the room for expansion here is virtually unlimited,
and of course it is at the same time very seriously interesting and
challenging THEORY. I would like to comment on that specifically at a
later point. FOR JUST ABOUT ANY USEFUL LITTLE CATEGORY OF SIMILARLY
STRUCTURED MATHEMATICAL ASSERTIONS, there is the matter of the little
ones that come up quite often. THESE SHOULD HAVE A FEASIBLE DECISION
PROCEDURE. There should be hundreds of these all through mathematics.
Let's TAKE THIS TO THE EXTREME FOR A SECOND. Any intelligible
mathematical assertion you make, whether or not it is correct, leads
to a DECISION PROBLEM. The problem is: what statements of this rough
shape and size are true? Depending on the organization of this, there
could be anywhere from a few hundred to a few thousand to a few
million really interesting decision problems and useful for proof
technology. One million people across the globe working on somewhat
different but obviously interlocking DECISION problems eating up
increible resources is really something to IMAGINE!
2. Making the proof tech more interactive. Years ago I got into
exploring some fairly obvious ideas along these lines and I don't
remember what the response was and whether people have followed this
course. It may be by now a line that is totally woven into the present
state of the art. Again I want to take this up. The idea was simply
this. You can view a proof as a series of what I call HAVE/WANT
statements on top of, of course, the axioms, and the all important
HIERARCHICAL DEFINITIONS. There are obvious general purpose beautiful
HAVE/WANT moves that are demonstrably complete for logic. But there
are some CRUCIAL DECISIONS to make along the way as very very few
roads lead to GOLD. These include first of all which kinds of moves to
make as there generally will be a choice of a few. Which notions to
unravel with their definition. Which term or terms to use to
instantiate a universal quantifier with. Which term or terms to try to
use for existential generalization. Which earlier facts to invoke. As
the computer says where it is in the present HAVE/WANT and also allow
the user to access usefully the data bank of previous HAVE/WANTS, this
is displayed nicely on the screen with a list of moves being
considered, and queries of the author about "suggested terms,
please?", even with the computer's own suggestions and so forth. The
user can also interject new definitions, and also tell about the most
relevant prior facts. So this is ENTIRELY HIGHLY USER DRIVEN, with the
computer making its best judgments on its list of suggestions, so
hopefully NORMALLY the user can spot their favorite moves just looking
at the top of the list of possible moves. WHAT IS THE STATE OF THE ART
HERE?
3. THE USE OF THINKING ABOUT PROOF TECHNOLOGY FOR THE INVENTION OF NEW
INTERESTING THEORY!
4. THE USE OF PROOF TECHNOLOGY TO CREATE NEW KINDS OF ELECTRONIC TEXTBOOKS.
5. There are some reports of proof technology FINDING ERRORS by
refusing to accept things they were expected to accept. And then
helping find the fix. You can put in suggested fixes and see which
stick. Probably somebody will come up with PROOF FIXING ROUTINES, so
when something is rejected, it responds with intelligent possible
fixes, all BUILT IN.
6. There are reports of proof technology GENERATING CONJECTURES. I
don't know much about this, but I know that at least this is very
powerful in Euclidean Geometry from decades back.
I barely know where to begin. As you can see, I AM GROPING IN THE DARK
and its FUN! Hoping you also find it fun, if not inspirational.
CONJECTURE ABOUT ELEMENTARY NUMBER THEORY IN PA
You are allowed to do only the following:
1. Make definitions hierarchically, explicitly, or by recursion, of
function symbols of several variables, and relation symbols of several
variables, on N. There is a question about how to handle rationals
here which I will sidestep. Answers range from one extreme to another.
One is that we use a two sorted version of PA, variables over
integers, and variables over rationals. These include negative numbers
of course.
2. Order that induction proofs be made by giving the induction
statement and induction variable. NEVER work one out. That is for the
TECH. Unofficially of course you look into whether this is going to
work.
3. In a manageable way, give a list of relevant previous facts and
previous definitions to be used at any stage. Prioritized.
4. Mention some important terms (terms as in math logic) that figure
into your understanding of how the proofs go.
This input is VERY READABLE and pleasant and looks NONTECHNICAL.
CONJECTURE: This is enough for the technology to find all of the
proofs - in elementary number theory. That is, if you the author
understand that you are supplying all of the real IDEAS.
I.e., the Electronic Textbook consists of your easy to read and
understand suggestions to the proof technology. And the proof
technology confirms offline that you are good.
*A THEORETICAL ISSUE ARISING OUT OF THINKING ABOUT PROOF TECHNOLOGY*
Here is one of many. In using PA or ZFC to prove A, there is what I
was calling the SUFFICIENT FRAGMENT. There seem to be some issues
concerning the nature of these Sufficient Fragments.
Now it is expected that the whole of elementary number theory is
easily provable formally in EFA = exponential function arithmetic. We
can take this here as a rather robust system of ours based on 0,S,+,x,
and exp n^m, and <, as well as the well known obvious quantifier free
axioms in these primitives. But then one takes induction for all
delta_0 formulas. There is a messy well known proof that this is
finitely axiomatized, and in fact, a single instance of delta_0
induction suffices. Of course bounded quantifiers are allowed here.
EFA is an incredibly powerful system that is incredibly weak. I
conjectured a lot that FLT is provable in EFA.
QUESTION: IS THERE A NEAT LITTLE PLEASANT TO READ FINITE SET OF TINY
AXIOMS FOR EFA?
I am sure that the answer is yes, exploiting properly and cleverly, a
lot of Hilbert 10th Problem type stuff here.
*ANOTHER THEORETICAL ISSUE ARISING OUT OF THINKING ABOUT PROOF TECHNOLOGY*
Do this for ZFC. A very good fragment of ZFC is of course WZC = weak
Zermelo set theory with choice, which is well known to be finitely
axiomatizable.
BUT I HAVE ESSENTIALLY DONE THIS SORT OF THING in
https://u.osu.edu/friedman.8/foundational-adventures/downloadable-manuscripts/
#112 For NBG and also for WZC.
**COMMENT ON THE ABOVE**
Maybe if you strategically pick interesting hierarchically defined
concepts, the UNIVERSAL AXIOMS I am talking about can be made also
very interesting and tiny.
##########################################
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 874th 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
870: Structural Proof Theory/2 2/18/21 6:30PM
871: Structural Proof Theory/3
872: Structural Proof Theory/4
873: Structural Proof Theory/5
Harvey Friedman
More information about the FOM
mailing list