12,080
edits
Changes
Directory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 15:06, 25 March 2009
, 15:06, 25 March 2009→Transposition, or the Transposer: markup
===Step 3 (Optional)===
===Step 3 (Optional)===
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
| |
| |
| |
| |
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
| |
| |