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.
Using teletype parentheses for the logical negation of a proposition and simple concatenation for the logical conjunction of propositions and enables writing the theorem in the following in-line and lispish ways.
- 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.
- This Blog
- OEIS Wiki • (1) • (2) • (3)
- PlanetMath • Praeclarum Theorema
- Metamath Proof Explorer • Praeclarum Theorema
- Frithjof Dau • Computer Animated Proof of Leibniz’s Praeclarum Theorema
- Logic Syllabus
- Logical Graphs
- Cactus Language
- Futures Of Logical Graphs
- Minimal Negation Operators
- Survey of Theme One Program
- Survey of Animated Logical Graphs
- Propositional Equation Reasoning Systems
- How To Succeed In Proof Business Without Really Trying
- Applications of a Propositional Calculator • Constraint Satisfaction Problems
- Exploratory Qualitative Analysis of Sequential Observation Data