Inspired by Peter Auer’s proof

Inspired by Peter Auer's proof

When proofs are constructed from strengthening (or weakening) transformations common form of the proof of [R] show

(0) $\left\lbrack {R \Leftarrow \text{true}}\right\rbrack$ or $\left\lbrack {\text{false} \Leftrightarrow \neg R}\right\rbrack$

Though the last form has a special name - "proof by contradiction" - the distinction is not profound because a strengthening sequence from R to true can be translated mechanically into a strengthening sequence from false to iR (viz. the reverse sequence of the negated elements).

Strengthening sequences are formally the easier to construct, the weaker the starting element , and the stronger the final element. This note is devoted to the observation that it suffices to take from (0) the weaker of the consequents and the stronger of the antecedents:

(1) $\left\lbrack {R \Leftarrow \widehat{r}}\right\rbrack$

Formulation (1) is an optimum in the sense that of all implications equivalent to $R$ it is the one with the weakest consequent and the strongest antecedent. Furthermore, we draw attention to the fact that, whereas the implications of (0) are each other's contrapositive,

implication (1) is its own contrapositive. Finally we remark that, whereas the $\Leftarrow s$ in (0) can be replaced by $\equiv \cdot s$ ,(1) remains an implication: when proved,the consequent (true) is strictly weaker than the antecedent (false).

Had the original proof obligation been an implication - i.e. of the form $\left\lbrack {P \Leftrightarrow Q}\right\rbrack -$ (1) would have yielded the rephrasing (2) $\left[P \vee \neg Q \Leftarrow P \wedge \neg Q\right];$

compared with the original $\left\lbrack {P \Leftrightarrow Q}\right\rbrack$ ,the consequent has been weakened by the disjunction with the negated antecedent, the antecedent has been strengthened by the conjunction with the negated consequent.

The above observation has been triggered by the following proof by Peter Auer (of Vienna), that $[X \Rightarrow X; X]$ when it has been given that

$[X \Rightarrow J]$ (ii) $J$ is the identity element of $\phi$ ; (iii) ; distributes in both directions over $v$ (from which ;s monotonicity follows).

Auer's proof went as follows (here the

unay $\eta$ is the only logical operator with higher binding power than ; ,proving $\left\lbrack {X \Rightarrow X;X \vee {\eta X}}\right\rbrack$ :

$$ \begin{array}{l} = {J \mathrm {i s i d e n t i t y e l e m e n t o f} j } \ \Rightarrow \left{ \begin{array}{l l} ; \mathrm {m o n o t o n i c a n d} & [ ] \Rightarrow X \lor X ] \rbrace \ X; (X \lor \neg X) \end{array} \right. \ = \begin{array}{l} {{\vdots d i s t r i b u t e s o v e r \nu }} \ {X; X \vee X; \nabla X} \end{array} \ \Rightarrow \quad {[ X \Rightarrow J ] a n d; m o n o t o n i c } X; X \vee J; \neg X \ = {j \mathrm {i s i d e n t i l y e l e m e n t o} p; } \ \end{array} $$

Pedernales Falls State Park 29 March 1991

prof. dr. Edsger W. Dgkstra Department of Computer Sciences The University of Texas at Austin Austin, TX 78712-1188 USA