# Does the intuitionistic logic contain classical (in a sense)?

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.

• Good realization. I suggest you edit your title, and in places your question, to remove that sidetrack.
– J.G.
Oct 16, 2022 at 22:14
• As for your question about the law of the excluded middle, it's a rule of inference, not an ordinary premise.
– J.G.
Oct 16, 2022 at 22:16
• In a sense YES; see Intuitionistic Logic: Translating classical into intuitionistic logic: "A fundamental fact about intuitionistic logic is that it has the same consistency strength as classical logic. For propositional logic this was first proved by Glivenko [1929]: an arbitrary propositional formula $A$ is classically provable, if and only if $¬¬A$ is intuitionistically provable." Oct 17, 2022 at 6:58
• The "axiom of excluded middle" can't really be expressed as a formula in first-order logic. However, my guess would be that for any given case of $a_0, \ldots, a_n, t$, making $e$ into the conjunction of a finite number of instances of excluded middle should be sufficient. Oct 17, 2022 at 17:18
• @DanielSchepler Doesn't $\lnot a \lor a$ express this axiom? Oct 18, 2022 at 18:30

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.