Representation of Functions and Total Antisymmetric Relations in Monadic Third Order Logic

We analyze the representation of binary relations in general, and in particular of functions and of total antisymmetric relations, in monadic third order logic, that is, the simple typed theory of sets with three types. We show that there is no general representation of functions or of total antisymmetric relations in this theory. We present partial representations of functions and of total antisymmetric relations which work for large classes of these relations, and show that there is an adequate representation of cardinality in this theory (a result already shown in a somewhat different way by Henrard in unpublished work, but our approach differs from his in providing representations of bijections between sets in a stronger sense). The relation of our work to similar work by Henrard (to whom we are indebted) and Allen Hazen (who arrived at related results independently) is discussed. This work can be understood as part of a program of assessing the capabilities of (relatively) weak logical frameworks: our results are applicable for example, to the framework in David Lewis’s Parts of Classes.