## Tarski Formalization Project: Testing The Master List
This page explains the "correctness issues" about the master list,
and how the program Here are the correctness issues for the entire project: - Is the positive form of each theorem in the master list really the correct Skolemization of the negative form?
- Does the diagram entry in the master list have the form of an equation with a new constant on the left? And on the right, does it mention only previously-introduced Skolem functions?
- Is each Skolem function introduced in exactly one theorem?
- Does the master list actually correspond to the statements of the theorems in the book?
- Are the input files being correctly generated?
- Do they all produce proofs?
- And of course: are the proofs produced by OTTER correct? (This is not a novel issue and will not be discussed here.)
Of these issues, the first four concern the master list, and are discussed on this page. Each theorem has both a
When we computed (by hand) the positive form, we followed rigid rules that were easy to program.
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$. Thus,
An issue in Skolemization was the order of arguments to Skolem functions. We carried out
Skolemization in two stages: first, we inserted the correct Skolem function symbol with no arguments.
For example,
Each theorem that introduces a Skolem function must introduce a `list(sos)` , they need to be of a syntactic
form that is known to be conservative, so that we do not introduce any bogus proofs via the diagram.
Adding equations defining a new constant is conservative, i.e., no new theorems can be
proved by adding such axioms. However, the meaning of "new constant" is not quite
as obvious as one might think. Consider, for example, the diagram for Satz 3.17.
There are two equations:
$$ e = ip(c,b1,a1,a,p)$$
$$ d = ip(c,b,a,b1,e)$$
The new constants are $d$ and $e$. The equation for $d$ has $e$ on the right, but
that is all right. What would be wrong is if the equation for $d$ had $d$ on the right,
or if the equation for $e$ had $d$ on the right and the equation for $d$ had $e$ on the right.
What we mean by "new constant" is, "constant not occurring in the theorem or the
right sides of the previous diagram equations."
The syntactic requirement checked by `TestMasterList` is that each diagram clause has the form of an
equation with a new constant on the left, in the precise sense defined above. `TestMasterList`
checks this condition as well. When we first ran this check, it exposed exactly one violation, in which
a diagram contained an illegal equation. (That was a harmless case, but still it showed that our program was
doing its job.)
The question, whether the diagram in the master list corresponds to the book's diagram, is not relevant. If you get a proof with any diagram whatsoever (meeting the above conditions) it is fine. Sometimes OTTER can find a proof if $a=b$, and also if $a \neq b$, but cannot find a proof with neither assumption.
Then it sometimes help to add $a=b \lor a \neq b$. After that one can usually remove the tautology, but sometimes not.
Therefore, in the master list there is a field in the We have observed other errors in the master list. For example, the members of various arrays are separated by commas at the end of lines. If one of those commas is accidentally a period intead of a comma, that is not a PHP error, because period concatenates strings. Then an incorrect string is written into the input file. The result might be an OTTER syntax error, but at least once, it was not. Which correctness condition was violated? It was the condition that the form of the theorem in the master list should match the form in the book. Suppose the error occurred in Theorem 5.1. It might be caught when Theorem 5.1 did not prove. But it could also happen that the bogus input file does produce a proof (but not of the real Theorem 5.1, only of the bogus Theorem 5.1). Then we would hope that the error would be caught when Theorem 5.2 or Theorem 5.3 does not prove. (That was how we found this error when it really happened.) But in general, there is no mechanical way to check that each theorem in the master list correctly expresses what Szmielew meant in writing the theorem in the book. However, if under those circumstances we did still find a proof of Theorem 5.3, the proof would be correct, because the "bogus" theorem 5.1 was still correctly proved and correctly used to prove Theorem 5.3. |