[Inquiry] Re: Propositions As Types -- Series A

[Jon Awbrey]

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o

PAT.  Note A7

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o

Composition, or the Composer (cont.)

Step 3 (optional).

Check that the propositional type of the composer P is a theorem
of classical propositional calculus, which is logically necessary
to its being a theorem of intuitionistic propositional calculus,
but easier to check.

o-------------------------------------------------o
|                                                 |
|                                                 |
|                   A   B     A   C               |
|                   o---o     o---o               |
|                   |         |                   |
|         B   C     |         |                   |
|         o---o     o---------o                   |
|         |         |                             |
|         |         |                             |
|         o---------o                             |
|         |                                       |
|         |                                       |
|         @                                       |
|                                                 |
o=================================================o
|                                                 |
|     B   C   A   B                               |
|     o---o   o---o                               |
|      \     /                                    |
|       \   /                                     |
|        \ /                                      |
|       A o---o C                                 |
|         |                                       |
|         |                                       |
|         @                                       |
|                                                 |
o=================================================o
|                                                 |
|     B   C       B                               |
|     o---o   o---o                               |
|      \     /                                    |
|       \   /                                     |
|        \ /                                      |
|       A o---o C                                 |
|         |                                       |
|         |                                       |
|         @                                       |
|                                                 |
o=================================================o
|                                                 |
|       B o---o C                                 |
|         |                                       |
|         |                                       |
|      AB o---o C                                 |
|         |                                       |
|         |                                       |
|         @                                       |
|                                                 |
o=================================================o
|                                                 |
|         o---o C                                 |
|         |                                       |
|         |                                       |
|      AB o---o C                                 |
|         |                                       |
|         |                                       |
|         @                                       |
|                                                 |
o=================================================o
|                                                 |
|     ABC o---o C                                 |
|         |                                       |
|         |                                       |
|         @                                       |
|                                                 |
o=================================================o
|                                                 |
|     ABC o---o                                   |
|         |                                       |
|         |                                       |
|         @                                       |
|                                                 |
o=================================================o
|                                                 |
|         o---o                                   |
|         |                                       |
|         |                                       |
|         @                                       |
|                                                 |
o=================================================o
|                                                 |
|         @                                       |
|                                                 |
o-------------------------------------------------o

QED.

Jon Awbrey

o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
inquiry e-lab: http://stderr.org/pipermail/inquiry/
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o