[FOM] 182:Ideas in Proof Checking 1

Harvey Friedman friedman at math.ohio-state.edu
Sat Jun 21 22:50:42 EDT 2003


I have made several postings concerning proof checking, 2:00PM 
6/17/03, 11:49PM 6/17/03, 1:04AM 6/21/03. It is now time to write 
about them more systematically.

The ideas in these postings can all be viewed as components, or 
auxiliary packages, for a UNIVERSAL MATHEMATICAL DATABASE (UMD).

1. I will give a particularly user friendly language for expressing 
mathematical statements, with a well defined semantics and 
completeness theorem. Something like this is to become the 
universally accepted gold standard for expressing mathematical 
statements. This will be a particularly user friendly flexible form 
of ZFC. It will support information retrieval.

2. The first part of UMD, called UMD1, is an hierarchical database of 
definitions within the framework of 1. These definitions must be 
adhered to by any contributor to any of the three main parts of UMD. 
There should be humans to referee entries into UMD1, to guarantee the 
quality of the entries. Humans should entertain challenges to 
entries, and remove them or modify them as appropriate. Of course, if 
an entry is modified or removed, then automatically all entries 
dependent on that entry are removed. Of course, removal of entries is 
generally traumatic, and is to be avoided.

Also there is the matter of the definitions being in legal form. Any 
acceptable entries must be simple and clear, and perhaps broken down 
into suitably small bite sizes, so that humans will regard as certain 
that in fact any accepted entries are in legal form. However, there 
is still probably a good use to be put to special purpose programs 
running on special purpose hardware, such as parsers of small 
formulas, that are also components in the core proof checker 
discussed in 5 below. E.g., have you ever left off a parenthesis?

3. UMD2 is a database of mathematical claims, which are author signed 
and time stamped. Claims can be retracted. The record of claims in 
force, and their authors and email addresses, are available, and also 
the historical record is available. Again, these are refereed by 
humans for their interest, and for their legality. See end of 2 
above. Standards are not meant to be high (for legality, the 
standards are infinite!).

4. I will give a crude complete set of axioms and rules for 1, in the 
style of a Hilbert system. These are very very very far from being 
directly useable by  humans. However, they are simple enough that 
soundness and completeness are humanly digestible. Soundness should 
be the subject of intense investigation with the aim of creating an 
appropriate kind of certainty surrounding any statement that, in 
fact, is provable using these axioms and rules for 1.

5. UMD3 is a database of mathematical claims that have been verified 
by UMD. A mathematical claim is strictly interpreted on the basis of 
UMD1. All verification takes place by submitting certain files to the 
core proof checker of UMD. The files must contain a purported proof 
in the sense of 4, appended by what is called "extreme annotation". 
The core proof checker is a special kind of low level automaton 
running on custom hardware. Its program is particularly simple and 
transparent, and there are humanly generated mathematical proofs that 
it is correct. Because of the simple nature of 4, the specs for the 
core proof checker are particularly clear to humans. The mathematical 
model of the custom hardware used by the core proof checker is clear, 
and the appropriate theorems about it have mathematical proofs. The 
core proof checker system taken as a whole, including the special 
purpose hardware, is verified by a mathematical proof.

6. It is understood that the purported proofs discussed in 5 start 
with the statement being proved. The definitional leadin must already 
exist in UMD1. The purported proof will import existing entries in 
UMD3 and existing entries in UMD1 by their official names.

7. Customization. (Not a high priority right now). Say you don't like 
the official notation in UMD1. You can fill out a change of notation 
form with UMD, and it will reassemble UMD1, UMD2, UMD3 based on your 
filled out form. You can even submit entries to UMD1, UMD2, UMD3, in 
your notation, appended with the change of notation form.

8. All of this is completely worthless in any practical sense unless 
systems are in place whereby users can in fact create completely 
correct proofs in the sense needed for 5, together with completely 
correct extreme annotations. This is the role of existing systems 
like Mizar and Isabelle, etc. Once UMD is in place, it will not be 
hard for Mizar and Isabelle to create an export program that conforms 
to UMD.

In 8, we are talking about

interactive proof checking systems.

Technically speaking, the official, final, gold standard, universally 
accepted, proof checking is done by the famed low level CORE PROOF 
CHECKER of the UMD, running on custom hardware, as discussed in 5. 
Note that this extra protocol, above and beyond what comes out of the 
interactive proof checking systems, is intended to enforce absolute 
certainty at a central location by a central authority.

I have some new(?) ideas about the design of interactive proof checkers.

The interactive proof checker is to adhere to the system T of 1 and 4 above.

There are two overarching strategies here. One has been discussed in 
11:49PM 6/17/03.

Specifically, the user is strongly urged to go for a LEMMA RICH 
DEVELOPMENT of mathematics. Generally, don't allow any one Lemma or 
Theorem to have any significant complexity. Rather, the significant 
ideas should be unpacked in the form of more Lemmas. This way, one 
has a completely modular context free setup with no side effects.

Setting up new Lemmas often involves the introduction of ad hoc 
definitions of functions (or relations and constants). These should 
be encouraged. In fact, they are usually quite natural, and provide 
sharper, more explicit forms of Lemmas and Theorems. They are often 
useful in other contexts.

However, there are situations where Lemma creation can be awkward, 
and obviously not worth the effort. This generally happens when a 
proof has a little complexity in it, but not more than that.

Under these circumstances, we would like to support human/machine 
interaction within the proof of a single statement.

Generally, we hope that our Lemmas will be trivial, in a sense to be 
made rigorous later, so that the machine does not need human help.

So we need to concentrate on how the interaction is going to take 
place when the proof is nontrivial, but sufficiently close to trivial 
that there is no reasonable Lemma(s) to be added.

We claim (feel) that this is a rather focused situation, where 
human/computer interaction is particularly feasible, pleasant, 
rewarding, satisfying, and easy.

If the proof was more trivial then the computer would find it. If the 
proof was less trivial then the human would gravitate towards Lemma 
enrichment.

NOTE: The user generally only submits the Theorem, together with the 
supporting documentation in the form of a proof in T appended with 
extreme annotation. In this case, any symbols introduced for the 
purposes of Lemmas toward the Theorem do not appear in the official 
record of the UMD, and therefore have a temporary status as far as 
the public is concerned. However, the user may with to make a series 
of submissions, which amount to submitting a series of Lemmas, one at 
a time, to the UMD, culminating with the Theorem. If these are all 
accepted, then these symbols introduced in order to support the Lemma 
enrichment - as well as the Lemmas themselves - become part of the 
official record of the UMD.

NOTE: All submissions to the UMD of statements are not only checked 
by the CORE PROOF CHECKER, but also are subject to human judgment as 
to their quality. Since the UMD does not publish proofs - or at least 
perhaps it publishes them in UMD4 and not UMD1,2,3 - the human 
judgment only concerns the interest of the statements being 
submitted. In UMD1-3, the proofs of these statements are utterly 
irrelevant, as long as they pass the CORE PROOF CHECKER.

In the next posting, we will discuss the design of an IPC 
(interactive proof checker). Specifically, our IPC will be driven by

1) a truly appropriate language for the formalization of mathematics;
2) model trees (Beth tableaux);
3) trivial proofs;
4) interaction protocols for constructing nontrivial proofs.

*********************************************

I use http://www.mathpreprints.com/math/Preprint/show/ for manuscripts with
proofs. Type Harvey Friedman in the window.
This is the 182nd 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-149 can be found at 
http://www.cs.nyu.edu/pipermail/fom/2003-May/006563.html  in the FOM 
archives, 5/8/03 8:46AM. Previous ones counting from #150 are:

150:Finite obstruction/statistics  8:55AM  6/1/02
151:Finite forms by bounding  4:35AM  6/5/02
152:sin  10:35PM  6/8/02
153:Large cardinals as general algebra  1:21PM  6/17/02
154:Orderings on theories  5:28AM  6/25/02
155:A way out  8/13/02  6:56PM
156:Societies  8/13/02  6:56PM
157:Finite Societies  8/13/02  6:56PM
158:Sentential Reflection  3/31/03  12:17AM
159.Elemental Sentential Reflection  3/31/03  12:17AM
160.Similar Subclasses  3/31/03  12:17AM
161:Restrictions and Extensions  3/31/03  12:18AM
162:Two Quantifier Blocks  3/31/03  12:28PM
163:Ouch!  4/20/03  3:08AM
164:Foundations with (almost) no axioms, 4/22/0  5:31PM
165:Incompleteness Reformulated  4/29/03  1:42PM
166:Clean Godel Incompleteness  5/6/03  11:06AM
167:Incompleteness Reformulated/More  5/6/03  11:57AM
168:Incompleteness Reformulated/Again 5/8/03  12:30PM
169:New PA Independence  5:11PM  8:35PM
170:New Borel Independence  5/18/03  11:53PM
171:Coordinate Free Borel Statements  5/22/03  2:27PM
172:Ordered Fields/Countable DST/PD/Large Cardinals  5/34/03  1:55AM
173:Borel/DST/PD  5/25/03  2:11AM
174:Directly Honest Second Incompleteness  6/3/03  1:39PM
175:Maximal Principle/Hilbert's Program  6/8/03  11:59PM
176:Count Arithmetic  6/10/03  8:54AM
177:Strict Reverse Mathematics 1  6/10/03  8:27PM
178:Diophantine Shift Sequences  6/14/03  6:34PM
179:Polynomial Shift Sequences/Correction  6/15/03  2:24PM
180:Provable Functions of PA  6/16/03  12:42AM
181:Strict Reverse Mathematics 2  6/19/03  2:06AM

Harvey Friedman


More information about the FOM mailing list