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 $P$ such that $\forall x \in X, ((\forall y \prec x, P(y)) \Rightarrow P(x))$, let $A = \{x\in X \mid P(x)\}$. Then $A$ is $\prec$-inductive; that’s precisely what the assumption about $P$ says. Therefore, by the definition of well-foundedness, $A=X$, which is to say $\forall x\in X, P(x)$.

]]>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 $\{x \in X \mid P(x) \}$ is (in the terminology of the nlab article) ≺-inductive? If $X$ is well-founded, then this set has to be equal to $X$ (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 $\{n \in \mathbb{N} \mid n = 1 \, \text{ or } \, n = 0 \, \text{ and the continuum hypothesis is true} \}$. Then constructively finding a minimal element of this set (wrt. to the usual order on $\mathbb{N}$) is equivalent to proving or disproving the continuum hypothesis and hence impossible. However, $\mathbb{N}$ is well-founded as defined on the nlab (“every <-inductive subset of $\mathbb{N}$ is equal to $\mathbb{N}$”).

]]>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 $P$ of all $x \in X$ how can we show the following:

$\forall x \in X, P(x) \iff \forall x \in X, ((\forall y \prec x, P(y)) \Rightarrow P(x))$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 $x$ such that $\neg P(X)$, then constructing the set $\{ x \in X \mid \neg P(x)\}$ which is well founded, hence has a $\prec$-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 $x_0 \ne x$’; it should be ‘if $R(x_0,x) \:\&\: Q$’. Your phrasing makes it appear that you’re using LEM, assuming that $x_0 = x$ or $x_0 \ne x$. What we actually have is that $x_0 \in \{x\}$ or $x_0 \in \{a \;|\; R(a,x) \:\&\: Q\}$, or equivalently that $x_0 = x$ or $R(x_0,x) \:\&\: Q$. (OK, $x_0 \ne x$ does follow from $R(a,x) \:\&\: Q$, but what matters is that $Q$ follows, so it's misleading to bring in that $x_0 \ne x$.)

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 $Set$. If so, then at least if we have subobject classifiers, it must be classified by a LT operator on $Set$, 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 $Set$ 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 $Set$ 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 $Set$. I found a note that I wrote to myself a while ago claiming that if $E$ is the Sierpinski topos and $U$ the interesting subterminal therein, that “$E/U$ is well-pointed” is true in the stack semantics of $E$. I haven’t tried to re-verify that right now.

]]>If a theory $T$ has a model that’s an $E$-indexed category, then the metalogic isn’t $E$ but rather some “2-categorical logic” of $E$-indexed categories — and we can’t expect an $E$-indexed category to have all coproducts indexed by objects of

thattheory (even to the eyes of that theory). In the 2-categorical logic of $E$-indexed categories, $E$ 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 $E$.

and if $U$ 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 $T$ is formulated in some metatheory $T'$, then a model of $T$ is an *object* of $T'$ (with structure), but categories indexed over a topos $E$ are not objects in the theory of $E$. If a theory $T$ has a model that’s an $E$-indexed category, then the metalogic isn’t $E$ but rather some “2-categorical logic” of $E$-indexed categories — and we can’t expect an $E$-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 $E$-indexed categories, $E$ 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, $Set$ can have nontrivial proper subtoposes, such as $Set/U$ for a truth value $U$, and if $U$ is chosen appropriately such a subtopos can be well-pointed.

]]>