## 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 - 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.
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.
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.)
After that come arrays defining
The master list was prepared by hand, by the following method:
First, we entered the negated form of a theorem, by copying
it from
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 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 |