The definition in my paper is the same as the one on the nLab.
]]>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.
]]>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 .
]]>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?
]]>@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 ”).
]]>See Prop. 1.4 in Paul Taylor’s Intuitionistic Sets and Ordinals, also mentioned in #54, and the UniMath formalization by Peter Lumsdaine.
]]>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.
]]>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.
]]>Can you prove well-founded induction from your definition of well-foundedness, without LEM? Every proof I’ve found has used LEM.
]]>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.
]]>Any good references for well-founded relations?
]]>Added the proof of uniqueness of simulations from a well-founded coalgebra to a weakly extensional coalgebra.
]]>Great, thanks!
]]>I have updated the page with the proof.
]]>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'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.
]]>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
]]>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.
]]>Sometimes those can be avoided, but I don't see how in this case, not immediately.
]]>Yeah, I think that would work. But it brings in a large quantification.
]]>I suppose that we could talk about the terminal Grothendieck topos.
]]>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.
]]>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.
]]>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.
]]>