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:
After that come arrays defining TarskiAxioms},
TarskiDefinitions, and TarskiTheorems.
The TarskiTheorems array is the heart of the master list.
It starts off like this:
The master list was prepared by hand, by the following method:
First, we entered the negated form of a theorem, by copying
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