# Natural Deduction Proof search algorithm for Classical Propositional logic?

I know of two algorithms for determining classical propositional validity:

1. Convert the problem into a SAT problem, run a SAT solver. These algorithms are efficient, but it seems difficult/infeasible to construct a formal proof of the tautology using this approach.

2. Brute force all truth table values. Constructing a formal proof may be feasible in some systems, but this will always take exponential time.

Is there an alternative approach for determining and proving classical propositional tautologies from basic boolean algebra laws? Dyckhoff 92 describes such an approach for intuitionistic sequent calculus (and natural deduction). Is there an equivalent result for classical propositional calculus? If not, what makes the classical case "harder"?

• Commented Dec 22, 2021 at 14:43
• So exactly what rules should this algorithm be employing? In the title you refer to natural deduction, but at the end of your post you refer to boolean algebra rules. There are systematic algorithms for both, and both will be exponential, but I am just wondering which kind you are looking for Commented Dec 22, 2021 at 16:16
• Context on any/all of those systematic algorithms would be great! My intuition is that those Natural Deduction algorithms would be somewhat transferrable to boolean algebra, and possibly vice-versa (after all, the inference rules used in Natural Deduction can each be represented by tautologies, on which boolean algebra can be performed). Commented Dec 22, 2021 at 16:55
• Any updates @Bram28? Thanks! Commented Dec 24, 2021 at 3:38
• You could combine Dyckhoff's algorithm that you cite with Glivenko's theorem -- in order to determine whether $\Gamma \vdash P$ classically, use Dyckhoff's algorithm to determine whether $\Gamma \vdash \lnot\lnot P$ intuitionistically. (This for example is what Coq does if you run the tauto algorithm with the classic axiom imported, and in practice it usually works fairly well.) Commented Dec 28, 2021 at 19:29

The method of semantic tableaux, or truth trees (which sounds friendlier), provides a proof system for classical propositional logic which easily suggests an algorithm for checking whether a formula of propositional logic is valid.

Let's do an example straight away.

Suppose you have a propositional formula, such as $$p \rightarrow (q \rightarrow (p \wedge q))$$ and you want to know whether it is valid in classical propositional logic. Begin by writing down the negation of the formula:

\begin{align} 1 \space & \neg(p \rightarrow (q \rightarrow (p \wedge q))) \end{align}

There is a rule $$(\alpha)$$ which covers the case of a formula with the form $$\neg(A \rightarrow B)$$. It tells us to write down $$A$$ and $$\neg B$$ - both on the same branch as the original formula. Node $$1$$ is now spent or used.

\begin{align} 1 \space & \neg(p \rightarrow (q \rightarrow (p \wedge q))) \\ 2 \space & p & \alpha, 1 \\ 3 \space & \neg(q \rightarrow (p \wedge q)) & \alpha, 1 \\ \end{align}

Node $$2$$ is atomic, so we can't do anything with that. Node $$3$$ is also susceptible to $$(\alpha)$$:

\begin{align} 1 \space & \neg(p \rightarrow (q \rightarrow (p \wedge q))) \\ 2 \space & p & \alpha, 1 \\ 3 \space & \neg(q \rightarrow (p \wedge q)) & \alpha, 1 \\ 4 \space & q & \alpha, 3 \\ 5 \space & \neg(p \wedge q) & \alpha, 3 \\ \end{align}

A different rule, $$(\beta)$$, applies to $$5$$ because it is the negation of a conjunction. You will no doubt recall that, if a conjunction is false, at least one of its conjuncts is false. However, considering only this piece of information, we don't know which conjunct is false. In a truth tree, this causes the tree to branch:

\begin{align} 1 \space & \neg(p \rightarrow (q \rightarrow (p \wedge q))) \\ 2 \space & p & & \alpha, 1 \\ 3 \space & \neg(q \rightarrow (p \wedge q)) & & \alpha, 1 \\ 4 \space & q & & \alpha, 3 \\ 5 \space & \neg(p \wedge q) & & \alpha, 3 \\ 6 \space \neg p \space & & 7 \space \neg q \space & \beta, 5 \\ \end{align}

Now there are two branches. The left branch contains $$\neg p$$, but also includes the earlier node $$2$$, which is $$p$$. Similarly, the right branch bears the contradictory fruit $$q$$ and $$\neg q$$. Here we apply another rule, which states that if a branch contains a propositional atom and its negation, the branch must be closed, i.e. we have nothing further to do with it. Since both branches are closed, we are done drawing the truth tree. (In a different situation, we might also have finished if there were no more 'unspent' formulae which we could apply rules to.)

Considering truth trees as proof systems, we can stipulate that a propositional formula $$A$$ is provable if, in drawing the truth tree for $$\neg A$$, every branch closes. It turns out that if $$A$$ is provable in this sense, then $$A$$ is valid. This is the soundness property of truth trees as a proof system, and it certifies that drawing truth trees algorithmically decides whether a propositional formula is valid.

I learnt about truth trees from the book Logic with Trees by Colin Howson; but I think Raymond Smullyan is to be credited for the way that book presents semantic tableaux.

• It's worth noting that, in order to make the truth tree system classical, there is also a rule of double negation: if you have $\neg \neg A$ on a branch, write $A$ on that branch. Commented Dec 25, 2021 at 13:12