Not signed in (Sign In)

Start a new discussion

Not signed in

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

  • Sign in using OpenID

Site Tag Cloud

2-category 2-category-theory abelian-categories adjoint algebra algebraic algebraic-geometry algebraic-topology analysis analytic-geometry arithmetic arithmetic-geometry book bundles calculus categories category category-theory chern-weil-theory cohesion cohesive-homotopy-theory cohesive-homotopy-type-theory cohomology colimits combinatorics complex complex-geometry computable-mathematics computer-science constructive cosmology deformation-theory descent diagrams differential differential-cohomology differential-equations differential-geometry differential-topology digraphs duality elliptic-cohomology enriched fibration finite foundations functional-analysis functor gauge-theory gebra geometric-quantization geometry goodwillie-calculus 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 kan lie lie-theory limits linear linear-algebra locale localization logic manifolds mathematics measure-theory modal-logic model model-category-theory monads monoidal monoidal-category-theory morphism motives motivic-cohomology 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 science set set-theory sheaf simplicial space spin-geometry stable-homotopy-theory string string-theory superalgebra supergeometry svg symplectic-geometry synthetic-differential-geometry terminology theory topology topos topos-theory type type-theory universal variational-calculus

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).
    • CommentRowNumber1.
    • CommentAuthorMike Shulman
    • CommentTimeJan 31st 2017

    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 ¬¬(xx)\neg\neg(x\approx x) and ¬(xy)¬(yx)\neg (x\approx y) \to \neg(y\approx x), so the only thing to worry about is comparison. If ¬(xz)\neg (x\approx z), then contraposing transitivity gives ¬(xyyz)\neg (x\approx y \wedge y\approx z), which by de Morgan gives ¬(xy)¬(yz)\neg (x\approx y) \vee \neg (y\approx z).

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 1st 2017

    Also, why did I never notice this before: an apartness relation on a set XX is the same as a (strongly) closed equivalence relation on the discrete locale of XX, and the apartness topology is its quotient in LocLoc. 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

    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

    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

    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 PQP\to Q, yielding QPQ\to P. The original statement “the negation of an apartness relation is an equivalence relation” has the form x,(P(x)Q(f(x)))\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 x,(Q(f(x))P(x))\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 x,(Q(x)P(f(x)))\forall x, (Q(x) \to P(f(x))) is somewhat less defensible, but it still seems more like a converse than y,(Q(y)x,(P(x)f(x)=y))\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

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

    If PP means that xx is the negation of an apartness relation and QQ means that xx is an equivalence relation, then the statement in question is PQP \to Q, and the converse QPQ \to P is the one that I thought of. But if PP means that xx is an apartness relation and QQ means that the negation of xx is an equivalence relation, then the statement in question is still PQP \to Q, but now the converse QPQ \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 SS is a set and xx is an apartness relation on SS. Then the statement in question is PQP \to Q in a trivial way, where PP is truth and QQ means that the negation of xx is an equivalence relation. The converse of that one is always true!

    • CommentRowNumber7.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 2nd 2017

    I disagree that “we are working in the context of a set SS and a binary relation on SS”. 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 xx 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 SS to be “in the context”.

    • CommentRowNumber8.
    • CommentAuthorTobyBartels
    • CommentTimeFeb 2nd 2017

    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:Set,x:Rel(S,S)S\colon Set, x\colon Rel(S,S) (I also had a third, sillier analysis with the context S:Set,x:ApRel(S)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 x,P(x)Q(x)\forall x, P(x) \to Q(x) is x,Q(x)P(x)\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 PP, if QQ, then RR.’ with the converse ‘Given PP, if RR, then QQ.’. Much of the ambiguity in a statement's converse is going to come from deciding how much to put in the context PP. Often, it's quite a lot!

    • CommentRowNumber9.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 3rd 2017

    Fair enough. Thanks for adding to my correction.

    • CommentRowNumber10.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 3rd 2017

    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}\{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},=OR)(\{true, false\},\otimes = OR) seems necessarily to be an indiscrete groupoid over its set of objects. (Because hom(a,a)=truehom(a,a) = true for all objects aa and then hom(a,b)=hom(a,a)ORhom(a,b)=truehom(a,b) = hom(a,a) OR hom(a,b) = true, too, for all bb.)

    • 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 TT is the subobject classifier, (1)Cat:=Ω(-1)Cat := \Omega?

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

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

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeNov 22nd 2017

    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

    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

    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

    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

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

Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)