| Line 114: |
Line 114: |
| | ===Exemplary proofs=== | | ===Exemplary proofs=== |
| | | | |
| − | With the meagre means afforded by the axioms and theorems given so far, it is already possible to prove a multitude of much more complex theorems. A couple of all-time favorites are given next.
| + | 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. |
| | | | |
| | ====Peirce's law==== | | ====Peirce's law==== |
| | | | |
| − | ''[[Peirce's law|Main article: Peirce's law]]'' | + | : ''Main article : [[Peirce's law]] |
| | | | |
| − | This section presents a proof of Peirce's law, commonly written:
| + | Peirce's law is commonly written in the following form: |
| − | :* <nowiki>[[p ⇒ q] ⇒ p] ⇒ p</nowiki>
| |
| | | | |
| − | The first order of business is present the statement as it appears in the so-called ''existential interpretation'' of Peirce's own ''logical graphs''. Here is the statement of Peirce's law, as rendered under the existential interpretation into (the topological dual forms of) Peirce's logical graphs:
| + | <center> |
| | + | <p><math>((p \Rightarrow q) \Rightarrow p) \Rightarrow p</math></p> |
| | + | </center> |
| | | | |
| − | o-----------------------------------------------------------o
| + | The existential graph representation of Peirce's law is shown in Figure 12. |
| − | | Peirce's Law` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | o-----------------------------------------------------------o
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` p o---o q ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` o---o p ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` o---o p ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` @ ` ` ` ` ` ` ` ` = ` ` ` ` ` ` ` ` ` @ ` ` ` ` |
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | o-----------------------------------------------------------o
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` `(((p (q)) (p)) (p))) ` = ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | o-----------------------------------------------------------o
| |
| | | | |
| − | Finally, here's the promised proof of Peirce's law:
| + | {| align="center" border="0" cellpadding="10" cellspacing="0" |
| | + | | [[Image:PERS_Figure_12.jpg|500px]] || (12) |
| | + | |} |
| | | | |
| − | o-----------------------------------------------------------o
| + | A graphical proof of Peirce's law is shown in Figure 32. |
| − | | Peirce's Law. `Proof` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| + | |
| − | o-----------------------------------------------------------o
| + | {| align="center" border="0" cellpadding="10" cellspacing="0" |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| + | | [[Image:PERS_Figure_13.jpg|500px]] || (13) |
| − | | ` ` ` ` p o---o q ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| + | |} |
| − | | ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` o---o p ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` o---o p ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | o==================================< Collect >==============o
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` o---o q ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` o---o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` p o---o p ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | o==================================< Recess >===============o
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` o---o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` p o---o p ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | o==================================< Refold >===============o
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` p o---o p ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | o==================================< Delete >===============o
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` o---o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | o==================================< Refold >===============o
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` @ ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | o==================================< QED >==================o
| |
| | | | |
| | ====Praeclarum theorema==== | | ====Praeclarum theorema==== |
| | | | |
| − | Now to take up a more interesting example, here is the statement and a proof of the ''Praeclarum Theorema'' or ''Splendid Theorem'' of Leibniz.
| + | 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> |
| | | | |
| − | : If ''a'' is ''b'' and ''d'' is ''c'', then ''ad'' will be ''bc''.
| + | Under the existential interpretation, the praeclarum theorema is represented by means of the following logical graph. |
| − | : <br>
| |
| − | : This is a fine theorem, which is proved in this way:
| |
| − | : <br>
| |
| − | : ''a'' is ''b'', therefore ''ad'' is ''bd'' (by what precedes),
| |
| − | : <br>
| |
| − | : ''d'' is ''c'', therefore ''bd'' is ''bc'' (again by what precedes),
| |
| − | : <br>
| |
| − | : ''ad'' is ''bd'', and ''bd'' is ''bc'', therefore ''ad'' is ''bc''. Q.E.D.
| |
| − | : <br>
| |
| − | : ([[Leibniz]], ''Logical Papers'', p. 41).
| |
| | | | |
| − | o-----------------------------------------------------------o
| + | {| align="center" border="0" cellpadding="10" cellspacing="0" |
| − | | Praeclarum Theorema (Leibniz) ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| + | | [[Image:PERS_Figure_14.jpg|500px]] || (14) |
| − | o-----------------------------------------------------------o
| + | |} |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` b o ` o c ` ` o bc` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` | ` | ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` a o ` o d ` ` o ad` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` `\ /` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` o---------o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` @ ` ` ` ` ` ` ` ` ` = ` ` ` ` ` ` ` ` ` @ ` ` ` ` |
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | o-----------------------------------------------------------o
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | `((a(b))(d(c))((ad(bc)))) ` = ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | o-----------------------------------------------------------o
| |
| | | | |
| − | And here's a neat proof of this nice theorem: | + | And here's a neat proof of that nice theorem. |
| | | | |
| − | o-----------------------------------------------------------o
| + | {| align="center" border="0" cellpadding="10" cellspacing="0" |
| − | | Praeclarum Theorema (Leibniz).` Proof.` ` ` ` ` ` ` ` ` ` |
| + | | [[Image:PERS_Figure_15.jpg|500px]] || (15) |
| − | 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
| |
| | | | |
| | ==Formal extension : Cactus calculus== | | ==Formal extension : Cactus calculus== |