I have just embarked on a journey in logic. Currently I am getting acquainted with axiom schemas and formal proofs. In the process of constructing such a (formal) proof, I have used the Law of Excluded Middle (LoEM), and found myself asking two questions:
- Can I proof the statement without LoEM?
- More generally, is it possible to characterize (in some appropriate sense) the set of statements provable without LoEM?
Concretely, I am working with the following axiom schemas: \begin{align} &\text{LoEM}\colon \varphi \lor \lnot\varphi\\ &\text{L}_1\colon \varphi \to (\psi \to \varphi)\\ &\text{L}_2\colon (\psi \to (\varphi_1 \to \varphi_2)) \to ((\psi \to \varphi_1) \to (\psi \to \varphi_2))\\ &\text{L}_3\colon (\varphi \land \psi) \to \varphi\\ &\text{L}_4\colon (\varphi \land \psi) \to \psi\\ &\text{L}_5\colon \varphi \to (\psi \to (\varphi \land \psi))\\ &\text{L}_6\colon \varphi \to (\varphi \lor \psi)\\ &\text{L}_7\colon \psi \to (\varphi \lor \psi)\\ &\text{L}_8\colon (\varphi_1 \to \varphi_3) \to ((\varphi_2 \to \varphi_3) \to ((\varphi_1 \lor \varphi_2) \to \varphi_3))\\ &\text{L}_9\colon \lnot\varphi \to (\varphi \to \psi) \end{align}
I wish to produce a formal proof of the statement $(\alpha \to (\beta \land \lnot\beta)) \to \lnot\alpha$. (A formal proof is a finite sequence of statements, where each statement is derived from its predecessors or from the axiom schemas above via modus ponens.) To produce a formal proof on the basis of LoEM, note that by $\text{L}_1$, \begin{equation} \lnot\alpha \to ((\alpha \to (\beta \land \lnot\beta)) \to \lnot\alpha). \end{equation} It is also not too difficult to show (via ex falso quodlibet) that \begin{equation} \alpha \to ((\alpha \to (\beta \land \lnot\beta)) \to \lnot\alpha). \end{equation} The desired statement then follows from $\text{L}_8$ and, crucially, LoEM (because $\alpha \lor \lnot\alpha$). My first question, now stated precisely, is whether we can prove $(\alpha \to (\beta \land \lnot\beta)) \to \lnot\alpha$ without LoEM? My intuition tells me that this is not possible, because $\text{L}_1$ - $\text{L}_9$ differ fundamentally from LoEM in that the the former represent inference rules, not assumptions - and our proof has to start with at least one such.
My dilemma is that I don't see a way of formalizing this intuition. This naturally leads to the second question, which asks for a (formally verifiable?) criterion to determine if LoEM is required for the proof of a statement.
Many thanks in advance for your interest and help!