Prove the undecidability of a formula

Question

I'm studying natural deduction for classical propositional logic, and I'm struggling with a point I cannot understand: when the book listed all the rules for natural deduction, it simply said that we have a list of objects in this logic: $\top, \bot, \land, \lor, \lnot, \implies $ (the symbols denotes respectively a true statement, a false statement, the "and" connective, the "or", the "not" and the "implies" connectives) and, based on the semantic function (sometimes called the interpretation function), we build up the rules for natural deduction.

Then, at a point, it says that only with the introduction and elimination rules for those symbols and connectives, we cannot prove some statements (for instance $A \lor \lnot A$, or $\lnot \lnot A \!\implies\! A$), so we need to add another rule called the Reductio ad Absurdum (RAA).

The point I cannot grasp is the lack of a proof that such wfs (well formed formulas) are undecidable without RAA or the excluded middle (tertium non datur, EM).

From that point I ask myself: in the intuitionistic logic (therefore a logic where the RAA or the EM does not hold), is there a way to show that a formula is undecidable? I'm not asking if there is a way to conclude that a formula is false (because the converse is true), I'm asking if there is a way to prove that neither $A$ nor $\lnot A$ are provable.

Answer 1

In intuitionistic and classical logic there is a standard way to show that a formula $A$ is unprovable or undecidable (i.e. both $A$ and $\lnot A$ are unprovable), it is based on the completeness theorem.

Completeness theorem says that a formula $A$ is provable (in intuitionistic natural deduction or equivalent system) if and only if $A$ is valid in all the structures (in intutionistic logic these structures are intuitionistic Kripke models).

So:

1. To prove that $A$ is unprovable in intuitionistic logic, it is sufficient to show that $A$ is not valid in some Kripke model (this entails that $A$ is not provable in intutionistic natural deduction by the completeness theorem).
2. To prove that $A$ is undecidable in intuitionistic logic, it is sufficient to apply point 1. to both $A$ and $\lnot A$; i.e. to show that $A$ is not valid in some Kripke model (this entails that $A$ is not provable in intutionistic natural deduction by the completeness theorem), and $\lnot A$ is not valid in some Kripke model (this entails that $\lnot A$ is not provable in intutionistic natural deduction by the completeness theorem).

As correctly remarked by Henning Makholm in his comment, if a formula $B$ is provable in classical logic, then $\lnot B$ is unprovable in intuitionistic logic (since all intuitionistically provable formulas are classically provable). Therefore, a classically provable formula $B$ is intuitionistically undecidable (take for instance $A \lor \lnot A$, or $\lnot\lnot A \to A$) if and only if $B$ is intuitionistically unprovable.

---

Let us show that $A \lor \lnot A$ and $\lnot \lnot A \to A$ are unprovable (and then undecidable, since they are classically provable) in intuitionistic logic using the completeness theorem. Assume $A$ is a propositional variable. Consider the following Kripke model for propositional logic: $\mathcal{K} = (\{0,1\},\leq, \Vdash)$ where $\leq$ is the (total) order relation over $\{0,1\}$ defined by \begin{align} 0 \leq 0 && 0 \leq 1 && 1 \leq 1, \end{align} and $\Vdash$ is a binary relation from $\{0,1\}$ to the set of propositional variables such that $0 \not\Vdash A$ and $1 \Vdash A$. According to the definition of intuitionistic Kripke model for propositional logic, it is easy to check that $0 \not\Vdash A \lor \lnot A$ and $0 \not \Vdash \lnot\lnot A \to A$, which means that neither $A \lor \lnot A$ nor $\lnot\lnot A \to A$ are valid in $\mathcal{K}$. Thus, both $A \lor \lnot A$ and $\lnot \lnot A \to A$ are unprovable (and hence undecidable) in intuitionistic logic.

---

There is also a completeness theorem for classical logic: in the formulation given above, replace intutionistic natural deduction with classical natural deduction (or equivalent system), and Kripke models with truth tables (in the propositional case). Therefore, also in classical logic the completeness theorem (for classical logic) can be used to show that a formula is unprovable or undecidable.

Answer 2

One possible way to see this is to provide a model of "truth values" such that intuitionistic logical proofs translate to statements which are true in that model, but $A \to \lnot \lnot A$ is not true in this model.

One such model is to take truth values to be open subsets of $\mathbb{R}$, with $\top := \mathbb{R}$, $\bot := \emptyset$, $U \wedge V := U \cap V$, $U \vee V := U \cup V$, $\lnot U := \operatorname{int}(U^c)$, $U \rightarrow V := \operatorname{int}(U^c \cup V)$. Then it is possible to prove by structural induction on the proof that whenever $p_1, \ldots, p_n \vdash q$ in natural deduction without reductio ad absurdum ($ND - RAA$), then for any assignment $\mathfrak{U}$ of open subsets of $\mathbb{R}$ to atomic variables, we have $p_1(\mathfrak{U}) \cap \cdots \cap p_n(\mathfrak{U}) \subseteq q(\mathfrak{U})$. On the other hand, if you choose an assignment where an atomic variable $A$ gets mapped to $\mathbb{R} \setminus \{ 0 \}$, then $\lnot A \mapsto \emptyset$, $\lnot \lnot A \mapsto \mathbb{R}$, $(\lnot \lnot A \rightarrow A) \mapsto \mathbb{R} \setminus \{ 0 \}$. Since $\mathbb{R} \not\subseteq \mathbb{R} \setminus \{ 0 \}$, this implies that $\not\vdash (\lnot \lnot A \rightarrow A)$ in $ND - RAA$.

You can look up the theory of Heyting algebras for more on this interpretation of intuitionstic logic. Another example of a Heyting algebra which is not a Boolean algebra is the lattice $\{ 0, \frac{1}{2}, 1 \}$ with an appropriate choice of $\rightarrow$ operation; this example has the advantage that it doesn't depend heavily on set-theoretic or topological constructions as the other one, but I personally find it less intuitive to work with. Other examples that are easy to prove using this formulation: $\not\vdash (A \vee \lnot A)$, and $\not\vdash (\lnot(A \wedge B) \rightarrow \lnot A \vee \lnot B)$.

---

Another completely different approach is through the theory of sequent calculus. Essentially, the idea here is that any proof in $ND - RAA$ can be "simplified" to a "normal form" in which there isn't any redundancy or "cleverness" left in the proof. Here "cleverness" mostly refers to the use of the cut rule: \begin{align*} \Gamma & \vdash P \\ P, \Gamma & \vdash Q \\ \hline \Gamma & \vdash Q \end{align*} where $P$ is a cleverly chosen intermediate step that clarifies the proof. So, in the end, you get a proof with severely restricted possibilities, and from these restrictions you can conclude that certain things can't be proved at all.

Moreover, there are variants of the sequent calculus which lend themselves to a totally automated proof search, which give the result that there is a mechanical decision procedure which decides for each formulas $p_1, \ldots, p_n, q$ whether or not $p_1, \ldots, p_n \vdash q$ in $ND - RAA$.

Another interesting application is that it makes it easy to prove: if $p \vee q$ is a tautology in $ND - RAA$, then either $p$ or $q$ is a tautology in $ND - RAA$. Which is a surprising result at first, given that $A \vee \lnot A$ is a tautology in $ND + RAA$ whereas obviously neither $A$ nor $\lnot A$ is a tautology in $ND + RAA$.