Interpretability of Robinson arithmetic in the ramified second-order theory of dense linear order.
Allen Hazen · Notre Dame Journal of Formal Logic · 1991
After a description of the ways in which predicative higher-order logic is thought too weak to be of interest, it is shown to be in some ways surprisingly rich: dense linear order, which has a decidable first-order theory, has an essentially undecidable theory in ramified second-order logic.Extensions of the main result are described and their philosophical significance briefly discussed.Although some claims have been made for the philosophical interest of predicative higher-order logics (Hacking [3], Hazen [4] and [5]), the general impression among mathematical logicians seems to be that systems like Ramified Type Theory are too complicated (in uninteresting ways) and too weak to be worth studying.It cannot be denied that these systems are, in some ways, extremely weak.As pointed out in Sundholm [8], Ramified Type Theory satisfies the hypotheses of Lindstrom's Theorem (these hypotheses could be summed up roughly as being that a completeness proof by Henkin's methods is possible for the logic, which was shown for Ramified Type Theory in Leblanc [6]), so that in one way its language has no more expressive power than that of first-order logic: if two possible worlds are not discriminated by any first-order sentence, then they will not be discriminated by sentences of a ramified higher-order language (based, in an appropriate sense, on the same primitive predicates) either.The significance of Lindstrom's Theorem, however, should not be overrated.There are other possible measures of the expressive power of a language.For example, first-order logic with predicate modifiers is, from the point of view of completeness theorems, only trivially different from ordinary first-order logic, but a predicate modifier language with a finite vocabulary may be able to define more subsets of the domain of a model than can be defined in any ordinary firstorder language with finitely many predicates, all definable in the first language: