3
$\begingroup$

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.

Thanks a lot for your time and your help.

$\endgroup$
  • $\begingroup$ $A \to \lnot \lnot A$ is provable also in intuitionistic logic. $\lnot\lnot A \to A$ is not provable in intuitionistic logic because its proofs needs RAA (or an equivalent inference rule). $\endgroup$ – Taroccoesbrocco Jan 26 '18 at 18:21
  • 1
    $\begingroup$ Let us clarify the terminology: you confuse "unprovable" with "undecidable". See here for a clarification. $\endgroup$ – Taroccoesbrocco Jan 26 '18 at 18:24
  • 1
    $\begingroup$ @Taroccoesbrocco: It is clear enough that they are not disprovable, since they are classical tautologies and everything intuitionistic logic proves is classically valid. $\endgroup$ – Henning Makholm Jan 26 '18 at 18:48
  • $\begingroup$ @HenningMakholm - Good point, thank you! I included it in the edit of my answer. $\endgroup$ – Taroccoesbrocco Jan 26 '18 at 21:40
  • $\begingroup$ Mmhh... so as far as I've understood, $F$ is unprovable if $\lnot F$ is provable, whereas $F$ is undecidable if neither $F$ nor $\lnot F$ are provable (and therefore they're both unprovable). So $2+2=5$ is unprovable because I can prove that $\lnot(2+2=5)$, whereas the existence of a cardinal between $\aleph_0$ and $\aleph_1$ in ZFC is undecidable. And, as far as I have understood, in intuitionistic logic, the proposition $A \lor \lnot A$ (or $\lnot \lnot A \implies A$) is undecidable, right? Thanks for the clarifications $\endgroup$ – LuxGiammi Jan 27 '18 at 15:59
2
$\begingroup$

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.

$\endgroup$
3
$\begingroup$

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$.

$\endgroup$
  • $\begingroup$ ... with the caveat that the "totally automated proof search" works only for propositional (classical or intuitionistic) logic. If we extend to predicate logic we need to be clever again. $\endgroup$ – Henning Makholm Jan 26 '18 at 18:51
  • $\begingroup$ Actually, I thought I'd seen a version of sequent calculus which worked for predicate calculus, as long as it was without an equality symbol and substitution rule (aka equality-elimination). But I could be wrong as my knowledge in this area is mostly from self-study... $\endgroup$ – Daniel Schepler Jan 26 '18 at 18:56
  • $\begingroup$ Another caveat is that the automated proof search could take exponential time in the worst case. (Which is unsurprising since it would be possible to use it to solve the NP-complete SAT problem, so it's at least as hard as an NP-complete problem.) In most practical cases, though, the proof search is reasonably fast. $\endgroup$ – Daniel Schepler Jan 26 '18 at 19:08
  • 1
    $\begingroup$ Well, both intuitionistic and classical validity of first-order formulas, even without equality, are algorithmically undecidable as soon as there is a binary predicate symbol in the language, so I think you must be misremembering. $\endgroup$ – Henning Makholm Jan 26 '18 at 21:59
  • $\begingroup$ @HenningMakholm Ah, OK, I guess I see how allowing a general binary predicate symbol would cause the same sort of problems. Luckily there's still the slightly generalized approach to #1 of trying to come up with a topos model which doesn't satisfy the statement... $\endgroup$ – Daniel Schepler Jan 26 '18 at 22:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.