Type Labels II
12/19/09
Extending the notation
At first site, having an equivalence between types (lower case letters a..v) and monadic predicates (upper case A..V) might seem limiting. But it can be extending to a degree by introducing definitions for more complex single variable predicates. For example, say you have
(Mx∧Dx)⊃Nx (*notice the free variable x*)
as a fancier category (those things which if they are M and D are also N), then you could introduce a monadic predicate definition for this, via an equivalence eg