Talk:Principle of explosion

Circular reasoning in "formal proof"

The formal proof on the page is suffering from circular reasoning. It peruses the disjunctive syllogism; however, the disjunctive syllogism can only be proved when EFQ is already assumed to be true. Therefore, the "proof" prooves that "EFQ is true given that EFQ is true". 5.18.95.241 (talk) 00:33, 30 September 2022 (UTC)

Move discussion in progress

There is a move discussion in progress on Talk:Ex Falso (tag editor) which affects this page. Please participate on that page and not in this talk page section. Thank you. —RMCD bot 17:47, 7 April 2023 (UTC)

Unfinished Proof

The supposed proof of POE leaves its first assumptions undischarged. How many poor souls has it sent down the proverbial rabbit hole of no return? The final result after 2 lines would be P => [~P => Q] from which, regardless of the truth value of P, you cannot infer that Q is true. Danchristensen (talk) 21:15, 5 August 2023 (UTC)

It is a little misleading as written, but those are not assumptions that need to be discharged. They are premises in an argument, or sentences in a theory. I've changed 'Assumption' to 'Premise' to make this clearer. Dezaxa (talk) 11:07, 7 August 2023 (UTC)

Here is a finished proof that P => [~P => Q]

1. P (Assume)

2. ~P (Assume)

3. ~Q (Assume)

4. P & ~P (Join 1, 2)

5. ~~Q (Discharge 3)

6. Q (Elim ~~ 5)

7. ~P => Q (Discharge 2)

8. P => [~P => Q] (Discharge 1)

Danchristensen (talk) 16:12, 3 September 2024 (UTC)

As the article correctly states, the principle of explosion holds that from a contradiction any proposition follows. Symbolically:

$P,\lnot P\vdash Q$

P and ¬P are not assumptions that need to be discharged. When we write $P,\lnot P\vdash Q$ it means that Q is derivable from P together with ¬P. So, the proof given is complete as it stands. While it is true that $P\rightarrow (\neg P\rightarrow Q)$ is a theorem, and also that $(P\wedge \neg P)\rightarrow Q$ is a theorem, neither of these is needed to prove explosion. There are many ways to prove explosion and the one given is simple and straightforward. This is why I reverted the changes made on 3 September 2024. Dezaxa (talk) 19:02, 3 September 2024 (UTC)

Yeah, well, you know, that's just, like, uh, your opinion, man. WP:PROVEIT. Paradoctor (talk) 19:06, 3 September 2024 (UTC)

No it's not just my opinion. It can be found in logic textbooks. I shall add some further citations. Dezaxa (talk) 20:00, 3 September 2024 (UTC)

Your symbolic representation of POE "P, ~P |- Q," is equivalent to both the theorems "(P & ~P) => Q" and "P => (~P => Q)." Essentially, both theorems tell us that an implication is true whenever its antecedent is false. We cannot infer from either theorem, that the consequent is true or that it is false. Danchristensen (talk) 23:44, 3 September 2024 (UTC)

Fair is fair: WP:PROVEIT. Paradoctor (talk) 00:33, 4 September 2024 (UTC)

It is correct to say that from the theorems $P\rightarrow (\neg P\rightarrow Q)$ and $(P\wedge \neg P)\rightarrow Q$ you cannot infer the truth of Q. But that is not the point. The POE states that starting from a contradiction anything can be derived. In fact, if your object language contains the falsum symbol $\bot$ then you could state the POE even more simply as $\bot \vdash Q$. Although it is possible to write a version of the principle in sentential form as $P\rightarrow (\neg P\rightarrow Q)$, doing so is unnecessarily complicated. POE can be stated and proved without introducing the material conditional. And on the basis that simple proofs are superior to complicated ones, the simple four line proof given by C I Lewis should be preferred. Dezaxa (talk) 15:27, 4 September 2024 (UTC)

(clears throat) WP:TALK: Talk pages are for discussing the article, not for general conversation about the article's subject. If you're proposing changes to the article, please clarify which ones (and source them). Paradoctor (talk) 22:42, 4 September 2024 (UTC)

If you actually want to apply POE in a formal proof, the general rule is that P => (~P => Q) for any propositions P and Q. Danchristensen (talk) 15:21, 5 October 2024 (UTC)

Is there a change to the article you're proposing? Paradoctor (talk) 15:42, 5 October 2024 (UTC)

EFQ vs ECQ

nLab does not collapse ex falso ($\bot \vdash B$, EFQ) to ex contradictione ($A,\neg A\vdash B$, ECQ).

This separation helps draw out, for instance, properties of paraconsistent logics defined more generally as any logic without ECQ, rather than classical logic without ECQ. For example, one can construct a paraconsistent logic without LNC, such that EFQ can be adopted without violating the omission of ECQ. Tule-hog (talk) 19:39, 9 January 2025 (UTC)