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?