[Inquiry] Re: Propositions As Types -- Series A
Jon Awbrey
jawbrey at att.net
Thu Jul 1 15:30:20 CDT 2004
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
PAT. Note A23
o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o~~~~~~~~~o
Transposition, or the Transposer (cont.)
Step 5 (extended).
Redo the development of the proof tree in existential graph format.
Each frame of the developmental scheme that follows is divided by
a dotted line, with terms that contribute to the main term under
development being shown above it and the main term itself being
shown below it.
o---------------------------------------------------------------------o
| Hypotheses: x : A, y : B, z : A=>(B=>C) |
o---------------------------------------------------------------------o
| |
| y(xz) |
| |
| A x |
| [1] |
| |
| B y |
| [2] |
| |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
| |
| B C y(xz) |
| [2]--o |
| | |
| A | xz |
| [1]--o |
| | |
| | z |
| @ |
| |
o=====================================================================o
| |
| (x(yK))(xz) |
| |
| A B x(yK) |
| o--[3] |
| | |
| B | yK |
| o---o |
| | |
| | K |
| @ |
| |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
| |
| B C (x(yK))(xz) |
| [3]--o |
| | |
| A | xz |
| o---o |
| | |
| | z |
| @ |
| |
o=====================================================================o
| |
| x((yK)(zS)) |
| |
| A B |
| o---o |
| | |
| B | yK |
| o--[4] |
| | |
| | K |
| @ |
| |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
| |
| B C A B A C x((yK)(zS)) |
| o---o o---o o---o |
| | | | |
| A | | yK | (yK)(zS) |
| o---o [4]------o |
| | | |
| | z | zS |
| o-----------o |
| | |
| | S |
| @ |
| |
o=====================================================================o
| |
| x((yK)(y((zS)K))) |
| |
| A B |
| o---o |
| | |
| B | yK |
| o--[4] |
| | |
| | K |
| @ |
| |
| B C A B A C |
| o---o o---o o---o |
| | | | |
| A | | | |
| o---o o-------o |
| | | |
| | z | zS |
| o----------[5] |
| | |
| | S |
| @ |
| |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
| |
| A B A C x((yK)(y((zS)K))) |
| o---o o---o |
| | | |
| A B A C | yK | (yK)(y((zS)K)) |
| o---o o---o [4]------o |
| | | | |
| | | B | y((zS)K) |
| o-------o o---o |
| | | |
| | zS | (zS)K |
| [5]--------------o |
| | |
| | K |
| @ |
| |
o=====================================================================o
| |
| x(y(K(((zS)K)S))) |
| |
| B C A B A C |
| o---o o---o o---o |
| | | | |
| A | | | |
| o---o o-------o |
| | | |
| | z | zS |
| o----------[5] |
| | |
| | S |
| @ |
| |
| A B A C |
| o---o o---o |
| | | |
| A B A C | | |
| o---o o---o o-------o |
| | | | |
| | | B | |
| o-------o o---o |
| | | |
| | zS | (zS)K |
| [5]-------------[6] |
| | |
| | K |
| @ |
| |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
| |
| A B A C A B A C x(y(K(((zS)K)S))) |
| o---o o---o o---o o---o |
| | | | | |
| | | B | B | y(K(((zS)K)S)) |
| o-------o o---o o---o |
| | | | |
| B | | K | K(((zS)K)S) |
| o---o o----------o |
| | | |
| | (zS)K | ((zS)K)S |
| [6]-----------------o |
| | |
| | S |
| @ |
| |
o=====================================================================o
| |
| x(y(K(((zS)(z(KK)))S))) |
| |
| B C A B A C |
| o--o o--o o--o |
| | | | |
| A | | | |
| o--o o-----o |
| | | |
| | z | zS |
| o-------[5] |
| | |
| | S |
| @ |
| |
| A B A C |
| o--o o--o |
| | | |
| A B A C A B A C | | |
| o--o o--o o--o o--o o-----o |
| | | | | | |
| A B A C | | B C | | B | |
| o--o o--o o-----o o--o o-----o o--o |
| | | | | | | |
| | | B | A | | zS | (zS)(z(KK)) |
| o-----o o--o o--o [5]---------[7] |
| | | | | |
| | | | z | z(KK) |
| o-----------o o--------o |
| | | |
| | K | KK |
| o--------------------------o |
| | |
| | K |
| @ |
| |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
| |
| A B A C A B A C |
| o--o o--o o--o o--o x(y(K(((zS)(z(KK)))S))) |
| | | | | |
| | | B | B | y(K(((zS)(z(KK)))S)) |
| o-----o o--o o--o |
| | | | |
| B | | K | K(((zS)(z(KK)))S) |
| o--o o---------o |
| | | |
| | (zS)(z(KK)) | ((zS)(z(KK)))S |
| [7]--------------o |
| | |
| | S |
| @ |
| |
o=====================================================================o
| |
| x(y(K((z(S((KK)S)))S))) |
| |
| A B A C |
| o--o o--o |
| | | |
| A B A C A B A C | | |
| o--o o--o o--o o--o o-----o |
| | | | | | |
| A B A C | | B C | | B | |
| o--o o--o o-----o o--o o-----o o--o |
| | | | | | | |
| | | B | A | | | |
| o-----o o--o o--o o-----------o |
| | | | | |
| | | | | |
| o-----------o o--------o |
| | | |
| | K | KK |
| o-------------------------[8] |
| | |
| | K |
| @ |
| |
| A B A C A B A C |
| o-o o-o o-o o-o |
| | | | | |
| A B A C | | B C A B A C B C | | |
| o-o o-o o----o o-o o-o o-o o-o o----o |
| | | | | | | | | |
| B C | | B | A | | | A | B | |
| o-o o----o o-o o-o o----o o-o o-o |
| | | | | | | | |
| A | | | | | | z | z(S((KK)S)) |
| o-o o--------o o------o o----[9] |
| | | | | |
| | | | S | S((KK)S) |
| o------o o---------------o |
| | | |
| | KK | (KK)S |
| [8]-------------------------o |
| | |
| | S |
| @ |
| |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
| |
| A B A C A B A C x(y(K((z(S((KK)S)))S))) |
| o--o o--o o--o o--o |
| | | | | |
| | | B | B | y(K((z(S((KK)S)))S)) |
| o-----o o--o o--o |
| | | | |
| B | | K | K((z(S((KK)S)))S) |
| o--o o--------o |
| | | |
| | z(S((KK)S)) | (z(S((KK)S)))S |
| [9]--------------o |
| | |
| | S |
| @ |
| |
o=====================================================================o
| |
| x(y(K((z(S((KK)S)))(z(SK))))) |
| |
| A B A C |
| o--o o--o |
| | | |
| A B A C A B A C | | |
| o--o o--o o--o o--o o-----o |
| | | | | | |
| A B A C | | B C | | B | |
| o--o o--o o-----o o--o o-----o o--o |
| | | | | | | |
| | | B | A | | | |
| o-----o o--o o--o o-----------o |
| | | | | |
| | | | | |
| o-----------o o--------o |
| | | |
| | K | KK |
| o-------------------------[8] |
| | |
| | K |
| @ |
| |
| A B A C A B A C |
| o-o o-o o-o o-o |
| | | | | |
| A B A C | | B C A B A C B C | | |
| o-o o-o o----o o-o o-o o-o o-o o----o |
| | | | | | | | | |
| B C | | B | A | | | A | B | |
| o-o o----o o-o o-o o----o o-o o-o |
| | | | | | | | |
| A | | | | | | z | z(S((KK)S)) |
| o-o o--------o o------o o----[9] |
| | | | | |
| | | | S | S((KK)S) |
| o------o o---------------o |
| | | |
| | KK | (KK)S |
| [8]-------------------------o |
| | |
| | S |
| @ |
| |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
| |
| x(y(K((z(S((KK)S)))(z(SK))))) |
| ^ |
| A B A C A B A C | |
| o-o o-o o-o o-o |
| | | | | |
| A B A C A B A C | | B | B | |
| o-o o-o o-o o-o o---o o-o o-o |
| | | | | | | | |
| | | B | B | B C B | | K | K((z(S((KK)S)))(z(SK))) |
| o---o o-o o-o o-o o-o o----o |
| | | | | | | |
| B | | | A | | | (z(S((KK)S)))(z(SK)) |
| o-o o----o o-o [9]-------o |
| | | | | |
| | | | z | z(SK) |
| o--------o o-----o |
| | | |
| | S | SK |
| o------------------o |
| | |
| | K |
| @ [9] = z(S((KK)S)) |
| |
o=====================================================================o
| |
| x(y(K(z((S((KK)S))((SK)S))))) |
| |
| A B A C |
| o--o o--o |
| | | |
| A B A C A B A C | | |
| o--o o--o o--o o--o o-----o |
| | | | | | |
| A B A C | | B C | | B | |
| o--o o--o o-----o o--o o-----o o--o |
| | | | | | | |
| | | B | A | | | |
| o-----o o--o o--o o-----------o |
| | | | | |
| | | | | |
| o-----------o o--------o |
| | | |
| | K | KK |
| o-------------------------[8] |
| | |
| | K |
| @ |
| |
| A B A C A B A C |
| o-o o-o o-o o-o |
| | | | | |
| A B A C | | B C A B A C B C | | |
| o-o o-o o----o o-o o-o o-o o-o o----o |
| | | | | | | | | |
| B C | | B | A | | | A | B | |
| o-o o----o o-o o-o o----o o-o o-o |
| | | | | | | | |
| A | | | | | | | |
| o-o o--------o o------o o-----o |
| | | | | |
| | | | S | S((KK)S) |
| o------o o-------------[10] |
| | | |
| | KK | (KK)S |
| [8]-------------------------o |
| | |
| | S |
| @ |
| |
| A B A C A B A C |
| o-o o-o o-o o-o |
| | | | | |
| A B A C A B A C | | B | B | |
| o-o o-o o-o o-o o---o o-o o-o |
| | | | | | | | |
| | | B | B | B C B | | | |
| o---o o-o o-o o-o o-o o----o |
| | | | | | | |
| B | | | A | | | |
| o-o o----o o-o o--------o |
| | | | | |
| | | | | |
| o--------o o-----o |
| | | |
| | S | SK |
| o----------------[11] |
| | |
| | K |
| @ |
| |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
| |
| A B A C A B A C A B A C A B A C x(y(K(zG))) |
| o-o o-o o-o o-o o-o o-o o-o o-o |
| | | | | | | | | |
| | | B | B | B C | | B C B | B | y(K(zG)) |
| o---o o-o o-o o-o o---o o-o o-o o-o |
| | | | | | | | | |
| B C B | | | A | B | A | | K | K(zG) |
| o-o o-o o----o o-o o-o o-o o----o |
| | | | | | | | |
| A | | | | | | z | zG |
| o-o o--------o o----o o-----o |
| | | | | |
| | | | F | G |
| o-----o [10]---------o |
| | | |
| | SK | (SK)S |
| [11]--------------------o |
| | |
| | S F = S((KK)S) |
| @ G = F((SK)S) = (S((KK)S))((SK)S) |
| |
o=====================================================================o
| |
| x(y((z(KK))(z((S((KK)S))((SK)S))))) |
| |
| B C A B |
| o---o o---o |
| | | |
| A B A | B | |
| o---o o---o o---o |
| | | | |
| B | | z | z(KK) |
| o---o o---------[12] |
| | | |
| | K | KK |
| o-----------o |
| | |
| | K |
| @ |
| |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
| |
| x(y((z(KK))(zG))) |
| ^ |
| A B A C A B A C A B A C A B A C | |
| o-o o-o o-o o-o o-o o-o o-o o-o |
| | | | | | | | | |
| | | B | B | B C | | B C B | B | y((z(KK))(zG)) |
| o---o o-o o-o o-o o---o o-o o-o o-o |
| | | | | | | | | |
| B C B | | | A | B | A | | | (z(KK))(zG) |
| o-o o-o o----o o-o o-o o-o [12]--o |
| | | | | | | | |
| A | | | | | | z | zG |
| o-o o--------o o----o o-----o |
| | | | | |
| | | | F | G |
| o-----o o-----------o |
| | | |
| | SK | (SK)S |
| o----------------------o |
| | |
| | S F = S((KK)S) |
| @ G = F((SK)S) = (S((KK)S))((SK)S) |
| |
o=====================================================================o
| |
| x(y(z((KK)(((S((KK)S))((SK)S))S)))) |
| |
| B C A B |
| o---o o---o |
| | | |
| A B A | B | |
| o---o o---o o---o |
| | | | |
| B | | | |
| o---o o-----------o |
| | | |
| | K | KK |
| o---------[13] |
| | |
| | K |
| @ |
| |
| A B A C A B A C A B A C A B A C |
| o-o o-o o-o o-o o-o o-o o-o o-o |
| | | | | | | | | |
| | | B | B | B C | | B C B | B | |
| o---o o-o o-o o-o o---o o-o o-o o-o |
| | | | | | | | | |
| B C B | | | A | B | A | | | |
| o-o o-o o-----o o-o o-o o-o o-----o |
| | | | | | | | |
| A | | | | | | | |
| o-o o---------o o-----o o-----o |
| | | | | |
| | | | S((KK)S) | (S((KK)S))((SK)S) |
| o-----o o-------------[14] |
| | | |
| | SK | (SK)S |
| o--------------------------o |
| | |
| | S |
| @ |
| |
| . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . |
| |
| A B A C B C A B B C A C |
| o--o o--o o--o o--o o--o o--o |
| | | | | | | |
| B C B | B | A | B | A | B | |
| o--o o--o o--o o--o o--o o--o o--o |
| | | | | | | | |
| A | | | | | | | |
| o--o o--------o o--------o o--------o |
| | | | | |
| | | | KK | T |
| o--------o [13]--------------[o] |
| | | |
| | (S((KK)S))((SK)S) | ((S((KK)S))((SK)S))S |
| [14]------------------------o |
| | |
| | S |
| @ T = (KK)(((S((KK)S))((SK)S))S) |
| |
o---------------------------------------------------------------------o
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