Calculational proof design; an experiment

Calculational proof design; an experiment

In this note, all variables are -at least to begin with- of the same, as yet anonymous type. There are two predicates, tri and col on unordered triples, i.e. for all $\alpha ,\beta ,\gamma$

$$ \operatorname {t r i}. \alpha . \beta . \gamma \equiv \operatorname {t r i}. \beta . \gamma . \alpha $$

$$ t r i. \alpha . \beta . \gamma = t r i. \gamma . \beta . \alpha $$

$$ c o l. \alpha . \beta . \gamma \equiv c o l. \beta . \gamma . \alpha $$

$$ c o l. \alpha . \beta . \gamma \equiv c o l. \gamma . \beta . \alpha $$

These predicates satisfy a few laws, which I shall introduce when I need them. (Whether these laws are axioms or theorems is currently irrelevant.)

We would like to design a proof of the Theorem Let $p,q,r,s$ satisfy

(0) tri.p.q.r $\wedge$ triq.r.s $\wedge$ tri.r.s.p $\wedge$ tri.s.p.q; let $x,y,z$ satisfy in some order equations

(1) $\alpha : \operatorname{col}.p,q.\alpha \land \operatorname{col}.r.s.\alpha$

$$ \begin{array}{l} \alpha : c o l. p. r. \alpha \wedge c o l. q. s. \alpha \ \alpha : \operatorname {c o l}. p. s. \alpha \wedge \operatorname {c o l}. q. r. \alpha \ \end{array} $$

then tri.x.y.z holds (End of Theorem.)

Remark Since the demonstrandum $x,y,z$ is symmetric in $x,y,z$ ,we can postpone the choice which of these three solves which of the equations (1). (End of Remark.)

So we need a law that allows us to conclude tri, and I give you one such law: for all $\alpha ,\beta ,\gamma ,\delta$

(2) $\alpha \neq \beta \land \operatorname{col.}\alpha .\beta .\gamma \land \operatorname{tri.}\alpha .\gamma .\delta \Rightarrow \operatorname{tri.}\alpha .\beta .\delta$

Remark Although col and tri are predicates on unordered triples, I found it - in order to come to grips with the "symbol dynamics" essential to choose carefully how to formulate (2), and to stick to that formulation. Without that discipline, I got totally confused. Notice (i) that it is the left-most argument $\alpha$ that occurs in all 4 atoms, and (ii) that the occurrence of $\beta ,\gamma ,\delta$ in the last 3 atoms reflects a transitivity structure. (End of Remark.)

The first thing we are going to do is to design our appeals to (2), which allows us to conclude one tri from another. In order to carry out our analysis, we call $p,q,r,s$ our "sources" and $x,y,z$ our "targets" - in this context

meaningless identifiers

We now note that

(i) our demonstrandum is a tri on 3 targets (type TTT)

(ii) we are only given -see (o)- tri-atoms on 3 sources (type Sss)

(iii) the two tri-atoms in (antecedent and consequent of) (2) have 2 arguments common.

These observations imply that we need intermediate tri-atoms of types TSS and TTS, i.e. at least three appeals to (2).

An appeal to (2) with tri. $\alpha .\beta .\delta$ of type TTT and tri. $\alpha .\gamma .\delta$ of type TST would have in the antecedent col. $\alpha .\beta .\gamma$ of type TTS,whereas the only given col- atoms -see (1)- are of type SST. That is a problem,but since we are given no way of concluding a col-atom ,the only thing we can do is to postulate it.To minimize our commitment,we introduce a new variable t,which could be neither source nor target. Instantiating

(2) with

(3) $\alpha ,\beta ,\gamma ,\delta \mathrel{\text{:=}} x,y,t,z$

we get

(4) $x \neq y \land \operatorname{col}x \cdot y.t \land \operatorname{tri}x \cdot t.z \Rightarrow \operatorname{tri}x \cdot y.z$

In instantiation (3), component $\gamma : t$ is essential; how $x,y,z$ have been distributed over $x,\beta ,\delta$ is irrelevant.

Our next appeal to (2) has to conclude tri.x.t.z, and in view of our goal of using (0), tri.x.y.s should be of type TTS. This settles β:=t and, for our source choosing p say, γ:=p. For the other two, we have to choose between α,δ := x,z and α,δ:=z,x. We choose the latter and shall say in a moment why - and obtain with instantia. tion from (2)

(5) $\alpha ,\beta ,\gamma ,\delta \mathrel{\text{:=}} 2,t,p,x$ (6) $2 \neq t \land \operatorname{col}z.t.p \land \operatorname{tri}.z.p.x \Rightarrow \operatorname{tri}.z.t.x$ .

Remark At this stage, the choice between $\alpha ,\delta \mathrel{\text{:=}} x,z$ and $\alpha ,\delta \mathrel{\text{:=}} z,x$ is guided by the following consideration. With the choice made we must hope -see (2) and (4)- that auxiliary

(7) $\operatorname{col.}x \cdot y \cdot t \land \operatorname{col.}z \cdot t \cdot p\;,\;$

a 5-variable relation , apart from the spec- cif variables involved of the familiar shape of equations (1).Thanks to laws not men

tioned yet, the rejected alternative has unac- ceptable consequences.

For the instantiation of $\gamma$ with a source we were free to select $p$ ; note that (0) and (1) are symmetric in $p,q,r,s$ . (End of Remark)

Our third appeal to (2) should conclude tri. z.p.x and now tri.a.y.s hould be of type TSS , i.e. y has to be instantiated with a next source -say q: we are free- and β with a target, more precisely with either x or z . In view of (1), we want col.a.y to be of type SST, and with β a target, we conclude that α should be instantiated with source p. We hope that the choice between β,δ:=z,x and β,δ :=x,z does not matter, and with instantiation

(8) $\alpha ,\beta ,\gamma ,\delta \mathrel{\text{:=}} p,x,q,z$

we obtain from (2)

(9) $p \neq 2 \land \operatorname{col}.p \cdot x \cdot q \land \operatorname{tri}.p \cdot q \cdot 2 \Rightarrow \operatorname{tri}.p \cdot x \cdot z$

The occurrence of col.p.x.q makes us decide that $x$ satisfy the first equation of (1), hence

(10) col. $p,q$ . $x\; \land \;$ col. $r,s$ . $x$

Our final appeal to (2) should conclude tri. p. q. z from , say tri. p. q. r . For the instantiation that settles $\beta ,\gamma \mathrel{\text{:=}} 2,\gamma$ ; we still have to choose between $\alpha ,\delta \mathrel{\text{:=}} p,q$ and $\alpha ,\delta \mathrel{\text{:=}} q,p$ . We hope that the choice does not matter and take the latter: with the initiation

(1) $\alpha ,\beta ,\gamma ,\delta \mathrel{\text{:=}} q,z,r,p$

we obtain from (2)

(12) $q \neq z \land \operatorname{col}.q \cdot z.r \land \operatorname{tri}.q \cdot r.p \Rightarrow \operatorname{tri}.q \cdot z.p,$

and the occurrence of col. q. z. r makes us decide that 2 satisfies the third equation of (1); in summary (1) is replaced by - see (10)-

(13) col. $p,q$ . $x\; \land \;$ col. $r,s$ . $x$

col. p. r. y A col. q. s. y

col. p. s. z A col. q. r. z

Having dealt with the trin-atoms and

$x \neq y\;\left( {\text{from}\left( 4\right) }\right)$ $2 \neq t$ (from (6)) $p \neq 2\;$ (from (9)) $\cdots \neq 2$ (from (12))

but, so far, we have no way of concluding

a difference. Fortunately, there is a law allowing us to do so:

$$ (1 4) \quad \operatorname {c o l.} \alpha . \beta . \gamma \wedge \operatorname {t r i.} \beta . \gamma . \delta \Rightarrow \alpha \neq \delta $$

We deal with the last two remaining obligations first:

$$ \begin{array}{l} \bullet \quad q \neq 2 \ \Leftrightarrow {1 4) w i t h \alpha , \beta , \gamma , \delta := z, s, p, q } \ c o l. z. s. p \wedge f r i. s. p. q \ = {(1 3); (0) } \ t r u e \ \end{array} $$

$$ \begin{array}{l} \cdot \quad p \neq 2 \ \Leftrightarrow {(\alpha , \beta , r, \delta) := z, q, r, p } \ \operatorname {c o l}. z. q. r \wedge \operatorname {t r i}. q. r. p \ = {(1 3); (0) } \ \end{array} $$

$$ t r u e $$

The above are two instances of the general theorem that any source differs from any target.

Now we deal with the first of the re- maining obligations

$$ \begin{array}{l} \bullet \quad x \neq y \ \Leftrightarrow {(\alpha , \beta , \gamma , \delta) := x, p, q, y } \ c o l. x. p. q \wedge t r i. p. q. y \ = {1 3 } \ t r i. p. y. q \ \end{array} $$

[\left( 2\right) \text{with}\alpha ,\beta ,r,\delta \mathrel{\text{:=}} p,y,r,q} ]

$p \neq y \land \operatorname{col}p.y.r \land \operatorname{tri}p.r.q$

$= { {any}\;{source}\;{differs}\;{from}\;{any}\;{target};$ $\left( {13}\right) ;\left( 0\right) }$

true

But with our last proof obligation, viz. $z \neq t$ ,we run into trouble. What we need is the existence of a $t$ satis- flying - see (7)

(15) $2 \neq t \land \operatorname{col}x.y.t \land \operatorname{col}z.t.p$

Suppose we had an existence proof of a $t$ satisfying (7). To satisfy (15), we would then have to show that $t = 2$ does not satisfy (7), i.e.

$n\left( {\operatorname{col}x.y.z\; \land \;\operatorname{col}z.z.p}\right)$

the above, however, reduces to our original demonstrum

tri. $x.y.z$

thanks two further laws

(16) col. $\alpha .\alpha .\beta$

(17) col. $\alpha .\beta .\gamma \neq$ tri. $\alpha .\beta .\gamma$

The type of axiom that is missing postulates

the existence of solutions that differ from parameters occurring in the equations. In what I saw (Pasch, Peano, Veblen, Hilbert), such existence axioms do occur.

All this has been triggered by the study of (the beginnings of) axiomatizations of plane geometry - in Hilbert's "Foundations of Geometry" and Coxeter's "Introduction to Geometry". The proofs I encountered were verbal and pictorial and often I could not convince myself that the arguments were complete. I can now give you a picture illustrating the above argument

with "col" meaning "collinear" and "tri" standing for "triangular". But you must take my word for it that this picture was only drawn after the above proofs were designed: the whole point of the experiment was to try out the feasibility of proof design without leaning on the pictorial crutch.

The trouble with pictures, of course, is that

This is "the same picture" as the previous one!

Remark The trouble could really be serious. In the existence axiomatizations I saw, the notion "between" plays a central role. In the one picture t lies between x and y , in the other it does not. (End of Remark

I was also interested in the calculational consequences of the fact that, while having variables of only one type "points", say $-$ I had no expressions of that type. After the fact, I think that the consequences are minor.

Before I started on this, I did not know which predicates to use; the decision to introduce both col and tri helped a lot.

Though (17) clearly states that one of the two predicates is superfluous, we leave open which one. It was also a surprise to see that (17) played no role beyond making law (14) a derivable theorem:

$$ \begin{array}{l} \operatorname {c o l}. \alpha . \beta . \gamma \wedge \operatorname {t r i}. \beta . \gamma . \delta \ \Rightarrow \quad {\mathrm {p r e d . c a l c .} } \ c o l. \alpha . \beta . \gamma \equiv t r i. \beta . \gamma . \delta \ = {1 7 } \ \operatorname {c o l}. \alpha . \beta . \gamma \neq \operatorname {c o l}. \delta . \beta . \gamma \ \Rightarrow {Z i n b i e l } \ \alpha \neq \delta \ \end{array} $$

I have been wondering whether, instead of what we have done, these predicates should rather be defined on unordered triples or, even more general, on sets. Thanks to this exercise I know that those alternatives deserve to be rejected: in law (2) - a linchpin of the whole argument - the consequent is symmetric in $\alpha, \beta, \delta$ , but the antecedent is not. Finding the proper instantiation of (2) was, in fact, in each appeal to it the major and not trivial decision.

Nuenen, 21 December 1995

Prof. Dr. Edsger W. Dyrkstra Department of Computer Sciences The University of Texas at Austin Austin, TX 78712-1188, USA