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.


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


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


  • 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.

Praeclarum Theorema



cc: CyberneticsOntolog • Peirce (1) (2) (3) (4) (5) (6)Structural ModelingSystems

This entry was posted in Amphecks, Animata, Boolean Algebra, Boolean Functions, C.S. Peirce, Cactus Graphs, Constraint Satisfaction Problems, Deduction, Diagrammatic Reasoning, Duality, Equational Inference, Graph Theory, Laws of Form, Logic, Logical Graphs, Mathematics, Minimal Negation Operators, Model Theory, Painted Cacti, Peirce, Proof Theory, Propositional Calculus, Propositional Equation Reasoning Systems, Spencer Brown, Theorem Proving, Visualization and tagged , , , , , , , , , , , , , , , , , , , , , , , , , . Bookmark the permalink.

6 Responses to Animated Logical Graphs • 40

  1. Pingback: Survey of Animated Logical Graphs • 3 | Inquiry Into Inquiry

  2. Pingback: Animated Logical Graphs • 41 | Inquiry Into Inquiry

  3. Pingback: Animated Logical Graphs • 42 | Inquiry Into Inquiry

  4. Pingback: Sign Relations, Triadic Relations, Relation Theory • Discussion 2 | Inquiry Into Inquiry

  5. Pingback: Survey of Animated Logical Graphs • 4 | Inquiry Into Inquiry

  6. Pingback: Survey of Animated Logical Graphs • 5 | Inquiry Into Inquiry

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

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