Does the principle of explosion follow from the stability axioms?

Question

I am supposed to prove the drinker paradox - that is, the formula $$\lnot\forall_x\lnot (Px\to \forall_xPx)$$ for some relation symbol $P$. I know that it follows from the principle of explosion, which corresponds to the axiom $$\lnot A\to A\to B$$for any formulas $A$ and $B$. However, the problem asks to prove the drinker paradox based only on the rules of natural deduction and the stability axioms, i.e. by assuming $$\forall_\vec x(\lnot\lnot R\vec x\to R\vec x)$$ for each relation symbol $R$. Thus, I am wondering if the principle of explosion follows from the stability axioms. Please note that I am a beginner in logic.

Answer 1

We can use the stability axiom to show explosion $\bot \to \varphi$ for all formulas $\varphi$. The proof works by induction on the depth of the formula $\varphi$:

If the depth is $0$, then we must have $\varphi = \bot$ or $\varphi = Rx$ for some relation $R$ and term-vector $x$. The first case then obviously works out.

To prove $\bot \to Rx$ we assume $H : \bot$ and try to show $R x$. Actually, by the stability axiom for relations it suffices to show $\neg \neg Rx$, so we can further assume $\neg Rx$ and are now trying to produce a proof of $\bot$. But we have this by the assumption $H$.

For the induction step, we know that the depth is $> 0$. We therefore have the following cases:

• $(\varphi = \varphi_1 \land \varphi_2)$ We can assume $H : \bot$ and must show $\varphi_1 \land \varphi_2$. Since $\varphi_k$ has smaller depth than $\varphi$, we know by the induction hypothesis that $\bot \to \varphi_k$. Combined with $H$ this gives $\varphi_k$ for $k = 1,2$ and $\varphi_1 \land \varphi_2$ then easily follows.

• $(\varphi = \varphi_1 \lor \varphi_2)$ Similar to above.

• $(\varphi = \varphi_1 \to \varphi_2)$ Again, similar to the above.

• $(\varphi = \forall x : \phi$ or $\varphi = \exists x : \phi)$ By the induction hypothesis we have $\bot \to \phi$. This suffices to show both $\bot \to (\forall x : \phi)$ and $\bot \to (\exists x : \phi)$. $~~\Box$

The above proof contains a more general and quite useful result: In minimal logic, any closed formula $\varepsilon$ is explosive for all formulas (i.e. for all $\varphi$ we have $\varepsilon \to \varphi$) if and only if it is explosive on the atomic formulas. So we only need to check its explosiveness on atomic formulas.

Anyways, from $\bot \to \varphi$ we can of course conclude $\color{blue}{\neg \alpha \to \alpha \to \varphi}$ for all formulas $\alpha, \varphi$ and we will use this in the below proof of the drinker paradox.

---

Here is a derivation of $\neg \forall_x \neg (P x \to \forall_y P y)$ from the stability axiom.

Assume $H : \forall_x \neg (P x \to \forall_y P y)$ and try to reach a contradiction.

Let's first show that we have $\neg \neg Py$ for any $y$. So assume $\neg Py$, then by $\color{blue}{\text{the above}}$ $\color{blue}{\text{explosion}}$ $\color{blue}{\text{principle}}$ we have $Py \to \forall_z Pz$. But this contradicts $H$, so we can indeed conclude $\neg \neg P y$.

We then get $\forall_y P y$ by the stability axiom and the fact that $y$ was arbitrary in the above.

But with this, we can now take just any $a$$^{(\ast)}$ and obviously have $Pa \to \forall_y Py$. This finally gives us the contradiction to $H$ we desired.

---

$(\ast)$ Note that depending on the details of the used deduction rules and semantics, the drinker paradox should really be written $\forall_a \neg \forall_x \neg (P x \to \forall_y P y)$ to make sure that we have this $a$. Without the $\forall_a$ the paradox can atually be wrong, if we allow empty models.

Answer 2

In what follows, let $P$ denote a relation symbol in your language. Your task is to prove $\neg \forall x. \neg (Px \rightarrow \forall y. Py)$, and you are allowed to assume $\forall x. \neg\neg Rx \rightarrow Rx$ for any relation symbol $R$, but not allowed to use the principle of explosion.

Remark: Note the wording! Any relation symbol, not any formula. If you were allowed to assume stability for any formula, this would be a different, much easier task. Nonetheless, even under these strict restrictions, the answer to the question is positive: It is indeed possible to derive the drunkard sentence (as stated above) under these restrictions, although it took me a while to figure out how.

I'll give a derivation in a common natural deduction system. I'll leave it up to you to translate it into the precise natural deduction system used by Schwichtenberg and Wainer.

We have to prove $\neg \forall x. \neg (Px \rightarrow \forall y. Py)$. We will do this by assuming $\forall x. \neg (Px \rightarrow \forall y. Py)$, and reaching a contradiction. We will additionally freely assume $\forall x. \neg\neg Px \rightarrow Px$, which we're entitled to do, since $P$ is a relation symbol according to the problem statement.

1. Assume $\forall x. \neg\neg Px \rightarrow Px$.
2. Assume $\forall x. \neg (Px \rightarrow \forall y. Py)$.
3. Assume $Pt$.
4. Assume $\neg Py$.
5. Have $\neg (Py \rightarrow \forall z. Pz)$ from assumption 2 by universal elimination.
6. Assume $Py$.
7. Assume $\neg Pz$.
8. Have a contradiction from $Py$ (assumption 6) and $\neg Py$ (assumption 4).
9. Have $\neg\neg Pz$ from 8 by negation introduction, discharging assumption 7.
10. Have $\neg\neg Pz \rightarrow Pz$ from assumption 1 by universal elimination.
11. Have $Pz$ from 9 and 10 by implication elimination.
12. Have $\forall z. Pz$ from 11 by universal introduction.
13. Have $Py \rightarrow \forall z. Pz$ from 12 by implication introduction, discharging assumption 6.
14. Have a contradiction from $Py \rightarrow \forall z. Pz$ (13) and $\neg(Py \rightarrow \forall z. Pz)$ (5).
15. Have $\neg\neg Py$ from 14 by negation introduction, discharging assumption 4.
16. Have $\neg\neg Py \rightarrow Py$ from assumption 1 by universal elimination.
17. Have $Py$ from 15 and 16 using universal elimination.
18. Have $\forall y. Py$ from 17 using universal introduction.
19. Have $Pt \rightarrow \forall y. Py$ from 18 using implication introduction, discharging assumption 3.
20. Have $\neg(Pt\rightarrow \forall y. Py)$ from assumption 2 using universal elimination.
21. Have a contradiction from $Pt \rightarrow \forall y. Py$ (19) and $\neg(Pt\rightarrow \forall y. Py)$ (20).
22. Have $\neg\forall x. \neg (Px \rightarrow \forall y. Py)$ from 21 by negation introduction, discharging assumption 2.

Note that we do not have to discharge assumption 1 (we're allowed to assume it freely as per the text of the problem), and all other assumptions have been discharged by an appropriate rule. Hence, we have a proof of $\neg\forall x. \neg (Px \rightarrow \forall y. Py)$, which is what we need (up to renaming the bound variable $y$).