Proof checking Euclid

Tarski Formalization Project: The Master List

Wos and I formalized about 200 theorems from Szmielew's development of Tarski geometry, as presented in "the book", by which we mean Schwäbhauser, Szmielew, and Tarski's Metamathematische Methoden in der Geometrie. When working with two hundred files, the following concerns arose:

Possibly manual editing could introduce errors, leading possibly to bogus proofs.
We wanted to be able to perform experiments involving changes to many files at a time.

We addressed both of these concerns by creating the master list of our Tarski theorems. The master list is a list of data items, one for each theorem. We felt that the master list should be

Human readable, so that we could check whether the formalized theorems correspond to the contents of the book.
Machine readable, so that we could use computer programs to generate input files for different experiments, hopefully without introducing errors.

At first it may seem that these requirements conflict, but we think we have met both criteria by making the master list a text file (so it is human readable) containing PHP code (so it is machine-readable). The syntax requirements of PHP intrude only minimally on the human readability, mainly requiring us to write some extra occurrences of the word array, which are easily ignored. The master list itself is available on our Tools page; this page only explains it. The master list begins with class definitions of classes called Theorem, Definition, and Axiom. The class Theorem, for example, looks like this (but for simplicity we here omit the constructor function). (Those unfamiliar with PHP should just ignore {\em var} and the dollar signs.)

class Theorem
{ var $name;
  var $PositiveForm;     // array of clauses 
  var $NegatedForm;      // array of clauses
  var $Diagram;          // array of diagram equations
  var $SkolemSymbols = ""; // array of Skolem symbols introduced
  var $Cases = ""; // cases we used to split the problem, if any.
}

After that come arrays defining TarskiAxioms}, TarskiDefinitions, and TarskiTheorems. The TarskiTheorems array is the heart of the master list. It starts off like this:

$TarskiTheorems = array(
	new Theorem( "Satz2.1", 
		array("E(xa,xb,xa,xb)"), 
		array("-E(a,b,a,b)")
	),  
	new Theorem( "Satz2.2", 
		array("-E(xa,xb,xc,xd) | E(xc,xd,xa,xb)"),
		array("E(a,b,c,d)","-E(c,d,a,b)")
	),

The master list was prepared by hand, by the following method: First, we entered the negated form of a theorem, by copying it from list(sos) of the existing hand-crafted input file. It was, we realized, important that the constants in the master list have the same names as the constants in the corresponding existing proofs, to avoid incompatibilities when those proofs are used as hints. (Of course, that only matters for the theorems that cannot be proved without hints.)

Then, we computed (by hand) the positive form. Here constants such as $a$ were changed to variables such as $xa$. In some cases we had constants $cu$ or $cx$, where the book proof had $u$ or $x$; in computing the positive form these become $u$ or $x$ again, rather than $xcx$ or $xcu$. Although this was originally done by hand, we checked it (and other things about the master list) with a PHP program TestMasterList.php. What that program does is discussed here, which also discussed the various issues of correctness that must be addressed. The program itself can be found from our Tools page.

Another concern is whether each theorem in the master list corresponds to the version in the printed book. There are several considerations here:

First, Szmielew treated lines as sets of points, so her treatment is not strictly first order. We translated "line $L$'' to two points $p,q$ and the literal $p \neq q$, and $x \in L$ to $Col(p,q,x)$, where $Col$ means "collinear'' and is defined in terms of betweenness. The correctness issue has to be understood modulo this translation.

Second, as a result of that treatment of lines, some simple theorems had to be formulated in our development that are not in the book. For example, perpendicularity of lines becomes a 4-ary relation $perp(a,b,c,d)$, and we have to prove that, for example, $a$ and $b$ can be interchanged, and $c$ and $d$ can be interchanged, or both. This gives rise to some theorems that do not occur in the book. But for those theorems that do occur in the book, it can only be checked by hand that they correspond to the book. Since the Skolemization has been checked by machine, it is only necessary to check that the negative form corresponds to the book. There are only a few cases where this is at all problematic. Lemma~9.4, p.~68 is an example.

The question whether the formal theorem corresponds to the intended theorem arises also in using a proof-checker. Mathematics books written in the twentieth century do not contain machine-readable formulas, and even if they did, we would still need to know if those really represented Szmielew's intent. (There are a few typographical errors in Szmielew.) If we want to know if, for example, the proof that inner Pasch implies outer Pasch has really been formally proved, we will have to check by hand that one of the forms of the theorem in the master list is correct, and also that the axioms and definitions needed have been correctly formulated in the arrays TarskiAxioms and TarskiDefinitions. But we will not need to check that the intermediate theorems have been correctly formulated. Even if they do not correspond to the theorems in the book, they have been proved and they imply the theorem that inner Pasch implies outer Pasch!

Michael Beeson's Research

Tarski Formalization Project: The Master List