Is it true that for every finite set of axioms $a_0$, …, $a_n$, if a statement $t$ follows from these axioms in the classical first-order predicate logic, then in intuitionistic first-order predicate logic (without axioms $a_0$, …, $a_n$, only basic intuitionistic logic axioms) it can be proved
$$(e\land a_0\land\cdots\land a_n)\Rightarrow t?$$
(where $e$ is the axiom of excluded middle).
Informally, does the intuitionistic logic contain all the finitely axiomatizable mathematics (any statement $t$)?
Is it true that for every finite set of axioms $a_0$, …, $a_n$, if a statement $t$ follows from these axioms in the intuitionistic first-order predicate logic, then in intuitionistic first-order predicate logic (without axioms $a_0$, …, $a_n$, only basic intuitionistic logic axioms) it can be proved
$$(a_0\land\cdots\land a_n)\Rightarrow t?$$
I could solve this myself, but the calculations seems to be long, and somebody may already know the answer.
Best Answer
This is a bit of a subtle question.
First, we must choose a specific logic to work in. Some choices include propositional logic, first order logic, and second order logic. Note that propositional logic is a subset of first order logic, which in turn is a subset of second order logic.
If we work in first-order or propositional logic, we run into an immediate issue. In general, the law of excluded middle cannot be expressed as a single proposition. For suppose we could express excluded middle as some statement $\Phi(P_1, \ldots, P_n)$. This statement cannot possibly be enough to conclude that $P_{n + 1} \lor \neg P_{n + 1}$, since $P_{n + 1}$ doesn’t even appear in $\Phi$.
Instead, the law of excluded middle can be viewed as an axiom scheme. In general, given any proposition $\psi(x_1, \ldots, x_n)$, we have an instance of LEM of the form $LEM(\psi) :\equiv \forall x_1 \ldots \forall x_n (\psi(x_1, \ldots, x_n) \lor \neg \psi(x_1, \ldots, x_n))$. Note that if $P$ is a proposition with no free variables, $LEM(P)$ is just $P \lor \neg P$.
Here is what we can say. If we have prove with classical logic that $a_1 \land \cdots \land a_n \implies t$, then there exist $\psi_1, \psi_2, \ldots, \psi_m$ such that in intuitionist logic, we can prove $LEM(\psi_1) \land \cdots \land LEM(\psi_n) \land a_1 \land \cdots \land a_n \implies t$. The converse is also true, since each $LEM(\psi_i)$ is a theorem of classical logic and all intuitionist proofs are also classical proofs.
Of course, if we are working in 2nd-order logic, we can indeed write $LEM$ as a single axiom $e :\equiv \forall P (LEM(P))$, in which case we can classically prove $a_1 \land \cdots \land a_n \implies t$ if and only if we can prove in intuitionist logic that $e \land a_1 \land \cdots \land a_n \implies t$.
Finally, in the special case of propositional logic over a finite list of propositions $P_1, \ldots, P_n$, LEM is axiomatizable as $e :\equiv LEM(P_1) \land \cdots \land LEM(P_n)$. So your claim also holds here.