26
$\begingroup$

My experience with foundations is rather scant, but I've run into some types of objects that seem to resist the sort of set-theoretic encoding schemes via Kurowski tuples that are rather common for objects like groups and manifolds. In particular, they tend to be something like functions that can accept arbitrarily large inputs. I am wondering if such objects can be given foundations in a reasonably parsimonious way, so we don't have to include all possible inputs when considering such a function. The following are three examples:

  1. Random variables: I read from Gowers's blog post that analysts define random variables as measurable functions satisfying some conditions, but that probabilists use them in a manner inconsistent with that definition. In particular, one has the problem of respecifying the sample space when new random variables come into play. If someone came up to me on the street and asked me to formalize this, I would probably respond by encoding a random variable using a proper class of all possible extensions of sample spaces. Naturally, this seems to be a rather weighty thing to carry around if I want to say that a particular probability manipulation is well-defined. From what I read in Tao's blog post, it seems that in practice, one encloses all mention of random variables in something like a type theory where the only allowable operations and quantities are those that are invariant under extension of sample space. Unfortunately, I know next to nothing about formal type theory - would this yield a decent answer?

  2. Presheaves and sheaves on a site: Sometimes in algebraic geometry, one considers Grothendieck topologies like the fpqc topology, where even over a point, the isomorphism types of open sets and open covers form a proper class. One then encounters problems in the literature, where people claim that fpqc sheafification is a functor, but they prove it using a forbidden colimit over all open covers. This is an honest problem: in his paper Basically bounded functors and flat sheaves (Pac. J. Math. 57 no. 2 1975), Waterhouse produces a presheaf that has no fpqc sheafification. However, he also shows that for those presheaves that are left Kan extensions of presheaves on rings with a cardinality bound, sheafification and cohomology are independent of the bound for any topology (e.g., fpqc) satisfying a small approximation property. These left Kan extensions are commonly known as small presheaves, and essentially all geometrically interesting presheaves are small. In less technical and more general terms, we don't really need to make set-theoretic assumptions about the existence of universes, or truncate our presheaves to only take rings of size below some (possibly strongly inaccessible) bound, as long as we are only doing operations that preserve a sense of smallness. It would be nice, though perhaps not of fundamental importance, to have a formalism that made the recognition of such operations straightforward.

  3. Supergeometry: While mathematicians often view supermanifolds as manifolds with sheaves of supercommutative rings, physicists doing first variation calculations for superfields often make use of an "odd parameter" that acts like an odd free variable that (as far as I can tell) completely fails to fit into the mathematicians' rings. In his book "Supermanifolds", DeWitt attempts to resolve this problem by adjoining countably infinitely many odd variables to everything in sight, but this seems to make physicists unhappy because infinitely many of those variables are unused and therefore "physically unmeaningful". Presumably, one should have a formalism that allows you to add odd parameters to your superalgebras at will, without carrying all possible extensions around with you all the time.

I hope these examples convey the flavor of what I'm seeking: some method for considering flexible or extendable objects that doesn't require the consideration of all possible extensions all the time.

$\endgroup$
5
  • 2
    $\begingroup$ I don't think 3 is an issue. That's how variables are always used in any formal language; you have some infinite supply of them but you only use finitely many at a time. For 1 and 2, Charles Wells has been giving some thought to "just-in-time foundations" that seem to specifically address those issues. abstractmath.org/Word%20Press/?p=1467 $\endgroup$ Apr 6, 2012 at 12:32
  • 2
    $\begingroup$ Thanks for the pointers. Wells's idea seems to be that in practice, most mathematicians will only appeal to foundational arguments when a problem comes up, and that they will come up with ad hoc techniques that work for their purposes. I was hoping instead for a general method for making these things tick. It seems like one may take a hint from his post, and construct some kind of object-oriented "extendable gadget" type, but in that case, I don't know how one convinces oneself that the constructions do not lead to contradictions. $\endgroup$
    – S. Carnahan
    Apr 9, 2012 at 7:23
  • $\begingroup$ Carnahan, this is a good question. But are you still interested in it? If so, I might have a go at answering; not because I've got the answer, but just to let you know my own thinking on the issue. $\endgroup$ May 5, 2014 at 7:11
  • $\begingroup$ @user18921 I've been a bit dissatisfied with the way I organized the question, but not enough to invest the time needed for a substantial revision. If you have something interesting to say about the current version, I will be happy to read it. $\endgroup$
    – S. Carnahan
    May 5, 2014 at 17:43
  • $\begingroup$ I have used the "direct" or "inductive" limit as a way to construct the full Fock space for a free quantum field theory. See en.wikipedia.org/wiki/Direct_limit $\endgroup$ Feb 21, 2023 at 14:19

4 Answers 4

6
$\begingroup$

I don't know enough about (1) or (3) to address them confidently, although I suspect that, as you suggested, some kind of internal type theory will do the trick. (Maybe ask a separate question about each of them, with more details provided?)

For (2), I believe one sort of partial answer, at least, is contained in my paper Exact completions and small sheaves, specifically section 9 and more specifically 9.6-9.10. The idea is that we can give a direct description of "the category of small sheaves on a large site" that doesn't require consideration of "large sheaves" at all. There are several ways to give such a description, which are discussed in the paper in the more general context of a non-inaccessible cardinality bound (in which case it also includes "exact completion"). But in general, the objects of the category (the "small sheaves") are a sort of many-object internal equivalence relation in the site, i.e. a small family of representables "formally glued together".

Lemma 9.1 and Theorem 9.2 show that if we do consider the very-large category of large sheaves, then the category of small sheaves is equivalent to its full subcategory consisting of the objects that are small colimits of sheafified representables, or equivalently are the left Kan extension of a sheaf on some small full subcategory of the site. Thus, for instance, the category of condensed sets is the category of small sheaves on the site of profinite spaces. On the other hand, if the topology is trivial, we obtain the better-known category of small presheaves mentioned in the question. There is thus a sheafification functor from small presheaves to small sheaves --- although there is not in general a right adjoint to it, i.e. the underlying presheaf of a small sheaf may not be a small presheaf.

The category of small sheaves is not in general a topos (neither Grothendieck nor elementary), but it is the next best thing: a locally small infinitary-pretopos, i.e. a category satisfying all the exactness conditions of Giraud's theorem but not the existence of a small generating set. Thus it lacks "higher-order" structure like exponential objects, power objects, and universes, but it has all the same "first-order" structure as an ordinary topos of sheaves; this seems to me a reasonable way to make sense of your idea of "operations that preserve a sense of smallness".

This is fairly specific to the case (2) of sheaves. But it does relate in some way to my guess at the probable answer of (1) and (3). Namely, any object of any category determines its representable functor, and if the category is large, the representable functor will take a proper class of possible inputs --- but in most cases, the object of the category can be described by a small amount of data. Thus, if we have a "large function" of some sort, we can try to view it as the representable functor of an object of some category, for which we can give a more direct "small" presentation. Type-theoretic internal languages can be viewed as a way of working conveniently with representable functors or generalized elements (the type-theoretic "context" being the domain of a generalized element).

$\endgroup$
1
  • 1
    $\begingroup$ (1) seems closely related to a question I asked several years later (unaware of this one) where you gave probably the best answer so far mathoverflow.net/a/308132/745 (to my shame I have not been able to follow up on your answer.) $\endgroup$ Feb 22, 2023 at 9:49
5
+50
$\begingroup$

For (2), Colin McLarty has written papers about using higher order arithmetic as a foundation for Grothendieck-style constructions. His "The large structures of Grothendieck founded on finite order arithmetic" [arXiv link] is the primary reference here, but see also "A univalent universe in finite order arithmetic" [arXiv link].

This is similar to the approach mentioned in Alec Rhea's answer, but using arithmetic as the base rather than set theory. In either approach, you start with type $0$ objects—integers or sets—and build upward from there to have one type for every $n \in \mathbb N$, with type $n+1$ objects being more-or-less collections of type $n$ objects. Higher-order set theory is overkill in terms of consistency strength for a lot of results, as McLarty's work shows. But depending on what you're doing it may be more convenient to work in the stronger setting.

$\endgroup$
3
$\begingroup$

I am not familiar with (1) and only have passing familiarity with superalgebra, but for (2) you may find the foundation laid out in my paper An axiomatic approach to higher order set theory satisfying.

Working in this theory we have countably many levels of 'largeness' for 'collections', with sets as $0$-collections, classes as $1$-collections, so on and so forth.

This foundation was originally developed to handle things like topology/analysis/measure theory etc. over the surreals; they form a proper class so a topology on the surreals would be a collection of proper classes, etc., and working in this foundation we can collect that stuff up no problem without relying on things like Scott's trick.

In this context, the isomorphism class you want to consider is a proper $1$-collection assuming you want the fpqc topology on all set-sized affine schemes -- more generally, the isomorphism classes for the fpqc topology on affine schemes whose underlying rings are all $n$-collections will be proper $n+1$-collections, and we can collect these up no problemo.

This foundation also makes explicit the notion of "small vs. large-ness" at the axiomatic level, allowing us to collect up all $n$-collections satisfying some predicate as an $n+1$-collection which sometimes also forms an $n$-collection if replacement applies.

$\endgroup$
2
  • $\begingroup$ I think you are mistaken about the strength of your theory. Since you have an axiom saying that $\mathcal{C}_n$ is an elementary submodel of $\mathcal{C}_{n+}$, your theory should be at least as strong as Ord is Mahlo. For example, since the height of $\mathcal{C}_0$ is an inaccessible cardinal, the fact that $\mathcal{C}_0 \prec \mathcal{C}_1$ means that the inaccessible cardinals are unbounded in $\mathcal{C}_0$. $\endgroup$ Feb 25, 2023 at 0:24
  • $\begingroup$ @ArvidSamuelsson That is possible; the consistency strength of the theory isn't necessarily the OP's main concern for this question, but I'm currently beefing up on Kanamori to see if/how I'm incorrect about the consistency strength of the theory. If you would like to write me an email about it that would be very welcome. $\endgroup$
    – Alec Rhea
    Feb 27, 2023 at 1:57
2
$\begingroup$

Concerning (1): In 2020 Alex Simpson gave a talk on synthetic probability theory: https://youtu.be/XtsBsLM9ofk where he provides foundations of probability theory in which random variables are treated as a primitive notion. I assume that there's no difficulty in adding new random variables in this setting. But I haven't found any publication of his on this yet.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.