| Line 43: |
Line 43: |
| | | | |
| | ===Step 3 (Optional)=== | | ===Step 3 (Optional)=== |
| | + | |
| | + | Check that <math>A \Rightarrow A</math> is a theorem of classical propositional calculus. |
| | | | |
| | <pre> | | <pre> |
| − | Check that A => A is a theorem of classical propositional calculus.
| |
| − |
| |
| | A A | | A A |
| | o---o o---o | | o---o o---o |
| | | | | | | | |
| | @ = @ = @ | | @ = @ = @ |
| | + | </pre> |
| | | | |
| | Check. | | Check. |
| − | </pre>
| |
| | | | |
| | ===Step 4=== | | ===Step 4=== |