Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorUrs
   • CommentTimeMar 17th 2017
   • PermaLink
   Author: Urs
   Format: MarkdownItexcreated _[[law of double negation]]_ with just the absolute minimum. Added a link from _[[double negation]]_, but nothing more.

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

2. • CommentRowNumber2.
   • CommentAuthorTodd_Trimble
   • CommentTimeMar 17th 2017
   • PermaLink
   Author: Todd_Trimble
   Format: MarkdownItexClosely related article: [[excluded middle]].

   Closely related article: excluded middle.

3. • CommentRowNumber3.
   • CommentAuthorNikolajK
   • CommentTimeMar 17th 2017
   • PermaLink
   Author: NikolajK
   Format: MarkdownItex>The statement (in intuitionistic mathematics) that I think something unintended happened there.

   The statement (in intuitionistic mathematics) that

   I think something unintended happened there.

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeMar 17th 2017
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI clarified a bit.

   I clarified a bit.

5. • CommentRowNumber5.
   • CommentAuthorNikolajK
   • CommentTimeMar 17th 2017
   • (edited Mar 17th 2017)
   • PermaLink
   Author: NikolajK
   Format: MarkdownItexDoes $((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.

   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.

6. • CommentRowNumber6.
   • CommentAuthorIngoBlechschmidt
   • CommentTimeMar 21st 2017
   • PermaLink
   Author: IngoBlechschmidt
   Format: MarkdownItexNikolaj, 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?

   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?

7. • CommentRowNumber7.
   • CommentAuthorNikolajK
   • CommentTimeMar 22nd 2017
   • PermaLink
   Author: NikolajK
   Format: MarkdownItexSomewhere 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.

   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.

8. • CommentRowNumber8.
   • CommentAuthorTobyBartels
   • CommentTimeMar 30th 2017
   • PermaLink
   Author: TobyBartels
   Format: MarkdownItex@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).

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