Praeclarum Theorema
Contents |
Theorem
The praeclarum theorema (PT), or splendid theorem, is a theorem of classical propositional calculus:
- $\left({p \implies q}\right) \land \left({r \implies s}\right) \vdash \left({p \land r}\right) \implies \left({q \land s}\right)$
It can alternatively be rendered as:
- $\vdash \left({\left({p \implies q}\right) \land \left({r \implies s}\right)}\right) \implies \left({\left({p \land r}\right) \implies \left({q \land s}\right)}\right)$
The two forms can be seen to be logically equivalent by application of the Rule of Implication and Modus Ponendo Ponens.
Representing propositions as logical graphs under the existential interpretation, the praeclarum theorema is expressed by means of the following formal equation:
Proof
Proof by Logical Graphs
Proof by Truth Table
We apply the Method of Truth Tables to the proposition.
As can be seen for all models by inspection, where the truth value under the main connective on the LHS is $T$, that under the one on the RHS is also $T$:
$\begin{array}{|ccccccc||ccccccc|} \hline
(p & \implies & q) & \land & (r & \implies & s) & (p & \land & r) & \implies & (q & \land & s) \\
\hline
F & T & F & T & F & T & F & F & F & F & T & F & F & F \\
F & T & F & T & F & T & T & F & F & F & T & F & F & T \\
F & T & F & F & T & F & F & F & F & T & T & F & F & F \\
F & T & F & T & T & T & T & F & F & T & T & F & F & T \\
F & T & T & T & F & T & F & F & F & F & T & T & F & F \\
F & T & T & T & F & T & T & F & F & F & T & T & T & T \\
F & T & T & F & T & F & F & F & F & T & T & T & F & F \\
F & T & T & T & T & T & T & F & F & T & T & T & T & T \\
T & F & F & F & F & T & F & T & F & F & T & F & F & F \\
T & F & F & F & F & T & T & T & F & F & T & F & F & T \\
T & F & F & F & T & F & F & T & T & T & F & F & F & F \\
T & F & F & F & T & T & T & T & T & T & F & F & F & T \\
T & T & T & T & F & T & F & T & F & F & T & T & F & F \\
T & T & T & T & F & T & T & T & F & F & T & T & T & T \\
T & T & T & F & T & F & F & T & T & T & F & T & F & F \\
T & T & T & T & T & T & T & T & T & T & T & T & T & T \\
\hline
\end{array}$
Hence the result.
$\blacksquare$
Note that the two formulas are not equivalent, as the relevant columns do not match exactly.
Also see
Compare the Constructive Dilemma, which is similar in appearance.
History
-
Praeclarum Theorema
The praeclarum theorema was 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).
Sources
- Gottfried W Leibniz: Addenda to the Specimen of the Universal Calculus (1679 – 1686): pp. $40 - 46$
- Donald Kalish and Richard Montague: Logic: Techniques of Formal Reasoning (1964): $\text{II}: \S 3$: Theorem $\text{T32}$
- E.J. Lemmon: Beginning Logic (1965): $\S 1.3$: Exercise $1 \ \text{(g)}$
- Michael R.A. Huth and Mark D. Ryan: Logic in Computer Science: Modelling and reasoning about systems (2000): $\S 1.2.1$: Exercises $1.4: \ 2 \ \text{(g)}$
- John F. Sowa: Peirce's Rules of Inference: Online version (2002)
- Frithjof Dau: Computer Animated Proof of Leibniz's Praeclarum Theorema (2008).
- Norman Megill: Praeclarum Theorema @ Metamath Proof Explorer (2008)
