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).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeMar 17th 2017

    created law of double negation with just the absolute minimum. Added a link from double negation, but nothing more.

    • CommentRowNumber2.
    • CommentAuthorTodd_Trimble
    • CommentTimeMar 17th 2017

    Closely related article: excluded middle.

    • CommentRowNumber3.
    • CommentAuthorNikolajK
    • CommentTimeMar 17th 2017

    The statement (in intuitionistic mathematics) that

    I think something unintended happened there.

    • CommentRowNumber4.
    • CommentAuthorMike Shulman
    • CommentTimeMar 17th 2017

    I clarified a bit.

    • CommentRowNumber5.
    • CommentAuthorNikolajK
    • CommentTimeMar 17th 2017
    • (edited Mar 17th 2017)


    ((PQ)Q)P((P\to Q)\to Q)\to P

    have a name? In the case of the law of excluded middle, statements still make sense if you replace absurdum with a general proposition. And proving those is often simpler.

  1. Nikolaj, personally I don’t know a name for this, other than saying that it’s the “\Box-translation of ¬¬PP\neg\neg P \Rightarrow P”, where the \Box-translation for any modal operator \Box is like the double negation translation, only putting \Box’s instead of ¬¬\neg\neg’s all over the place. Here, the modal operator \Box is given by φ(φQ)\Box\varphi \equiv (\varphi \vee Q).

    Do you have a specific situation in mind where you’d want to have a name for this formula?

    • CommentRowNumber7.
    • CommentAuthorNikolajK
    • CommentTimeMar 22nd 2017

    Somewhere else I wrote down an elaboration about constructively provable classical equivalents to LEM*. When I saw Urs made a page for the double negation I thought about writing down those for the nLab in a parallel fashion. Since the abstraction from \bot to some generic proposition makes the case for LEM more clear, I was thinking if there’ a name for the above.

    *An inhabitant of

    ((AB)×((AB)C))C\left((A\to B)\times((A\to B)\to C)\right)\to C


    eat=λx.(π 2x)(π 1x)eat=\lambda x.(\pi_2x)(\pi_1 x)

    which acts like e.g.

    eat(xx 2,f 1 3f(x)dx)= 1 3x 2dx=263eat\,(\,x\mapsto x^2,\, f\mapsto \int_1^3f(x)\,dx\,) = \int_1^3 x^2\,dx = \frac{26}{3}

    A less general type expression would be

    ((A)×((A)))\left((A\to \bot)\times((A\to \bot)\to \bot)\right)\to \bot

    which in logic reads

    ¬(¬A¬¬A)\neg\left(\neg A\wedge \neg \neg A\right)

    Classically: Using De Morgan’s law we get

    ¬¬A¬¬¬A\neg\neg A \vee \neg \neg \neg A

    and with double negation we end up at LEM

    A¬A A\vee \neg A

    Made me think of what those laws used are when we don’t look at \bot but general propositions.

    • CommentRowNumber8.
    • CommentAuthorTobyBartels
    • CommentTimeMar 30th 2017

    @NikolajK #5:

    Well, ((PQ)Q)P((P\to Q)\to Q)\to P is not a theorem of classical logic. The superficially similar ((PQ)P)P((P\to Q)\to P)\to P, which is equivalent to excluded middle, is known as Peirce’s Law (after Charles Peirce).