Double Negation and Law of Excluded Middle in Natural Deduction: Cyclic Dependency?

Question

All proofs for LEM and double negation I looked at had the one needing the other to do the proof. Is there a way to prove one without the other or is it necessary to make one of them an axiomatic inference rule?

Answer 1

You could take yet another rule, e.g. Peirce's law, axiomatically and prove both from that, but this just moves things around. You can separate classical logic into intuitionistic/constructive logic plus the addition of any of a number of rules that capture classical reasoning, e.g. Law of Excluded Middle (LEM), Double Negation Elimination (DNE), Peirce's Law, $(\neg Q\to\neg P)\to(P\to Q)$, and others. If any of these latter rules/axioms are added to intuitionistic logic, then any of the others can be derived, but none of them are derivable from intuitionistic logic.

Of course, you can axiomatize classical logic in such a way that there isn't quite so clean a separation and some other axiom provides the power of LEM while also supporting other logical concepts. Indeed, typical axiomatizations of classical logic, e.g. Hilbert's, heavily rely on DNE, say, and if removed can no longer describe things like disjunction, say. One of the nice things about natural deduction and the sequent calculus (and Gentzen's work in general) is that it goes a good way toward describing the logical connectives in a modular fashion so they aren't all tangled together like this.

So, yes, you more or less need to take one or the other or some other equivalent principle as axiomatic, particularly with respect to even a quite rich intuitionistic logic.