| Line 564: |
Line 564: |
| | The axioms are just four in number, and they come in a couple of flavors: the ''arithmetic initials'' ''I''<sub>1</sub> and ''I''<sub>2</sub>, and the ''algebraic initials'' ''J''<sub>1</sub> and ''J''<sub>2</sub>. | | The axioms are just four in number, and they come in a couple of flavors: the ''arithmetic initials'' ''I''<sub>1</sub> and ''I''<sub>2</sub>, and the ''algebraic initials'' ''J''<sub>1</sub> and ''J''<sub>2</sub>. |
| | | | |
| − | <pre>
| + | {| align="center" cellpadding="10" |
| − | o-----------------------------------------------------------o
| + | | [[Image:Logical_Graph_Figure_20.jpg|500px]] |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | + | |- |
| − | | ` ` ` ` ` ` ` ` o ` o ` ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` |
| + | | [[Image:Logical_Graph_Figure_21.jpg|500px]] |
| − | | ` ` ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` |
| + | |- |
| − | | ` ` ` ` ` ` ` ` ` @ ` ` ` ` = ` ` ` ` @ ` ` ` ` ` ` ` ` ` |
| + | | [[Image:Logical_Graph_Figure_22.jpg|500px]] |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| + | |- |
| − | o-----------------------------------------------------------o
| + | | [[Image:Logical_Graph_Figure_23.jpg|500px]] |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| + | |} |
| − | | ` ` ` ` ` ` ` `( ) ( )` ` ` = ` ` ` `( )` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | o-----------------------------------------------------------o
| |
| − | | Axiom I_1.` ` Distract <--- | ---> Condense ` ` ` ` ` ` ` | | |
| − | o-----------------------------------------------------------o
| |
| − | </pre>
| |
| − | <pre>
| |
| − | o-----------------------------------------------------------o
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | |
| − | | ` ` ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` ` ` ` ` @ ` ` ` ` = ` ` ` ` @ ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | o-----------------------------------------------------------o
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | |
| − | | ` ` ` ` ` ` ` ` (( )) ` ` ` = ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | o-----------------------------------------------------------o
| |
| − | | Axiom I_2.` ` ` Unfold <--- | ---> Refold ` ` ` ` ` ` ` ` | | |
| − | o-----------------------------------------------------------o
| |
| − | </pre>
| |
| − | <pre>
| |
| − | o-----------------------------------------------------------o
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` | | |
| − | | ` ` ` ` ` ` ` ` a o ` ` ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` ` ` ` a @ ` ` ` ` = ` ` ` ` @ ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | o-----------------------------------------------------------o
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` ` ` ` a(a)` ` ` ` = ` ` ` `( )` ` ` ` ` ` ` ` ` | | |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | o-----------------------------------------------------------o
| |
| − | | Axiom J_1.` ` ` Insert <--- | ---> Delete ` ` ` ` ` ` ` ` |
| |
| − | o-----------------------------------------------------------o
| |
| − | </pre>
| |
| − | <pre>
| |
| − | o-----------------------------------------------------------o
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` ` ` `ab ` ac` ` ` ` ` ` ` b ` c ` ` ` ` ` ` ` ` | | |
| − | | ` ` ` ` ` ` ` ` o ` o ` ` ` ` ` ` ` o ` o ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` `\ /` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` o ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` | ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` ` ` ` ` @ ` ` ` ` = ` ` ` a @ ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | o-----------------------------------------------------------o
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` ` `((ab)(ac)) ` ` = ` ` a((b)(c)) ` ` ` ` ` ` ` |
| |
| − | | ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` ` |
| |
| − | o-----------------------------------------------------------o
| |
| − | | Axiom J_2.` Distribute <--- | ---> Collect` ` ` ` ` ` ` ` |
| |
| − | o-----------------------------------------------------------o
| |
| − | </pre>
| |
| | | | |
| | Notice that all of the axioms in this set have the form of equations. This means that all of the inference steps they allow are reversible. In the proof annotation scheme below, I will use a double bar "=====" to mark this fact, but I may at times leave it to the reader to pick which direction is the one required for applying the indicated axiom. | | Notice that all of the axioms in this set have the form of equations. This means that all of the inference steps they allow are reversible. In the proof annotation scheme below, I will use a double bar "=====" to mark this fact, but I may at times leave it to the reader to pick which direction is the one required for applying the indicated axiom. |