3
$\begingroup$

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.

$\endgroup$
10
  • 2
    $\begingroup$ Good realization. I suggest you edit your title, and in places your question, to remove that sidetrack. $\endgroup$
    – J.G.
    Oct 16, 2022 at 22:14
  • 1
    $\begingroup$ As for your question about the law of the excluded middle, it's a rule of inference, not an ordinary premise. $\endgroup$
    – J.G.
    Oct 16, 2022 at 22:16
  • 2
    $\begingroup$ 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." $\endgroup$ Oct 17, 2022 at 6:58
  • 1
    $\begingroup$ 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. $\endgroup$ Oct 17, 2022 at 17:18
  • 1
    $\begingroup$ @DanielSchepler Doesn't $\lnot a \lor a$ express this axiom? $\endgroup$
    – porton
    Oct 18, 2022 at 18:30

1 Answer 1

4
$\begingroup$

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.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .