[FOM] 622: Adventures in Formalization 6

[Harvey Friedman]

I am thrilled to see so many of the heavyweights in Provers come in on
the FOM! I will soon get to directly commenting on some points being
made.

But now let me step back and talk about what could possibly be my role
in this discussion.

1. The impressive achievements in this area have and must come from a
long term effort over a long period of time, involving more or less
full time researchers and very substantial overall resources (although
less than say the development of jet fighters by the US Military
(smile)). Consequently, some fundamental decisions about how to
proceed must have been made a long time ago, and pretty much all of
the excitement is now directed to what is fairly readily implementable
based on current infrastructure. This of course is the way the main
line needs to progress.

2. As an outsider, I naturally am more engaged in going back to square
0 or square 0.1, and see if there are missed opportunities in several
senses.

i. Missed opportunities in terms of fundamental design, especially
that might impact ultimate Prover friendliness now and in the future.
ii. Missed opportunities in terms of new theory. What I see is a
limited but significant amount of significant theory already, and an
awful lot of heuristic engineering.
iii. I am particularly interested in the EASIEST, EARLIEST possible
places where complexity seems to set in - where imperfections become
apparent - where heuristics become seductive - where theory looks
ineffective.
iv. Specifically, I am particularly interested in the EASIEST,
EARLIEST possible places where the way mathematicians - or a certain
effective productive kind of mathematician - want to do things, think
things, write things, starts to DIFFER from the way Proving technology
works.
v. I am more concerned, as an outsider, with a much deeper
understanding of what is really going on just as things get
nontrivial, than I am in trying to effectively deal with incomparably
more involved things which are sitting way on top of a large
infrastructure of things that increasingly differ from ordinary
beautiful mathematical exposition.

I think PA(Q) is a good choice for the beginnings of this back to
basics approach, because it is both simple enough and complex enough
to get started. It lends itself naturally to crucially important
subsystems. E.g., pure order, Q,Z, or pure groups Q,Z, or pure ordered
groups, Q,Z, and so forth.

It seems like I already have a few non mainline ideas that already
suggests some theory. Of course, every idea I think I now have and
will have in this area has probably been thought of to some extent by
at least a few people among the many people in the area, and, perhaps
necessarily, been put at a lower or much lower level of priority than
other ideas.

1. Use of Free Logic. By the way, I believe that there is only one
really good Free Logic, and it has its very natural completeness
theorem. It is important to use the idea that a term is undefined if
some substorm is undefined, and NOT get into treating things like 0 x
(1/0) as 0, or as perhaps 1. Please resist that. 0 x (1/0) is
undefined, pure and simple. 1/0 - 1/0 is also undefined. AND, don't
try to solve this problem by creating a type. Also constants and
variables are automatically defined, and if an atomic formula is true
then its component terms must be defined. So 1/0 <= 1/0 is definitely
FALSE. You need far more compelling reasons to create a type.

2. The creative part of the manipulation of quantifiers is kind of fun
in a Prover setting, whereas quantifier free stuff is not fun in a
Prover setting. I envision the qf components as under the hood. The qf
components need to have (at least) two brands. One is intensely
mathematical domain specific stuff - e.g., linear arithmetic, real
arithmetic, boolean algebras, and so forth, including new stuff.
Another brand is general purpose qf stuff The two brands must
seamlessly interact, and as new domain specific qf packages come in,
they must be dropped into the soup seamlessly.

3. I want three components under the hood. There is the domain
specific SPPA(Q). There is the general purpose GPQF. Both of these two
are purely quantifier free. Then there is the SELF PROVER. This is
also under the hood, and uses HAVE/WANT unravelling, with the
quantifier free packages always on the lookout to satisfy WANTS using
the HAVES.

3. When the Self Prover gets stuck, and the user is ready to push
their fist through the computer screen, it is time to calm down and
give a HINT. The exact definitions of SELF PROVING, and HINTS need to
be carefully considered in the SIMPLEST of nontrivial situations.
HINTS appear nicely in the beautiful output text.

4. Unconventional Exploratory Methodology for uncovering new useful
decision procedures that are right on target. I believe in what
appears to be a switch in tactics here. OF COURSE, nothing I say is
really new, as indicated above, just new in HOW LOUD I SAY IT.

5. The decision procedures of the future for this REAL WORLD stuff, in
the face of staggering computational explosion, goes like this. One
develops, incrementally over time, various FINITE SPACES of assertions
that one does THEORY on. You can take the most HORRENDOUS of
UNDECIDABLE problems, and if you say that you want the instances to be
TINY, then you have a piece of HOPEFULLY DELICIOUS THEORY.

6. Predicate calculus horribly undecidable? Who cares?? Decide
validity for all tiny formulas. Second order predicate calculus even
more horribly undecidable??? Doesn't bother me. Decide validity for
all tiny formulas. ZFC set theory so horribly undecidable as to cause
you to faint? Not deterred. Decide all tiny formulas. E.g., look at
something like Three quantifier sentences, Fundamenta Mathematicae,
177 (2003), 213-240 - but only as an example, not necessarily to
implement. START BELIEVING that everything really basic is DECIDABLE
even if its UNDECIDABLE! Is there enuf theory here to do for the next
100,000 years? Not long enuf, clearly. The Sun will die before we
really understand this.

Recall in http://www.cs.nyu.edu/pipermail/fom/2015-September/019165.html
my suggestion about going beyond linear packages.

"1. Start easy. Look at all quantifier free formulas satisfying the
following conditions.
a. The total number of variables is at most 4.
b. Every term has at most two uses of multiplication and division
combined, and no exponentiation and no factorial. It can use any
constants, +,-,floor,ceiling.
The qf formula itself uses the connectives,
=,~,uparrow,downarrow,<,<=,>,>=,=,not=,Z.
2. Gradually go bigger than 1. How much and in what way depends on
what is involved in getting a good crushing software for 1."

What about GPQF = general purpose quantifier free package? We need
some systematically develop theory along the above lines.

PARAMETERS. Let X be a finite list of atomic formulas, using any
constants, relations, and functions, and k be a positive integer. The
smaller X,k are the better.

INVESTIGATE: Which propositional  formulas in quantifier free free
logic are valid in free logic, where all atomic formula components lie
in X, and there are at most k occurrences of atomic formula
components?

NOTE: Using X,k gives the theorist great control. But of course, one
wants to replace X by, say, all atomic formulas of tiny size, in given
constants, relations, and functions. Or you might want more control
than this, but saying things like "unseated", or controlling the kind
of nesting.

At this point, I want to least try to plunge into something trivial to
just beyond trivial, with Proving.

THEORY OF DIVISIBILITY IN PA(Q)
we have Q,Z

As part of the presentation of PA(Q), we have declared
p,q,r,s,t,x,y,z,w,u,v as ranging over Q, whereas a,b,c,d,e,i,j,k,m,n
range over Z. The convention on conventions is that you can use, e.g.,
p1 as a variant of the variable p.

DEFINITION 1. p|q if and only if (there exists n)(n*q = p).

THEOREM 1. p|0 defined if and only if p = 0.

We cannot rely purely on the qf package here since it is required to
treat (there exists n)(n*q = p) as a black box, totally indivisible.
So the SELF PROVER must kick in. It starts off, under the hood, with

HAVE (for all p,q)(p|q if and only if (there exists n)(n*q = p)).
WANT p|0 defined if and only if p = 0.

We now come to a fundamental design decision. Obviously this design
decision can be heuristically tweaked as implementers see fit.

Obviously the issue here is whether we want the Self Prover (component) to

i. Split up the Want into two Wants, each an implication, and then go
on unravelling these implications, then proceed with another fork in
the road. OR?
ii. Perform universal instantiation on the Have first.

Also, in either case, after i settles down, or immediately in ii,

iii. The Self Prover guesses the term substitutions: replace p by p
and replace q by 0. OR?
iv. The Self Prover has to stop since it is not allowed to make any
term substitutions except those prompted by the user in their HINTS.

We now take a BREAK from this greatly exciting moment, to watch a TV
commercial...

**********************************************************
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 622nd 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  9/14/15  1:43PM
615: Adventures in Formalization 2  9/14/15  1:44PM
616: Adventures in Formalization 3  9/14/15  1:45PM
617: Removing Connectives 1  9/115/15  7:47AM
618: Adventures in Formalization 4  9/15/15  3:07PM
619: Nonstandardism 1  9/17/15  9:57AM
620: Nonstandardism 2  9/18/15  2:12AM
621: Adventures in Formalization  5  9/18/15  12:54PM

Harvey Friedman