# 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

## Discussion Tag Cloud

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

• 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)

Does

$((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 $\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 $\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

$\left((A\to B)\times((A\to B)\to C)\right)\to C$

is

$eat=\lambda x.(\pi_2x)(\pi_1 x)$

which acts like e.g.

$eat\,(\,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

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

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

Classically: Using De Morgan’s law we get

$\neg\neg A \vee \neg \neg \neg A$

and with double negation we end up at LEM

$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, $((P\to Q)\to Q)\to P$ is not a theorem of classical logic. The superficially similar $((P\to Q)\to P)\to P$, which is equivalent to excluded middle, is known as Peirce’s Law (after Charles Peirce).