Not signed in (Sign In)

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categorical categories category category-theory chern-weil-theory cohesion cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry digraphs duality elliptic-cohomology enriched fibration foundation foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry graph graphs gravity grothendieck group group-theory harmonic-analysis higher higher-algebra higher-category-theory higher-differential-geometry higher-geometry higher-lie-theory higher-topos-theory homological homological-algebra homotopy homotopy-theory homotopy-type-theory index-theory integration integration-theory k-theory lie-theory limit limits linear linear-algebra locale localization logic mathematics measure-theory modal modal-logic model model-category-theory monad monads monoidal monoidal-category-theory morphism motives motivic-cohomology nlab noncommutative noncommutative-geometry number-theory of operads operator operator-algebra order-theory pages pasting philosophy physics pro-object probability probability-theory quantization quantum quantum-field quantum-field-theory quantum-mechanics quantum-physics quantum-theory question representation representation-theory riemannian-geometry scheme schemes set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory stack string string-theory subobject superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
  1. starting discussion page for this page


    diff, v24, current

    • CommentRowNumber2.
    • CommentAuthorGuest
    • CommentTimeOct 14th 2022
    There's a giant discussion between Mike Shulman and Toby Bartels on the bottom of the page, and I don't think that really belongs on this page.
  2. added section on propositional resizing


    diff, v24, current

    • CommentRowNumber4.
    • CommentAuthorDavidRoberts
    • CommentTimeOct 15th 2022

    Here’s the 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.

    • CommentRowNumber5.
    • CommentAuthorDavidRoberts
    • CommentTimeOct 15th 2022

    Removed the discussion and archived in the nForum with a link

    diff, v25, current

  3. Added a paragraph about predicative mathematics where power sets are proper classes vs predicative mathematics where power sets simply don’t exist in the theory


    diff, v29, current

    • CommentRowNumber7.
    • CommentAuthorAshley
    • CommentTimeJun 21st 2024

    Adding the paper

    diff, v35, current

    • CommentRowNumber8.
    • CommentAuthorAshley
    • CommentTimeJun 21st 2024

    Also adding the paper

    diff, v35, current

    • CommentRowNumber9.
    • CommentAuthorAshley
    • CommentTimeJun 21st 2024

    Finally adding the paper

    diff, v35, current