Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

January 23, 2011

Topos Theory Can Make You a Predicativist

Posted by Mike Shulman

Recall that predicative mathematics is mathematics which rejects “impredicative definitions,” and especially power sets. (Power sets are “impredicative” because you can say things like “let XX be the intersection of all blah subsets of SS” and proceed to prove that XX is itself blah; thus XX has been defined “impredicatively” in terms of a collection of which it is a member.) So it might seem odd to claim that topos theory can make you a predicativist, since the basic ingredient in the definition of an elementary topos is a power object.

However, I mean instead to refer to Grothendieck topos theory. This is usually regarded as a sub-field of elementary topos theory, since every Grothendieck topos is an elementary topos. But actually, that’s really only true if SetSet is itself an elementary topos! So if we were predicativists, we would instead say that SetSet is some kind of pretopos, and we would conclude instead that any category of sheaves is a pretopos of the same kind. Moreover, we could do lots of ordinary Grothendieck-topos-theory with these “Grothendieck pretopoi” (modulo the usual sorts of difficulties that come up in doing any sort of mathematics predicatively). So “Grothendieck topos theory” is, aside from the confusion of names, fully compatible with predicativism.

But how can Grothendieck topos theory make you a predicativist?

To be precise, it’s not really ordinary Grothendieck 1-topos theory that I’m referring to, but higher topos theory and lower topos theory. Just as a 1-topos (I’m going to drop the “Grothendieck” from now on), or (1,1)-topos, is a category of sheaves of sets on a site, and sets are 0-groupoids, so an (n,1)-topos is an (n,1)(n,1)-category of sheaves of (n1)(n-1)-groupoids on an (n,1)(n,1)-site. It’s established by now, due to the work of many people (but Jacob Lurie wrote a big book about it), that the theory of (n,1)(n,1)-topoi makes good sense for any 0n0\le n\le \infty, and mirrors the behavior of 1-topos theory in many ways (and improves on it in others).

In particular, that is so for n=0n=0. A (0,1)-topos is a (0,1)-category of sheaves of (-1)-groupoids on a (0,1)-site. There’s a nice description of this process at (0,1)-site; sheaves in this case are often called ideals.

However, when one starts to think about (n,1)(n,1)-topoi for arbitrary nn, one is struck by some curiously distinctive features of the case n=0n=0. Most of these arise from the fact that:

  • a (0,1)-topos, unlike an (n,1)(n,1)-topos, is an (essentially) small category. As a poset, it can be identified with a frame or a locale, depending on which direction one takes the morphisms as going.

And of course, this fact is a consequence of the power set axiom for SetSet. So if you think about these things a lot, you might start to wonder (as I have), why should the case n=0n=0 be different from all other values of nn? We’ve learned not to expect the (n+1)(n+1)-category of all small nn-categories to be itself a small (n+1)(n+1)-category for any value of n0n\ge 0; why should we expect it to be so for n=1n=-1?

By the way, the analogue for higher nn of the impredicative definition “let XX be the intersection of all blah subsets of SS” would be “let XX be the limit of the diagram of all blah presheaves on SS.” We know that a presheaf category is complete, but that only means that it has small limits, so if we don’t know that there are only set-many blah presheaves, that latter “definition” of XX is illegitimate. For instance, “let XX be the product of all (set-valued) presheaves on SS” is certainly illegitimate! So why should we expect to be able to say something analogous like “let XX be the intersection of all subsets of SS”? (Since a subset of SS is just a (-1)-groupoid-valued presheaf on SS.)

So that’s half of how topos theory can make you a predicativist: you might start wondering why we believe that the case n=0n=0 is special. The other half is that topos theory (and, really, category theory in general) can show you that often it doesn’t really matter whether or not n=0n=0 is special. When you first encounter predicativism, you might be shocked at the idea of not having a power set and thus not being able to do any of the familiar things with power sets. (I know I was.) But the negative-thinking approach suggests that that should be no more or less shocking than the idea of not having a category of all sets.

But, of course, we do have a category of all sets and we work with it all the time; it’s just a large category, which is itself a proper class instead of a set. Likewise, predicatively any set has a power class. In particular, when doing topos theory, we can work with frames and locales in the same way as before, except that they will no longer necessarily be small (0,1)-categories. Rather, they will just be assumed to have a small set of generators, just like we do for Grothendieck (n,1)(n,1)-topoi for all other values of nn. Yes, certainly, some things will get a bit more tedious, but they won’t come completely crashing down around our ears. This is, I believe, essentially what predicative mathematicians do under the name of formal topology.

Posted at January 23, 2011 8:26 PM UTC

TrackBack URL for this Entry:   http://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/2344

44 Comments & 2 Trackbacks

Re: Topos Theory Can Make You a Predicativist

Interesting. Simple as it is now that you say it, I had not been aware of this connection.

So what precisely do we do to set us up in the predicative context in which (0,1)(0,1)-sheaf toposes do show size behaviour analogous to (n,1)(n,1)-sheaf toposes for higher nn?

We

  • discard the power set axiom from the definition of SETSET;

  • and from the definition of Grothendieck universes.

Anything else we need/want to fine tune about our foundations?

Posted by: Urs Schreiber on January 23, 2011 11:40 PM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

Well, of course (as you probably know) we have to be a bit careful about what’s left when we “discard power sets.” For instance, if we start with “Set is a well-pointed category with finite limits and power objects and the axiom of choice” (one version of ETCS), and we discard power objects (and choice), we won’t be left with a very good definition of SetSet. The predicative version of ETCS says that SetSet is a well-pointed pretopos, possibly locally cartesian closed (depending on the sort of predicativist you are). There seems to be some debate about whether to use classical logic either, although if you want function sets then you have to use intuitionistic logic, since a cartesian closed Boolean category is an elementary topos.

But regarding the particular matter at hand, I believe that for the basic theory of Grothendieck (0,1)-toposes, it should be enough to just assume that SetSet is a well-pointed pretopos. Obviously we won’t be able to use the parts of topos theory that invoke subobject classifiers, but if we assume function sets in SetSet then we’d be able to use the parts that invoke cartesian closure.

Hmm, I just thought of another interesting connection between higher topos theory and predicativism. Subobject classifiers in 1-topoi generalize to “(truncated-)object classifiers” in (n,1)-topoi, except that for n>1n\gt 1 you can’t classify all objects, only some cardinality-bounded collection of them. So it might be reasonable to consider the claim that SetSet (and likewise any 1-topos) has, not a single subobject classifier, but a family of them which jointly “exhast all subobjects”. I think people have considered that sort of axiom before also, in the direction of “predicative elementary topos”. (Similarly, I believe the proof that an (n,1)-topos has object classifiers uses the existence of arbitrarily large regular cardinals, which is not a theorem constructively but has to be taken as an additional axiom.)

Posted by: Mike Shulman on January 24, 2011 12:14 AM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

The moment you said this here:

Obviously we won’t be able to use the parts of topos theory that invoke subobject classifiers,

I had this very same thought:

Subobject classifiers in 1-topoi generalize to “(truncated-)object classifiers” in (n,1)(n,1)-topoi, except that for n>11n \gt 11 you can’t classify all objects, only some cardinality-bounded collection of them.

So maybe the axioms of elementary toposes deserve some refinement after all:

So it might be reasonable to consider the claim that Set (and likewise any 1-topos) has, not a single subobject classifier, but a family of them which jointly “exhast all subobjects”.

That sounds like it would make a lot of things fall nicely into place.

That reminds me, I need to think about and understand explicit descriptions of kk-truncated object classifiers in more general (n,1)(n,1)-toposes than (n1)Grpd(n-1)Grpd. Have you thought about that?

Posted by: Urs Schreiber on January 24, 2011 1:15 AM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

I realize that probably we wouldn’t get all that far without function sets, since otherwise SetSet isn’t locally small or complete, we don’t have a good adjoint functor theorem, and our geometric morphisms probably don’t have right adjoint parts. I think a Π\Pi-pretopos with “object classifiers” has been studied by someone under a name like “stratified pseudo-topos”, but I can’t remember who it was at the moment.

I need to think about and understand explicit descriptions of k-truncated object classifiers in more general (n,1)-toposes

I would guess that it’s just something like, for each UU in the site CC, consider the category of k-sheaves on C/UC/U of cardinality below some bound. As UU varies that should form a (k+1)-sheaf on CC which is an object of the (n,1)-topos in question when n is sufficiently larger than k.

Posted by: Mike Shulman on January 24, 2011 5:05 AM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

I think a Π\Pi-pretopos with “object classifiers” has been studied by someone under a name like “stratified pseudo-topos”, but I can’t remember who it was at the moment.

Moerdijk and Palmgren

Posted by: Richard Garner on January 25, 2011 5:57 AM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

Right, thank you.

Posted by: Mike Shulman on January 25, 2011 6:27 AM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

Geometric logic also points in the direction of predicativism: the powerset construction is not geometric. This is a reason why many constructions in formal topology are, in fact, geometric. Steve Vickers has a program to restrict even to arithmetical universes.

Posted by: Bas Spitters on January 24, 2011 9:08 AM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

[I’ve picked this up very late, but I hope the comment is still of interest.]

I thank Bas for mentioning my programme. I want to elaborate on that by explaining how topos theory did make me a predicativist.

The realm of geometric logic is essentially that fragment of the internal mathematics of Grothendieck toposes that is preserved by the inverse image functors of geometric morphisms. (In fact that is pretopos structure + some other stuff, so this provides one answer to Mike’s original thought of Grothendieck toposes as being “some kind of” pretopos.)

The wonderful thing about this fragment is that if you use it to reason about points of a point-free space X, then the reasoning applies not only to global points (maps 1 -> X), of which there may be insufficient, but also to generalized points (maps W -> X) such as the generic point (Id: X -> X). This overcomes most of the disadvantages that arise from the insufficiency of points in a non-spatial space.

In short, if your reasoning is geometric you can deal with point-free spaces as though they had enough points.

This is a huge improvement on having to work explicitly with the frames or their presentations, and for a decade or two now I have been doing my best to work geometrically wherever possible.

Since geometric reasoning does not include powersets, I have found that that in effect makes me a predicativist and I have found it very easy to participate in predicative mathematics such as formal topology.

To repeat, topos theory did make me a predicativist.

Note that geometric reasoning does not even include exponentials (function types). This sounds terribly weak, but in practice there are ways round. One important observation is that the exponential of sets, although not another set, is a locale. What underlies this is that the exponential of sets has a natural topology that is non-discrete. You can see this very clearly if you think of equality of functions: it is of a different nature from the equality on the sets, and it is not open in the function space topology.

Bas also mentioned Joyal’s Arithmetic Universes. These are pretoposes equipped with parametrized list objects. The idea is that the infinitary disjunctions of geometric logic can (in practical examples) be eliminated in favour of finitary disjunctions and existential quantification over types such as N and Q constructible within AUs.

Here the lack of exponentials is impossible to fudge: they are not just absent from the logic, they are completely absent from the categories (AUs instead of Grothendieck toposes). Milly Maietti and I have started to explore how to work in these, in “An induction principle for consequence in arithmetic universes”.

Posted by: Steve Vickers on April 26, 2012 1:06 PM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

Does the predicative/impredicative distinction correspond to anything that a working mathematician, say, an analyst, might notice in their work, in the way that the constructive/nonconstructive distinction can make itself felt:

I hope that he [the sort of hard-nosed ‘working mathematician’ who regards logic like a disease] might…notice the fact that a constructively valid proof of a given theorem is generally more elegant than one which relies heavily on the law of excluded middle; constructivity is almost as much a matter of style as of logic. (Johnstone, Stone Spaces, xi)

Posted by: David Corfield on January 24, 2011 2:06 PM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

Yes. For example: given a set X, and a collection R of subsets of X, how do you construct the smallest topology making every subset in R open?

Predicative answer (“bottom-up”): take R. Throw in all unions of sets in R. Throw in all finite intersections. Throw in all unions. Throw in all finite intersections. Repeat (possibly transfinitely) until you have a topology.

Impredicative answer (“top-down”): consider the set of all topologies on X making every subset in R open. This set is closed under arbitrary intersection. So take the intersection of everything in it.

Posted by: Richard Garner on January 25, 2011 6:06 AM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

take R. Throw in all unions of sets in R. Throw in all finite intersections. Throw in all unions.

You're done now (and you could have skipped the first step about unions).

To generate a σ\sigma-algebra instead of a topology, however, that requires transfinite iteration in general.

Regardless, it's a great example, probably better than mine.

Posted by: Toby Bartels on January 25, 2011 6:37 AM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

You’re done now (and you could have skipped the first step about unions).

Although predicatively, what you’ve “got” now is a proper class rather than a set.

To generate a σ\sigma-algebra instead of a topology, however, that requires transfinite iteration in general.

In this case, I think each step should be a set if \mathbb{N} is exponentiable (which I suppose a predicativist who believes in classical logic might object to, since in classical logic any exponentiable set has a power set). But can one prove, predicatively, that the transfinite iteration converges in any sense? The nLab seems skeptical.

Posted by: Mike Shulman on January 25, 2011 6:51 AM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

But can one prove, predicatively, that the transfinite iteration converges in any sense?

One can prove this in mathematics which is predicative over ω 1\omega_1. I don't think that this weak level of predicativity is very popular (although what I wrote at the nnLab now sounds unduly pessimistic to me), but as we're just discussing the feel of predicativity here, I don't think that this matters very much.

Posted by: Toby Bartels on January 25, 2011 7:31 AM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

Good question. I think predicativity can also roughly be described under the heading of “constructive”, in the informal sense of “giving a construction”, even if it doesn’t necessarily imply intuitionistic logic. An impredicative definition like “let RR be the intersection of all equivalence relations containing SS” is certainly not as “constructive” a way to define RR as the predicative version “let xRyx R y mean that there is a finite sequence (x=x 0,x 1,,x n=y)(x=x_0,x_1,\dots,x_n=y) such that for all 0i<n0\le i\lt n, either x iSx i+1x_i S x_{i+1} or x i+1Sx ix_{i+1} S x_i.” In particular, a constructive predicative proof can often have an algorithm formally extracted from it via the Curry-Howard correspondence for λ\lambda-calculus or Martin-Löf type theory. So perhaps one answer is that predicativity may be noticed by someone trying to make their proofs effectively computable.

One could of course try to make the same argument for predicativity as Johnstone does for constructivity. I have to say that I find a lot of impredicative proofs and definitions more elegant than their predicative versions (to the extent that I occasionally waste time wishing that we could make (n,1)-toposes more like (0,1)-toposes, rather than the other way round), but others may disagree.

Posted by: Mike Shulman on January 25, 2011 6:17 AM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

Yes, constructive mathematics is elegant, while predicative mathematics is concrete; these don't always go together.

Posted by: Toby Bartels on January 25, 2011 6:46 AM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

Do note that while Martin-Löf type theory is predicative, there are impredicative type theories. For instance, anything in the line of System F (which includes the calculus of constructions, and typically extensions thereof) allows types like (T:Type).TT\forall (T : Type). T \to T, which is a type that quantifies over all types.

Coq, for instance, originally had an impredicative universe of types at its lowest level, and still has a switch for enabling it (such a universe is anti-classical, in that it can be used to prove ¬((P:Prop).P¬P)\neg (\forall (P : Prop). P \vee \neg P), though, so it’s off by default). Using such facilities, you can construct a data type that models a constructive set theory with a powerset operation:

dataZ:Set=con:(I:Type)(IZ)Zdata\, Z : Set = con : (I : Type) \to (I \to Z) \to Z

Where SetSet is Coq’s impredicative universe. This allows II to be instantiated to something like JPropJ \to Prop for some other index type JJ. So if a set s:Zs : Z is indexed by JJ, we can create a set indexed by its power type JPropJ \to Prop.

By contrast, something like Agda, based on Martin-Löf can build a similar type, but it must either be stratified, with the powerset of a Z iZ_i set living in Z i+1Z_{i+1}, or one must just ditch the powerset.

Posted by: Dan Doel on January 25, 2011 10:56 PM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

Coq, for instance, originally had an impredicative universe of types at its lowest level

Yes, I’ve always been somewhat intrigued by this. That sort of universe is actually even more impredicative than just having power sets; it seems to me to be more along the lines of making 1-toposes act like (0,1)-toposes.

To be more specific: it seems that what’s really impredicative is not power sets, but quantification over sets or subsets. So in particular, the set-theoretic axiom of unbounded separation is also impredicative. Power sets are only impredicative because power sets + bounded separation allows you to quantify over subsets, and not many people are willing to do away with bounded separation.

As I understand it, the impredicativity of Coq’s “impredicative Set” encompasses not just power sets, but also unbounded separation, and something even stronger. If we interpret the sort Prop as a subobject classifier, then from exponentiation we get power types, and the “impredicativity of Prop” means that in defining propositions we allow quantified variables ranging over types, which is like unbounded separation. Those sorts of impredicativity are, I believe, still there in the current version of Coq; what’s been turned off by default is something still stronger, saying something like “for any set A, there is a set of functions SetASet \to A.” Am I right about that?

I’ve always been curious how one shows that such an “anti-classical impredicative universe” is consistent; it seems quite a precarious assumption.

Posted by: Mike Shulman on January 26, 2011 4:02 AM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

The discussion is here.

In standard Coq you can write:
Definition id: Type := forall X:Set,X->X.

But you need the option -impredicative-set to write:
Definition id: Set := forall X:Set,X->X.

Please note the type of id. (Type is a universe containing Set).

Bas

Posted by: Bas Spitters on January 26, 2011 8:33 AM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

Yes, I’ve always been somewhat intrigued by this. That sort of universe is actually even more impredicative than just having power sets; it seems to me to be more along the lines of making 1-toposes act like (0,1)-toposes.

I’m afraid I don’t know enough to really comment on this. However, you did mention that (0,1)-toposes are in some sense small. I’ve been reading off and on about modelling type theory with fibred categories, and the book mentions how these sort of ‘products over all types’ cannot be modeled (other than trivially) by fibrations derived from Fam(C)Fam(C) over SetsSets, because products over the set of all objects in CC are ‘too big’ to live in CC itself. Perhaps that’s related somehow? Are (0,1)-toposes ‘small’ enough to have products indexed by their own collection of objects?

To be more specific: it seems that what’s really impredicative is not power sets, but quantification over sets or subsets.

This is certainly what gets directly labelled as impredicative in type theories: types that are defined via quantification over all types.

If we interpret the sort Prop as a subobject classifier, then from exponentiation we get power types, and the “impredicativity of Prop” means that in defining propositions we allow quantified variables ranging over types, which is like unbounded separation. Those sorts of impredicativity are, I believe, still there in the current version of Coq …

Yes, Prop is still impredicative in Coq. And to some degree, that makes sense. Even though Prop lives along side the other universes, and interacts with them in ways that make it distinctly type theory rather than a first-order logical theory, Prop is supposed to fill that sort of role. Predicativists stratify their sets (or whatever), but they don’t stratify their propositions.

what’s been turned off by default is something still stronger, saying something like “for any set A, there is a set of functions Set→A.” Am I right about that?

Yes, and more generally, if Γ,T:SetU:Set\Gamma, T : Set \vdash U : Set then Γ(Π T:SetU):Set\Gamma \vdash (\Pi_{T : Set} U) : Set. And even if TT inhabits an arbitrarily high universe (so long as UU still inhabits SetSet).

I’ve always been curious how one shows that such an “anti-classical impredicative universe” is consistent; it seems quite a precarious assumption.

It certainly is precarious. In fact, it’s very easy to introduce inconsistency. For instance, the above is about Π\Pi types. If we try to introduce Σ\Sigma types:

Γ,T:TypeU:SetΓΣ T:TypeU\frac{\Gamma, T : Type \vdash U : Set}{\Gamma \vdash \Sigma_{T:Type} U}

Then we can do the following:

(Set,tt):Σ T:Type:Set(Set, tt) : \Sigma_{T:Type}\top : Set

So we can trick SetSet into (essentially) inhabiting a SetSet. Coq deals with this by disallowing strong and/or large elimination of impredicative inductives (so, you can define Σ T:Type w\Sigma^w_{T:Type}\top, but not π 1 w:Σ T:Type wType\pi^w_1 : \Sigma^w_{T:Type}\top \to Type, which makes the type isomorphic to \top).

And also, there’s Girard’s paradox, which shows that if we have a universe hierarchy like Type 1:Type 2:Type 3Type_1 : Type_2 : Type_3, and Type 2Type_2 allows impredicative Π\Pi types, then a contradiction is derivable (Type 1Type_1 may need to be impredicative, too, I forget).

So, allowing one impredicative universe at the bottom is something of a balancing act that no one has yet proved inconsistent (kind of like set theory :)). And I think there are plenty of folk that prefer more predicative theories (I lean that way myself). Impredicative theories do have certain appealing properties, though. For instance, any inductive type (minus the strong eliminator) can be encoded using impredicative Π\Pi types via Church encoding.

I don’t know what really counts as far as demonstrating consistency goes. System F and the calculus of constructions (and many others) have proofs of strong normalization. And although they don’t have non-trivial set-theoretic models, I think they do have trivial ones. Perhaps that lends confidence? Certainly if you trust set theory, you can probably trust the normalization theorems. Of course, if you don’t trust impredicativity, maybe you shouldn’t trust set theory. :)

Coq may be another matter, since I think it’s been shown to be as powerful as something like (constructive?) ZF + axioms about inaccessible cardinals.

Posted by: Dan Doel on January 26, 2011 8:50 AM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

Perhaps that’s related somehow?

Yes, that’s exactly it. Classically, only a preorder (= a (0,1)-category) can have products indexed by its own collection of morphisms.

Predicativists stratify their sets (or whatever), but they don’t stratify their propositions.

I’m not sure exactly what you mean, but many predicativists do indeed restrict the ability to define propositions by quantification over all types (or even over all propositions). That’s what I meant by saying that set-theoretic unbounded separation is impredicative. All the replies to David’s question were of that nature. I could be wrong, but to me it seems that to a mathematician with a classical set-theoretic intuition, quantifying over all sets in defining a proposition is “impredicative” (if they know what that word means) and defining a set {f:TU} TSet\{ f: T \to U \}_{T \in Set} is “obviously impossible.”

System F and the calculus of constructions (and many others) have proofs of strong normalization.

Can you explain to a non-type-theorist why that should be regarded as evidence of consistency?

Of course, if you don’t trust impredicativity, maybe you shouldn’t trust set theory. :)

I have no trouble trusting impredicative definitions of propositions, which is all that ordinary set theory allows (i.e. unbounded separation). It’s the stronger form of “impredicativity” that makes me queasy.

Posted by: Mike Shulman on January 27, 2011 3:54 AM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

Yes, that’s exactly it. Classically, only a preorder (= a (0,1)-category) can have products indexed by its own collection of morphisms.

Ah, okay. In that case, I can probably elaborate a little more, although I’m a little hazy on this myself.

The key, I think, is that when you make set-theoretic models of (say) System F, one sets it up as follows:

  1. Let’s consider Fam(C)\mathbf{Fam(C)} fibred over Set\mathbf{Set}. Objects of Fam(C)\mathbf{Fam(C)} are set-indexed families of objects of C\mathbf{C}, and morphisms are a function between the index sets together with an arbitrary family of functions that respect the index function.

  2. Our model is a pullback of that fibration along the inclusion functor from a subcategory of Set\mathbf{Set} containing as objects only finite products of the set of elements of C\mathbf{C} (C 0\mathbf{C_0} is standard notation for that set, I believe).

The only such models that are closed under C 0\mathbf{C_0}-indexed products are posets, or preorders, or what have you. However, I emphasized a bit above. Arbitrary families of functions are a poor match up to the functions we are able to write in System F. If we consider an endomorphism on {X} XC 0\{X\}_{X \in \mathbf{C_0}}, the \mathbb{N} \to \mathbb{N} component could be the successor function, while every other component could be the identity. However, it’s impossible to write such a function in System F, because there is no type-case construct. Every morphism denotable in System F is uniform in some sense.

The book I’ve been reading gives the following example: let C\mathbf{C} be the category whose objects are subsets of the natural numbers, and morphisms XYX \to Y are endofunctions ff on the natural numbers such that f(X)Yf(X) \subseteq Y. Then there are two fibrations that can be viewed as set-indexed versions of this category:

  1. Objects are set indexed families of sets of natural numbers, and morphisms {X i} iI{Y j} jJ\{X_i\}_{i \in I} \to \{Y_j\}_{j \in J} are a function ϕ:IJ\phi : I \to J together with a family {f i:X iY ϕ(i)}\{f_i : X_i \to Y_{\phi(i)}\} where each f if_i is an appropriate C\mathbf{C}-morphism.

  2. Objects are the same as above, but morphisms are a function ϕ:IJ\phi : I \to J together with a single function ff that is a valid C\mathbf{C}-morphism X iY ϕ(i)X_i \to Y_{\phi(i)} for all ii.

Now, I’m afraid that this is where my knowledge runs out. However, the idea is that System F is appropriately modeled by this sort of fibration with uniform morphisms, and that when this fibration is used, the category admits products indexed by ‘all types’, and you get impredicative quantification in this manner. The uniformity is key to getting non-trivial models, though, and even my hazy understanding can see where that’d be a problem for a set-based model (because, what the hell is a uniform family of set theoretic functions?).

This uniformity is often referred to as “parametricity,” which you may have heard of before. As a punchline, consider the type Π A:Set.AA\Pi_{A:Set}. A \to A. Looks pretty big, product over all types/sets. And in set theory, it certainly would be big. However, a type theorist will tell you that, by consequence of parametricity, this set has exactly one inhabitant.

I’m not sure exactly what you mean, but many predicativists do indeed restrict the ability to define propositions by quantification over all types (or even over all propositions). That’s what I meant by saying that set-theoretic unbounded separation is impredicative. All the replies to David’s question were of that nature. I could be wrong, but to me it seems that to a mathematician with a classical set-theoretic intuition, quantifying over all sets in defining a proposition is “impredicative” (if they know what that word means) and defining a set {f:T→U} T∈Set is “obviously impossible.”

I mean, for instance, we could have 0-sets, and then 1-sets, which are allowed to be defined by quantifying over 0-sets, and 2-sets that are allowed to be defined by quantifying over 1-sets, and so on. But I would expect our logic would not also be divided into 0-propositions and 1-propositions and whatnot. Perhaps it is necessary to classify them as such in order to make the stratification of sets happen, though. I’m not sure.

I’d kind of not expect propositions to be able to quantify over propositions at all in a “logic.” As opposed to a type theory where we’re interpreting propositions as types. But the lines can be blurry, I guess.

Can you explain to a non-type-theorist why that should be regarded as evidence of consistency?

It is like proving cut elimination for a logic. If a type theory is strongly normalizing, then every reduction strategy is terminating and results in a canonical form for every term. The only remaining piece would be a proof that there is no canonical inhabitant of Π A:Set.A\Pi_{A:Set}. A, or, perhaps we have a primitive false type, for which there is by definition no canonical inhabitant.

Hopefully this formats correctly. The math prettifying seems to be stopping half-way through the preview on my obscure browser.

Posted by: Dan Doel on January 27, 2011 6:38 AM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

the idea is that System F is appropriately modeled by this sort of fibration with uniform morphisms, and that when this fibration is used, the category admits products indexed by ‘all types’, and you get impredicative quantification in this manner.

Ah, that sounds a bit familiar. What you describe sounds very much like a preliminary to the construction of the effective topos, which does contain a complete small category, and now I seem to recall hearing that that category can be used in modeling this sort of type theory.

I’d kind of not expect propositions to be able to quantify over propositions at all in a “logic.”

Well, I think most logicians would disagree with you, as would most non-type-theorists. In classical logic, up to equivalence there are only two propositions (“true” and “false”) so we can certainly quantify over them. In impredicative constructive logic, we can’t assert that there are only two propositions, but we still have a set of all of them, so we can quantify over them; one way to define it is as the power set of the one-element set.

The only remaining piece would be a proof that there is no canonical inhabitant of Π A:Set.A\Pi _{A:Set}.A

Ah, that’s what I would call a “consistency proof.” (Except that I would probably want there to be no inhabitant at all, not just no canonical one, but maybe in the presence of “parametricity” the two are equivalent?) So in language that’s familiar to me, maybe you’re saying that strong normalization is a necessary prerequisite to a consistency proof.

Posted by: Mike Shulman on January 27, 2011 4:18 PM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

Ah, that sounds a bit familiar. What you describe sounds very much like a preliminary to the construction of the effective topos, which does contain a complete small category, and now I seem to recall hearing that that category can be used in modeling this sort of type theory.

Yes, that sounds right. In fact, the book I’m reading is called An Introduction to Fibrations, Topos Theory, the Effective Topos and Modest Sets.

Well, I think most logicians would disagree with you, as would most non-type-theorists. In classical logic, up to equivalence there are only two propositions (“true” and “false”) so we can certainly quantify over them. In impredicative constructive logic, we can’t assert that there are only two propositions, but we still have a set of all of them, so we can quantify over them; one way to define it is as the power set of the one-element set.

I don’t think we’re speaking the same language. When I think of propositions, I think of the things that can be substituted for the metavariable PP in ΓP\Gamma \vdash P. And that are elligible for use with the logical connectives. For instance, I wouldn’t expect to see something like:

Γ Propp.p¬p\Gamma \vdash \forall_{Prop} \, p. p \vee \neg p

Not in a logic. I think I know what you mean, though.

Ah, that’s what I would call a “consistency proof.” (Except that I would probably want there to be no inhabitant at all, not just no canonical one, but maybe in the presence of “parametricity” the two are equivalent?) So in language that’s familiar to me, maybe you’re saying that strong normalization is a necessary prerequisite to a consistency proof.

I don’t know about necessary, but it makes a consistency proof easier.

So, the goal of a consistency proof is indeed to show that there is no proof of \bot, whatever that is. What strong normalization shows is that if there is any proof of a proposition PP, then there is a canonical such proof, which can be derived via a terminating procedure. Cut elimination for a sequent calculus does the same thing. So, once you’ve proved strong normalization/cut elimination, all you have to do is show that there are no canonical proofs. In a sequent calculus, there is by definition no rule:

\frac{}{\vdash \bot}

So we’re done. For something like Π A:SetA\Pi_{A:Set}A, I expect it’s more like:

A:Sete:A(ΛA.e):Π A:SetA\frac{A : Set \vdash e : A}{\vdash (\Lambda A. e) : \Pi_{A:Set}A}

And no rules match the top part, so we’re again done. Is that satisfying enough? I realize my description isn’t particularly rigorous.

Posted by: Dan Doel on January 28, 2011 12:48 AM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

I wouldn’t expect to see something like: Γ Propp.p¬p\Gamma\vdash_{Prop} p. p\vee \neg p. Not in a logic.

I think your notion of “logic” is more narrow than mine, and more narrow than many that I’ve seen. For instance, in most presentations of the “higher-order logic” of an elementary topos, this is a perfectly meaningful statement (which is, of course, only true if the topos is Boolean).

Unless the point is to distinguish between propositions as syntactic constructions, on the one hand, and truth values in the logic, on the other? Type theory seems to blur the distinction, to my mind, so I assumed you were also.

Is that satisfying enough?

Yes, that makes sense. I wonder how strong of a metatheory is used in the proof of strong normalization?

Posted by: Mike Shulman on January 28, 2011 3:08 AM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

Unless the point is to distinguish between propositions as syntactic constructions, on the one hand, and truth values in the logic, on the other? Type theory seems to blur the distinction, to my mind, so I assumed you were also.

Yes, that is roughly the point. It is possible even to cast this distinction in type theory, now that I think about it, though.

For instance, we can imagine a Coq in which PropProp is classical. However, there is still a distinction between inhabitants of PropProp and inhabitants of Bool:SetBool : Set. Coq is not really a good example, though, because it actually allows quantification over PropProp, and for elements of SetSets to contain PropProps.

However, some folks have studied what are called logic-enriched type theories. These have a separate PropProp universe, like Coq, but it is unrelated to whatever hierarchy of sets is also in the theory. And in particular, there is no quantification over PropProp, No Π P:Prop...\Pi_{P : Prop} .... And so something like p:P:Prop.P¬P\vdash p : \forall P:Prop. P \vee \neg P could only be an abuse of notation for something more like p:b:Bool.True(b)¬True(b)\vdash p : \forall b:Bool. True(b) \vee \neg True(b), where BoolBool is a “set of truth values,” and True:BoolPropTrue : Bool \to Prop is a predicate.

And as the name “logic-enriched type theory” suggests, this separation seems particularly logic-like, as opposed to the wacky type theorists who really don’t make any distinction between types and propositions. Perhaps I’ve just missed logics that aren’t this way, though.

Yes, that makes sense. I wonder how strong of a metatheory is used in the proof of strong normalization?

Depends on the type theory, of course. Girard’s Proofs and Types proves normalization for (I think) three different theories. The first is the simply typed lambda calculus. He notes that you can prove normalization for it in a relatively weak metatheory (certainly in first-order arithmetic). The next two are System T and System F. T is related to Peano arithmetic via Curry-Howard, and so strong normalization of T implies the consistency of Peano arithmetic. So that might give you some idea of how strong a theory you’ll need. System F is in a similar situation, except with second-order arithmetic.

Posted by: Dan Doel on January 28, 2011 5:59 AM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

Okay. But I thought we were comparing “quantifying over propositions” to quantifying over sets, not quantifying over syntactic presentations of sets. It seems to me that quantifying over truth values is the natural thing to compare to quantifying over sets. And if you don’t want to quantify over syntactic presentations of propositions, then you shouldn’t be able to quantify over syntactic presentations of sets either, should you?

Posted by: Mike Shulman on January 28, 2011 8:15 PM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

I may not be expressing myself well, but I don’t think the distinction has to do with quantifying over syntax versus actual sets and whatnot. Syntax is just how logic enforces the distinction (while type theory can use types, like the stuff with logic-enriched theories).

I’m not really sure how to explain myself better. But, maybe I can make another example. Pretty much every functional programming language has higher-order functions. So, when you write a definition f x = ..., that f : S -> T is useful both as a mapping from type S to type T, and as a value that can be passed to some higher-order function g : (S -> T) -> U.

Now, when we go to model this in category theory (with, say, Cartesian closed categories), these notions of value and function are kept separate. (Global) values of a type T are given by morphisms 1T1 \to T. And so, we have a conceptual distinction between functions-as-morphisms f:STf : S \to T and functions-as-values f:1T Sf : 1 \to T^S. They are in correspondence, but you cannot just use one where the other is expected.

And similarly, in ZF, b.b¬b\forall b \in \wp\wp\varnothing. b \vee \neg b is not a well-formed formula, because even though bb ranges over the set of truth values, bb is still a set variable, not a proposition variable. And I (and others, I think) expect logics (even higher-order logics) to be this way. Quantification builds propositions, but the variables range over particulars, or sets of particulars, not, strictly speaking, propositions. There may be a subset classifier, and functions into that classifier may correspond to subsets, which in turn correspond to predicates, but purely from a formal rules perspective, the elements of that set aren’t propositions.

At this point, though, I’ve forgotten why we’re even talking about this. :) I don’t think it’s a fundamentally important distinction. Just something that sounded odd to me.

As an amusing side note, the paper where I heard about logic-enriched type theories is called: Weyl’s Predicative Classical Mathematics as a Logic-Enriched Type Theory. So it’s very on-topic since it’s about predicativism.

Posted by: Dan Doel on January 29, 2011 2:00 AM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

Yes, perhaps this discussion is going nowhere interesting. But it does seem to me that what you describe is a distinction without a difference for purposes of quantification. You can’t literally use a value 1T S1\to T^S where a function STS\to T is expected, but if you can quantify over one, then for all practical purposes you can quantify over the other as well. Similarly maybe you can’t literally write b,b¬b\forall b\in \wp\wp\emptyset, b\vee \neg b, but you can write b,bb c=\forall b\in \wp\wp\emptyset, b\cup b^c = \wp\wp\emptyset, which is functionally the same thing.

Posted by: Mike Shulman on January 30, 2011 11:41 PM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

Yes, you’re right about how it works. The basic idea is that you get to index over all types[1] when constructing types – that is, you can have types like α:Type.αα\forall \alpha:\mathrm{Type}.\; \alpha \to \alpha.

I think you would like the way models of System F and its higher-kinded cousins are constructed. The basic idea is to give a relational realizability model (I understand you might have heard the idea described as “fibrations of modest sets”).

First, you start with a universe of computational realizers. Traditionally, computer scientists start with a domain theoretic model of the untyped lambda calculus (VVVV \simeq V \to V), and logicians start with VV \triangleq \mathbb{N}, the set of Godel codes. Then, each type is interpreted as a partial equivalence relation (ie, symmetric and transitive, but not necessarily reflexive relations) on the universe VV.

Then, the interpretation of the function space ABA \to B in a type environment η\eta is the set:

[[AB]]η={(f,g)V×V|(u,v)[[A]]η.(fu,gv)[[B]]η}[\!\![A \to B]\!\!]\;\eta = \{(f,g) \in V \times V \;|\; \forall (u,v) \in [\!\![A]\!\!]\;\eta.\; (f\;u, g\;v) \in [\!\![B]\!\!]\;\eta\}

That is, the interpretation of the function space is the set of functions that take related arguments to related results. The interpretation of the universal quantifier, which is what you’re probably most interested in, goes like this:

[[α:Type.A]]η= RV×V[[A]](η,R)[\!\![\forall \alpha:\mathrm{Type}.\;A]\!\!]\;\eta = \bigcap_{R \subseteq V \times V} [\!\![A]\!\!]\;(\eta,R)

The interpretation of the universal quantifier are just the pairs of values which are in every type interpretation, no matter what relation is chosen for α\alpha.

By fixing a universe VV at the outset, we can take subrelations over it impredicatively when we need to interpret \forall.

[1] As an aside, I am deliberately not saying “set”, since Andy Pitts has shown that the powerset axiom is inconsistent with F-style indexing. I don’t think he needed full separation, since IIRC he used a topos model. I’m not sure about this, though, since I don’t know much set theory.

Posted by: Neel Krishnaswami on February 2, 2011 9:24 AM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

Thanks Neel! I wonder if the following description is accurate. Impredicativism seems to be justified by a belief (or an assumption) that there is a prior existing “true universe of things” about which we prove things, as opposed to the predicative conception whereby we merely construct things one after another, so that we can’t make such a construction with reference to objects that we haven’t constructed yet. The difference between set-theoretic impredicativism (power sets, unbounded separation) and type-theoretic impredicativism (system F) is that in the former, the “true universe of things” consists of sets, whereas in the latter it consists of… well, I was going to say “functions,” but that could be misinterpreted (e.g. categorial set theory can be defined with just “functions” as basic objects, but those are set-theoretic functions, not type-theoretic ones); maybe “instructions” or “algorithms” would be more appropriate.

Posted by: Mike Shulman on February 13, 2011 10:48 PM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

Impredicativism seems to be justified by a belief (or an assumption) that there is a prior existing “true universe of things” about which we prove things, as opposed to the predicative conception whereby we merely construct things one after another, so that we can’t make such a construction with reference to objects that we haven’t constructed yet.

This sounds remarkably similar to the debate in the late 1920s between Finsler and Baer over set theory. In my post on coalgebra I discuss Herbert Breger’s paper on the debate. He writes in that paper

To the revolutionary, the most striking difference between Zermelo’s and Finsler’s axioms is the certain ontological flavour of Finsler’s axioms. To the conservative, the philosophical background of Zermelo’s axioms is the implicit assumption that sets do not exist unless they can be derived from given sets by axiomatically fixed rules. Axiom 3 [the axiom of completeness] is of particular interest. It is the analogue of Hilbert’s somewhat problematic axiom of completeness for geometry. Weyl and Fraenkel purposefully took the contrary into consideration, namely an axiom of restriction postulating the minimal system which fulfils the other axioms. Weyl’s and Fraenkel’s axiom is obviously motivated by the revolutionary idea that axioms and definitions create objects, and that sets which are too big should not be brought into existence, whereas Finsler’s axiom of completeness is motivated by the conservative idea that big sets exist anyway, so set theory should investigate them. (Breger, 1992, pp. 258-259)

But maybe the impredicative/predicative distinction concerns a rather specific sense of construction, so can be found already operating on the ‘algebraic’ side in algebraic set theory.

Posted by: David Corfield on February 14, 2011 8:54 AM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

Yes, phrased that way it does sound similar! It’s ironic, then, that Zeremlo’s axioms are so impredicative. I guess there are, as you say, different conceptions of “construction” or “derivation” involved. Although I suppose a predicativist might argue that Zermelo and his school did not honestly follow the precept that “sets do not exist unless they can be derived from given sets by axiomatically fixed rules” to its logical conclusion (namely predicativism).

On the other hand, if the main difference between Zermelo and Finsler set theory was well-foundedness, as Aczel seems to think, then one might argue that that has nothing to do with predicativism: all four combinations of predicative/impredicative and well-founded/non-well-founded are perfectly consistent.

Posted by: Mike Shulman on February 14, 2011 7:24 PM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

I think of the underying type-theoretic intuition as actually being a bit different from the set theoretic view. Informally, I would gloss it as “impredicativity is a safe method of definition for sufficiently uniform definitions”.

The idea is that since the rules of type theory let you do nothing exciting to a term of variable type α\alpha (not even testing membership or equality), then a definition which is parametric in α\alpha will work for any possible choice of α\alpha. (Hence the name “parametric polymorphism”.) This then justifies impredicative indexing over any possible type, including other polymorphic types — the term simply doesn’t depend on the properties of the specific choice of type. This principle of uniform definition seems to me to differ from the size restrictions of set theory.

If I had infinite time, I would like to try developing category theory within an impredicative type theory. I have a vague hunch that many of the “big” constructions of category theory (e.g., involving functor categories) are so well-behaved that they are expressible using polymorphic types. For example, the Yoneda embedding is expressible as the isomorphism α,β.(αβ)(γ.(γα)(γβ))\forall \alpha, \beta.\; (\alpha \to \beta) \Leftrightarrow (\forall \gamma.\; (\gamma \to \alpha) \to (\gamma \to \beta)).

It would be fun to see what did and didn’t work.

Posted by: Neel Krishnaswami on February 15, 2011 4:38 PM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

Interesting; I see what you mean. Is there any way that set-theoretic impredicativism could (or some weaker form of it) could be interpreted in a similar way, do you think?

Posted by: Mike Shulman on February 16, 2011 3:35 AM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

For set theories of the strength of bounded ZF/topos logic, I’m confident it’s doable, since the calculus of constructions has the same consistency strength as higher-order arithmetic. Offhand, I don’t know an elegant way to do it, since for obvious reasons the majority interest is in giving models of polymorphism in set theory, rather than the other way around.

For set theories with unbounded separation, I don’t know how. Logics such as Coq are equiconsistent with various extensions of ZFC, but these type theories are basically stratified systems with a universe hierarchy.

Posted by: Neel Krishnaswami on February 17, 2011 5:31 PM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

I would be interested even in seeing an “inelegant” way to do it. Do you just mean “build the model of set theory inside type theory that you use to show it has the same consistency strength?”

Posted by: Mike Shulman on February 17, 2011 6:32 PM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

Yes, that’s what I meant. IMO it’s not a construction that offers much enlightenment on this question.

I think it might be tricky to do well, too. I mentioned Andy Pitts’ paper, but I should give the reference explicitly, since it bears directly on this question:

“Nontrivial Power Types Cannot be Subtypes of Polymorphic Types”

This paper establishes a new, limitative relation between the polymorphic lambda calculus and the kind of higher-order type theory which is embodied in the logic of toposes. It is shown that any embedding in a topos of the cartesian closed category of (closed) types of a model of the polymorphic lambda calculus must place the polymorphic types well away from the powertypes, P(X), of the topos, in the sense that P(X) is a subtype of a polymorphic type only in the case that X is empty (and hence P(X) is terminal). As corollaries, we obtain strengthenings of Reynolds’ result on the non-existence of set-theoretic models of polymorphism.

Post-hoc, it shouldn’t be surprising that combining two different techniques to tame unbounded impredicativity can subvert the invariants each relies on.

Posted by: Neel Krishnaswami on February 18, 2011 1:58 PM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

Hi Neel, did you mean something analogous to this post? There it seems one can work with a universe, but since the universe you started with was arbitrary, then the results hold always. Mike explains it much better after the link.

Posted by: David Roberts on February 16, 2011 3:48 AM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

Yes, certainly! A predicative definition (predicativism is more about definitions, while constructivism is more about proofs, although of course these can't be completely disentangled) has a much more concrete feel than an impredicative definition.

Compare these two (nonconstructive) proofs of the (classical) Intermediate Value Theorem (and so much for my claim that predicativism is more about definitions, since this example is a proof).

Theorem: If f:[0,1]f\colon [0,1] \to \mathbb{R} is continuous, f(0)<0f(0) \lt 0, and f(1)>0f(1) \gt 0, then f(c)=0f(c) = 0 for some cc.

Proof 1: Let cc be sup{x|f(x)0}\sup \{ x \;|\; f(x) \leq 0 \}, which exists (in [0,1][0,1]) since [0,1][0,1] is compact. If f(c)<0f(c) \lt 0 or f(c)>0f(c) \gt 0, we use continuity to derive a contradiction (skipped here). Therefore, f(c)=0f(c) = 0.

Proof 2: Let a 0a_0 be 00, let b 0b_0 be 11, and inductively define:

  • c n=(a n+b n)/2c_n = (a_n + b_n)/2,
  • a n+1=a na_{n+1} = a_n if f(c n)>0f(c_n) \gt 0 but a n+1=c na_{n+1} = c_n if f(c n)0f(c_n) \geq 0,
  • b n+1=b nb_{n+1} = b_n if f(c n)<0f(c_n) \lt 0 but b n+1=c nb_{n+1} = c_n if f(c n)0f(c_n) \leq 0.

Then (c n) n(c_n)_n is a Cauchy sequence (by elementary algebra, skipped here), so has a limit cc (in [0,1][0,1], since that is Cauchy complete), and f(c)=0f(c) = 0 (again by contradiction and continuity, skipped).

Proof 1 is impredicative and abstract, while Proof 2 is predicative and concrete. In Proof 1, cc is basically defined as the largest number that will do; in Proof 2, cc is explicitly constructed. You could try to program a computer to calculate cc (to any desired degree of accuracy) using Proof 2 as a guide; good luck trying that with Proof 1! (Because Proof 2 is not constructive, your program may eventually have to give up and round off when trying to decide the sign of f(c n)f(c_n), but it'll be good enough for many purposes. Trying to overcome this limitation leads to various constructive versions of the IVT.)

Here's another example (a definition finally, and incidentally constructively valid either way).

We may define a smooth (or whatever) manifold as a set equipped with a covering collection of mutually compatible charts (called an atlas) and we wish to define the maximal atlas M(A)M(A) associated to the original atlas AA. (This is allegedly useful since two atlases with the same maximal atlas are be regarded as defining the same manifold structure, so that we may formally define a smooth manifold as a set equipped with a maximal smooth atlas. Whether this is actually useful is another matter.)

Definition 1: M(A)M(A) is the union of all those atlases MM with the property that every chart in MM is compatible with every chart in AA.

Definition 2: M(A)M(A) is the collection of all charts CC such that CC is compatible with every chart in AA.

(In both cases, we should go on to prove the desired claims about M(A)M(A), beginning with the fact that it is an atlas at all.)

I have seen Definition 1 in textbooks. Definition 2 strikes me as obviously superior: both simpler and more concrete. While Definition 1 is impredicative, Definition 2 is predicative. (Predicatively, M(A)M(A) may be a proper class even if AA is not, which kind of obviates the motivation for defining M(A)M(A), but that was a silly motivation anyway. And even if you impredicatively accept that M(A)M(A) is a small set, Definition 2 is still more concrete.)

Posted by: Toby Bartels on January 25, 2011 6:29 AM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

As I said, there is a close connection between predicativity and geometricity, preservation under geometric morphisms. By working directly with a theory, rather then the set, or topological space, of its models, we deal with a more robust notion. This saves a lot of bookkeeping.

In another direction, there have been heated discussions on the FOM-list on predicativity (in this context combined with classical logic). Nik Weaver claims that the spaces in functional analysis that have a name are all predicatively definable, illustrating his point that real mathematicians (functional analysists) do not use impredicativity. As a warning I should add that there is a distinction between predicative (roughly, upto Γ 0\Gamma_0 and generalized predicative (roughly, no power set).

Bas

Posted by: Bas Spitters on January 25, 2011 8:14 AM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

[The links above should be fixed; the desired URI is in the title instead of the href.]

I've heard ‘generalized predicative’ to mean no power sets but with function sets (in a constructive framework where this is even possible).

I've never understood where people get these ordinals.

Posted by: Toby Bartels on January 25, 2011 3:20 PM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

I don’t know how people decide what ordinals are the cap for predicative theories. However, Martin-Löf type theory has proof theoretic ordinal Γ 0\Gamma_0 (apparently), yet has function types, which I assume is similar in power to having function sets. And it’s usually considered predicative.

Beyond that, you can add arbitrary inductive-recursive definitions to such a theory and get something much stronger (I don’t think anyone knows the proof-theoretic ordinal), but I think the theory is still arguably predicative. You cannot define a model of (constructive) set theory with a true power set like you can in Coq (I don’t have a proof, but my attempts have failed, and I’ve spent a fair amount of time on them :)).

But then, there are folks who take predicative to be even more restrictive (like, ‘Heyting Arithmetic is impredicative due to the induction schema’).

Posted by: Dan Doel on January 25, 2011 11:22 PM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

The links above should be fixed; the desired URI is in the title instead of the href.

Apparently that’s what Markdown does if you put quotation marks around the URI, inside the parentheses. I.e. [link]("http://place") produces <a href="" title="http://place">link</a>.

I’ve fixed the links in the comment above.

Posted by: Mike Shulman on January 26, 2011 4:26 AM | Permalink | Reply to this

Re: Topos Theory Can Make You a Predicativist

Wonderful post! I was already suspicious of the suboject classifier in toposes; type theory is much more elegant without an equivalent of this (Prop, the type of propositions). While I heard of predicativism, I didn’t know my suspicion were exactly in favour of that (I thought the very existence of the category of sets, even if it was a large category, is a nonpredicativistic perspective). Additionally, I wondered why toposes have exactly the axioms they have – No more, no less. It turns out toposes aren’t a canonical objects at all, since weaker properties are enough to do anything topos theorists want to do (Grothendieck toposes on the other hand…). Now that these inelegances are out of the way, I am much more interested in topos theory.

Posted by: Itai Bar-Natan on January 25, 2011 10:45 PM | Permalink | Reply to this
Read the post Homotopy Type Theory, V
Weblog: The n-Category Café
Excerpt: What's still missing to make homotopy type theory into a complete internal language for (∞,1)-topoi?
Tracked: April 12, 2011 5:18 AM
Read the post PSSL 93 trip report
Weblog: The n-Category Café
Excerpt: A report on several talks from the PSSL 93 in Cambridge.
Tracked: April 25, 2012 4:14 PM

Post a New Comment