The theory of homogeneous simple types as a second-order logic.
Nino B. Cocchiarella · Notre Dame Journal of Formal Logic · 1979
In its original form the theory of simple types, hereafter called ST, is a theory of predication and not, or at least not primarily, a theory of membership.With that original form in mind we construct in this paper* a second order counterpart of ST which we call ST*.We briefly compare ST* with an alternative extension of second order logic, viz., the author's system T*(*) of [1], which was proposed as characterizing the original (and yet consistent!) logistic background of Russell's paradox of predication.In [2], the author showed the completeness of T**, plus an extensionality axiom (Ext*), relative to a Fregean interpretation of subject-position occurrences of predicates, viz., that such occurrences of predicates denote individuals correlated with the properties (or ''classes") designated by predicate-position occurrences of the same predicates.It is observed here that when the semantical Fregean frames characterized satisfy ST*'s stratified comprehension principle instead of T**'s general comprehension principle, then the same Fregean interpretation yields a completeness theorem for monadic ST* + (Ext*) as well.It has been found convenient, on the other hand, to consider (monadic) ST as a theory of membership rather than a theory of predication when axioms of extensionality are included in its characterization.So considered, Quine proposed his system NF as a first order counterpart of ST, though of course, as is well-known, NF far exceeds ST in deductive powers.We show here per contra that while (monadic) ST* + (Ext*) is motivated in its construction along lines followed by Quine in the construction of his first order counterpart NF, viz., the reduction of ST's metatheoretic feature of typical ambiguity to a stratified comprehension principle, our system, unlike NF, is equiconsistent with ST.This, along with the fact that the non-abstract individuals (or "urelements") of ST are retained unmodified in ST*, indicates that