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

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

which in logic reads

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

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

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

]]>I clarified a bit.

]]>The statement (in intuitionistic mathematics) that

I think something unintended happened there.

]]>Closely related article: excluded middle.

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