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

   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 “-translation of ”, where the -translation for any modal operator is like the double negation translation, only putting ’s instead of ’s all over the place. Here, the modal operator is given by .

   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 to some generic proposition makes the case for LEM more clear, I was thinking if there’ a name for the above.

   *An inhabitant of

   is

   which acts like e.g.

   A less general type expression would be

   which in logic reads

   Classically: Using De Morgan’s law we get

   and with double negation we end up at LEM

   Made me think of what those laws used are when we don’t look at 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, is not a theorem of classical logic. The superficially similar , which is equivalent to excluded middle, is known as Peirce’s Law (after Charles Peirce).