Talk:Law of Excluded Middle implies Peirce's Law

From ProofWiki
Jump to navigation Jump to search

This is done differently, and is proving a somewhat different sort of statement than the converse proof. This needs to be figured out. --Dfeuer (talk) 15:01, 1 June 2013 (UTC)

In a way, this is a stronger statement, in that it says under what circumstances Peirce's Law will hold in an intuitionistic setting. --Dfeuer (talk) 15:02, 1 June 2013 (UTC)
This result stands alone as a result. The context in which it is used is irrelevant. --prime mover (talk) 15:23, 1 June 2013 (UTC)
If you want to derive a different result, then feel free to do so. If this particular result is in error, then feel free to raise the matter in this page. But I do not believe it would be appropriate to turn this result into a different one. --prime mover (talk) 15:23, 1 June 2013 (UTC)
It's valid, though I've not inspected the argument. I'm not opposed to having it. I'm just not sure it presents the claim in its title as well as the proofs under Peirce's Law. Note that if one has intuitionistically proven $p \lor \neg p$, then one has already either proven $p$ or proven $\neg p$, so Peirce's law doesn't actually do anything useful for you, contrary to my suggestion a few minutes ago. --Dfeuer (talk) 15:32, 1 June 2013 (UTC)
I didn't understand a word of that. --prime mover (talk) 19:51, 1 June 2013 (UTC)
That's because I was thinking while typing, which is always a risky proposition. Assuming LEM means that for any $p$ we can conclude $p \lor \neg p$. Over at Peirce's Law/Formulation 2 there is a proof that if we accept LEM we can prove Peirce's Law/Formulation 2. That is, we can prove that for any $p$ and any $q$, $((p \implies q)\implies p)\implies p$.
On the other hand, what this page shows is for any $p$, if it should so happen that $p \lor \neg p$ holds then it will also be the case that for any $q$ $((p \implies q)\implies p)\implies p$. --Dfeuer (talk) 20:25, 1 June 2013 (UTC)

Yes, that's what this page shows. LEM says that $p \lor \neg p$ for all $p$. This page shows that if $p \lor \neg p$ then for any $q$ etc.

But assuming LEM means $p \lor \neg p$ for all $p$ then this shows that PL holds for all $p, q$. I think you're just trying to make difficulty where none exists just so as to prove you're smarter than me. --prime mover (talk) 20:36, 1 June 2013 (UTC)

No. My concern is that the proofs whose titles of the form "law foo implies law bar" don't match each other, even in the limited context of LEM/Clavius' Law/Peirce's Law. Perhaps we should have each form of each. --Dfeuer (talk) 21:34, 1 June 2013 (UTC)
Also, please note that I am every bit a hard on myself as on others. I don't hesitate to tag up proofs I have written myself as "horrible", "unreadable", "there must be a better way to do this", etc., and to admit on discussion pages when I have erred. --Dfeuer (talk) 21:38, 1 June 2013 (UTC)
Yes, and there we have a difference of opinion. Even if it is on a page you yourself have written, some of your childishly negative and destructive language is needlessly offensive. It inspires others to use similar language to you, through sheer rage and hatred.
IMO you are overly picky and critical, particularly in areas of mathematics which you declare to know not much about. If you genuinely don't know what you're talking about, shut up. If you're being deliberately falsely modest then nobody will take anything you say seriously because that's tantamount to lying. --prime mover (talk) 22:22, 1 June 2013 (UTC)
So your analysis is that I think I am better than I really am, and am pretending to think I am worse than I really think I am? Let me direct you to Occam's Razor. --Dfeuer (talk) 22:54, 1 June 2013 (UTC)

Okay I give up. Deleted as requested. I'll reserve my contributions to non-mathematical non-presentational aspects. --prime mover (talk) 07:29, 2 June 2013 (UTC)

Now you've got me really confused. Please explain what is wrong with this page. If it's correct, leave it alone and go and do something else. If it's incorrect, correct it. If it's terminally unsalvageable, then delete it. --prime mover (talk) 18:19, 2 June 2013 (UTC)
Probably best to leave it for now. In any case, things are a lot better than they were a few days ago. At some point, someone will have a brilliant idea for rearranging this area to make naming consistent, pages findable, etc. --Dfeuer (talk) 18:44, 2 June 2013 (UTC)