Not signed in

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

Site Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).

nLab > Latest Changes: apartness relation

Bottom of Page

1 to 17 of 17

- 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)$ .
- 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.
- 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.
- 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.)
- 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.
- 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!
- 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”.
- 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!
- 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.
- 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\}$ ?
- 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.
- 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.
- 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.
- 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.
- 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.
- 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
- 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

1 to 17 of 17

nForum

Discussion Feed

Not signed in

Site Tag Cloud

nLab > Latest Changes: apartness relation