moving material about inequality spaces to its own page inequality space

Anonymous

]]>adding a section on the foundational status of inequality spaces

Anonymous

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

]]>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.

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

]]>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.

]]>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.

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 isfalse.

Toby adds: Also, it's an enrichedgroupoid, not an enrichedcategory.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\}$onlyif 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\}$?

Fair enough. Thanks for adding to my correction.

]]>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!

]]>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”.

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!

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.

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

]]>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.

]]>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.

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

]]>