## Animated Logical Graphs • 40

Re: Richard J. LiptonLogical Complexity Of Proofs
Re: Animated Logical Graphs • (35) (36) (37) (38) (39)

One way to see the difference between insight proofs and routine proofs is to pick a single example of a theorem in propositional calculus and prove it two ways, one more insightful and one more routine.

The praeclarum theorema, or splendid theorem, is a theorem of propositional calculus noted and named by G.W. Leibniz, who stated and proved it in the following manner.

If a is b and d is c, then ad will be bc.
This is a fine theorem, which is proved in this way:
a is b, therefore ad is bd (by what precedes),
d is c, therefore bd is bc (again by what precedes),
ad is bd, and bd is bc, therefore ad is bc.  Q.E.D.

— Leibniz • Logical Papers, p. 41.

Expressed in contemporary logical notation, the theorem may be written as follows. $((a \Rightarrow b) \land (d \Rightarrow c)) \Rightarrow ((a \land d) \Rightarrow (b \land c))$

Using teletype parentheses $\texttt{(} ~ \texttt{)}$ for the logical negation $\texttt{(} p \texttt{)}$ of a proposition $p$ and simple concatenation $pq$ for the logical conjunction of propositions $p$ and $q$ enables writing the theorem in the following in-line and lispish ways.

#### Inline $\texttt{(} \quad \texttt{(} a \texttt{(} b \texttt{))} \texttt{(} d \texttt{(} c \texttt{))} \quad \texttt{(} \quad \texttt{(} ad \texttt{(} bc \texttt{))} \quad \texttt{))}$

#### Lispish $\begin{array}{lc} \texttt{(} & \texttt{(} a \texttt{(} b \texttt{))} \texttt{(} d \texttt{(} c \texttt{))} \\ \texttt{(} & \texttt{(} ad \texttt{(} bc \texttt{))} \\ \texttt{))}\end{array}$

### Reference

• Leibniz, Gottfried W. (1679–1686?), “Addenda to the Specimen of the Universal Calculus”, pp. 40–46 in G.H.R. Parkinson (ed., trans., 1966), Leibniz : Logical Papers, Oxford University Press, London, UK.

### 6 Responses to Animated Logical Graphs • 40

This site uses Akismet to reduce spam. Learn how your comment data is processed.