| Line 783: |
Line 783: |
| | |} | | |} |
| | | | |
| − | ==Exemplary proofs== | + | ===Exemplary proofs=== |
| | | | |
| − | Now to take up a more interesting example, here is the statement and a proof of the ''Splendid Theorem'' from Leibniz that was brought to my attention by John Sowa.
| + | Based on the axioms given at the outest, and aided by the theorems recorded so far, it is possible to prove a multitude of much more complex theorems. A couple of all-time favorites are given next. |
| | | | |
| − | <pre>
| + | ====Peirce's law==== |
| − | | 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', page 41.
| |
| − | |
| |
| − | | Leibniz, G.W., "Addenda to the Specimen of the Universal Calculus",
| |
| − | | pages 40-46 in Parkinson, G.H.R. (ed.), 'Leibniz: Logical Papers',
| |
| − | | Oxford University Press, London, UK, 1966. (Gerhardt, 7, p. 223).
| |
| | | | |
| − | o-----------------------------------------------------------o
| + | : ''[[Peirce's law|Main article: Peirce's law]]'' |
| − | | Praeclarum Theorema (Leibniz) ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | + | |
| − | o-----------------------------------------------------------o
| + | Peirce's law is commonly written in the following form: |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | + | |
| − | | ` ` b o ` o c ` ` o bc` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | + | {| align="center" cellpadding="10" |
| − | | ` ` ` | ` | ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | + | | <math>((p \Rightarrow q) \Rightarrow p) \Rightarrow p</math> |
| − | | ` ` a o ` o d ` ` o ad` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| + | |} |
| − | | ` ` ` `\ /` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | + | |
| − | | ` ` ` ` o---------o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | + | The existential graph representation of Peirce's law is shown in Figure 31. |
| − | | ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | + | |
| − | | ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| + | {| align="center" cellpadding="10" |
| − | | ` ` ` ` @ ` ` ` ` ` ` ` ` ` = ` ` ` ` ` ` ` ` ` @ ` ` ` ` |
| + | | [[Image:Logical_Graph_Figure_31.jpg|500px]] |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| + | |} |
| − | o-----------------------------------------------------------o
| + | |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| + | A graphical proof of Peirce's law is shown in Figure 32. |
| − | | `((a(b))(d(c))((ad(bc)))) ` = ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| + | |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | + | {| align="center" cellpadding="10" |
| − | o-----------------------------------------------------------o
| + | | [[Image:Logical_Graph_Figure_32.jpg|500px]] |
| − | </pre>
| + | |} |
| | + | |
| | + | ====Praeclarum theorema==== |
| | + | |
| | + | An illustrious example of a propositional theorem is the ''praeclarum theorema'', the ''admirable'', ''shining'', or ''splendid'' theorem of [[Leibniz]]. |
| | + | |
| | + | <blockquote> |
| | + | <p>If ''a'' is ''b'' and ''d'' is ''c'', then ''ad'' will be ''bc''.</p> |
| | + | |
| | + | <p>This is a fine theorem, which is proved in this way:</p> |
| | + | |
| | + | <p>''a'' is ''b'', therefore ''ad'' is ''bd'' (by what precedes),</p> |
| | + | |
| | + | <p>''d'' is ''c'', therefore ''bd'' is ''bc'' (again by what precedes),</p> |
| | + | |
| | + | <p>''ad'' is ''bd'', and ''bd'' is ''bc'', therefore ''ad'' is ''bc''. Q.E.D.</p> |
| | + | |
| | + | <p>([[Leibniz]], ''Logical Papers'', p. 41).</p> |
| | + | </blockquote> |
| | + | |
| | + | Under the existential interpretation, the praeclarum theorema is represented by means of the following logical graph. |
| | + | |
| | + | {| align="center" cellpadding="10" |
| | + | | [[Image:Logical_Graph_Figure_33.jpg|500px]] |
| | + | |} |
| | | | |
| | And here's a neat proof of that nice theorem. | | And here's a neat proof of that nice theorem. |
| | | | |
| − | <pre>
| + | {| align="center" cellpadding="10" |
| − | o-----------------------------------------------------------o
| + | | [[Image:Logical_Graph_Figure_34.jpg|500px]] |
| − | | Praeclarum Theorema (Leibniz).` Proof.` ` ` ` ` ` ` ` ` ` |
| + | |} |
| − | o-----------------------------------------------------------o
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` b o ` o c ` ` o bc` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` | ` | ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` a o ` o d ` ` o ad` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` `\ /` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` o---------o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | o=============================< C1. Reflect "ad(bc)" >======o
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` b o ` o c ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` | ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` a o ` o d ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` `ad o---------o bc` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | o=============================< Weed "a", "d" >=============o
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` b o ` o c ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` | ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` o ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` `\ /` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` `ad o---------o bc` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | |
| − | o=============================< C1. Reflect "b", "c" >======o
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` `abcd o---------o bc` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | |
| − | | ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | o=============================< Weed "bc" >=================o
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` `abcd o---------o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | o=============================< C3. Recess "abcd" >=========o
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` o---------o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | o=============================< I2. Refold "(())" >=========o
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | o=============================< QED >=======================o
| |
| − | </pre>
| |
| | | | |
| | ==Themes and variations== | | ==Themes and variations== |
