[Inquiry] Propositions As Types

[Jon Awbrey]

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

PAT.  Note 1

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

1.  Identity, or the Identifier

Step 1.

Given a syntactic specification (or paraphrastic definition):

   x = xI

where "x = x..." is the definiens,
or defining context, and "I" is
the definiendum,

Find a pure interpretant for I, that is, an equivalent term
in <<K, S>>, the combinatory algebra generated by K and S,
that does as I does.

Observe:

   x  =  (xK)(xK)  =  x(K(KS))

   =>

   I  =  K(KS)

and so K(KS) constitutes a syntactic algorithm for I.

Step 2.

Assign types in the specification:

   x_A  =  x_A I_(A=>A)

to arrive at a propositional typing for I : A => A,
whose type, read as a proposition, is a theorem of
intuitionistic propositional calculus.

Step 3 (optional).

Check that A => A is a theorem of classical propositional calculus.

   A   A
   o---o       o---o
   |           |
   @     =     @     =     @

Check.

Jon Awbrey

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