[FOM] 616: Adventures in Formalization 3

[Harvey Friedman]

REVERSE PROVER DESIGN - GENERAL PRINCIPLES

Let me stop complaining about Theorem Provers and stop talking about
Delicious Theory, and move to doing something.

In Reverse Prover Design, we FIRST write beautiful elementary proofs.
THEN we figure out how to support them with a Prover!

As the examples get more sophisticated, more issues arise in the
design of the DREAM PROVER.

We'll figure out just what kinds of SELF PROVING really work well.

KEY IDEAS.

1. We don't want to deprive the human of the fun stuff in proofs. We
only want to relieve the human from having to do the unpleasant stuff
in proofs.

2. Experience shows that the quantifier free parts of mathematics are
not the conceptually pleasant parts, and abound with trivialities that
are taken for granted conceptually. Therefore I am convinced that we
must continue to develop smarter and smarter algorithmic packages that
take care of the quantifier free reasoning as much as we can. Of
course, we only care here about the kind of simple real world
quantifier free reasoning that actually occurs.

3. The fun part is the manipulation of quantifiers, and the
imaginative construction of key terms and formulas, particularly when
they are not right in your face when you look at what you are trying
to prove. So in our three toy domains - undergrad set theory,
undergrad number theory (non analytic), undergrad graph theory, we
need to have powerful quantifier free packages. For all three.

4. I am going to start with the number theory stuff. Here we have the
ordered field of rationals, and a predicate for being an integer, and
also not everywhere defined exponentiation and factorial, also with
floor and ceiling. This is enough to really get started. We will use
PA(Q), which is the analog of PA for Q instead of N.

5. We will postpone for the moment discussion of what the capabilities
are for the quantifier free package associated with PA(Q). I need also
to inquire about the state of the art. I think there is gigantic room
here for imaginative fragments that have good decision procedures.
Fragments related to real world environments. Theoretical issues
abound as to decidability of various fragments.

6. So the fun part gets going when we automatically assume that any
weal world quantifier free inference in the PA(Q) environment is
immediately crushed by the computer. This is reflected in the
published Book by "by algebra, we have...".

7. As we go through toy examples of important fundamental actual
textbook theorems, we will accumulate a list of quantifier free stuff
that we Want to have crushed by the computer. This will give us a feel
as to what algorithmic work needs to be done.

CONJECTURE. The set of ALL real world quantifier free inferences in
our three textbook environments is efficiently decidable by a nice
piece of software. By ALL here, I mean those that in fact have a
quantifier free proof from the highlighted quantifier free facts
everybody uses all the time in the domain in question. I think that
this can be more exactly formulated, and is interesting in its own
right - to define the exact category of inferences we are talking
about here.

CONJECTURE. The above package will take us a long way in these three domains.

But we still want to be able to get into a quantifier free situation
and do something by hand, just in case a human cannot be expected to
actually see it - even if it is covered or not by the quantifier free
package.

WE NOW FOCUS on the fun part, assuming this quantifier free drudgery
is taken care of.

8. Get clear about self proving. These are proofs by obvious
unraveling. These proofs should come out essentially by force, with no
creativity of any kind. The process of getting a self proving should
be realistically finite. If we don't get stuck, then we are done.

9. At any stage in the proof, the user can put the computer to work as
follows. REMINDER: We are assuming that the quantifier free part is
always being crushed.
i. Firstly, the computer knows at any stage what the HAVES are and
what the WANT is. We adhere to the HAVE/WANT format.
ii. The computer attempts to get a self proof of the HAVE/WANT. This
is by a definite algorithm involving only unraveling and obvious
pattern matching that obviously are simplification steps. This does
involve using potentially all of the axioms and definitions, but with
only very limited term substitutions. In the case of schemes, very
limited instances. There is no intention of making this work except in
very trivial circumstances. The term and formula substitutions allowed
are extremely limited. But they at least are strong enough to cover
immediate trivialities. AND, very importantly, not so much to get near
any kind of blowup.

10. I view it important to have a good clean idea of just what 9 is,
for the user, for a number of reasons that I think will emerge. As we
go along, we need to fiddle with 9.

11. The user now has the opportunity of interacting with the computer
by providing hints in a special form. This is where some particularly
critical experimentation is needed in lots of real world situations.
How do we make it EXCITINGLY INTERESTING and EFFECTIVE for the user to
give the computer the right powerful HINTS?

12. WHAT GETS PUBLISHED? What gets published in the Formal Book is the
HAVE/WANT development with the successful hints that drive the
computer to find the proofs that are straightforward based on those
hints. We want it set up so that these HINTS serve two purposes. They
are sufficient for the computer to do its drudgery by an
understandable algorithm, AND they are also sufficient for the reader
to see the missing proof. Of course, for experienced readers, they
don't need such hints. Or maybe they might occasionally from time to
time find these published HINT lists of some use.

13. Back to the HINTS. There is the HINT system with computer
installation, and there is the HINT system by hand. Obviously, until I
convince everybody that they should stop what they are doing and back
my approach (not well formed yet), I am going to only be doing HINT
systems by hand with toy examples. I may then try to work with the
Theorem Proving community, if they still are willing to talk to me, to
get some real examples from the battlefield, and see what happens
there - again by hand.

8. So for a while I will be working by hand, maybe forever. I'm
thinking of the HINTS as taking the following forms.
   i. Citing Definitions.
   ii. Citing individual axioms.
   iii. Citing axiom schemes.
   iv. Citing previously established statements.
   v. Providing a finite list of terms.
   vi. Providing a finite list of formulas.

The idea is that the computer will do the SELF PROVING thing using
only the i,ii,iii,iv with only term and formula substitutions lying
within v,vi. Of course, the computer is also doing its SELF PROVING
thing with some default substitutions. This HINT only kicks in if it
gets stuck.

The computer will of course see that almost all of the substitutions
available are totally useless. The computer should be able to block
off almost all of these futile substitutions by general combinatorial
considerations. I see some tricky combinatorics and combinatorial
algorithm design challenges here! After all, the computer knows that
the computer MUST adhere to the SELF PROVING idea, and so a silly
substitution may be quite spottable on combinatorial grounds, walling
off a whole bunch of nonsense from consideration. This is of course to
keep the search from blowing up.

Nevertheless, despite all this, the search could blow up. At this
point, the user has to do HINT REFINEMENT. In the ultimate computer
installation, this would be an interactive process where the computer
provides sample information explaining away its failure. But we have
to proceed by hand here.

13, HINT REFINEMENT. In hint refinement, the list of terms and list of
formulas get marked for use only in conjunction with the cited items i
- iii. This way, the computer is only going to be using those terms in
the list in conjunction with certain items. This cuts down the search
space considerably. There can be even more refined HINTS. Certain
variables in certain items are assigned a substitution term list
marked to it only.

All of this needs careful experimentation to design properly. We need
to BEGIN by taking a real world baby environment and carefully
examining what SELF PROVING really should mean, and what the exact
effect of these HINTS are going to be. This should already be
interesting when examined by hand.

We plan first to work up a lot of examples and by hand experimentation
for elementary number theory. The environment will be the ordered ring
of rationals with a predicate for integers, and with exponentiation
and factorial, sitting on top of the usual free logic in a single
sort.

************************************************************
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 615th 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-599 can be found at the FOM posting
http://www.cs.nyu.edu/pipermail/fom/2015-August/018887.html

600: Removing Deep Pathology 1  8/15/15  10:37PM
601: Finite Emulation Theory 1/perfect?  8/22/15  1:17AM
602: Removing Deep Pathology 2  8/23/15  6:35PM
603: Removing Deep Pathology 3  8/25/15  10:24AM
604: Finite Emulation Theory 2  8/26/15  2:54PM
605: Integer and Real Functions  8/27/15  1:50PM
606: Simple Theory of Types  8/29/15  6:30PM
607: Hindman's Theorem  8/30/15  3:58PM
608: Integer and Real Functions 2  9/1/15  6:40AM
609. Finite Continuation Theory 17  9/315  1:17PM
610: Function Continuation Theory 1  9/4/15  3:40PM
611: Function Emulation/Continuation Theory 2  9/8/15  12:58AM
612: Binary Operation Emulation and Continuation 1  9/7/15  4:35PM
613: Optimal Function Theory 1  9/13/15  11:30AM
614: Adventures in Formalization 1
615: Adventures in Formalization 2

Harvey Friedman