1
$\begingroup$

I'm self-studying propositional calculus, and one of the exercises is to prove that replacing the law of excluded middle ($A \lor \lnot A$) with double negation elimination (that is, $\lnot \lnot A \rightarrow A$) does not change the set of provable theorems in the axiomatic set.

The most obvious way to prove this is to prove the claim in the title. I managed to prove it in one direction, that is $A \lor \lnot A$ along with other schemas implies $\lnot \lnot A \rightarrow A$, but I'm quite stuck with the other direction.

So, the ten remaining axiom schemas (after removing the law of excluded middle) are as follows:

  1. $A \rightarrow (B \rightarrow A)$;
  2. $(A \rightarrow (B \rightarrow C)) \rightarrow ((A \rightarrow B) \rightarrow (A \rightarrow C))$;
  3. $(A \land B) \rightarrow A$;
  4. $(A \land B) \rightarrow B$;
  5. $A \rightarrow (B \rightarrow (A \land B))$;
  6. $A \rightarrow (A \lor B)$;
  7. $B \rightarrow (A \lor B)$;
  8. $(A \rightarrow C) \rightarrow ((B \rightarrow C) \rightarrow (A \lor B \rightarrow C))$;
  9. $\lnot A \rightarrow (A \rightarrow B)$;
  10. $(A \rightarrow B) \rightarrow ((A \rightarrow \lnot B) \rightarrow \lnot A)$.

I'm only having modus ponens as the inference rule, and I'm not supposed to know about $\bot$ yet (since some similar questions here mention it).

I also managed to prove $\lnot \lnot \lnot A \rightarrow \lnot A$ and $A \rightarrow \lnot \lnot A$ in the meanwhile, but they don't seem to help here.

$\endgroup$
1
$\begingroup$

Hint

1) $\lnot (A \lor \lnot A)$ --- premise

2) $\vdash A \to (A \lor \lnot A)$ --- axiom Ax.6

3) $A \to \lnot (A \lor \lnot A)$ --- axiom Ax.1 and 1) by mp

4) $\lnot A$ --- 2) and 3) and axiom Ax.10 by mp twice

5) $\vdash \lnot A \to (A \lor \lnot A)$ --- axiom Ax.7

6) $\lnot A \to \lnot (A \lor \lnot A)$ --- axiom Ax.1 and 1) by mp

7) $\lnot \lnot A$ --- 5) and 6) and axiom Ax.10 by mp twice

8) $A$ --- from 7) by Double Negation Elimination : $\vdash \lnot \lnot \varphi \to \varphi$

Now we need Deduction Theorem (we can avoid it with more effort...) :

9) $\vdash \lnot (A \lor \lnot A) \to \lnot A$ --- from 1) and 4)

10) $\vdash \lnot (A \lor \lnot A) \to A$ --- from 1) and 8)

11) $\vdash \lnot \lnot (A \lor \lnot A)$ --- from 10) and 11) and Ax.10 nt mp twice

12) $\vdash A \lor \lnot A$ --- from 11) by DN-elim.

$\endgroup$
  • $\begingroup$ The trick to start with $\lnot (A \lor \lnot A)$ is really neat, thanks! $\endgroup$ – 0xd34df00d May 24 '18 at 13:57

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.