Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I added a proposition to this subsection which seems valid intuitionistically, but I wouldn’t mind a reality check from someone.
Should the definition of involve rather than ? And should the in the last line be a ?
Thanks, Mike! Good catches; I corrected both.
Ok, now it looks good to me. Nice!
Thanks again, Mike. I confess that I’m having some trouble seeing the assertion that “constructively” (I guess this means intuitionistically?) a set is well-founded if it is classically well-founded. My guess is that Toby wrote that sentence, so maybe he can help me out.
Suppose is a classically well-ordered relation on a set . (I think I’m back to my old conundrum of “what does the nLab really mean by ’set’?”. I think it would be better to ask: what does the nLab think is meant by a category of sets? Basically I was hoping that the assertion would generalize so as to be valid for classically well-ordered relations in a topos.) Let be an inductive subset of . I can prove intuitionistically that its complement is not inhabited, which I am told is exactly synonymous with being empty. (I actually have to think about that one as well.) But I don’t see how to conclude that is the entirety of , intuitionistically.
Re #5: oh, I think I see. Merely by assuming classical well-foundedness, classical logic is forced upon us. That must be the point (and in fact that point is made in the article).
There seems to be a little something missing though; the article says that as soon as an inhabited relation is classically well-founded we have LEM, but how do we know that is inhabited?
There might be more information on this in the Elephant, D4.5.13 according to choice object (I don’t have access to this currently). It’s noted at that article that excluded middle is equivalent to the assertion that the 2-element set is classically well-orderable.
The proof is straightforward enough – one forms a subset whose minimal member depends on the proposition you want to decide, and then one uses decidability of equality to decide everything. See here.
Nice of you to provide a Coq proof.
Re #7: yes, it looks to me there’s a little bit missing. If we assume excluded middle in the meta-background, so that externally speaking every relation on a type is either inhabited or empty, then any classically well-ordered relation on an inhabited type is either inhabited or empty. If it is empty, then we argue it is well-founded (in the inductive sense) by vacuity, or if it is inhabited, then we can follow Zhen’s line of argument (thanks, Zhen!). But do we feel that meta-assumption is kosher? Or maybe there’s another way to argue?
I don’t understand where meta-ness comes in, can you explain again?
If the background logic is classical, then for any property we might assert of an object of a topos (say), we have . Here I was taking to be the property of being inhabited.
But if the question is whether “any classically well-ordered relation is well-ordered” is true constructively, it seems that the quantifier “any classically well-ordered relation…”, being part of that statement, should be interpreted in the same (constructive) logic in question, not the meta-logic (classical or not).
Thanks for your reaction, Mike. But we might be talking past one another here.
Let me try a different tack. You raised the question in #7, what if the (classically well-ordered) relation were not inhabited? Can we still prove it is well-ordered, constructively? That’s the question I’d like to focus on right now (and I thought that’s what you were driving at as well). My comment in #11 was an attempt to patch together some type of response to that, but I’m happy to put it aside so long as we can satisfactorily answer the question I’m putting out there now.
Well, if it’s not inhabited, then that means that we never have for any . (I presume that the meaning of “the relation is inhabited” is that the relation itself is inhabited, not that its carrier set is inhabited.) Therefore, any inductive subset must contain every , since it contains all the such that (of which there are none). So the relation is well-founded. Maybe this is what you meant by “by vacuity”. But the point I was making in #7 is that constructively, we can’t say that every relation is either inhabited or not inhabited. (That’s why I didn’t phrase the question as “what if the relation were not inhabited?”)
Yes, you’re absolutely right that I phrased #15 inaccurately, and yes, you just recalled the argument I had in mind, i.e., what I meant by “vacuity”. I think we agree on what the issue is, and presently I don’t have a good answer for it.
The statement “every relation is inhabited or not” can be interpreted internally (e.g., for a fixed object we can write down “every relation on is inhabited or not” as a proposition in the internal language). Or, there is an external statement “every object in a topos is inhabited or not”, and I was proposing in #11 that if one accepts LEM in the meta-logic, then of course that statement is true, and we’d be set. (And usually, I personally do accept LEM when reasoning at the meta-level.) But I gather you feel that would be a less than satisfactory response, and I can understand that.
I’ve gathered that you always think of intuitionistic mathematics as the internal language of some topos. I think it’s good to try to get away from that and think of it as a kind of mathematics in its own right, which happens to be interpretable into any topos. And the universally quantified statement “every relation is inhabited or not” makes perfect sense in this intuitionistic mathematics, without needing to either pass to the meta-language or restrict to relations on a particular set. (It can also be interpreted into a topos, if you use stack semantics, but that’s not the point.)
I’ve gathered that you always think of intuitionistic mathematics as the internal language of some topos.
No, that’s not an accurate description of what I think. Not at all.
I think it’s good to try to get away from that and think of it as a kind of mathematics in its own right, which happens to be interpretable into any topos.
In fact I do, and yes certainly. I’m quite happy working in intuitionistic mathematics or in classical mathematics, depending on the context. I actually don’t take a dogmatic stand, but when reasoning around other mathematicians, I’m usually happy to adopt classical first-order logic as a default for reasoning at the meta-level if that is an agreed-upon standard for discussion.
But somehow this discussion seems to be taking a philosophic turn? Right now I’m more concerned with finding a proof of something, or getting straight on the contents of the article.
(That said, I don’t see any philosophic problem in saying something like “every well-pointed topos is Boolean” (Mac Lane and Moerdijk, proposition VI.7) – provided we allow excluded middle in the metalogic. If we don’t allow that, well then, that’s no longer a theorem.)
And the universally quantified statement “every relation is inhabited or not” makes perfect sense in this intuitionistic mathematics…
It makes sense, but it’s not accepted as true in intuitionistic mathematics. (And hey, if that’s the mathematics we agree to have a conversation in, I have no problem with that, but I do want to be clear on the matter.)
I’m very sorry; we really do seem to be talking past each other. I must have misinterpreted what you meant in #11 and #18. You’re right, we should focus on just being clear about what we have a proof of. It sounds like we can prove the following constructively:
Now what exactly is it that we can prove with a classical metatheory? I’m not actually sure I believe that “externally speaking every relation on a type is either inhabited or empty”. The internal meaning of “inhabited” in a topos (for instance) is that the map to 1 is epi, while the internal meaning of “empty” is that it’s isomorphic to 0 — but even in a classical metatheory it’s not true that every object of a topos has one of these properties. On the other hand, the external meaning of “inhabited” is that it admits a map from 1, while the external meaning of “empty” is that it doesn’t admit such a map — but while it’s certainly true in a classical metatheory that every object of a topos has one of these properties, I don’t see how that kind of “emptiness” suffices for the argument by vacuity.
(This is after having drunk some single malt scotch a little while ago; hopefully some of it will be sensible.)
I’m very sorry; we really do seem to be talking past each other. I must have misinterpreted what you meant in #11 and #18.
No worries whatsoever. I was aware that I wasn’t expressing myself as articulately as I should have.
Now what exactly is it that we can prove with a classical metatheory? I’m not actually sure I believe that “externally speaking every relation on a type is either inhabited or empty”. The internal meaning of “inhabited” in a topos (for instance) is that the map to 1 is epi, while the internal meaning of “empty” is that it’s isomorphic to
I actually completely agree with this. First, I agree with these meanings of ’inhabited’ and of ’empty’ (and therefore I think some stuff should be added to inhabited set). This “not inhabited = empty” assertion which was stated in inhabited set obviously holds not in the general topos setting but in some more specific setting; when I was muttering incoherently in #5 about the conundrum of what the nLab means by ’set’, it was really against the backdrop of understanding the exact context of this specific assertion. I.e., there must be some underlying assumptions about what is meant by which I’m not fully clear on, possibly including a well-pointedness assumption, projectivity of , and maybe a few others. (By the way, when I said ’type’ earlier, I meant 0-type, but maybe you understood that.)
The same issues might also play into what we’re discussing now, so for me it’s worthwhile to have this discussion.
Your analysis of what we can prove constructively so far seems spot on.
FWIW: for my own benefit I’m writing up (or have already written up at home) a proof that given an inhabited classically well-founded relation in a topos, the topos must be Boolean. (Perhaps Johnstone covers this?) This might be very easy to see using stack semantics, but for now I’m using just good old-fashioned topos-theoretic reasoning. Not that you need it, but I might make it more public soon.
I had a discussion with Toby a while ago about the meaning of “inhabited” in a topos. It appears to still be present at the bottom of inhabited object. I think I still agree with the conclusions there, that in a general topos one should talk about “internally inhabited” or “externally inhabited”, whereas for a well-pointed topos the two agree, and when talking about sets one should by definition be in the context of a well-pointed topos (such as, for instance, the internal language of an arbitrary topos). But in any case, inhabited set could probably use some clarification.
Re FWIW: I just glanced through the section in the Elephant about AC, and I didn’t see anything about this. I think it will be worthwhile to have such a proof recorded.
Hmm, how about this for a sneaky trick? Suppose is classically well-founded; we want to show it is well-founded. So let be inductive, and let ; we want to show . Since is inductive, it suffices to show that every is in , i.e. we may assume given a such that and show . But now is inhabited, so LEM holds; therefore is well-founded by the previous argument, and so and thus .
Well, I’m not seeing anything wrong with it, but it is indeed tricky! I can’t recall seeing this trick before. It reminds me vaguely (but only vaguely) of the inductive proof that all pigs are yellow. :-)
To me it has a sort of call/cc feel, kind of like the constructive proof that .
Re #23: I wrote up a proof of the topos-theoretic statement alluded to at the end of #21, which can be found here. It’s just a slightly more elaborate form of what Zhen wrote up at math.SE (see #9).
And now I’ve expanded well-founded relation to take into account the fruits of this discussion. (Thanks again, Mike.)
very nice; thanks!
Finally, I added a little to inhabited set.
Thinking a little about some of the relevant issues, I feel as if maybe there should be some declared default assumptions about the category for nLab purposes, that should be considered as in effect unless one specifies otherwise. (Well, this would probably help me anyway, as I’ve frequently been confused what it is we’re assuming or not assuming whenever we speak of or sets in some random nLab article. The article set I haven’t found particularly helpful in this regard, although I might be missing something.)
Some core assumptions might include those stated at well-pointed topos, including projectivity and indecomposability of . Possibly also up for consideration are relatively mild choice principles such as the presentation axiom (is that considered a choice principle? I sort of want to consider it one). Any thoughts on this?
I for one think of presentation axiom as a choice principle.
Presentation is definitely a choice principle. I don’t think it should be included in any “default” core of axioms that’s intended to be constructive. It might not be a bad idea to state a default collection of assumptions about sets somewhere. Or perhaps several default collections, depending on whether the context is “classical”, “constructive”, “predicative”, etc.? E.g. something like “classical” means ETCS+R, “constructive” means a (constructively) well-pointed topos, “predicative” means a well-pointed -pretopos. I do think we should emphasize that this doesn’t mean proofs need to be phrased in “arrow-theoretic” language; the whole point of well-pointedness is that you can treat sets as “things with elements” in the usual way.
You’re right that set is not very helpful, since it mostly discusses “definitional set theories” according to which sets are defined in terms of some other objects. Maybe it could have two sections, one explaining the default axioms/properties that we assume of sets on the nLab, and another explaining how such notions of “set” arise in foundational theories that don’t assert them axiomatically?
Default assumptions about should probably be at Set rather than at set. (Or at foundations or some place like that.)
FWIW, my default assumptions about are that it's a well-pointed Grothendieck topos, that is a well-pointed category satisfying Giraud's axioms. Of course, this is circular, since Giraud's axioms discuss ‘small’ coproducts, but really the point is the other axioms. And you have to be careful how you state those; sometimes people list the existence of small colimits among these axioms, but I wouldn't (and so the list in the nLab doesn't). You also have to be careful how you define well-pointedness, which is something that Mike and I worked out before (and is also in the Lab in the constructivist section); many famous consequences of this condition require excluded middle, and only the right ones (projectivity of , for example, but not booleanness, for example) go into this definition.
As for Giraud's axioms, some important properties of follow directly from these, principally the existence of quotient sets. (Thus notions of ‘set’ or ‘type’ that lack these, such as the types in straight Martin-Löf type theory, are not good enough.) Other properties, such as the existence of arbitrary small (or even finite) colimits, -types (or even a natural numbers object), exponentials, and a subobject classifier, only follow (via the circular axiom about small coproducts) if you already believe in these things in your meta-logic. (The same goes for booleanness, as discussed above about well-pointedness.) So it's up to you whether or not you believe in them; my default assumptions allow for strict finitism and strict predicativism (as well as constructivism, of course).
I forgot to thank you, Toby, for your last comment. These look like eminently reasonable assumptions to me: they are both flexible and principled. I think it might be a good idea to work those into the article Set more formally, as declared default assumptions for our use around the nLab (as many of the relevant articles bear your authorship, this could be helpful).
I’m confused. How are such circular assumptions helpful? And what does it mean to believe in (say) a subobject classifier “in the meta-logic”?
In a higher-order logic, we might have a type (a -type) of truth values. It's a category error to call that a subobject classifier in the metalogic; but a coproduct indexed by it of the terminal object in is a subobject classifier in .
There is only one well-pointed Grothendieck topos (up to a geometric isomorphism which is unique up to a unique natural isomorphism), which I denote . Accordingly, every property of follows from its characterization as a well-pointed Grothendieck topos. Most of this is circular and therefore uninteresting. It is simply noted.
But some of this is not circular. I think that this amounts to saying that is a Heyting pretopos, but you can probably pick this apart.
I feel like there is a size problem. If the metalogic is a HOL like the internal language of a topos, then formulating an object theory such as that of a Heyting pretopos in that logic will be like describing an internal category in that topos. But an internal category can’t reasonably be expected to have coproducts indexed by all objects of the ambient category — it happens occasionally, such as in the effective topos, but that’s a very special situation and you have to be very careful there to even make sense of it.
There is only one well-pointed Grothendieck topos
I don’t think that’s true constructively, even with the constructive definition of “well-pointed”.
an internal category can’t reasonably be expected to have coproducts indexed by all objects of the ambient category
But the ambient category thinks that it does.
Let's try to make this precise. We're working in a Lawvere–Tierney topos (so it has a subobject classifier), we define a well-pointed Grothendieck topos internal to that. This is defined to satisfy Girard's axioms, which say nothing about a subobject classifier, so it may not be (internally) a Lawvere–Tierney topos. But we should be able to prove that it is, using the subobject classifier in the ambient category.
But I realize now that I never did finish learning how to properly describe a large category internal to a topos, which is what we want here. Aren't we supposed to do treat it as an indexed category?
There is only one well-pointed Grothendieck topos
I don’t think that’s true constructively, even with the constructive definition of “well-pointed”.
Do you remember what goes wrong?
Yes, large categories “relative to” a topos are categories indexed over that topos. But I don’t think they should be called “internal” because “internal category” has a standard meaning that’s different. The latter is the sort of internal category that I meant in 38, and I still believe that that’s what you would have to mean if you mean “metalogic” in the usual sense: if a theory is formulated in some metatheory , then a model of is an object of (with structure), but categories indexed over a topos are not objects in the theory of . If a theory has a model that’s an -indexed category, then the metalogic isn’t but rather some “2-categorical logic” of -indexed categories — and we can’t expect an -indexed category to have all coproducts indexed by objects of that theory (even to the eyes of that theory). In the 2-categorical logic of -indexed categories, itself is a sort of “universe of small sets” like in algebraic set theory.
Do you remember what goes wrong?
It’s been a while since I thought about this, but I think the point is that constructively, can have nontrivial proper subtoposes, such as for a truth value , and if is chosen appropriately such a subtopos can be well-pointed.
If a theory has a model that’s an -indexed category, then the metalogic isn’t but rather some “2-categorical logic” of -indexed categories — and we can’t expect an -indexed category to have all coproducts indexed by objects of that theory (even to the eyes of that theory). In the 2-categorical logic of -indexed categories, itself is a sort of “universe of small sets” like in algebraic set theory.
Well, I want the model to be have all small coproducts, that is all coproducts indexed by .
and if is chosen appropriately such a subtopos can be well-pointed.
H'm, this is striking a bell somewhere in my brain.
Okay, this is making a little more sense to me now. We’re assuming a metatheory that has some notion of “small”, such as the “categories of classes” used in algebraic set theory, or a “2-category of large categories” with a discrete opfibration classifier. Then the statement is that is a (large) category in this metatheory which is well-pointed, has “small” coproducts, and satisfies the rest of Giraud’s axioms. Then I’ll believe that if the metatheory has a small subobject classifer in an appropriate sense, it follows that has a subobject classifier, etc.
However, the constructive non-uniqueness of well-pointed Grothendieck topoi makes me somewhat wary of taking this as our “default assumptions” about . I found a note that I wrote to myself a while ago claiming that if is the Sierpinski topos and the interesting subterminal therein, that “ is well-pointed” is true in the stack semantics of . I haven’t tried to re-verify that right now.
I suppose that we could talk about the terminal Grothendieck topos.
Yeah, I think that would work. But it brings in a large quantification.
Sometimes those can be avoided, but I don't see how in this case, not immediately.
We might be able to show constructively that any well-pointed Grothendieck topos must be a subtopos of . If so, then at least if we have subobject classifiers, it must be classified by a LT operator on , of which there are only a small number.
I didn’t fully understand all the details the Todd Trimble’s proof that classical well-foundedness implies LEM, but I figured there is a purely logical proof which is basically Zhen Lin’s proof. Assume that R is inhabited: R(y,x) holds; and R is classically well-founded, then consider the set P = { x } ∪ { a | R(a, x) & Q }. It is inhabited and thus have a minimal element x_0. If x_0 = x then Q does not hold: for if it does, then y<x and hence x is not a minimal element. If x_0 =/= x, then Q must hold.
I have formalised this proof and some of the others in Coq, if it is of interest to someone: https://gist.github.com/co-dan/887fb4dbe4cc2f51be868e4a27721b97
I'd avoid the phrasing ‘if ’; it should be ‘if ’. Your phrasing makes it appear that you’re using LEM, assuming that or . What we actually have is that or , or equivalently that or . (OK, does follow from , but what matters is that follows, so it's misleading to bring in that .)
Anyway, I agree with the proof. Combined with Mike's trick from #24, this proves that any classically well-founded relation is (constructively) well-founded.
Yes, this seems to work and is simpler than Todd’s proof. Thanks! Would you like to record this on the page well-founded relation?
I have updated the page with the proof.
Great, thanks!
Any good references for well-founded relations?
Classically or constructively? Classically, there is probably an embarrassment of riches; probably most books on set theory will discuss them to some extent. Constructively, some references that pop into my (totally biased) mind are Paul Taylor’s book PFM and his paper Intuitionistic sets and ordinals, the HoTT Book chapter 10, and section 8 of this paper of mine.
Can you prove well-founded induction from your definition of well-foundedness, without LEM? Every proof I’ve found has used LEM.
Which definition are you talking about? The ones in the constructive references I cited are essentially the same as the one at well-founded relation, which basically asserts well-founded induction by definition.
If we have some property of all how can we show the following:
Which is the statement for well-founded induction in classical logic. I am not following how this follows from the definitions.
Clearly showing one way is trivial, but the the converse… all proofs I have seen do this by contradiction. Suppose some such that , then constructing the set which is well founded, hence has a -minimal element eventually leading to a contradiction.
See Prop. 1.4 in Paul Taylor’s Intuitionistic Sets and Ordinals, also mentioned in #54, and the UniMath formalization by Peter Lumsdaine.
@57 Alizter: Doesn’t it follow from the right-hand side of your equivalence that is (in the terminology of the nlab article) ≺-inductive? If is well-founded, then this set has to be equal to (by definition of well-foundedness on the nlab), hence your left-hand side.
I think you might currently be using the “every inhabited subset has a minimal element” definition of well-foundedness. This is constructively not equivalent to the definition on the nlab. For example, consider the set . Then constructively finding a minimal element of this set (wrt. to the usual order on ) is equivalent to proving or disproving the continuum hypothesis and hence impossible. However, is well-founded as defined on the nlab (“every <-inductive subset of is equal to ”).
Re 59. I should have probably made it clearer that I was giving the classical proof of well-founded induction using the classical definitions.
The classical definition of well-founded relation on a set is exactly what one needs in order to prove well-founded induction. The proof for this requires LEM and not to mention the non-constructivity when talking about minimal elements.
I see this intuitionistic definition and it avoids talking about minimal elements, so I wonder how can it be used to prove well-founded induction?
As I said, the intuitionistic definition is exactly written so as to imply well-founded induction. As mbid said, given such that , let . Then is -inductive; that’s precisely what the assumption about says. Therefore, by the definition of well-foundedness, , which is to say .
OK my confusion was coming from the definitons I was using. I originally had Mike’s paper’s definitions in mind, not the nlab article. But now reading the nlab article it makes more sense.
The definition in my paper is the same as the one on the nLab.
1 to 63 of 63