Negative Type Theory
Stephen Simpson repeatedly talks about certain subsystems of second-order arithmetic as ‘natural’ or as ‘arising naturally’ (SOAS, e.g. pp. 33, 43, etc.). In a similar context, John Burgess contrasts ‘artificial examples’ with ‘theories that it is natural to consider’ (Fixing Frege, p. 54). But what idea of naturalness is at work here? There’s more than one sort of naturalness that can be in play when we talk about mathematical theories. Which is a trite point, but which bears some discussion. In fact, there’s a number of things to be said. But here’s a nice case which is perhaps relatively unfamiliar but which very vividly illustrates one basic, preliminary, distinction we need to draw.
As background, recall the structure of a simple theory of types. The entities in its universe are divided into levels. At level 0, there are individuals. At level 1, there are sets of individuals. Then at level 2, sets of level 1 sets; at level 3, sets of level 2 sets; and so on up an unending but non-cumulative hierarchy. The two key principles structuring this hierarchy are an extensionality principle for sets,and a comprehension principle to the effect that given any condition satisfied by zero or more level n − 1 entities, there exists a level n set containing just those entities.
Now, to get an interesting system in which we can actually do some mathematics, we’ll also need to add a third independent principle governing the hierarchical universe, an axiom of infinity which tells us that there is an infinite set. And why do we need a substantive axiom of infinity? Because, to labour the obvious point, there are only a finite number of predecessor levels below any given level in the hierarchy. So if there are only finitely many individuals at ground level, then – although the population at each succeeding level grows exponentially – when we reach the given level the population need still only be finite.
So far, all so very familiar. But the alert mathematician might pick up on the point I’ve just laboured, and wonder whether we can’t after all get a type theory which guarantees infinitely populated levels by changing our structural assumptions about the levels, and imagining the hierarchy continuing infinitely downwards as well as upwards.
So now think of the denizens of level 0, and the lower levels, as more sets. It is easy to see that comprehension alone will guarantee an infinite population at every level.For example, comprehension guarantees that there is an empty set ∅n at level n. And so, at level zero, again by comprehension, there are all the following sets: ∅0 , {∅−1 }, {{∅−2 }}, {{{∅−3 }}}, . . . , which by extensionality are all distinct. So we’ve conjured infinite populations just out of the structure of the hierarchy, without making any additional substantive assumption. We’ve shown how to get more out of less.
Now, that is indeed very cute! And, after all, if we are considering a typed universe, with the levels indexed by N, what – in one good sense – is more natural than to explore by way of contrast, on the one hand, a restricted universe with only a finite number of levels and, on the other hand, a richer universe with the levels indexed by Z? These formal variants on a standard simple theory of types immediately suggest themselves for mathematical investigation. But while the idea of a ‘negative type theory’ is a formally natural one – and there is indeed some fun to be had exploring the resulting theory, which can readily be proved consistent – it is of course conceptually highly artificial. For the original idea of a type hierarchy, after all, involved the conception of building from the ground up by repeatedly applying an operation of set-formation. Remove the distinguished ground level and it seems that we can make no conceptual sense of what is supposed to be going on in the resulting hierarchy. And we can make even less sense of the theory when we find e.g. that, by a little theorem of Thomas Forster (1989), all its models are nonstandard in the sense that the population of level n + 1 is not reliably of the expected standard size in a type theory, i.e. not the size of the power set of level n.
This lack of a clear conceptual motivation is presumably why Hao Wang, who first noted the possibility of a negative type theory in his (1952), calls it ‘a kind of curiosity’. So let’s take this as a cautionary tale, to illustrate the contrast we surely do need to draw between what we might call formal naturalness and conceptual naturalness. Or, as we might be tempted to put it in some cases, between purely mathematical and philosophical naturalness. Though note, talking the second way might suggest that we are presupposing that there’s a place for a ‘first philosophy’, critically assessing mathematics from outside. But that, I’d argue, is the wrong picture: conceptual naturalness is itself already one kind of mathematical virtue, well recognized in the actual practice of mathematicians.
It seems rather easy to be seduced by a Bourbarkiste fantasy, and to fall into thinking that mathematics – real mathematics – is, or ought to be, an entirely formal game, with theories evolving purely by linear deduction from definitions and axioms. But as Imre Lakatos, for one, reminds us, that isn’t how mathematics in fact proceeds. There is, rather, more of a to-and-fro between intuitive ideas, analogies, pattern-recognitions, informal proofs, and the development of sharpened concepts and the more rigorous proofs which deploy them (though sufficient unto the day is the rigour thereof ). The conceptually unnatural theories are the ones where, in the process of formalizing, we lose touch with, or distort too far, the informal mathematical ideas that were originally supposed to be guiding the theory-building. More on all this anon.