Not signed in

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

• Username
• Password
• Remember me

• Sign in using OpenID
• Remember me

• Forgot your password?
• Apply for membership

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 definitions 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 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 nforum 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 superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory tqft type type-theory universal variational-calculus

1. • CommentRowNumber1.
   • CommentAuthorMike Shulman
   • CommentTimeFeb 1st 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItex[[apartness relation]] says > The negation of an apartness relation is an equivalence relation. (The converse of this is equivalent to excluded middle.) But it seems to me that the converse ("the negation of an equivalence relation is an apartness relation") only requires de Morgan's law. If $\approx$ is an equivalence relation, then certainly $\neg\neg(x\approx x)$ and $\neg (x\approx y) \to \neg(y\approx x)$, so the only thing to worry about is comparison. If $\neg (x\approx z)$, then contraposing transitivity gives $\neg (x\approx y \wedge y\approx z)$, which by de Morgan gives $\neg (x\approx y) \vee \neg (y\approx z)$.

   apartness relation says

   The negation of an apartness relation is an equivalence relation. (The converse of this is equivalent to excluded middle.)

   But it seems to me that the converse (“the negation of an equivalence relation is an apartness relation”) only requires de Morgan’s law. If $\approx$ is an equivalence relation, then certainly $\neg\neg(x\approx x)$ and $\neg (x\approx y) \to \neg(y\approx x)$, so the only thing to worry about is comparison. If $\neg (x\approx z)$, then contraposing transitivity gives $\neg (x\approx y \wedge y\approx z)$, which by de Morgan gives $\neg (x\approx y) \vee \neg (y\approx z)$.

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeFeb 1st 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexAlso, why did I never notice this before: an apartness relation on a set $X$ is the same as a (strongly) closed equivalence relation on the discrete locale of $X$, and the apartness topology is its quotient in $Loc$. Similarly, an antiideal is a closed ideal in a discrete localic ring, and so on. I've added this to [[apartness relation]].

   Also, why did I never notice this before: an apartness relation on a set $X$ is the same as a (strongly) closed equivalence relation on the discrete locale of $X$, and the apartness topology is its quotient in $Loc$. Similarly, an antiideal is a closed ideal in a discrete localic ring, and so on. I’ve added this to apartness relation.

3. • CommentRowNumber3.
   • CommentAuthorTobyBartels
   • CommentTimeFeb 1st 2017
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexThe converse isn\'t "the negation of an equivalence relation is an apartness relation"; it\'s ‘every equivalence relation is the negation of an apartness relation’. That\'s equivalent to excluded middle. But your fact is also noteworthy.

   The converse isn't “the negation of an equivalence relation is an apartness relation”; it's ‘every equivalence relation is the negation of an apartness relation’. That's equivalent to excluded middle.

   But your fact is also noteworthy.

4. • CommentRowNumber4.
   • CommentAuthorTobyBartels
   • CommentTimeFeb 1st 2017
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexThat localic stuff is interesting! You might want to put something at [[antisubalgebra]] too. (That hadn\'t been linked to from [[apartness relation]], but I fixed that a little bit.)

   That localic stuff is interesting! You might want to put something at antisubalgebra too. (That hadn't been linked to from apartness relation, but I fixed that a little bit.)

5. • CommentRowNumber5.
   • CommentAuthorMike Shulman
   • CommentTimeFeb 1st 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItex> The converse isn\'t "the negation of an equivalence relation is an apartness relation"; it\'s ‘every equivalence relation is the negation of an apartness relation’. Hmm. Ordinarily we take the converse of an implication $P\to Q$, yielding $Q\to P$. The original statement "the negation of an apartness relation is an equivalence relation" has the form $\forall x, (P(x) \to Q(f(x)))$, which is not an implication at top-level. One might argue that the most natural thing to call its "converse" would be $\forall x, (Q(f(x)) \to P(x))$, i.e. "if the negation of a relation $\#$ is an equivalence relation, then $\#$ is an apartness relation". My interpretation $\forall x, (Q(x) \to P(f(x)))$ is somewhat less defensible, but it still seems more like a converse than $\forall y, (Q(y) \to \exists x, (P(x) \wedge f(x)=y))$ to me. In any case, I've edited the page to say specifically what it means.

   The converse isn't “the negation of an equivalence relation is an apartness relation”; it's ‘every equivalence relation is the negation of an apartness relation’.

   Hmm. Ordinarily we take the converse of an implication $P\to Q$, yielding $Q\to P$. The original statement “the negation of an apartness relation is an equivalence relation” has the form $\forall x, (P(x) \to Q(f(x)))$, which is not an implication at top-level. One might argue that the most natural thing to call its “converse” would be $\forall x, (Q(f(x)) \to P(x))$, i.e. “if the negation of a relation $\#$ is an equivalence relation, then $\#$ is an apartness relation”. My interpretation $\forall x, (Q(x) \to P(f(x)))$ is somewhat less defensible, but it still seems more like a converse than $\forall y, (Q(y) \to \exists x, (P(x) \wedge f(x)=y))$ to me.

   In any case, I’ve edited the page to say specifically what it means.

6. • CommentRowNumber6.
   • CommentAuthorTobyBartels
   • CommentTimeFeb 2nd 2017
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexWe\'re working in the context of a set (called $S$ in the article) and a binary relation on $S$ (called $x$ in your comment); there is no need to confuse the issue by introducing a universal quantification in an emptier context. If $P$ means that $x$ is the negation of an apartness relation and $Q$ means that $x$ is an equivalence relation, then the statement in question is $P \to Q$, and the converse $Q \to P$ is the one that I thought of. But if $P$ means that $x$ is an apartness relation and $Q$ means that the negation of $x$ is an equivalence relation, then the statement in question is still $P \to Q$, but now the converse $Q \to P$ is what you said it was in your most recent comment. This underscores that the converse is not an operation on statements as such but an operation on a particular presentation of a statement, so it can be ambiguous. Yet another way to analyse it would be to work in context where $S$ is a set and $x$ is an *apartness* relation on $S$. Then the statement in question is $P \to Q$ in a trivial way, where $P$ is [[truth]] and $Q$ means that the negation of $x$ is an equivalence relation. The converse of that one is always true!

   We're working in the context of a set (called $S$ in the article) and a binary relation on $S$ (called $x$ in your comment); there is no need to confuse the issue by introducing a universal quantification in an emptier context.

   If $P$ means that $x$ is the negation of an apartness relation and $Q$ means that $x$ is an equivalence relation, then the statement in question is $P \to Q$, and the converse $Q \to P$ is the one that I thought of. But if $P$ means that $x$ is an apartness relation and $Q$ means that the negation of $x$ is an equivalence relation, then the statement in question is still $P \to Q$, but now the converse $Q \to P$ is what you said it was in your most recent comment.

   This underscores that the converse is not an operation on statements as such but an operation on a particular presentation of a statement, so it can be ambiguous.

   Yet another way to analyse it would be to work in context where $S$ is a set and $x$ is an apartness relation on $S$. Then the statement in question is $P \to Q$ in a trivial way, where $P$ is truth and $Q$ means that the negation of $x$ is an equivalence relation. The converse of that one is always true!

7. • CommentRowNumber7.
   • CommentAuthorMike Shulman
   • CommentTimeFeb 2nd 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI disagree that "we are working in the context of a set $S$ and a binary relation on $S$". There are *two* relations that play a role in the statement, one of which is the negation of the other. Your two analyses use the letter $x$ to denote one or the other of these relations; this makes it clear to me that there is no obvious or canonical choice of *one* binary relation on $S$ to be "in the context".

   I disagree that “we are working in the context of a set $S$ and a binary relation on $S$”. There are two relations that play a role in the statement, one of which is the negation of the other. Your two analyses use the letter $x$ to denote one or the other of these relations; this makes it clear to me that there is no obvious or canonical choice of one binary relation on $S$ to be “in the context”.

8. • CommentRowNumber8.
   • CommentAuthorTobyBartels
   • CommentTimeFeb 3rd 2017
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItexYes, the precise way to analyse the statement with logical operators is ambiguous, as I remarked. Even for my two analyses based on the context $S\colon Set, x\colon Rel(S,S)$ (I also had a third, sillier analysis with the context $S\colon Set, x\colon ApRel(S)$), even though they appear to have the same context, the interpretations of that context differ in the two analyses. If that\'s all that you want to point out, then I agree. I mentioned context to explain why you should never complain that something is ‘not an implication at top-level’ (comment \#5) when it *is* an implication immediately inside a universal quantification, because you can move the quantifier to the context. It is perfectly standard that the converse of $\forall x, P(x) \to Q(x)$ is $\forall x, Q(x) \to P(x)$. (That\'s arguably the original form, going back to Aristotle, although of course he didn\'t analyse it as a quantifier and implication.) See [examples on the English Wikipedia page](https://en.wikipedia.org/wiki/Converse_%28logic%29). That page also has the helpful advice ‘In practice, when determining the converse of a mathematical theorem, aspects of the antecedent may be taken as establishing context.’, offering the format ‘Given $P$, if $Q$, then $R$.’ with the converse ‘Given $P$, if $R$, then $Q$.’. Much of the ambiguity in a statement\'s converse is going to come from deciding how much to put in the context $P$. Often, it\'s quite a lot!

   Yes, the precise way to analyse the statement with logical operators is ambiguous, as I remarked. Even for my two analyses based on the context $S\colon Set, x\colon Rel(S,S)$ (I also had a third, sillier analysis with the context $S\colon Set, x\colon ApRel(S)$), even though they appear to have the same context, the interpretations of that context differ in the two analyses. If that's all that you want to point out, then I agree.

   I mentioned context to explain why you should never complain that something is ‘not an implication at top-level’ (comment #5) when it is an implication immediately inside a universal quantification, because you can move the quantifier to the context. It is perfectly standard that the converse of $\forall x, P(x) \to Q(x)$ is $\forall x, Q(x) \to P(x)$. (That's arguably the original form, going back to Aristotle, although of course he didn't analyse it as a quantifier and implication.) See examples on the English Wikipedia page.

   That page also has the helpful advice ‘In practice, when determining the converse of a mathematical theorem, aspects of the antecedent may be taken as establishing context.’, offering the format ‘Given $P$, if $Q$, then $R$.’ with the converse ‘Given $P$, if $R$, then $Q$.’. Much of the ambiguity in a statement's converse is going to come from deciding how much to put in the context $P$. Often, it's quite a lot!

9. • CommentRowNumber9.
   • CommentAuthorMike Shulman
   • CommentTimeFeb 3rd 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexFair enough. Thanks for adding to my correction.

   Fair enough. Thanks for adding to my correction.

10. • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 3rd 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexMoving old discussion to here from the page [[apartness relation]]: > _[[Urs Schreiber|Urs]] says_: What you say at the entry [[vector space]] about the relation between apartness relations and topology and the continuum sounds very interesting. It would be nice if you could move these comments here and maybe flesh them out a little. Because, while it sounds interesting, I don't yet understand what you are saying! > * _[[Toby Bartels|Toby]] replies_: I will try to write a bit about the topological ideas that come up. But keep in mind that classically it is all trivial, unless you rephrase it internal to some more general notion of category than a boolean topos, and these things are not normally so phrased. > _[[Urs Schreiber|Urs]] replies to the reply:_ Okay, I'll keep it in mind. But I am still interested! :-) > I already have problems with the above definition. When you say "coproduct" do you mean to equip $\{true, false\}$ with the monoidal structure given by logical OR? This is the only meaning I can give this word here, but a category enriched over $(\{true, false\},\otimes = OR)$ seems necessarily to be an indiscrete groupoid over its set of objects. (Because $hom(a,a) = true$ for all objects $a$ and then $hom(a,b) = hom(a,a) OR hom(a,b) = true$, too, for all $b$.) > * _[[Toby Bartels|Toby]] replies_: To begin with, I defined it incorrectly; the trouble with these slick category-theoretic definitions is that a small error makes things completely messed up! I rephrased it quite a bit, but the key point is the new word 'opposite'. That said, your analysis of even my original definition is unsound; keep in mind that the unit of disjunction is *false*. > _Toby adds_: Also, it\'s an enriched *groupoid*, not an enriched *category*. > I am also not sure in which sense you refer to the law of the excluded middle. Should we maybe more generally say that the 0-category of (-1)-categories internal to a given topos $T$ is the subobject classifier, $(-1)Cat := \Omega$? > * _[[Toby Bartels|Toby]] replies_: Yes, that is correct; $(-1)\Cat = \Omega$. Even when $T := \Set$, you have $(-1)\Cat = \{\top, \bot\}$ *only* if you believe excluded middle, which constructivists do not. Thus, constructivists will talk about apartness relations in $\Set$, while a classical mathematician will have to put the discussion internal to $T$ to get nontrivial results. > _[[Urs Schreiber|Urs]] replies to the reply:_ I like this statement "$(-1)\Cat = \Omega$". Would we also want to say $(-2)Cat = \{1 \stackrel{\top}{\to} \Omega\}$?

    Moving old discussion to here from the page apartness relation:

    Urs says: What you say at the entry vector space about the relation between apartness relations and topology and the continuum sounds very interesting. It would be nice if you could move these comments here and maybe flesh them out a little. Because, while it sounds interesting, I don’t yet understand what you are saying!

    • Toby replies: I will try to write a bit about the topological ideas that come up. But keep in mind that classically it is all trivial, unless you rephrase it internal to some more general notion of category than a boolean topos, and these things are not normally so phrased.

      Urs replies to the reply: Okay, I’ll keep it in mind. But I am still interested! :-)

    I already have problems with the above definition. When you say “coproduct” do you mean to equip $\{true, false\}$ with the monoidal structure given by logical OR? This is the only meaning I can give this word here, but a category enriched over $(\{true, false\},\otimes = OR)$ seems necessarily to be an indiscrete groupoid over its set of objects. (Because $hom(a,a) = true$ for all objects $a$ and then $hom(a,b) = hom(a,a) OR hom(a,b) = true$, too, for all $b$.)

    • Toby replies: To begin with, I defined it incorrectly; the trouble with these slick category-theoretic definitions is that a small error makes things completely messed up! I rephrased it quite a bit, but the key point is the new word ’opposite’. That said, your analysis of even my original definition is unsound; keep in mind that the unit of disjunction is false.

      Toby adds: Also, it's an enriched groupoid, not an enriched category.

    I am also not sure in which sense you refer to the law of the excluded middle. Should we maybe more generally say that the 0-category of (-1)-categories internal to a given topos $T$ is the subobject classifier, $(-1)Cat := \Omega$?

    • Toby replies: Yes, that is correct; $(-1)\Cat = \Omega$. Even when $T := \Set$, you have $(-1)\Cat = \{\top, \bot\}$ only if you believe excluded middle, which constructivists do not. Thus, constructivists will talk about apartness relations in $\Set$, while a classical mathematician will have to put the discussion internal to $T$ to get nontrivial results.

      Urs replies to the reply: I like this statement “$(-1)\Cat = \Omega$”. Would we also want to say $(-2)Cat = \{1 \stackrel{\top}{\to} \Omega\}$?

11. • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeNov 23rd 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexThe page [[apartness relation]] used to say that the general notion was probably not introduced by Bishop but only by Troelstra+van Dalen (1988). I have a copy of the 1985 Bishop + Bridges and they *do* define the general notion of apartness relation (under the name "inequality relation"). But I looked at the original 1967 Bishop on Amazon preview and I didn't see it there (searching for "inequality" didn't turn up a definition; and the definition of "complemented subset", which uses an inequality in the 1985 version, in 1967 instead uses "a nonvoid set of functions to $\mathbb{R}$" to essentially induce an inequality on the domain). So I'm guessing this was an addition in the 1985 version, and I've updated the references accordingly.

    The page apartness relation used to say that the general notion was probably not introduced by Bishop but only by Troelstra+van Dalen (1988). I have a copy of the 1985 Bishop + Bridges and they do define the general notion of apartness relation (under the name “inequality relation”). But I looked at the original 1967 Bishop on Amazon preview and I didn’t see it there (searching for “inequality” didn’t turn up a definition; and the definition of “complemented subset”, which uses an inequality in the 1985 version, in 1967 instead uses “a nonvoid set of functions to $\mathbb{R}$” to essentially induce an inequality on the domain). So I’m guessing this was an addition in the 1985 version, and I’ve updated the references accordingly.

12. • CommentRowNumber12.
    • CommentAuthorfwaaldijk
    • CommentTimeNov 23rd 2017
    • PermaLink
    Author: fwaaldijk
    Format: MarkdownItexI'm completely claimed by other activities, so just a historical comment in passing. I believe Brouwer introduced apartness relations, already way early in the 1920s. Anyway, they were standard in intuitionistic mathematics for decades before Bishop1967. If ever I get some time, I'll look it up properly.

    I’m completely claimed by other activities, so just a historical comment in passing. I believe Brouwer introduced apartness relations, already way early in the 1920s. Anyway, they were standard in intuitionistic mathematics for decades before Bishop1967. If ever I get some time, I’ll look it up properly.

13. • CommentRowNumber13.
    • CommentAuthorMike Shulman
    • CommentTimeNov 23rd 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexThanks! That's not surprising to me, but then it is surprising that Bishop 1967 didn't use them.

    Thanks! That’s not surprising to me, but then it is surprising that Bishop 1967 didn’t use them.

14. • CommentRowNumber14.
    • CommentAuthorMike Shulman
    • CommentTimeNov 24th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexAccording to Troelstra & van Dalen, > Brouwer (1919) introduced the notion of apartness (örtlich verschieden, Entfernung).... The axioms of the theory of apartness were formulated by Heyting (1925). I'll add this to the page, as soon as the nLab can be edited again.

    According to Troelstra & van Dalen,

    Brouwer (1919) introduced the notion of apartness (örtlich verschieden, Entfernung)…. The axioms of the theory of apartness were formulated by Heyting (1925).

    I’ll add this to the page, as soon as the nLab can be edited again.

15. • CommentRowNumber15.
    • CommentAuthorMike Shulman
    • CommentTimeNov 26th 2017
    • PermaLink
    Author: Mike Shulman
    Format: MarkdownItexOkay, I added this note to [[apartness relation]], and a related quote to [[antisubalgebra]].

    Okay, I added this note to apartness relation, and a related quote to antisubalgebra.

16. • CommentRowNumber16.
    • CommentAuthornLab edit announcer
    • CommentTimeDec 8th 2022
    • PermaLink
    Author: nLab edit announcer
    Format: MarkdownItexadding a section on the foundational status of inequality spaces Anonymous <a href="https://ncatlab.org/nlab/revision/diff/apartness+relation/60">diff</a>, <a href="https://ncatlab.org/nlab/revision/apartness+relation/60">v60</a>, <a href="https://ncatlab.org/nlab/show/apartness+relation">current</a>

    adding a section on the foundational status of inequality spaces

    Anonymous

    diff, v60, current

17. • CommentRowNumber17.
    • CommentAuthornLab edit announcer
    • CommentTimeDec 8th 2022
    • PermaLink
    Author: nLab edit announcer
    Format: MarkdownItexmoving material about inequality spaces to its own page [[inequality space]] Anonymous <a href="https://ncatlab.org/nlab/revision/diff/apartness+relation/60">diff</a>, <a href="https://ncatlab.org/nlab/revision/apartness+relation/60">v60</a>, <a href="https://ncatlab.org/nlab/show/apartness+relation">current</a>

    moving material about inequality spaces to its own page inequality space

    Anonymous

    diff, v60, current