Strategies for constructing proofs in propositional logic

General strategy

Break complex propositions into simpler sentences by using the elimination rules
Recombine simple propositions into complex propositions using the introduction rules.

Goal analysis

The approach above describes the general form of a proof but of course it will not always work and there will be cases where the route to the desired derivation is more circuitous. In these instances it is to best to combine this general top level strategy with goal analysis.

Goal analysis is a recursive strategy which proceeds by using a ‘goal’ proposition to guide the construction of intermediary derivations.

Assume that we want to show that an argument is valid. Then our ultimate goal is to derive the conclusion from the premises we are given. We first ask ourselves: which propositions if we could derive them, would allow us to easily derive the conclusion? (For example, these propositions might be two simple propositions that when combined with Conjunction Introduction give us the conclusion.) Deriving these propositions then becomes the new intermediate goal.

If arriving at these propositions is not trivial, we then ask ourselves the question again: which propositions would permit us to derive the intermediary propositions we need? You keep working back in this manner until you reach a base level. Then it is just a matter or working upwards from each set of derived intermediary propositions until you reach the ultimate goal.

Demonstration

Let’s say we want to prove $(L \lor A) \land D$ from the propositions $\lnot N$ and $((\lnot N \rightarrow L) \land (D \leftrightarrow \lnot N))$.

First, we consider what is the easiest possible way of achieving the proposition $(L \lor A) \land D$. Clearly it is to separately derive each disjunct ($L \lor A$ and $D$) and then combine them with Conjunction Introduction. This provides us with our first goal: to derive each of the separate conjuncts.

Let’s start with $D$: where does it occur in the assumptions? It occurs in the compound $(\lnot N \rightarrow L) \land (D \leftrightarrow \lnot N)$, but only in the first conjunct. We can get this simply but applying Conjunction Elimination.

So far we have:

Now we just need to get $D$ from the proposition at line 3. This is easy since we already have access to the consequent of the biconditional at line 1. Therefore we can apply Biconditional Elimination) at line 3 to get $D$. We are now halfway there:

Next we need to turn our attention to deriving $L \lor A$. How can we obtain $L$ ? Well it is contained within the first conjunct of the assumption on line 2. Again, we can get this through the application of Conjunction Elimination. Now, how do we get $L$ from $(\lnot N \rightarrow L)$? Well, we already have the antecedent $\lnot N$ as an assumption on the first line, so we can use Conditional Elimination to derive $L$. These two steps give us:

Now we need to get from $L$ to $L \lor A$. This is really straightforward because by using Disjunction Introduction) we can get from any sentence to a disjunction. Finally, having assembled all the constituent parts of the conjunction that is the conclusion, we can combine them with Conjunction Introduction as we had planned at the outset.

A further example

We will seek to prove the following:

$$ \{ \lnot L \leftrightarrow [X \land (\lnot S \lor B) ], (E \land C) \rightarrow \lnot L, (E \land R) \land C \} \vdash X \land (\lnot S \lor B) $$

The requirements here could easily mislead us. We see that the target proposition is a conjunction so we might think that the best strategy is to seek to derive each conjunct and then combine them via Conjunction Introduction).

Actually, if we look more closely, there is a better approach. The target proposition is contained in the first premise as the consequent to the biconditional ($\lnot L \leftrightarrow [X \land (\lnot S \lor B)]$). A better approach is therefore to seek to derive the antecedent ($\lnot L$) and then use Biconditional Elimination to extract the target sentence which is the consequent.

Proving theorems

When we are proving theorems we do not have a set of assumptions to work from when constructing the proof. We must derive the target sentence from the ‘empty set’ which is the target sentence itself. It is therefore like a process of reverse engineering.

Demonstration

Prove: $\vdash (U \land Y) \rightarrow [L \rightarrow (U \land L)]$

Our strategy here is to identify the main connective in the proposition we want to derive (the material conditional). We then assume the antecedent and attempt to derive the consequent from it.

A complex theorem proof

Prove $\vdash (\lnot A \lor \lnot B) \leftrightarrow \lnot(A \land B)$

Walkthrough

Lines 1-12

Our auxiliary goal is to prove $\lnot (A \lor B) \rightarrow \lnot (A \land B)$.
Our starting assumption is to a disjunction. Thus we can apply Disjunction Elimination to show that our goal sentence $\lnot(A \land B)$ follows from each of the disjuncts ($\lnot A$ and $\lnot B$) in dedicated sub-proofs. If we can do this, we have the right to derive $\lnot (A \land B)$.
In both cases($\lnot A \vdash \lnot (A \land B)$) and ($\lnot B \vdash \lnot (A \land B)$ we require another sub-proof to reach the target as there is no easy path available. So we derive a negation from $A \land B$ so that we can negate it as $\lnot (A \land B)$.
Having done this, we can discharge the Disjunction Elimination sub-proofs and derive $\lnot (A \land B)$ from $\lnot A \lor \lnot B$

Lines 13-26

Our auxiliary goal is to prove $\lnot (A \land B) \rightarrow \lnot A \lor \lnot B$. This will require a different approach to the above because we are not working from a disjunction anymore, we have a negated conjunction.
We will do this by assuming the negation of what we want to prove ($\lnot (\lnot A \lor \lnot B)$) and then apply Negation Elimination to get $\lnot A \lor \lnot B$.
This requires us to derive a contradiction. We get this on lines 23 and 24. This requires as previous steps that we have two sub-proofs that use Negation Elimination to release $A$ and $B$