[FOM] 615: Adventures in Formalization 2

[Harvey Friedman]

1. Beautiful Formalization Project.
2. Self Proving.
3. Delicious Theoretical Issues..

1. BEAUTIFUL FORMALIZATION PROJECT.

In 614: Adventures in Formalization 1, I wrote

"Take a look at the statements of theorems in
http://www.cs.ru.nl/~freek/100/ They are all unconscionably ugly to
read and digest for a typical person outside the Theorem Proving
community. In the Theorem Proving community, they are probably looked
at as breathtaking works of art.

Now this is something that is a missed opportunity and CAN DEFINITELY
BE LARGELY FIXED. Is it worth fixing? ABSOLUTELY, but probably no one
in the Theorem Proving community thinks it is worth their time to fix
it, and should have a low priority. Conventional wisdom is often very
wrong."

Now if you look further into links on http://www.cs.ru.nl/~freek/100/
you will see the actual formalized proofs. These are so disgusting
that a 1/2 second glance at them would make anyone outside the Theorem
Prover community vow to never experience such a traumatic experience
the rest of their lives, and would much prefer root canal in their
dentist office. Of course, people in the Theorem Proving community
think that these proofs are masterpieces of art, and can't wait to
generate and take a hard look at the next one coming down the pike.

The Beautiful Formalization Project is designed to address this issue.
I doubt if anyone in the Theorem Proving community thinks of this as a
high priority, as expected.

But the tools needed to do the BFP have a lot of overlap with things
that the Theorem Proving community grapples with all the time. So
there is destined to be a lot of overlap.

Some GOLD STANDARDS for BFP:

1. Choose carefully three undergraduate texts. One on elementary set
theory. One on elementary number theory (non analytic). One on graph
theory.
2. Design a language for presenting proofs that is general purpose
enough to be used in all three of these contexts.
3. The language for presenting proofs should also be accompanied by
software implementing certain algorithms. This is explained carefully
below.
4. The three texts are written in the language, with ABSOLUTELY
RIGOROUS MACHINE CHECKABLE PROOFS.
5. The resulting three texts are viewed as BEAUTIFUL by all readers.
6. Brilliant naive young people cannot tell that these were created in
the Beautiful Formalization Project.

With regard to 3. All mathematicians have to stop their expositions as
triviality sets in. Otherwise, they will get nothing done in a
reasonable amount of time. The Theorem Prover community lives off of
just this. The Proof Assistant is supposed to take care of all
trivialities. Of course, what we find is that it never takes care of
nearly enough trivialities, and more power is constantly added to
overcome these disappointments.

In the course of adding all of this new power, the Prover starts to
take on a black box character where the user doesn't really have much
of a clear idea as to just what is in that black box.

This is just fine and great for the main stated purpose of the Theorem
Provers. The more ABSOLUTELY CORRECT power the better!

But for the BFP, we really want the user to have great control on what
the computer is filling in. Ideally, we want a ROBUST measure of the
levels of triviality. This is also going to be important when we get
into the serious investigation as to the real nature of actual
mathematical proofs.

2. SELF PROVING.

Instead of trivialities, it is preferable to speak of ISELF PROVING
statements. Now this SELF PROVING concept is extremely crucial for the
BFP.

To clear the air, because of the Goedel Completeness Theorem and
related reasons, we can view EVERYTHING as SELF PROVING. That is,
given an unlimited amount of computer resources, we will prove it, if
it is provable. In predicate logic, it is provable if it is merely
valid.

So the right way to look at this is through more nuanced notions of
SELF PROVING. And also LEVELS OF SELF PROVING.

It is of course easiest to see just what I am talking about in the
classical propositional calculus. This is of course much too babyish
to really be representative of the real issues. After all, any real
world case coming up in proving real world mathematics (I am not
talking about verifying engineering systems), has not many variables
and can be clobbered by your old phone in a millisecond via truth
tables.

And furthermore, let's just talk about only implication. I like the
HAVE/WANT calculus. I will be talking about this much later, and now
is not the time. I just want to give a few examples of SELF PROVING.

Here are 6 toy theorems in implicational propositional calculus.

1. WANT p --> p.
2. WANT p --> (q --> p).
3. HAVE p --> q, q --> r. WANT p --> r.
4. HAVE p --> (q --> r). WANT (p --> q) --> (p --> r).
5. WANT (p --> (q --> r)) --> (q --> (p --> r).
6. WANT ((p --> q) --> p) --> p.

1. WANT p --> p.
HAVE p. WANT p.

2. WANT p --> (q --> p).
HAVE p. WANT q --> p.
HAVE q. WANT p.

The Have's cumulate and the Want's override.

3. HAVE p --> q, q --> r. WANT p --> r.
HAVE p --> q, q --> r, p. WANT r.
HAVE q.
HAVE r.

When we don't write a Want clause, we mean that the last want clause
written is operative.

4. HAVE p --> (q --> r). WANT (p --> q) --> (p --> r).
HAVE p --> q. WANT p --> r.
HAVE p. WANT r.
HAVE q --> r.
HAVE q.
HAVE r.

5. WANT (p --> (q --> r)) --> (q --> (p --> r)).
HAVE p --> (q --> r). WANT (q --> (p --> r).
HAVE q. WANT p --> r.
HAVE p. WANT r.
HAVE q --> r.
HAVE r.

6. WANT ((p --> q) --> p) --> p.
HAVE (p --> q) --> p. WANT p.
OUCH!

Now I am not talking about building a SAT solver, or being powerful. I
am just illustrating a very restricted form of SELF PROVING.

Now obviously we can imagine being free to add TACTICS. I.e., user
specified tactics, so that even more is SELF PROVING. An important
tactic is case splitting. But note that this is going outside the
purely implicational fragment.

6. WANT ((p --> q) --> p) --> p.
HAVE (p --> q) --> p. WANT p.
case 1. HAVE p.
case 2. HAVE not p.
HAVE not(p --> q).
HAVE p.

So what I have in mind is this. In the first 5 examples, you can write
SELF PROVING. You don't give any proof. The computer algorithm
associated with the text verifies this. In example 6, you can write
"SPLIT ON p".

DO NOT TAKE THIS literally. This is just a prototype of what I have in
mind, and the exact form that I will arrive at for this approach is
way unclear at the moment.

3. DELICIOUS THEORETICAL ISSUES.

A naive person may think that if you have a beautiful mathematical
statement, and you can give a proof of it in a generous beautiful
formalism, then you should be able to prove it using ideas that are
close to, or in and around, that given beautiful statement.

Experienced people of course know that for anything but the most
trivial things, you are going to be going well beyond the beautiful
statement being proved. This phenomena of NON SELF CONTAINMENT is
pervasive at many many different levels. It is of course, a candidate
for the most singularly important and interesting feature of
mathematical thought of the last several thousand years.

But let's slow down and discuss this systematically a bit, starting at
very low levels.

We have seen that in our 6 examples, we really where self contained.
EXCEPT that there was a small hint of non self containment with
example 6. It's not the choice of p to split on so much as the use of
negation, when we are just talking about implication only!

In fact, in a sense, we know that you can't avoid use of negation
here. Because if you do avoid it, you are stuck with constructive
proofs (needs to be verified in the right generality), and we know
that example 6 cannot be proved constructively.

On the other hand, it is well known that if we just add example 6 as a
scheme to our toolbox, we can stay within implication. HOWEVER, we may
be given up any reasonable kind of SELF CONTAINMENT, where we are
proving purely implicational statements using implicational statements
that are not in and around the given one.

So it is natural to look for a short - if not beautiful - example with
just implication, where any reasonable proof has seriously foreign
elements in it? Even mildly so? I'm not sure that this is well
understood. Here I am not really talking about the full blown
exponential blowup issues related to versions of P not= NP. I'm
talking about much more mild stuff here.

Moving up to intuitionsitic and classical propositional calculus with
all of the connectives, we would like to have some small examples
where any proof even close to being self contained is substantially
longer than some non self contained proof. Of course, all valid
statements in classical propositional calculus have reasonably self
contained proofs by case splitting on all of the atoms. But that
generally is exponential. It's quite long if there are say only 4
atoms. Is there a reasonably short 4 atom example where you provably
get huge mileage by going considerably beyond the given 4 atom example
in its proof?

By the way, in the intuitionistic proppositional calculus, how big and
what does it look like - the corresponding default self contained
proof? How does it compare in size to the one for classical
propositional calculus?

Now let's move on to FOL = first order logic. Here a lot is known at
the theoretical level. The cut elimination theorem tells us that we
can always be self contained in a very precise sense. This is the
notion of subformula. But a word of caution: subformulas allow for
term substitution. So even if there are no constants or functions, we
can get a proliferation of variables.

But the cut elimination theorem involves iterated exponentiation that
is not removable. In fact, there are some reasonably natural examples
of super exponential blowup. In a nutshell, it is the single instance
of induction with respect to a unary predicate symbol P, up to
2^2^,...^2, sitting on top of a little bit of infrastructure
surrounding base 2 exponentiation. If you just want to use j
alternations of quantifiers, and the exponential stack is of height n,
then you are stuck giving a proof of length at least roughly 2^2^...^2
of height n-j, even if cuts are allowed. NOTE THAT THIS FORMULATION OF
THE WELL KNOWN RESULT DOES NOT INVOLVE CUTS.

Now here is the issue. In the course of REAL WORLD theorem proving, we
come across endless examples of first order validities (or
equivalently, valid implications). More about that later.

We really have the feeling that even with these validities, frequently
the proof that we have in mind, and the proof that the Prover is
helping us generate, DOES INVOLVE at least slightly foreign stuff. Can
we PROVE that there must be foreign stuff, or else we are at least
going to get some significant blowup?

Of course, our Provers are generating a lot of validities. Because
typically they go into the libraries either directed by the user, or
on their own, enough to get a validity going, and THEN crush the
validity by special subtools. I know this spills over into some
interesting subtools like Resolution Provers. So maybe a more direct
supply of candidates situations where we have real world validities
proved with foreign stuff would be Resolution Provers or other kinds
of FOL provers. We can look there to see if we can prove that the
foreign elements is necessary to avoid at least some kind of blowups.

Now, moving out of the FOL realm, we come to the totally pervasive
situation of where we want to prove X, and we find ourselves citing
stuff from libraries and of course axioms as well. In this case, we
expect a much stronger theoretical result. That if we don't go quite
foreign, we won't be able to prove X at all, no matter how big a proof
we are willing to tolerate!!

Yes, if we go quite foreign, we have a nice proof. If we don't go
quite foreign, we have NO PROOF AT ALL.

I don't think this has been looked at much, or at least
systematically, even for nice versions of PA or EFA. This is a form of
Micro Incompleteness Investigation which probably will take 1000 years
to understand well. I think I could generate quickly thousands of
DELICIOUS problems of this character, just for EFA.

************************************************************
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

Harvey Friedman