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

[Jon Awbrey]

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

PAT.  Note A17

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

Transposition, or the Transposer (cont.)

Step 3 (optional).

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:

o-------------------------------------------------o
|                                                 |
|                B  C     A  C                    |
|                o--o     o--o                    |
|             A  |     B  |                       |
|             o--o     o--o                       |
|             |        |                          |
|             o--------o                          |
|             |                                   |
|         T : @                                   |
|                                                 |
o-------------------------------------------------o

And here is a classical logic proof of the type proposition:

o-------------------------------------------------o
|                                                 |
|                B  C     A  C                    |
|                o--o     o--o                    |
|             A  |     B  |                       |
|             o--o     o--o                       |
|             |        |                          |
|             o--------o                          |
|             |                                   |
|             @                                   |
|                                                 |
o=================================================o
|                                                 |
|            AB  C    AB  C                       |
|             o--o     o--o                       |
|             |        |                          |
|             o--------o                          |
|             |                                   |
|             @                                   |
|                                                 |
o=================================================o
|                                                 |
|             X        X                          |
|             o--------o                          |
|             |                                   |
|             @                                   |
|                                                 |
o=================================================o
|                                                 |
|             @                                   |
|                                                 |
o-------------------------------------------------o

Jon Awbrey

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