[FOM] 614: Adventures in Formalization 1

[Harvey Friedman]

1. General Remarks about Theorem Proving.
2. Theorem Statements.
3. Universal Gold Standards.
3a. Free Variable Formulations.
3b. Abbreviation Power.
4. Verifying Translations.
5. Verifying Proof Files.

1. GENERAL REMARKS ABOUT THEOREM PROVING.

The development of absolutely rigorous mathematical proofs, or Theorem
Proving, or Proof Assistants, and so forth, is a highly active and
highly impressive field at the interface between logic and computer
science. Yet there are a number of missed opportunities and challenges
that are already apparent. In this series within my numbered postings,
I hope to seize on some of these missed opportunities, which, in some
cases, come out of criticism of the way things are (being) done (now).

Before I begin, I want to highly recommend

http://www.cs.ru.nl/~freek/comparison/comparison.pdf
http://www.cs.ru.nl/~freek/100/

This gives you an idea and feel for just how impressive and highly
developed this field is. Probably most mathematicians have some deep
down to earth belief that serious mathematics is not really capable of
being formalized with a fixed set of axioms and rules. Many of these
people do not really properly internalize ZFC or even ZC or PA. And
many that do internalize, nevertheless feel that serious mathematics
is just too involved for there to be any construction of absolutely
rigorous proofs.

The two references above show just how wrong the typical skeptical
mathematician has been.

There is another group of doubters who have a more nuanced position.
They acknowledge that this is being done, and probably that it can be
done for even deeper mathematical theorems. However, they doubt the
interest and/or importance of doing this.

These more nuanced doubters are also wrong but in a more subtle way.
First of all, the mere fact that traditional mathematicians have
doubted that it can be done at all for serious mathematics is itself a
reason to accomplish this as a kind of proof of concept for
foundations of mathematics. Can absolute rigor actually have an actual
physical existence? Secondly, and this spills over into the category
of missed opportunities, this provides a tremendous body of data as to
the actual structure of actual mathematical proofs - ok, or at least
those actual mathematical proofs that come out of the process. I would
be shocked if significant and highly surprising features of actual
mathematical proofs didn't emerge this Century from this work.
Thirdly, the actual construction of absolutely rigorous proofs
requires, on a practical level, or will require as it becomes more
powerful, an extremely interesting array of new decision procedures
applying to all sorts of interesting everyday mathematical
environments. Fourthly, there is a major need for the verification of
hardware and software systems, and these require that mathematical
statements be proved with absolute rigor. So Proof Assistants will
become a vital tool as formal verification of hardware/software starts
really taking off this Century.

So now I am now temporarily finished with being so positive.

Now for the negative. The Theorem Proving infrastructure is, as far as
I can tell, not close to ABSOLUTE INFALLIBILITY. Or at least not
nearly as close to it as we can make it. And making it much closer is
a missed opportunity that is going to be very interesting,
philosophically, foundationally, practically, and theoretically, and
even emotionally.

Below I want to take up the ingredients or some of the ingredients
needed to move to ABSOLUTE INFALLIBILITY. Now people think that this
is not achievable, and they have a good case for that. So we can speak
of moving closer to ABSOLUTE INFALLIBILITY. Far closer than we are
now.

2. THEOREM STATEMENTS.

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.

Part of the reason it should be of a very high priority is that it
spills over into another NASTY issue.

IN WHAT SENSE are we constructing absolutely rigorous proofs of
mathematical theorems WHEN there is an issue constantly surfacing
about whether or not the ACTUAL STATEMENT of the theorems to be proved
is a CORRECT STATEMENT of the theorems to be proved??? The phrase "bug
in the statement of the theorem" actually has been known to be heard
(smile).

It doesn't help matters if nobody (outside the Theorem Prover
community) can, or can even want to, read the actual statements.

REST ASSURED, this can be largely fixed. I started up an effort along
these lines, furthered by others, and I think now things have gone
somewhat further, but I don't know the latest:

(with S. Kieffer, J. Avigad), A language for mathematical knowledge
management, in: Computer Reconstruction of the Body of Mathematics,
ed. A. Grabowski, A. Naumowicz, Studies in Logic, Grammar and
Rhetoric, p. 51-66, 2009.

In this series of postings on Formalization, I will be actually
constructing some mathematical proofs by hand in a nonexistent dream
system, where everything is EXTREMELY PLEASANT to read, and so I will
be presenting FRIENDLY  LANGUAGES.

3. UNIVERSAL GOLD STANDARDS.

So what axioms/rules do we want our proofs to live in? We must make a
distinction here of the utmost importance.

a. The axioms/rules used interactively between the human and the Proof
Assistant.
b. The ultimate Gold Standard axioms/rules for the ultimate INFALLIBILITY STAMP.

Everybody is free to choose their a) according to taste, judgement,
and prejudice. But there must be a meeting of minds as to some b).

THIS IS NOT DRACONIAN. Rebel groups can be easily accommodated. Yes,
we need the rebels to conform to our b). I.e., to export for checking
that we have a file for b). IN EXCHANGE, we can graciously offer
resources to go the other way around, so that the rebels can pretend
to be in charge.

So the issue is really b).

I envision a large system and various important weaker subsystems.
Since to much math can be done in systems much weaker than ZFC, this
should be reflected in the choice of Gold Standards. There should be a
few major Gold Standards ranging from Finite Set Theory to full blown
ZFC.

To simplify the discussion, I will only be talking about a Gold
Standard which is a ZFC variant.

What should the criteria be for choosing the Gold Standard for
mathematical proofs?

i. It has to serve as a Gold Standard in the following sense. Provers
are required to submit files for Central Authority certification, and
what is being certified is that the file constitutes an absolutely
correct proof in the Gold Standard system - generally together with
other helpful data. The other helpful data is supplied in order to
make the program that verifies that it is indeed a proof in the Gold
Standard easier and simpler to write, and easier and simpler to
execute, and easier and simpler to verify that this writing and
execute is infallible, and so forth.

ii. It has to be set up so as to maximize its intrinsic infallibility.
The usual way of presenting ZFC has a number of issues. One is that it
is almost never done. The predicate calculus part is notoriously
difficult to get just right, with the free/bound variable clashes and
the like. Maybe the chances that experts screw up the axiomatization
of ZFC in the usual form, is something like 2^-100, which is far too
high an error rate.

iii. There has to, or should be some philosophy done as to why and
what it means to say that ZFC and/or fragments are infallible.

Each of i,ii,iii are subjects onto themselves, with plenty of missed
opportunities.

3a. FREE VARIABLE FORMULATIONS.

With regard to i. Much more reliable in my mind than the usual ZFC
axioms as presented, is the FREE VARIABLE formulation of ZFC. There is
epsilon, equality, and function symbols associated with
extensionality, pairing, union, power set, infinity, foundation,
choice. With Replacement, there is first a handful of general purpose
Skolem functions.

There seems to be a missing subject of GENERAL PURPOSE SKOLEM
FUNCTIONS. They are small in number, have very simple axioms
indicating what they do, and they provably generate Skolem functions
for all first order formulas (even those that mention the Skolem
functions themselves), via composition only. And THEN Replacement is
still a scheme, involving all terms.

I prefer not to use NBG and adhere to ZFC for this purpose - in fact
free variable ZFC for this purpose. I don't think enough is to be
gained by going to variables over classes, to be worth its
repercussions for what I am trying to do here.

I want to EMPHASIZE that this basement is INVISIBLE to any human
involved in Theorem Proving.

Now let's focus on FVZFC = free variable ZFC, Free variable logic is
obviously much more basic than full logic. Of course, the key
ingredient is TERM SUBSTITUTION.

TERM SUBSTITUTION is the DNA of mathematical thought. Everything
arises from it (along with =).

3b. ABBREVIATION POWER.

Now requiring all Certified Installations to conform to FVZFC is not
going to work. The problem is that we desperately need to use
ABBREVIATION POWER in order to avoid blowups. So we really need to use
FVAPZFC = free variable abbreviation power ZFC. We are allowed to
define, or nondeterministically specify, new function symbols by free
variable statements.

CAUTION. I am not saying that we want humans to be interacting with
their computer in a free variable way. I am simply talking about what
is to be going on in the basement of the Central Authority
Headquarters.

4. VERIFYING TRANSLATIONS.

At this point, we need the first of MANY translation modules. Here is
a list of ones, some of which are crucially needed, but others are a
very good idea to have anyway. And maybe will turn out to be crucial.

i. Going from FVAPZFC to FVZFC.
2. Going from FVZFC to ZFC.
3. Going from ZFC to FVAPZFC.

We should have a general format for and theory of SYSTEM TRANSLATION.
We need to address the issue of INFALLIBILITY here, and the
INFALLIBILITY of code used to implement these translations. We need to
push this little corner of things, comparatively unproblematic, down
to as close as we can to ABSOLUTE INFALLIBILITY. More generally,
elemental, in your face, finite string manipulation theory. We
probably need to address also the hardware implementation of this,
including what we do about cosmic rays?

SAMPLE ISSUE: how do we implement term substitution (the DNA), and
what kind of INFALLIBILITY can we achieve in doing so?

5. VERIFYING PROOF FILES.

We now come to the interaction between the Certified Installation
Theorem Provers and the Central Authority.

The Provers are to submit

a. The statement of the Theorem.
b. A file with a proof of the Theorem in FVAPZFC.
c. Another larger file with an annotated proof of the Theorem in FVAPZFC.

All of these three MUST adhere to the universally accepted GOOD FORM.

The purpose of c) with its annotations, in universally accepted form,
is to facilitate and improve the INFALLIBILITY of the Central
Authorities' checking process.

In general, these annotations consist of pointers so that the Central
Authority checker does not have to do any or much search. Obviously,
we cannot require annotations that cause significant blowup.

We have now, another little subject. Let's say we want to check that a
file meets certain criteria like being a proof in FVAPZFC. That is a
certain kind of specification. What is a best or really good way of
annotating it so as to greatly simplify the implementation of any
checker checking that it meets the criteria in question? There seem to
be two ways to go. One is to put a lot of important and useful
pointers all over the place. Another is to make copies of certain
things and put them in strategic positions. We want simpler kinds of
checkers in order to make it easier to argue that they are INFALLIBLY
EXECUTED. Remember, this is not just a matter of software, but
includes hardware infallibility issues as well.

E.g., it is far simpler to check that a file has an even number of
characters, as, e.g., having no two substrings of length 100 that are
the same - even though we know a lot about good efficient reliable
ways of checking for either one.

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

Harvey Friedman