Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
created law of double negation with just the absolute minimum. Added a link from double negation, but nothing more.
Closely related article: excluded middle.
The statement (in intuitionistic mathematics) that
I think something unintended happened there.
I clarified a bit.
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.
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?
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.
@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).
1 to 8 of 8