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

Jon Awbrey jawbrey at att.net
Wed Jun 23 10:40:22 CDT 2004


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

PAT.  Note A10

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

Composition, or the Composer (concl.)

Step 5.

Rewrite the proof tree in existential graph format:

o-----------------------------------------------------------o
|                                                           |
|                                       B  C  A  B  A  C    |
|                                       o--o  o--o  o--o    |
|                                       |     |     |       |
|            B  C  A  B  A  C        A  |     |     |       |
|            o--o  o--o  o--o        o--o     o-----o       |
|            |     |     |           |        |             |
|         A  |     |     |     B  C  |        |             |
|         o--o     o-----o     o--o  o--------o             |
|         |        |           |     |                      |
|         |        |           |     |                      |
|         o--------o           o-----o                      |
|         |                    |                            |
|         | S                  | SK                         |
|         o-------------------[1]                           |
|         |                                                 |
|         | K                                               |
|         @                                                 |
|                                                           |
o-----------------------------------------------------------o
|                                                           |
|                        B  C        A  B  A  C             |
|                        o--o        o--o  o--o             |
|                        |           |     |                |
|               B  C  A  |     B  C  |     |                |
|               o--o  o--o     o--o  o-----o                |
|               |     |        |     |                      |
|               |     |        |     |                      |
|               o-----o        o-----o                      |
|               |              |                            |
|               | K            | K((SK)S) = P               |
|               o-------------[o]                           |
|               |                                           |
|           SK  | (SK)S                                     |
|        [1]----o                                           |
|         |                                                 |
|         | S                                               |
|         @                                                 |
|                                                           |
o-----------------------------------------------------------o

NB.  Graphic convention used in the above style of display:
     Square bracketed nodes mark subtrees to be pruned from
     one tree and grafted into another at the indicated site,
     amounting in effect to "Facts" being recycled as "Cases".
     Square brackets are also used to mark the intended result.

Jon Awbrey

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



More information about the Inquiry mailing list