[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