Proving $P$ $\implies$ $Q$

Question

I was wondering about this form of logical proof in the book: Programming in the 1990s, by Edward Cohen.

To prove $P \implies Q$, the author uses this sequence:

\begin{align*} Q \\ \equiv\langle\text{Assuming P}\rangle \\ true \end{align*}

Could someone explain what’s the thought behind it ?

Answer 1

In an "equational-style" proof, to prove a formula $A$ amounts to prove $A \equiv \text {true}$.

See David Gries & Fred Schneider, A Logical Approach to Discrete Mathematics (Springer, 1993) for a more clear explanation.

See page 72, the:

(Extended) Deduction Theorem:

if adding $P_1, \ldots P_n$ as axioms we are able to prove $Q$, then $P_1 \land \ldots \land P_n \Rightarrow Q$ is a theorem.

---

How to apply it to your proof ?

We have an assumption $P$ and we prove - under that assumption - that $Q \equiv \top$ [using $\top$ for $\text {true}$].

Using the deduction Theorem, we conclude with $P \Rightarrow (Q \equiv \top)$.

Then we need the Distributivity law of $\Rightarrow$ over $\equiv$:

$(P \Rightarrow (Q \equiv R)) \equiv ((P \Rightarrow Q) \equiv (P \Rightarrow R))$.

With $\top$ in place of $R$, our formula above becomes: $(P \Rightarrow Q) \equiv (P \Rightarrow \top)$.

But $P \Rightarrow \top$ is $\top$; thus, we have arrived at:

$(P \Rightarrow Q) \equiv \top$

and this means that $P \Rightarrow Q$ is a theorem.