# Equivalence Between Law of Excluded Middle and Self-Implication

We know that $$P \to Q$$ is equivalent to $$\neg P \lor Q$$, as can be verified easily in truth table. Now suppose we have proof for self-implication below [the axiom system is Lukasiewicz's, with L1: $$P \to (Q \to P)$$, L2: $$(P \to (Q \to R) \to ((P \to Q) \to (P \to R))$$]:

(1) $$P \to ((P \to P) \to P)$$ --- (L1)

(2) $$(P \to ((P \to P) \to P)) \to ((P \to (P \to P)) \to (P \to P))$$ --- (L2)

(3) $$(P \to (P \to P)) \to (P \to P)$$ --- (1,2 MP)

(4) $$P \to (P \to P)$$ --- (L1)

(5) $$P \to P$$ --- (3,4 MP)

This proof establishes that $$P \to P$$. It is at this point that I realized two things:

First, since we know that $$P \to P$$ is equivalent to $$\neg P \lor P$$ and since $$\neg P \lor P$$ is the Law of Excluded Middle (or more precisely $$P \lor \neg P$$, but the order of negation don't matter), can it be said that the two are the same? That is, LEM is self-implication. If so, then a logic without LEM (intuitionistic logic) is a logic without self-implication. In other words, in a logic where LEM is not a theorem, self-implication is also not a theorem. Is my reasoning correct?

Second, as a corrolary of the first, can we concludes that the above proof is also (albeit in a disguised form, given semantic reading of equivalence between propositions) proof of LEM?

• I am not an expert on intuitionist logic, but the Wikipedia page seems to indicate that the two axioms you are using to derive $P \to P$ are axioms of intuitionist logic as well. So, $P \to P$ would seem to be a theorem of intuitionist logic. And if $P \lor \neg P$ is not, then the equivalence of $P \to P$ and $P \lor \neg P$ must be something that does not hold for intuitionist logic. – Bram28 May 23 at 19:25

Self-implication is true in intuitionistic logic as well. It really should be: if we assume $$P$$, we really should be able to derive $$P$$.
The point is that $$P \to Q$$ and $$\neg P \lor Q$$ are not equivalent in intuitionistic logic. The direction: $$P \to Q$$ implies $$\neg P \lor Q$$ uses LEM (and cannot be proved without LEM).
• As a bonus, another way of defining $P\to Q$ in classical logic is $\neg(P\land\neg Q)$. In intuitionistic logic, we end up with $\neg P\lor Q\implies P\to Q\implies\neg(P\land\neg Q)$ but neither of the reverse entailments. – Derek Elkins May 23 at 20:24