Talk:Proof by contradiction

Please help add sources

This is a decent article, though it is lacks any source.. Luckily, there seem to be several good web sites which can be cited for the majority of this article's content. Here's what a quick google search yielded: [1], [2], [3] Jellocube27 20:25, 11 March 2007 (UTC)

Hello User:Jellocube; I have just added the IEP link, thanks. — Gamall Wednesday Ida (t · c) 16:52, 19 December 2016 (UTC)

Use of tilda (~) for logical NOT

Is the tilda symbol ~ in common use to mean logical NOT? I have never seen its usage before. I am more familiar with ¬, if others agree then I think it should be changed.

The ¬ symbol is used later on in the article, so either ~ or ¬ should be used throughout (not both) for consistency.Bah23 12:51, 5 March 2007 (UTC)

It is extremely common. It was introduced by Giuseppe Peano, and is widely used, for example in Principia Mathematica. I agree with you that the usage in the article should be consistent. -- Dominus 16:48, 5 March 2007 (UTC)

One will also find ` and ! through the literature, as well as the bar.

I have replaced all instances of ~ by $\lnot$, which seems to me to be the standard symbol. cf Negation. I work in CS fields related to logic (though I'm not a logician), and I cannot recall having seen ~ in a paper. (Though it would still be clear enough in context that I may have seen it and not been shocked enough to commit such instances to memory.) — Gamall Wednesday Ida (t · c) 17:05, 19 December 2016 (UTC)

contraposition

I notice that there is a detailed discussion of contraposition in one of the comments above, but none of it seems to have made it into the article Reductio ad absurdum itself. It may be helpful to have a simple-minded comparison of the two as part of the article. Also, if anybody cares to explain the difference between "proof by contradiction" and law of excluded middle", I would be much obliged. Katzmik (talk) 12:43, 26 October 2008 (UTC)

Hello Katzmik; I have just added a paragraph Proof by contradiction#rel. Is it helpful? — Gamall Wednesday Ida (t · c) 19:46, 19 December 2016 (UTC)

Is it really contradiction?

I just made a minor edit to make statement names consistent. In the main part of the article, P was the name of the statement to be proven, and Q was the name of the statement that was contradicted to prove P. The section "Relationship with other proof techniques" in one place used both the name Q, and the compound statement "If P, then Q" as the statement to be proven. I changed the former to P, and the latter to "If A, then B" to show that A and B were components of P, not the P and Q in the main part.

And that distinction is related to what I think is a common misapplication; that is, confusing elements of the proof method, with elements of the statement to be proven. And it points to a problem with many claimed proofs-by-contradiction in general. The section describes how you can prove P="If A, then B" by proving the contrapositive "If ~B, then ~A". But that is not the only form of a proof that uses contraposition.

The section "Principle" lists two forms of proof by contradiction, but many claimed examples I've seen fit neither. They (1) assume that P is false, (2) show that a statement ~Q follows from ~P where (3) Q is a known truth that is independent of P. In a proof by contradiction, both Q and ~Q have to follow from ~Q.

In the Pythagorean example of proof by contradiction, the claimed contradiction is "a^2+b^2<c^2" and "a^2+b^2=c^2". But the latter does not follow from "a+b≤c," it is a truth that is known independently. What the method proves, is "if a+b≤c, then a^2+b^2<c^2". The contrapositive of this is "if a^2+b^2>=c^2, then a+b>c. Since we know that a^2+b^2=c^2, we can conclude that a+b>c.

And not only is Cantor's proof not a proof by contradiction, he never claimed it was one. JeffJor (talk) 22:16, 9 January 2018 (UTC)

Is it really contradiction? PART II

For the section "No least positive rational number", the proof is technically not a contradiction. In fact the statement itself is negative, so assuming its affirmation is just regular constructive practice. — Preceding unsigned comment added by Matteo.Ferrari95 (talk • contribs) 08:28, 6 May 2019 (UTC)

You're right in raising this issue. It's important! This issue - the difference between proof by contradiction and refutation by contradiction - has been dealt with now. John Baez (talk) 10:51, 3 October 2022 (UTC)

Is it really contradiction? PART III (NO! well, ok, yes, but very artificially)

"No least positive rational number" is technically a proof by contradiction as it is stated, but only artificially. Let me elaborate. Denote by R the claim that there is a smallest positive rational number. Then we wish to prove ~R. For that, we assume ~~R (!). By double-negation (which as it happens is the logical axiom used in proofs-by-contradiction) this implies R. Then we derive False as in the article. Thus ~~R is false, so R is false.

In fact, the proof that sqrt(2) is irrational is just as bad, because the property of being irrational is a negative property (not rational).

The hypotenuse example, though not as bad, is also not great because again one can quite easily avoid using proof-by-contradiction. In this case, once could directly use the trichotomy property, and have a+b<c or a+b=c or a+b>c, and derive a+b>c by cases - in the first two cases, one could derive false as explained in the example; and in the third derive a+b>c trivially.

This is really quite amazing. Better examples should be provided, preferably one that cannot be proven constructively, and one that can but where it is considerably more difficult. It might be educational to keep some of the current examples and explain why they are artificial (better than I did just now), but in an appropriate section dedicated to that objective. TheFountainOfLamneth (talk) 14:11, 19 June 2019 (UTC)

This is really quite amazing.

Yes, most of the supposed proofs by contradiction in this article were really not examples of that technique. I think the article is better now. John Baez (talk) 10:54, 3 October 2022 (UTC)

Necessity of law of excluded middle is not shown

In the section 'law of excluded middle' https://en.wikipedia.org/wiki/Proof_by_contradiction#Law_of_the_excluded_middle, the claim is made that a proof by contradiction requires the law of excluded middle. This isn't shown nor referenced, and I couldn't find a statement resulting to this claim on the page Law of excluded middle either ShearedLizard (talk) 17:19, 20 February 2018 (UTC) Although it is shown how the law of excluded middle is used, it necessity is not shown. I suppose this has been proven by someone? ShearedLizard (talk) 17:21, 20 February 2018 (UTC)

Some proofs that people often *call* "proofs by contradiction" - including some examples on this page - are in fact "refutations by contradiction", and those do not require the law of excluded middle. This issue has been dealt with now. John Baez (talk) 10:49, 3 October 2022 (UTC)

Same as other article

isn't this the same as the article reductio ad absurdum? Yelly314 (talk) 18:56, 1 June 2020 (UTC)

I mean, like, it's not actually the same content, but it means the same thing? 18:57, 1 June 2020 (UTC) — Preceding unsigned comment added by Yelly314 (talk • contribs)

Seems like it. There may be a case for making a distinction, but usage overlaps sufficiently that the two topics should be merged. Paradoctor (talk) 19:20, 1 June 2020 (UTC)

Oh me oh my.

• Talk:Proof by contradiction/Archive 1#Merge with Reductio ad absurdum? (2010)
• Talk:Reductio ad absurdum#Conflated with proof by contradiction (2017)

Slightly less sure about the merge now. Even if contradiction is a "mere" subtopic of reductio, merging might make sense, especially in light of the frequent conflation of the two. I'll propose a merger to see what others think, unless you tell me you've change your mind. Paradoctor (talk) 19:31, 1 June 2020 (UTC)

about Q.E.A.

Gauss seems to have written Q.E.A. sometimes.--SilverMatsu (talk) 15:43, 5 January 2022 (UTC)

ref

Disquisitiones arithmeticae at Google Books

Help of an expert

Hello. The page stated that the help of an expert was needed, and rightfully so. It was full of false statements and inaccuracies. I took the liberty of editing it, as I am an expert. Please note however, that I do not know various Wikipedia policies and rules, and that I do not have time to fight random Wikipedia administrators. So I kindly ask that you take these edits in good faith and improve on them (this is how Wikipedia used to be), rather than to revert them based on some random policy. Reverting is really, really bad, because the previous content was downright false. Thanks! AndrejBauer (talk) 19:54, 2 October 2022 (UTC)

Let me also say this: I am quite willing to conform the edits to the gazillion Wikipedia policies, if someone would be so kind to tell me precisely what needs to be done. I can probably come up with external references for most of the material, just let me know which bits you think should be properly cited. 19:56, 2 October 2022 (UTC) AndrejBauer (talk) 19:56, 2 October 2022 (UTC)

I'll just add that yes, Andrej Bauer is an expert on logic in general, and proof by contradiction in particular. His changes are a vast improvement. In particular, the article now explains - as various people in this talk page had requested - that some proofs often called "proofs by contradiction" are in fact "refutations by contradiction". These have a different logical status: even intuitionists accept them, because they don't require using the rule "not(not(P)) implies P". John Baez (talk) 10:48, 3 October 2022 (UTC)

@AndrejBauer: Thanks for your recent improvement of the article! I'd like to ask for two additional improvements:

(1) I feel that a proof method (like Proof by contradiction) is something quite different from a logical axiom (like law of excluded middle). However, your text can be misread to confuse both kinds, viz. in section "Principle" ("Formally, the principle may be written as the implication ¬¬P ⇒ P"), and "Law of the excluded middle" ("Proof by contradiction is equivalent to the law of the excluded middle"). I'd prefer something like "Proof by contradiction is essentially based on the law of the excluded middle", etc.

(2) In section "Proof by contradiction in intuitionistic logic", I suggest to start with a 1-sentence introduction of the intuitionistic notion of (constructive) proof, which requires, in order to prove "∃x ...", an algorithm (i.e. constructive method) to obtain a value for x. This would also prepare the reader to understand the paragraph on Turing machines and the halting problem. However, as I'm not an expert in intuitionism, I feel unable to come up with such a sentence. - Jochen Burghardt (talk) 17:36, 3 October 2022 (UTC)

Thanks for your suggestions!

Regarding (1): the correct distinction here is that of a Hilbert-style system with axioms, or a natural deduction-style with inference rules. So if we want to be precise, then we have to choose one option or mention both. I think I'd prefer the latter and say something like: "In a Hilbert-style system we write it as .... As a reference rule it is writen as ..." (and I would of course link to these concepts). Saying that one law is "essentially based" on another is imprecise and devoid of content. What does "based on" mean? Is derivable from? Is admissible? But I'll see how to improve the text.

Regarding (2): It is not correct to say that intuitionistic logic requires an algorithm to obtain a value of x. It asks for a proof, just like any other kind of logic. Again, I'll think about an acceptable improvement that is more explanatory for the casual reader.

AndrejBauer (talk) 07:25, 4 October 2022 (UTC)

Not actually a proof by contradiction, again

The infinitude of primes is stated as being proved by contradiction when Euclid's proof wasn't by contradiction, and as clearly stated at Euclid's_theorem#Euclid's_proof. One might argue that the article never claims this, just that "the usual proof" is by contradiction. But the lead-up and theorem statement are clearly about Euclid's version:

Euclid's theorem states that there are infinitely many primes. In Euclid's Elements the theorem is stated in Book IX, Proposition 20:[4]

Prime numbers are more than any assigned multitude of prime numbers.

At the very least, a comment about the fact *Euclid's original proof* was not by contradiction should be included, or else this example could go in the non-example section. — Preceding unsigned comment added by 118.210.42.219 (talk) 06:07, 5 October 2022 (UTC)

The argument that is currently there on the page, that a contradiction is arrived at—that 1 should be divisible by a prime, but cannot be—is actually almost in Euclid (see eg http://aleph0.clarku.edu/%7Edjoyce/java/elements/bookIX/propIX20.html). But Euclid's version is a refutation by contradiction, namely that it is used to conclude that the prime divisor of the newly constructed number is **not** equal to one of the original primes, hence a negative statement. This is only a subpart of the argument, based on cases (the new number is prime or not), and is only used to lead to the actual, positive, conclusion: that you have constructed a larger collection of primes than you started with. — Preceding unsigned comment added by 118.210.42.219 (talk) 06:23, 5 October 2022 (UTC)

I find it diffuclt to judge what precisely is in Euclid's proof becuause the theorem statement is not formally written down there. What is the precise statement that we are proving there? Is it "there does not exist a finite list of primes such that every prime is in that list"? In that case, yes, it is a refutation by contradiction. But if the theorem is "for every number there is a prime larger than it" or "for every list of primes there is one that is not in the list" (which I think is a reasonable interpretation of what Euclid stated) then the argument takes the form of proof by contradiction. I think this is all very interesting, but I am not sure an extended discussion belongs on this page. Maybe on Euclid's theorem? In any case, I explicitly stated how I formally interpreted Euclid's statement. Also, I am not sure whether you're suggesting that any changes be made, or just chatting :-) 07:40, 5 October 2022 (UTC) AndrejBauer (talk) 07:40, 5 October 2022 (UTC)

Here is a thought. We could use Euclid's theorem to illustrate how a proof may take the form of a proof by contradiction or refutation by contradiction, depending on how the statement is formalized. What do you think? 07:49, 5 October 2022 (UTC) AndrejBauer (talk) 07:49, 5 October 2022 (UTC)

I have edited the section (moving it to the non-examples) and included the refutation by contradiction proof, cleaned up both so you can see how the structure of the assumption/conclusion is different. At the translation http://aleph0.clarku.edu/%7Edjoyce/java/elements/bookIX/propIX20.html we have

I say that G is not the same with any of the numbers A, B, and C. If possible, let it be so. ..... which is absurd.

which to me clearly flags the start of a refutation by contradiction ("I claim a negative statement. Suppose the statement were in fact true... thus we arrive at an absurdity"). I think having both arguments side by side is useful to really hammer home the distinction, and pointing out the quite fine differences in where and what is assumed in order to arrive at a contradiction. — Preceding unsigned comment added by 118.210.42.219 (talk) 07:56, 5 October 2022 (UTC)

Thanks for writing up the refutation by contradiction. I split the section into two, each in its own section (but adjacent to each other). I think it works well. I dared reduce the verbosity of the refutation by contradiction a little bit, and I used the mathematical notation. By the way, I wouldn't be to hung up with what Euclid actually said. This is not a historical article, I would give priority to clarity of explanation. AndrejBauer (talk) 11:12, 5 October 2022 (UTC)

Thanks, the new version is good, and clearly flags the difference between the two proofs. 118.210.42.219 (talk) 23:14, 5 October 2022 (UTC)

Contradiction vs negation: treading carefully…

Let me begin by acknowledging that I’m no expert, and I have never delved into intuitionistic vs classical. Perhaps for that reason, I have not, to my knowledge, previously encountered the idea that these are not the same thing:

• Assume ¬P; ¬P ⇒ contradiction; hence P.
• Assume Q; Q ⇒ contradiction; hence ¬Q.

Since October, the article has been reorganised to distinguish these as "proof by contradiction" and "refutation by contradiction". This has me confused. And while my understanding (or lack thereof) is not material to the content of the article, it does mean that I had a second look (and a third, and…) at what has been going on. And there are two things that trouble me.

Firstly, it appears to be taking sides in what, to my outsider's perspective, seem like two creditable schools of mathematical–logical thought: intuitionistic logic and classical logic. ("Creditable" in the sense that neither appears to be considered discredited or fringe; I'm not saying we need to give equal weight to phlogiston theory!) This is both an NPOV issue and confusing to the average reader—who probably knows nothing about the debate, and can't grasp why the article is so emphatic about "refutation by contradiction" being something totally different.

Secondly, and I think more importantly, the sources cited for the difference have raised my eyebrows. On the one hand, we have a wiki article. On the other hand, we have a blog post and a paper by one Andrej Bauer, whom I dare to guess is the same person as Wikipedia editor AndrejBauer. (The title of that paper seems again to be taking a side on classical vs intuitionistic.) I hear alarm bells, and they sound like WP:SPS, WP:COI, and probably some other policies with three-letter acronyms.

I'm aware that I'm veering into "experts are scum" territory here by questioning the contributions by Andrej Bauer, whom John Baez asserted is "an expert on logic in general, and proof by contradiction in particular". But I'm going to lean into it and say that if Albert Einstein rocked up to edit the Wikipedia article on mass–energy equivalence, we would be right to politely point him to policy pages and ask him to take a step back! -- Perey (talk) 14:06, 11 January 2023 (UTC)

I can confirm that the distinction "proof vs refutation by contradiction" is an important issue in intuitionistic logic, and is far more than just a hobby of some Andrej Bauer. As far as I know, intuitionistic logic aim at constructive proofs, that is, from an intuitionstic proof of "there exists some x that has property P", one can obtain a "witness", i.e. a "value" that indeed satisfies P (see Constructive_proof#Non-constructive_proofs for existence proofs without witness in classical logic). The price for this property of intuitionstic proofs is (among others) that from "not not Q" one cannot infer "Q". For this reason, intuitionists have to distinguish refutation by contradiction and proof by contradiction, and admit the former, but forbid the latter. In classical logic, the latter follows from the former and the law "if not not Q, then Q". - Maybe the article becomes less confusing if we move the subsection "Refutation by contradiction" into the section "Proof by contradiction in intuitionistic logic"; this way, all intuitionstic stuff would be encapsulated there. - Jochen Burghardt (talk) 15:00, 11 January 2023 (UTC)

I think that's a good idea, collecting info on the intuitionistic view in one place. I think we should also avoid wording like "confused with", which implies those who take the classical logic view are confused. As for the sourcing issue, I certainly don't mean to imply that this is "just a hobby of some Andrej Bauer"! As a non-expert, I'm working under the presumption that everything Bauer has written is entirely factually correct. But correctness is orthogonal to propriety: we have rules that say we need to be careful with self-citing and self-published sources. "Careful" in my understanding here means we need to have more, independent, sources to go along with the existing ones. -- Perey (talk) 03:46, 12 January 2023 (UTC)

Let us distinguish here several issues.

The first is a matter of logic. The discussion about "proof by contradiction" and "refutation by contradiction" is prior to the distinction between classical and intuitionistic logic. It makes no sense to say that "proof by contradiction is different in intuitionistic logic than in classical logic". It's exactly the same. The difference is one of acceptance of it as true. It would be a bad idea to rewrite the page so that somehow we give the impression that "proof by contradiction" is a different animal in classical and intuitionistic logic. That would be like saying that the equation "x * y = y * x" stated for a general group is different from the equation "x * y = y * x" stated for a commutative group. It's the same equation, which happens to be true in one of the cases.

Whether "proof by contradiction" and "refutation by contradiction" are "the same" is also prior to any distinction between classical and intuitionistic logic. They are different simply because they have different syntactic forms throught which they receive different meanings. Obviously so, because in some situations one of the rules can be applied whereas the other cannot (irrespective of which kind of logic we are in since applicability of a rule is just about syntax and not about what is valid). To reiterate, the distinction in the meaning of the two rules is exactly the same in intuitionistic and classical lgoic. However, it is the case that in classical logic both rules are valid – but that does not cause the distinction to disappear! You would not say "2 * 2 = 4 and 2 + 2 = 4 are the same statement" even though they are logically equivalent (both are true), would you?

Perhaps a good plan would be to take "Proof by refutation" out of the page and make it into a separate one. The present page would then speak only of "Proof by contradiction", with two short remarks, namely: that proof by contradiction is not generally accepted in intuitionistic mathematics (this can be properly discussed ona page about intuitionistic mathematics), and that there is a related notion of "refutation by contradiction" which is not the same as "proof by contradiction" (but "refutation by contradiction" would be discussed on a separate page, I am not sure where the difference is to be discussed).

The second matter is one of terminology. You will notice that early versions of the page said "proof of negation" instead of "refutation by contradiction". After some discussions on Twitter, in particular with Noam Zeilberger and Joel Hamkins, the phrase "refutation by contradiction" was suggested as a better one (see here and here). The advantage is that "proof by contradiction" and "refutation by contradiction" nicely reflect the symmetry between the two principles. Of course, we need good external citation. I am indeed no expert on Wikipedia policies, and I have had very negative experiences with Wikipedia, so I am hesitant to contribute. I was advised that it was ok to quote my own work as a source. If I erred, well then, I shouldn't take advice from Twitter. I have tried to find some further sources, in particular for "refutation by contradiction", of which the nLab reference seemed most promising (notice that the nLab reference further points to my writing, but not with regards to "refutation by contradiction"). I shall ask Noam Zeilberger for some further references, as he knows this particular topic better than I do.

The third matter is how to apply various Wikipedia policies. I think that the "neutral point of view" is irrelevant, as I understand it. There may be a host of other policies that apply (as there usually are), but not NPOV. There is no matter of opinion here, nor are there different valid views. There may be differences in opinion on what terminology to use, where to provide more references, or which things to mention and which ones should go elsewhere – but those are editorial issues.

I am happy to continue helping with the page, and I appreciate the comments. Please bare with me, I am not a Wikipedia policy expert. I would appreciate some concrete suggestions on what needs to be done. AndrejBauer (talk) 14:45, 12 January 2023 (UTC)

TL;DR: I have two suggestions. ① Call the different usages of "proof of contradiction" broad and narrow, not confused. ② Find some citations from people who use the broad/confused sense, preferably addressing the distinction between them.

Here's the thing: I didn't come here to comment because when I read the article, I saw policies being violated. It was because I felt confronted by the way the article's written.

The reason I cited policies is that I didn't want to be the idiot who comes in here, saying we should be nicer about the whole "all these people are wrong" thing, and gets told to sit down and shut up because these are the facts. So I went and found policies to try and shore up my position, hoping that they would explain better than I could why something needs to change.

Instead, that makes me the idiot who comes in here waving a bunch of policies and makes you go, "See? I was right! Except it's not an administrator throwing policies in my face, it's just some random nobody." So I'll try and explain my position anyway, without reference to policies.

Roughly speaking, there are three kinds of people here. There are those who are completely unfamiliar with the topic, who don't know an excluded middle from a bare midriff. There are those (like me) who know something about it, and who probably learned that the proof that ${\sqrt {2}}$ is irrational is a great example of proof by contradiction! And then there are the actual experts.

Right now, the article is very dismissive of the second group. It says that they're confused, that they're wrong. Maybe that's so. But as someone in that group, it put me on the defensive. That's relevant for two reasons. One is that I think not alienating the audience is a worthy goal. (Assuming, of course, that I'm not alone in reading the article as confrontational.) Pedagogically, I think that moving people from the first group into the second is a good outcome, and a step on the road to expanding the third group.

The second reason it's relevant is that when I get defensive, I read. So I went digging further. This article, and my associated reading around it, has led me to the following understandings:

• "Classical logic" and "intuitionistic logic" are two schools of thought that disagree with each other. Both have adherents, and the debate is ongoing.
  • The distinction is sort of like Euclidean versus hyperbolic geometry, in that they accept different sets of definitions or axioms. It's quite unlike that, in that the thing being described is the very notion of truth: what constitutes valid reasoning about whether or not something is true?
• Classical logic accepts ¬¬P ⇒ P (the law of the excluded middle). Intuitionistic logic does not (not as a general principle; it needs to be shown to hold in a specific case).
• There are two things referred to as "proof by contradiction":
  1. Properly speaking, it means affirming P by showing that ¬P leads to a contradiction (both logics accept the law of noncontradiction). It then needs ¬¬P ⇒ P to transform this into an affirmative statement of P.
  2. The alternative—denying P by showing that P leads to a contradiction—is "refutation by contradiction" or "proof by negation". (This is acceptable in both logics.) The article asserts that calling this "proof by contradiction" is wrong.
• Given LEM, the one can be turned into the other by a trivial substitution of ¬Q for P. Hence, they are equivalent in classical logic.

Now, you wanted concrete suggestions. My first is to change how we describe the use of "proof by contradiction" to mean "refutation by contradiction". I think that the article should not call the usage "confused". It seems to me that you're fighting the same fight as prescriptivists in language: if a usage is common, at what point does it stop being wrong and become a part of a broader definition? Given that it is common, given the ongoing debate between logic camps, and given the simplicity of their equivalence when LEM is allowed, I contend that we're not able to call it wrong. Instead, I propose describing it in terms of a broad and a narrow definition. I don't support moving refutation to its own article.

My second is that we need citations that give a broader cross-section of views on these fine distinctions. This is where I appealed to policy earlier, and I do think those policies exist for good reasons, but I'm making the case myself now. When there's a disagreement, I want to know (= I want Wikipedia to address) what each side says about the other. Right now it seems like the citations all come from a handful of people who reference each other. When I see that, it doesn't matter whether they're the leading lights of the field or three cranks in a pub; I want to know what someone else thinks about what they're saying. Someone who might be expected to disagree with them. Can we cite someone whose work uses "proof by contradiction" in its broad ("confused") sense? Someone from the classical logic camp, maybe?

Those are my suggestions, anyway. I think we can restructure this article so that it's both accessible and accurate. The absolute last thing I want to do is to drive you away or make you feel that your expertise is not valued. -- Perey (talk) 05:52, 14 January 2023 (UTC)

I much appreciate your explanation of what you feel is wrong with the article (rather than citing policies), as I can actually act on that. I think we can easily incorporate your suggestion about broad/narrow distinction, and it's a good one. There is just one (technical) point which I disagree with. Stating that "assuming LEM, we can turn one of the principles into the other" is at best misleading. That is because "proof by refutation" is already valid in first-order logic (with or without LEM), and so all you are saying is "a principle which everybody already accepts can be re-rederived from LEM and proof by contradiction", and that's not very illuminating. Let me make the broad/narrow change, which I like very much, and then we see where we stand with the rest. AndrejBauer (talk) 09:39, 16 January 2023 (UTC)

Regarding better citations, I called for help, so we should be getting some soon. I am familiar with constructive logic literature, but less with philosophically slanted one, where this sort of thing is probably discussed. AndrejBauer (talk) 09:43, 16 January 2023 (UTC)

Thanks very much for your response. I think the article's looking better already.

"that's not very illuminating"—no, probably not! My thought wasn't to derive p.b.negation from p.b.contradiction. That'd be like deriving 2×2=4 from −2×2=−4. All I meant was that, given LEM (or in this analogy, −(−x)=x), you can freely switch back and forth between the two forms.

Which is why I think the broad usage comes about: people just take this freedom for granted. ("So we've proven the assertion that sqrt(2) is irrational…" "No, you’ve refuted the assertion that it’s rational." "But that's the same thing!") -- Perey (talk) 15:17, 16 January 2023 (UTC)

I have added a bit more text explaining that under $P=\neg \neg P$ (which is what everyone knows in pracrice) the difference betweeen the two principles is obscured. However, I will die on the hill of "they are not the same" :-) 07:08, 24 January 2023 (UTC) AndrejBauer (talk) 07:08, 24 January 2023 (UTC)

As somewhat of a side note to all of the above, let me say that, although I am hardly an expert on this topic, I do have a PhD in mathematics (my dissertation was on categorical topology), and used to believe, at least, that I had a nodding acquaintance with this topic, and that I find myself sharing some of the concerns being expressed by Perey, and would like to thank him for expressing those concerns here ;-) Paul August ☎ 13:50, 16 January 2023 (UTC)