nForum - Discussion Feed (well-founded relation) 2020-09-30T16:54:54-04:00 https://nforum.ncatlab.org/ Lussumo Vanilla & Feed Publisher Mike Shulman comments on "well-founded relation" (74457) https://nforum.ncatlab.org/discussion/5939/?Focus=74457#Comment_74457 2018-12-06T09:50:40-05:00 2020-09-30T16:54:53-04:00 Mike Shulman https://nforum.ncatlab.org/account/3/ The definition in my paper is the same as the one on the nLab.

The definition in my paper is the same as the one on the nLab.

]]>
Ali Caglayan comments on "well-founded relation" (74445) https://nforum.ncatlab.org/discussion/5939/?Focus=74445#Comment_74445 2018-12-06T04:14:22-05:00 2020-09-30T16:54:53-04:00 Ali Caglayan https://nforum.ncatlab.org/account/1731/ 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.

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.

]]>
Mike Shulman comments on "well-founded relation" (74402) https://nforum.ncatlab.org/discussion/5939/?Focus=74402#Comment_74402 2018-12-04T18:39:33-05:00 2020-09-30T16:54:53-04:00 Mike Shulman https://nforum.ncatlab.org/account/3/ As I said, the intuitionistic definition is exactly written so as to imply well-founded induction. As mbid said, given PP such that ...

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)$.

]]>
Ali Caglayan comments on "well-founded relation" (74393) https://nforum.ncatlab.org/discussion/5939/?Focus=74393#Comment_74393 2018-12-04T08:11:52-05:00 2020-09-30T16:54:54-04:00 Ali Caglayan https://nforum.ncatlab.org/account/1731/ 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 ...

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?

]]>
mbid comments on "well-founded relation" (74392) https://nforum.ncatlab.org/discussion/5939/?Focus=74392#Comment_74392 2018-12-04T06:53:37-05:00 2020-09-30T16:54:54-04:00 mbid https://nforum.ncatlab.org/account/1772/ @57 Alizter: Doesn’t it follow from the right-hand side of your equivalence that {x&Element;X&VerticalBar;P(x)}\{x \in X \mid P(x) \} is (in the terminology of the nlab article) ...

@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}$”).

]]>
Ulrik comments on "well-founded relation" (74390) https://nforum.ncatlab.org/discussion/5939/?Focus=74390#Comment_74390 2018-12-04T05:33:32-05:00 2020-09-30T16:54:54-04:00 Ulrik https://nforum.ncatlab.org/account/54/ See Prop. 1.4 in Paul Taylor’s Intuitionistic Sets and Ordinals, also mentioned in #54, and the UniMath formalization by Peter Lumsdaine.

See Prop. 1.4 in Paul Taylor’s Intuitionistic Sets and Ordinals, also mentioned in #54, and the UniMath formalization by Peter Lumsdaine.

]]>
Ali Caglayan comments on "well-founded relation" (74389) https://nforum.ncatlab.org/discussion/5939/?Focus=74389#Comment_74389 2018-12-04T02:15:43-05:00 2020-09-30T16:54:54-04:00 Ali Caglayan https://nforum.ncatlab.org/account/1731/ If we have some property PP of all x&Element;Xx \in X how can we show the ...

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.

]]>
Mike Shulman comments on "well-founded relation" (74381) https://nforum.ncatlab.org/discussion/5939/?Focus=74381#Comment_74381 2018-12-03T13:18:09-05:00 2020-09-30T16:54:54-04:00 Mike Shulman https://nforum.ncatlab.org/account/3/ 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 ...

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.

]]>
Ali Caglayan comments on "well-founded relation" (74380) https://nforum.ncatlab.org/discussion/5939/?Focus=74380#Comment_74380 2018-12-03T11:44:06-05:00 2020-09-30T16:54:54-04:00 Ali Caglayan https://nforum.ncatlab.org/account/1731/ Can you prove well-founded induction from your definition of well-foundedness, without LEM? Every proof I’ve found has used LEM.

Can you prove well-founded induction from your definition of well-foundedness, without LEM? Every proof I’ve found has used LEM.

]]>
Mike Shulman comments on "well-founded relation" (74351) https://nforum.ncatlab.org/discussion/5939/?Focus=74351#Comment_74351 2018-12-03T02:00:15-05:00 2020-09-30T16:54:54-04:00 Mike Shulman https://nforum.ncatlab.org/account/3/ 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 ...

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.

]]>
Ali Caglayan comments on "well-founded relation" (74345) https://nforum.ncatlab.org/discussion/5939/?Focus=74345#Comment_74345 2018-12-02T22:20:43-05:00 2020-09-30T16:54:54-04:00 Ali Caglayan https://nforum.ncatlab.org/account/1731/ Any good references for well-founded relations?

Any good references for well-founded relations?

]]>
Todd_Trimble comments on "well-founded relation" (70704) https://nforum.ncatlab.org/discussion/5939/?Focus=70704#Comment_70704 2018-08-10T09:45:33-04:00 2020-09-30T16:54:54-04:00 Todd_Trimble https://nforum.ncatlab.org/account/24/ Added the proof of uniqueness of simulations from a well-founded coalgebra to a weakly extensional coalgebra. diff, v37, current

Added the proof of uniqueness of simulations from a well-founded coalgebra to a weakly extensional coalgebra.

]]>
Mike Shulman comments on "well-founded relation" (61962) https://nforum.ncatlab.org/discussion/5939/?Focus=61962#Comment_61962 2017-04-07T13:33:18-04:00 2020-09-30T16:54:54-04:00 Mike Shulman https://nforum.ncatlab.org/account/3/ Great, thanks!

Great, thanks!

]]>
Daniil comments on "well-founded relation" (61958) https://nforum.ncatlab.org/discussion/5939/?Focus=61958#Comment_61958 2017-04-07T07:39:40-04:00 2020-09-30T16:54:54-04:00 Daniil https://nforum.ncatlab.org/account/1426/ I have updated the page with the proof.

I have updated the page with the proof.

]]>
Mike Shulman comments on "well-founded relation" (61952) https://nforum.ncatlab.org/discussion/5939/?Focus=61952#Comment_61952 2017-04-06T14:42:44-04:00 2020-09-30T16:54:54-04:00 Mike Shulman https://nforum.ncatlab.org/account/3/ 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?

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?

]]>
TobyBartels comments on "well-founded relation" (61933) https://nforum.ncatlab.org/discussion/5939/?Focus=61933#Comment_61933 2017-04-05T13:55:05-04:00 2020-09-30T16:54:54-04:00 TobyBartels https://nforum.ncatlab.org/account/7/ I'd avoid the phrasing ‘if x 0&ne;xx_0 \ne x’; it should be ‘if R(x 0,x)&amp;QR(x_0,x) \:\&amp;\: Q’. Your phrasing makes it appear that you’re using LEM, assuming that x ...

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.

]]>
Daniil comments on "well-founded relation" (61932) https://nforum.ncatlab.org/discussion/5939/?Focus=61932#Comment_61932 2017-04-05T13:16:44-04:00 2020-09-30T16:54:54-04:00 Daniil https://nforum.ncatlab.org/account/1426/ 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 ...

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

]]>
Mike Shulman comments on "well-founded relation" (47609) https://nforum.ncatlab.org/discussion/5939/?Focus=47609#Comment_47609 2014-06-05T00:58:11-04:00 2020-09-30T16:54:54-04:00 Mike Shulman https://nforum.ncatlab.org/account/3/ We might be able to show constructively that any well-pointed Grothendieck topos must be a subtopos of SetSet. If so, then at least if we have subobject classifiers, it must be classified by a LT ...

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.

]]>
TobyBartels comments on "well-founded relation" (47605) https://nforum.ncatlab.org/discussion/5939/?Focus=47605#Comment_47605 2014-06-04T20:16:22-04:00 2020-09-30T16:54:54-04:00 TobyBartels https://nforum.ncatlab.org/account/7/ Sometimes those can be avoided, but I don't see how in this case, not immediately.

Sometimes those can be avoided, but I don't see how in this case, not immediately.

]]>
Mike Shulman comments on "well-founded relation" (47601) https://nforum.ncatlab.org/discussion/5939/?Focus=47601#Comment_47601 2014-06-04T17:54:45-04:00 2020-09-30T16:54:54-04:00 Mike Shulman https://nforum.ncatlab.org/account/3/ Yeah, I think that would work. But it brings in a large quantification.

Yeah, I think that would work. But it brings in a large quantification.

]]>
TobyBartels comments on "well-founded relation" (47597) https://nforum.ncatlab.org/discussion/5939/?Focus=47597#Comment_47597 2014-06-04T11:17:42-04:00 2020-09-30T16:54:54-04:00 TobyBartels https://nforum.ncatlab.org/account/7/ I suppose that we could talk about the terminal Grothendieck topos.

I suppose that we could talk about the terminal Grothendieck topos.

]]>
Mike Shulman comments on "well-founded relation" (47576) https://nforum.ncatlab.org/discussion/5939/?Focus=47576#Comment_47576 2014-06-03T07:52:18-04:00 2020-09-30T16:54:54-04:00 Mike Shulman https://nforum.ncatlab.org/account/3/ 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 ...

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.

]]>
TobyBartels comments on "well-founded relation" (47567) https://nforum.ncatlab.org/discussion/5939/?Focus=47567#Comment_47567 2014-06-02T22:07:23-04:00 2020-09-30T16:54:54-04:00 TobyBartels https://nforum.ncatlab.org/account/7/ If a theory TT has a model that’s an EE-indexed category, then the metalogic isn’t EE but rather some “2-categorical logic” of EE-indexed categories — and we can’t expect an EE-indexed ...

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.

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.

]]>
Mike Shulman comments on "well-founded relation" (47529) https://nforum.ncatlab.org/discussion/5939/?Focus=47529#Comment_47529 2014-06-01T00:33:55-04:00 2020-09-30T16:54:54-04:00 Mike Shulman https://nforum.ncatlab.org/account/3/ 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 ...

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.

]]>