Not signed in (Sign In)

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

Discussion 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: double negation

Bottom of Page

1 to 14 of 14

  1.  
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeMay 9th 2017
    • (edited May 9th 2017)

    I have added to the References at double negation pointer to Andrej’s exposition:

    which is really good. I have also added this to double negation transformation, but clearly that entry needs some real references, too.

    • CommentRowNumber2.
    • CommentAuthorUrs
    • CommentTimeJun 1st 2017

    I have added a sentence mentioning forcing to the Idea-section at double negation,

    • CommentRowNumber3.
    • CommentAuthorMike Shulman
    • CommentTimeJun 1st 2017

    That is a nice post, but I have to take issue with

    classical logic is happy with lack of negative evidence.

    I would say that what classical logic is happy with is the impossibility of negative evidence, which is rather stronger than the present lack thereof.

    • CommentRowNumber4.
    • CommentAuthorDmitri Pavlov
    • CommentTimeJul 23rd 2019

    The article claims

    Classically, we have L=L¬¬ if and only if L is the discrete locale on some set S of points. In constructive mathematics, S must also have decidable equality.

    But any complete Boolean algebra is a frame for which the corresponding locale satisfies L=L_¬¬ because ¬¬=id. There are plenty of nonatomic complete Boolean algebras.

    • CommentRowNumber5.
    • CommentAuthorTodd_Trimble
    • CommentTimeJul 23rd 2019

    Yes, it seems that statement had been there since Day 1. I suspect Toby was thinking along roughly the following lines: a topological space XX in which every open is regular open is (classically) discrete. If you allow the luxury of T 1T_1 spaces, and if xx is any non-isolated point, then its set-theoretic complement UU has U∪{x}=XU \cup \{x\} = X as its closure, so ¬¬U=X\neg \neg U = X. So maybe with a sufficiently generous interpretation of “classical”, the statement is defensible – but I agree the statement is confusing as it stands.

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeJul 23rd 2019

    Maybe it should be “If LL is spatial, then L=L ¬¬L=L_{\neg\neg} if and only if …”?

    • CommentRowNumber7.
    • CommentAuthorDmitri Pavlov
    • CommentTimeJul 23rd 2019

    Yes, spatiality is certainly necessary here.

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeJul 24th 2019

    Add spatiality condition to the characterization of L=L ¬¬L=L_{\neg\neg}.

    diff, v58, current

    • CommentRowNumber9.
    • CommentAuthorMorgan Rogers
    • CommentTimeAug 13th 2024

    Corrected reference to Caramello ’09. Added reference to Sketches of an Elephant which removes the need for the ad hoc proof of the subsequent Proposition (moved up) that the double negation subtopos is the unique subtopos which is both dense and Boolean. Rearranged the other propositions and made the Sierpinski topos remark into an example. In my opinion, the page contained insufficient background for the proof to be reader-comprehensible anyway, so pointing to a detailed reference is more useful. Here is the removed proof, in case someone wishes to restore it later: Proof It remains to show that (1) and (2) imply that j=¬¬j=\not\not. First note that the dense monos corresponding to jj are classified by the subobject classifier Ω j\Omega_j of ℰ j\mathcal{E}_j. Since (2) implies that Ω j\Omega_j is an internal Boolean algebra, it follows that the dense subobjects of any object XX form a Boolean algebra.

    This Boolean algebra is a reflective sub-poset of the Heyting algebra of all subobjects of XX, whose reflector is lex, i.e. preserves finite meets. Thus, it will suffice to show that if BB is a Boolean algebra that is a lex-reflective sub-poset of a Heyting algebra HH and if 0∈B0\in B, then B={U|U=¬¬U}B = \{ U | U = \neg\neg U \}.

    To show this, first note that the Boolean negation in BB is the restriction of the Heyting negation in HH. Thus, Booleanness of BB implies U=¬¬UU=\neg\neg U for all U∈BU\in B. Thus, it remains to show that if U=¬¬UU=\neg\neg U then U∈BU\in B. But since 0∈B0\in B and BB is an exponential ideal, by the definition ¬U=(U⇒0)\neg U = (U\Rightarrow 0) it follows that ¬¬U∈B\neg\neg U\in B for any UU. Thus, if U=¬¬UU=\neg\neg U then U∈BU\in B as well.

    diff, v60, current

    • CommentRowNumber10.
    • CommentAuthorMorgan Rogers
    • CommentTimeAug 13th 2024
    Please could someone more familiar with the markdown used on the nLab fix the formatting of my recent edit to make the example less prominent?
    • CommentRowNumber11.
    • CommentAuthorUrs
    • CommentTimeAug 13th 2024

    Have looked at your latest edits, but it’s not easy to see what’s going on. (Am on the last day of a vacation – still just on my phone.)

    Probably the paragraph on the Sierpinski topos wants to be in an Example-environment. For that just enclose it inside

      \begin{example} 

  \end{example}

    And then not to forget to delete the spurious section header

      #### Example

    If you still get stuck, I can try to look into it later this week.

    • CommentRowNumber12.
    • CommentAuthorDavidRoberts
    • CommentTimeAug 14th 2024

    Formatting of examples fix

    diff, v61, current

    • CommentRowNumber13.
    • CommentAuthorUrs
    • CommentTimeAug 14th 2024
    • (edited Aug 14th 2024)

    Am still not sure what’s going on, hence what was really intended:

    The new example (currently still here)

    1. sits in between two propositions which look like they want to be directly subsequent,

    2. refers to “the above” topos which is probably meant to be ℰ ¬¬\mathcal{E}_{\not \not} but remains ambiguous,

    3. refers to a proposition with label “negdense”, which has not been declared.

    I suggest to edit further such as to

    • either clarify why this example is in the Properties-subsection right after the proposition that currently precedes it,

    • or else move it to a separate Examples-subsection (to be created, which may have been the original intention) after the Properties-subsection.

    diff, v62, current

    • CommentRowNumber14.
    • CommentAuthorUrs
    • CommentTimeAug 16th 2024
    • (edited Aug 16th 2024)

    So I have moved the example of the Sierpisnki topos out of the Properties-section into a new Examples-section (now here).

    In doing so I have replaced the words “the above” with “the double-negation subtopos”, which is probably what was meant (but check).

    And the broken reference to a Proposition labeled “negdense” I have replaced with “Prop. xy”, so that it’s visible that the reference needs fixing and hoping that this makes somebody go and fix it.

    diff, v63, current

1 to 14 of 14

  1.