12,089
edits
Changes
Directory:Jon Awbrey/Papers/Propositions As Types (view source)
Revision as of 19:12, 24 March 2009
, 19:12, 24 March 2009→Step 3 (Optional): markup
===Step 3 (Optional)===
===Step 3 (Optional)===
Check that the propositional type of the composer <math>\operatorname{P}</math> is a theorem of classical propositional calculus, which is logically necessary to its being a theorem of intuitionistic propositional calculus, but easier to check.
<pre>
<pre>
o-------------------------------------------------o
o-------------------------------------------------o
| |
| |
| |
| |
o-------------------------------------------------o
o-------------------------------------------------o
</pre>
QED.
QED.
===Step 4===
===Step 4===