PM’s Circumflex, Syntax and Philosophy of Types

Abstract

While second-order logic has its share of proponents, and specialized forms of type theory play a role in contemporary computer science and linguistics, I think it is fair to say that there’s relatively little contemporary interest in the sort of full-blown higher-order logic exemplified by the simple and ramified theories of types, at least for its own sake. One does not often see, for example, a new theory or development using it as its base system. The reasons for this are no doubt many. I think one major contributing factor, however, is a disconnect between the logicians who first advocated such an approach to logic and those who have been responsible for formulating it with modern standards of rigor. Principia Mathematica, remains, it is fair to say, the best known exemplar of a type-theoretic approach to logic, but exactly what its type-theory is is far from agreed-upon. Whitehead and Russell are accused of unclarity, sloppiness or even outright confusion with regard to the syntax of their language, their system’s axiomatic foundations, and even its philosophical justification. More recent formulations of simple and ramified type theories, such as those in Alonzo Church’s work, although formally unambiguous and irreproachable, are seen as idiosyncratic and needlessly restrictive ways of codifying the ‘iterative conception’ of sets or classes, more of a curiosity than a genuine rival to more flexible rival ways of codifying the same conception, such as ZFC and related set theories.