Line 956: |
Line 956: |
| ===Step 3 (Optional)=== | | ===Step 3 (Optional)=== |
| | | |
− | <pre>
| + | At this juncture we might want to verify that the proposition corresponding to the type of <math>\operatorname{T}</math> is actually a theorem of classical propositional calculus. Since nothing can be a theorem of intuitionistic propositional calculus wihout also being a theorem of classical propositional calculus, this is a necessary condition of our work being correct up to this point. Although it is not a sufficient condition, classical theoremhood is easier to test and so provides a quick and useful check on our work. |
− | At this juncture we might want to verify that the proposition corresponding | |
− | to the type of T is actually a theorem of classical propositional calculus. | |
− | Since nothing can be a theorem of intuitionistic propositional calculus | |
− | wihout also being a theorem of classical propositional calculus, this | |
− | is a necessary condition of our work being correct up to this point. | |
− | Although it is not a sufficient condition, classical theoremhood | |
− | is easier to test and so provides a quick and useful check on | |
− | our work. | |
| | | |
− | In existential graph format, T has the following generic typing: | + | In existential graph format, <math>\operatorname{T}</math> has the following generic typing: |
| | | |
| + | <pre> |
| o-------------------------------------------------o | | o-------------------------------------------------o |
| | | | | | | |
Line 980: |
Line 973: |
| | | | | | | |
| o-------------------------------------------------o | | o-------------------------------------------------o |
| + | </pre> |
| | | |
| And here is a classical logic proof of the type proposition: | | And here is a classical logic proof of the type proposition: |
| | | |
| + | <pre> |
| o-------------------------------------------------o | | o-------------------------------------------------o |
| | | | | | | |