nLab
predicative mathematics

Context

Foundations

Mathematics

Predicative mathematics

Idea

Predicative mathematics is a way of doing mathematics without allowing impredicative definitions.

Informally, a definition is impredicative if it refers to a totality which includes the thing being defined. For example, the definition of a particular real number xx as the least upper bound of a given set AA is impredicative, because it characterizes xx as a particular element of some set (the upper bounds of AA) which includes xx. Possibly xx can be defined in some other way and then proved to be the least upper bound of AA, but to define it thus by fiat is impredicative.

There are (at least) two broad schools of the foundations of predicative mathematics that don't talk much to each other: one school that uses lower-order forms of higher-order logic (or the set theory that this justifies) and classical logic, and a constructive school that uses first-order type theory (or the set theory that this justifies) and intuitionistic logic. The common ground is that both schools reject power sets; other axioms may vary. Here we tend to think of what predicative mathematics allows the category of sets to be.

Constructive predicativists sometimes accept principles (such as function sets and the axiom of replacement) that classical predicativists must reject because they imply impredicative results using excluded middle. Such mathematics may be called weakly predicative.

Impredicative axioms

Not all of these axioms are rejected by all predicativists, but they at least come under some suspicion.

Infinity

The axiom of infinity is not usually considered impredicative, but we list it anyway, as it is needed for the others to have force. Mathematics that does not require this axiom, finite mathematics, can be interpreted in a predicative framework even if it uses many of the axioms below.

Power set

The axiom that any set has a power set is perhaps the fundamental feature missing from predicative mathematics. In particular, the sequence

N,𝒫N,𝒫𝒫N, \mathbf{N}, \mathcal{P}\mathbf{N}, \mathcal{P}\mathcal{P}\mathbf{N}, \ldots

may be accepted in part, but not forever.

The failure of the power set axiom means that the category of sets is not an elementary topos.

Unbounded separation

The constructive school generally accepts the axiom of replacement but not unbounded forms of the axiom of separation. (This choice is not available to the classical school, since replacement and excluded middle together imply full separation.)

Naïvely, the axiom of separation says that, if AA is a set and PP is a function from AA to the set of truth values, then there is a set

{AP}={xAP(x)}. \{ A | P \} = \{ x \in A \;|\; P(x) \} .

To be precise, however, this PP should be written as a predicate in the language of set theory. The form of separation justified by type theory and such structural set theories as ETCS requires the quantifiers in this predicate to be guarded by sets; unbounded separation is the generalisation of this to arbitrary quantifiers.

Arguably, the impredicative core of both separation and power sets (in the presence of bounded separation) is limited separation: separation in which the quantifiers in PP may be guarded by power classes.

We need more on this, particularly with regards to the classical school and replacement.

Function sets

One sometimes speaks of forbidding function sets instead of power sets. That is, it is the sequence

N,N N,N N N, \mathbf{N}, \mathbf{N}^{\mathbf{N}}, \mathbf{N}^{\mathbf{N}^{\mathbf{N}}}, \ldots

that is avoided.

Of course, function sets can be constructed out of power sets (using bounded separation), so forbidding function sets certainly forbids power sets. The converse holds if there is a set Ω\Omega of truth values.

With excluded middle, the set of truth values is easy to achieve, as {0,1}\{0,1\}; in particular, if you have N\mathbf{N}, then you certainly have Ω\Omega. So the classical school of predicativism rejects function sets.

The constructive school, however, often accepts function sets (thus being weakly predicative). In this school, the sequence above is fine. Actually, the slightly stronger axiom of subset collection is adopted by Peter Aczel's CZFCZF and justified by Per Martin-Löf's ITTITT.

Brouwer, on the other hand, did not accept the sequence above, although his followers differ on when (if ever) it stops.

Excluded middle

Classical predicativists of course accept excluded middle; otherwise they would be constructivists. But from the perspective of weakly predicative constructive mathematics, excluded middle is impredicative, since it implies power sets (given function sets) and unbounded separation (given replacement).

Ill-founded structures

Most foundations of mathematics are predicative in one sense: no set may belong to itself. This (or rather, a certain strengthening of this) is the axiom of foundation. An alternative is the axiom of antifoundation, which explicitly allows for and tames such sets as \bullet, where ={}\bullet = \{\bullet\}. Indeed, this equation is a perfectly good way to define \bullet using antifoundation, yet this is about as impredicative as a definition can get.

Once one accepts the axiom of infinity, there's not much objection to accepting more general inductive types; these are sets that are defined recursively much like a natural numbers object. Categorially, we may see these as initial algebras of certain functors on SetSet. Coinductive types, which are the final coalgebras of these functors, also exist in impredicative theories, but not predicatively.

Polymorphic definitions

A different sort of impredicativity is to be found in some type theories, in which, roughly speaking, one is allowed to define “functions” whose “domain” is the class of all types. For instance, one might be able to form a type called α:Type,αα\forall \alpha:Type, \alpha\to\alpha, which has the property that an inhabitant of that type is a “function” which assigns to every type α\alpha, an endomorphism of α\alpha. This is clearly impredicative, since the type α:Type,αα\forall \alpha:Type, \alpha\to\alpha is also a possible value of α\alpha.

The philosophy behind this sort of impredicative definition is that any inhabitant of such a type must be defined “uniformly” enough that it uses no details about the type α\alpha, and thus can equally well be applied to any α\alpha. For instance, consider the operation which assigns to every α\alpha the identity id:ααid\colon \alpha\to\alpha; this is defined in exactly the same way for every α\alpha, and hence inhabits the type α:Type,αα\forall \alpha:Type, \alpha\to\alpha.

This sort of impredicativism can be shown to be incompatible with impredicative set-theoretic axioms such as power sets; see this paper of Andy Pitts. Since such type theories generally do have function types, it follows that they cannot be classical.

The category of sets

So what is the category of sets in predicative mathematics?

At bottom, let us suppose that SetSet is a Heyting pretopos; this is a category whose internal logic is first-order and contains only constructions that don't require any of the above axioms.

Since we're not doing finite mathematics, we may also include a natural numbers object. In fact, we could include more general inductive types, since these are no harder to justify philosophically than N\mathbf{N}, although the proofs that these exist if N\mathbf{N} does rely on possibly impredicative axioms. Then SetSet is a Heyting WW-pretopos.

If you accept function sets, then SetSet is locally cartesian closed and thus a Π\Pi-pretopos. In this case, N\mathbf{N} is enough to get all WW-types, so we have a Π\Pi-WW-pretopos. If you accept excluded middle, then SetSet is a Boolean pretopos or even a Boolean WW-pretopos. But a Boolean Π\Pi-pretopos is necessarily a topos, which would make the theory impredicative.

However, SetSet is still a Grothendieck topos, defined as a category of sheaves or in terms of Giraud's characterisation. We require the existence of power sets to prove the theorem that such a category is an elementary topos, so predicatively a Grothendieck topos may not be an elementary topos at all.

The real numbers

An important question in predicative mathematics is the status of the set R\mathbf{R} of real numbers. This set is often constructed as a subset R DR_D of 𝒫N\mathcal{P}\mathbf{N} or as a subquotient R CR_C of N N\mathbf{N}^{\mathbf{N}}, neither of which can be formed in an arbitrary Heyting WW-pretopos. The latter can be formed in a Π\Pi-WW-pretopos, but it is not necessarily correct.

The constructive school of predicativism can construct R\mathbf{R} in various ways. One method is to use R CR_C directly, but this will only go so far unless something is done to prove that it is Dedekind-complete. This will follow from weak countable choice (WCCWCC), which is accepted by most constructive schools. Using subset collection, a variation on R CR_C is possible which can be proved Dedekind-complete without WCCWCC; this is very natural from the perpective of type theory (but then, countable choice is also very natural from that perspective).

It is also possible to assert the existence of R\mathbf{R} by fiat, much like N\mathbf{N} exists by the axiom of infinity. This is the approach taken by the classical school; they use 𝒫N\mathcal{P}\mathbf{N} instead of R\mathbf{R} directly, but these are isomorphic by excluded middle. This is natural from the perspective of predicative set theory as a weak form of higher-order logic; you assert the existence of N\mathbf{N}, 𝒫N\mathcal{P}\mathbf{N}, and maybe 𝒫𝒫N\mathcal{P}\mathcal{P}\mathbf{N}, then stop.

There is also the question of what exactly it means to say that R\mathbf{R} exists; is it a set or a proper class? Without function sets, the distinction between these is not clear-cut; higher-order logic suggests a hierarchy of more and more proper (less and less small) classes rather than a single unified notion of set and class. If you allow N\mathbf{N} only as a proper class, then you are basically still doing finite mathematics; if you allow R\mathbf{R} only as a proper class, then you are doing predicative mathematics.

Formalising mathematics

How much of mathematics can be done predicatively?

A surprisingly large amount of mathematics can be formalised, using various coding tricks, in a theory in which N\mathbf{N} is a set but 𝒫N\mathcal{P}\mathbf{N} is a proper class. This is somewhat easier in Nik Weaver?'s ‘conceptualist’ approach, which accepts 𝒫𝒫N\mathcal{P}\mathcal{P}\mathbf{N} as a proper class (so that 𝒫N\mathcal{P}N and \mathbb{R} are small); the encoding is not really more complicated than what is usually done in material set theory for ordered pairs and the like. Note that these are conservative over Peano arithmetic? (PAPA); that is, anything expressible in PAPA and provable in these systems is provable in PAPA (which certainly cannot be said of ZFC or ETCS, which prove the consistency of PAPA).

Constructive mathematics generally requires great care with anything after the middle of the 19th century other than basic discrete mathematics, but requiring it to be predicative does not usually add much difficulty, as long as function sets are allowed. This even extends to category theory, which is not usually contemplated in the classical approach. (However, the internal logic of a Π\Pi-WW-pretopos is certainly not conservative over PAPA; it already proves consistency of the latter.)

References

Discussion of predicative toposes is in

Discussion

Mike: Is there a formal definition of “impredicative” other than “whatever predicativists don’t like?” In particular, I don’t understand why exponentials are any less problematic than power sets. If I have the set B AB^A, can’t I then use it to define a new function ABA\to B in terms of this set that contains the function being defined?

Toby: Arguably, Brouwer's school doesn't accept exponentiation, although they accept some cases of it (such as N NN^N). I've never heard them call it ‘impredicative’, however. Someday I want to figure out how much can be done using both W-types and co-W-types (equivalently, final coalgebras of polynomial functors) but not exponentiation. (So far, I can construct A NA^N as the final coalgebra of XA×XX \mapsto A \times X, but I can't prove that it is A NA^N!)


This discussion began at Grothendieck topology:

Mike: The passage from a collection of covering families (“coverage”) to a collection of sieves (“Grothendieck coverage”) is a higher-order construction. One thing this means is that you can’t do it if you happen to be a predicativist; thus to study “predicative sheaves” you need to use covering families instead of sieves. Another thing it means, which I care more about, is that many common coverages can be discussed in the first-order language of a category, while the corresponding Grothendieck coverages require an external set theory. For instance, I can say “a pretopos is a stack for its coherent coverage” in the first-order language of a category, but not if I replace “coverage” by “Grothendieck coverage.”

Toby: If you're going to be a predicativist, then you really have to take the attitude that a structure is defined by an arbitrary family of sets, and the closure conditions can be used afterwards (if the concept is really susceptible to predicativist understanding) to define equivalence of structures. (Note that a ‘family of subsets’ of XX is equivalent to an index set II and a single subset of I×XI \times X.)

For example, define a topological space to be a set equipped with an arbitrary family of subsets, called ‘subbasic open sets’. Define an ‘open set’ to be a subset whose every point belongs to the intersection of some finite family of subbasic open sets. Define two topologies on a given set to be equivalent if every subbasic open set in either is open in the other. All of this is predicative.

Actually, if you want to be finitist (in the sense that you have no axiom of infinity and hence no language to state that a family is ‘finite’) as well, then you must be subtler. Define a topological space to be a set equipped with a family of subsets (now called ‘basic open sets’) such that nullary and binary intersections of basic open sets are basic open sets (or at least always contain one). Define an ‘open set’ to be a subset whose every point belongs to some basic open set. Define equivalence as before.

These justify the importance of the concepts of ‘basis’ and ‘subbasis’ for a topology, taught in schools today. Perhaps there is a similar justification for ‘coverage’? (Or for ‘Grothendieck pretopology’, for that matter?)

Mike: Okay, well, I retract my comment about predicativism, since it is clear that I don’t understand (nor, really, care much about) predicative math. But my other comment about being first-order still stands.

Toby: I'd hoped that my example might give predicatvism (at least in the sense of not having a small set of truth value) some interest. I expect that it's related to being first-order and internalisable; after all, the internal logic of many categories is predicative, and rejecting power sets may be seen as an attempt to do all of mathematics in a first-order way. Ah, well.

Mike: Perhaps we should move the discussion about predicativity to predicativism? (Feel free to do so, snipping out the relevant paragraphs of my responses, if you like.) I also once had the thought that predicative math was interesting because of the internal logic of non-toposes. However, I have not encountered any naturally occurring examples (relative to classical mathematics) of, say, locally cartesian closed pretoposes which are not actually toposes. I am not a philosophical constructivist. I like constructive proofs for the same reason I like to prove things about arbitrary rings rather than about the integers: the result is more general and applies in more contexts. Toposes (of sheaves, usually) arise naturally in classical mathematics, so it is a good thing to know what proofs can be interpreted internally in a topos. If I knew a similar class of locally cartesian closed pretoposes that arose naturally in classical mathematics, I would be more favorably inclined towards predicativism.

Toby: Philosophically, I'm a pluralist, so I also like constructivism (in the sense of Bishop, without classically false axioms) for its wider applicability. And I even like mathematics with classically false axioms as much (potentially) as classical mathematics and wish it were more fully developed. But while you might be interested in such mathematics only if the categories that it can be internalised in come up in actual mathematical practice, it's enough for me if it comes up in actual philosophical practice; that is, if there is a school of constructivists interested in working with certain restrictions and axioms, then I'm interested in knowing what mathematics might apply there, and I try to do mathematics so that it will apply there.

(To be honest, I almost convinced myself that I'm interested, for their own sake as the ‘right’ way to do things, in foundations that amount to working in a locally cartesian closed pretopos whose category of lex endofunctors has enough injectives, but as soon as I got as far as figuring that out, I got onto something else.)

I hope that predicativism can still tell us something about how “a pretopos is a stack for its coherent coverage” works where “a pretopos is a stack for its coherent Grothendieck coverage” doesn't. But it's already enough to interest me in predicativism that there are predicativists.

Mike: Fair enough. I can understand that, even if it’s not my philosophy.

Actually, on further reflection, it’s not really accurate to say that I don’t care about predicativism. It’s the specific variety of predicativism that accepts things like exponentials, W-types, fullness, and/or collection, but not power sets, that I have trouble justifying. Because I do care about what can be made first-order, I care about the internal logic of a Heyting category, which could be called “even more” predicative; I’m just not used to giving it that label. And the category of classes in a membership-based set theory is a good example of a positive Heyting category that doesn’t even have exponentials.

Toby: I care about that too, and since predicativism in practice is a vague term that might not allow exponentials either (as Brouwer didn't), the practice might still be wroth examining for that purpose. But that is not something that can be established theoretically, so I'll just use any useful examples that I see, and leave it at that.

Mike: I realized that there is a class of locally cartesian closed extensive Heyting categories that I care about: extensive quasitoposes. I used to believe that the correct internal logic of a quasitopos used the fibration of regular subobjects, rather than the fibration of all subobjects, but that logic is kind of poorly behaved, for instance it doesn’t satisfy function comprehension (if you prove that for all aAa\in A there exists a unique bBb\in B such that blah, then all you get is a span ACBA\leftarrow C\to B where CAC\to A is monic and epic). Quasitoposes are always locally cartesian closed Heyting categories, and I think it’s fair to say that all the interesting ones are extensive as well.

Any quasitopos that is a pretopos is in fact a topos, so I still don’t know any interesting locally cartesian closed pretoposes that aren’t toposes. One could take the ex/reg completion of an extensive quasitopos to get an interesting pretopos, but I don’t know whether it would still be locally cartesian closed. But any locally cartesian closed Heyting category has an internal logic which is predicative with exponentials. I wonder which quasitoposes have W-types and stuff like that.

Mike: Also, the ex/lex completion takes extensive categories to pretoposes and preserves local cartesian closedness. So, in particular, the ex/lex completion of a topos is locally cartesian closed pretopos which is not, in general, a topos. I’m not sure what interesting categories of this sort there are.

Todd: Interesting discussion. Just wanted to add that I’d recently been thinking about small-colimit completions of toposes, which are examples of ex/lex completions of toposes that are (seemingly) almost never toposes.

Revised on March 9, 2014 08:55:12 by Toby Bartels (98.23.139.218)