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

[Jon Awbrey]

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

PAT.  Note A18

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

Transposition, or the Transposer (cont.)

Step 4.

The construction of the term T of the appropriate type in terms of the
primitive typed combinators of the forms K and S is analogous to the
proof of the corresponding proposition from the intuitionstic axiom
schemes attached to those forms.

Incidentally, note the inobtrusive appearance of renaming strategies in the
progress of this work.  Renaming is the natural operation that substitution
is the reverse of.  With these humble beginnings we have reached a birthplace,
a native ground, of the sign relation, an irreducible three-place relationship
among what is indicated, what happens to indicate it, and all the equivalent
or associated indications we may find or create in reference to it.

For example, let "G", the interposed interpretant,
denote whatever it is, the supposed object, that
"(F((SK)S))", the occurrent sign, denotes.

Jon Awbrey

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