| Version 3 |
Version 2 |
| \PMlinkescapeword{ad} |
\PMlinkescapeword{ad} |
| \PMlinkescapeword{AD} |
\PMlinkescapeword{AD} |
| \PMlinkescapeword{c} |
\PMlinkescapeword{c} |
| \PMlinkescapeword{C} |
\PMlinkescapeword{C} |
| \PMlinkescapeword{calculus} |
|
| \PMlinkescapeword{Calculus} |
|
| \PMlinkescapeword{qed} |
\PMlinkescapeword{qed} |
| \PMlinkescapeword{QED} |
\PMlinkescapeword{QED} |
| \PMlinkescapeword{reflect} |
\PMlinkescapeword{reflect} |
| \PMlinkescapeword{Reflect} |
\PMlinkescapeword{Reflect} |
|
|
|
The \textbf{praeclarum theorema} is theorem of propositional calculus that was noted and given this name --- meaning \textit{admirable}, \textit{shining}, or \textit{splendid theorem} --- by G.W. Leibniz, who stated and proved it in the following manner.
|
An illustrious example of a propositional theorem is the \textbf{praeclarum theorema}, the \textit{admirable}, \textit{shining}, or \textit{splendid} theorem of Leibniz.
|
|
|
| \begin{quote} |
\begin{quote} |
| If $a$ is $b$ and $d$ is $c$, then $ad$ will be $bc$. |
If $a$ is $b$ and $d$ is $c$, then $ad$ will be $bc$. |
|
|
| This is a fine theorem, which is proved in this way: |
This is a fine theorem, which is proved in this way: |
|
|
| $a$ is $b$, therefore $ad$ is $bd$ (by what precedes), |
$a$ is $b$, therefore $ad$ is $bd$ (by what precedes), |
|
|
| $d$ is $c$, therefore $bd$ is $bc$ (again 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. |
$ad$ is $bd$, and $bd$ is $bc$, therefore $ad$ is $bc$. Q.E.D. |
|
|
| (Leibniz, \textit{Logical Papers}, p. 41). |
(Leibniz, \textit{Logical Papers}, p. 41). |
| \end{quote} |
\end{quote} |
|
|
| Expressed in contemporary logical notation, the praeclarum theorema (PT) may be written as follows: |
|
|
|
| \[ ((a \Rightarrow b) \land (d \Rightarrow c)) \Rightarrow ((a \land d) \Rightarrow (b \land c)) \] |
|
|
|
| Under the existential interpretation of logical graphs, the praeclarum theorema is represented by means of the following formal equivalence or logical equation. |
Under the existential interpretation of logical graphs, the praeclarum theorema is represented by means of the following formal equivalence or logical equation. |
|
|
| \begin{verbatim} |
\begin{verbatim} |
| o-----------------------------------------------------------o |
o-----------------------------------------------------------o |
| | Praeclarum Theorema (Leibniz) . . . . . . . . . . . . . . | |
| Praeclarum Theorema (Leibniz) . . . . . . . . . . . . . . | |
| o-----------------------------------------------------------o |
o-----------------------------------------------------------o |
| | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| | . . b o . o c . . o bc. . . . . . . . . . . . . . . . . . | |
| . . b o . o c . . o bc. . . . . . . . . . . . . . . . . . | |
| | . . . | . | . . . | . . . . . . . . . . . . . . . . . . . | |
| . . . | . | . . . | . . . . . . . . . . . . . . . . . . . | |
| | . . a o . o d . . o ad. . . . . . . . . . . . . . . . . . | |
| . . a o . o d . . o ad. . . . . . . . . . . . . . . . . . | |
| | . . . .\ /. . . . | . . . . . . . . . . . . . . . . . . . | |
| . . . .\ /. . . . | . . . . . . . . . . . . . . . . . . . | |
| | . . . . o---------o . . . . . . . . . . . . . . . . . . . | |
| . . . . o---------o . . . . . . . . . . . . . . . . . . . | |
| | . . . . | . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . | . . . . . . . . . . . . . . . . . . . . . . . . | |
| | . . . . | . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . | . . . . . . . . . . . . . . . . . . . . . . . . | |
| | . . . . @ . . . . . . . . . = . . . . . . . . . @ . . . . | |
| . . . . @ . . . . . . . . . = . . . . . . . . . @ . . . . | |
| | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| o-----------------------------------------------------------o |
o-----------------------------------------------------------o |
| | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| | .((a(b))(d(c))((ad(bc)))) . = . . . . . . . . . . . . . . | |
| .((a(b))(d(c))((ad(bc)))) . = . . . . . . . . . . . . . . | |
| | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| o-----------------------------------------------------------o |
o-----------------------------------------------------------o |
| \end{verbatim} |
\end{verbatim} |
|
|
| And here's a neat proof of that nice theorem. |
And here's a neat proof of that nice theorem. |
|
|
| \begin{verbatim} |
\begin{verbatim} |
| o-----------------------------------------------------------o |
o-----------------------------------------------------------o |
| | Praeclarum Theorema (Leibniz) . Proof . . . . . . . . . . | |
| Praeclarum Theorema (Leibniz) . Proof . . . . . . . . . . | |
| o-----------------------------------------------------------o |
o-----------------------------------------------------------o |
| | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| | . . b o . o c . . o bc. . . . . . . . . . . . . . . . . . | |
| . . b o . o c . . o bc. . . . . . . . . . . . . . . . . . | |
| | . . . | . | . . . | . . . . . . . . . . . . . . . . . . . | |
| . . . | . | . . . | . . . . . . . . . . . . . . . . . . . | |
| | . . a o . o d . . o ad. . . . . . . . . . . . . . . . . . | |
| . . a o . o d . . o ad. . . . . . . . . . . . . . . . . . | |
| | . . . .\./. . . . | . . . . . . . . . . . . . . . . . . . | |
| . . . .\./. . . . | . . . . . . . . . . . . . . . . . . . | |
| | . . . . o---------o . . . . . . . . . . . . . . . . . . . | |
| . . . . o---------o . . . . . . . . . . . . . . . . . . . | |
| | . . . . | . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . | . . . . . . . . . . . . . . . . . . . . . . . . | |
| | . . . . | . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . | . . . . . . . . . . . . . . . . . . . . . . . . | |
| | . . . . @ . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . @ . . . . . . . . . . . . . . . . . . . . . . . . | |
| | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| o=============================< C1. Reflect "ad(bc)" >======o |
o=============================< C1. Reflect "ad(bc)" >======o |
| | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| | . . b o . o c . . . . . . . . . . . . . . . . . . . . . . | |
| . . b o . o c . . . . . . . . . . . . . . . . . . . . . . | |
| | . . . | . | . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . | . | . . . . . . . . . . . . . . . . . . . . . . . | |
| | . . a o . o d . . . . . . . . . . . . . . . . . . . . . . | |
| . . a o . o d . . . . . . . . . . . . . . . . . . . . . . | |
| | . . . .\./. . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . .\./. . . . . . . . . . . . . . . . . . . . . . . . | |
| | . . .ad o---------o bc. . . . . . . . . . . . . . . . . . | |
| . . .ad o---------o bc. . . . . . . . . . . . . . . . . . | |
| | . . . . | . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . | . . . . . . . . . . . . . . . . . . . . . . . . | |
| | . . . . | . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . | . . . . . . . . . . . . . . . . . . . . . . . . | |
| | . . . . @ . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . @ . . . . . . . . . . . . . . . . . . . . . . . . | |
| | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| o=============================< Weed "a", "d" >=============o |
o=============================< Weed "a", "d" >=============o |
| | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| | . . b o . o c . . . . . . . . . . . . . . . . . . . . . . | |
| . . b o . o c . . . . . . . . . . . . . . . . . . . . . . | |
| | . . . | . | . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . | . | . . . . . . . . . . . . . . . . . . . . . . . | |
| | . . . o . o . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . o . o . . . . . . . . . . . . . . . . . . . . . . . | |
| | . . . .\./. . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . .\./. . . . . . . . . . . . . . . . . . . . . . . . | |
| | . . .ad o---------o bc. . . . . . . . . . . . . . . . . . | |
| . . .ad o---------o bc. . . . . . . . . . . . . . . . . . | |
| | . . . . | . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . | . . . . . . . . . . . . . . . . . . . . . . . . | |
| | . . . . | . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . | . . . . . . . . . . . . . . . . . . . . . . . . | |
| | . . . . @ . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . @ . . . . . . . . . . . . . . . . . . . . . . . . | |
| | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| o=============================< C1. Reflect "b", "c" >======o |
o=============================< C1. Reflect "b", "c" >======o |
| | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| | . .abcd o---------o bc. . . . . . . . . . . . . . . . . . | |
| . .abcd o---------o bc. . . . . . . . . . . . . . . . . . | |
| | . . . . | . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . | . . . . . . . . . . . . . . . . . . . . . . . . | |
| | . . . . | . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . | . . . . . . . . . . . . . . . . . . . . . . . . | |
| | . . . . @ . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . @ . . . . . . . . . . . . . . . . . . . . . . . . | |
| | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| o=============================< Weed "bc" >=================o |
o=============================< Weed "bc" >=================o |
| | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| | . .abcd o---------o . . . . . . . . . . . . . . . . . . . | |
| . .abcd o---------o . . . . . . . . . . . . . . . . . . . | |
| | . . . . | . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . | . . . . . . . . . . . . . . . . . . . . . . . . | |
| | . . . . | . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . | . . . . . . . . . . . . . . . . . . . . . . . . | |
| | . . . . @ . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . @ . . . . . . . . . . . . . . . . . . . . . . . . | |
| | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| o=============================< C3. Recess "abcd" >=========o |
o=============================< C3. Recess "abcd" >=========o |
| | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| | . . . . o---------o . . . . . . . . . . . . . . . . . . . | |
| . . . . o---------o . . . . . . . . . . . . . . . . . . . | |
| | . . . . | . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . | . . . . . . . . . . . . . . . . . . . . . . . . | |
| | . . . . | . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . | . . . . . . . . . . . . . . . . . . . . . . . . | |
| | . . . . @ . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . @ . . . . . . . . . . . . . . . . . . . . . . . . | |
| | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| o=============================< I2. Refold "(())" >=========o |
o=============================< I2. Refold "(())" >=========o |
| | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| | . . . . @ . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . @ . . . . . . . . . . . . . . . . . . . . . . . . | |
| | . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . | |
| o=============================< QED >=======================o |
o=============================< QED >=======================o |
| \end{verbatim} |
\end{verbatim} |
|
|
| \section{Bibliography} |
\section{Bibliography} |
|
|
| \begin{itemize} |
\begin{itemize} |
| \item |
\item |
| Leibniz, Gottfried W. (1679--1686 ?), ``Addenda to the Specimen of the Universal Calculus'', pp. 40--46 in G.H.R. Parkinson (ed., trans., 1966), \textit{Leibniz : Logical Papers}, Oxford University Press, London, UK. |
Leibniz, Gottfried W. (1679--1686 ?), ``Addenda to the Specimen of the Universal Calculus'', pp. 40--46 in G.H.R. Parkinson (ed., trans., 1966), \textit{Leibniz : Logical Papers}, Oxford University Press, London, UK. |
| \end{itemize} |
\end{itemize} |
