Formal Proof for Predicate Logic

Question

Which of the following is NOT a good approach to constructing a formal proof?
(a) Use the main connective or the quantifier of the conclusion as the key to making an overall proof plan.
(b) Use the forward-backward technique if necessary.
(c) If the conclusion is a conjunction, it is a good idea to prove each conjunct one by one and apply the ∧-Intro rule.
(d) If the conclusion is a disjunction and none of the disjuncts are easily proved, it is a good idea to try a proof by cases or a proof by contradiction.
(e) Try to derive as many formulas as possible from the formulas that have been already derived to determine the most appropriate one from which to move forward with the proof.

My Thoughts: I am sure that (b) and (d) are one of the best approaches for a formal proof. However, I could not distinguish between (c) and (e). I would appreciate if anyone could provide some suggestions.

Answer 1

This is an excellent question! Basically, you are asking for ways to cut down the search space for finding a proof within some formal system. To be concrete let us say that you use this Fitch-style natural deduction system. Then the following hold within any subcontext:

1. If you can deduce $A∧B$, then you can deduce $A$ and $B$ separately. (This is your (c).)
2. If you can deduce $¬A$, then you can deduce $A ⊢ ⊥$, namely deduce contradiction under the subcontext "If $A$:".
3. If you can deduce $A⇒B$, then you can deduce $A ⊢ B$, namely deduce $B$ under the subcontext "If $A$:". (This is one case of your (a) that always works.)
4. If you can deduce $¬A ⊢ ⊥$, then you can deduce $¬A ⊢ A$.
5. If you can deduce $∀x{∈}S\ ( \ Q(x) \ )$, then you can deduce $∀x{∈}S ⊢ Q(x)$, namely deduce $Q(x)$ under the subcontext "Given $x∈S$:". (This is another case of your (a) that always works.)
6. If you can deduce $A∨B$, then sometimes you can deduce $A$ or $B$, but not always. But you can always deduce $¬A,¬B ⊢ ⊥$, and then using $¬(A∨B) ⊢ ¬A,¬B$ (easily proven) you can deduce $¬(A∨B) ⊢ ⊥$ and hence $A∨B$. (This is your (d).)
7. If you can deduce $∃x{∈}S\ ( \ Q(x) \ )$, then sometimes you can deduce $Q(c)$ for some $c∈S$, but not always. But you can always deduce $∀x{∈}S\ ( \ ¬Q(x) \ ) ⊢ ⊥$, which is sufficient because $∃x{∈}S\ ( \ Q(x) \ ) ⊢ ∀x{∈}S\ ( \ ¬Q(x) \ )$.

The above is for working backwards; read each of them as saying "if you want to deduce ... then you want to deduce ...". But of course you also need working forward:

1. If you have deduced $A∧B$, then you should deduce $A$ and $B$.
2. If you have deduced $A$ and $¬A$, then you should deduce $⊥$ and get out of the current subcontext by $¬$-intro.
3. If you have deduced $A$ and $A⇒B$, then you should deduce $B$.
4. If you have deduced $∀x{∈}S\ ( \ Q(x) \ )$, then you should deduce $Q(c)$ for every term $c$ in your current subcontext (including those generated later by $∃$-elim in the same subcontext). Start from the ones which look closest what you want to deduce, and try others later if they do not work.
5. If you have deduced $A∨B$, then you should use $∨$-elim.
6. If you have deduced $∃x{∈}S\ ( \ Q(x) \ )$, then you should use $∃$-elim.
7. If you have deduced $t=u$ and $Q(t)$, then you should deduce $Q(u)$.
8. You should always deduce $t=t$ for every term that occurs in some sentence you have deduced or want to deduce.

If you use the above guide, you should be able to easily obtain a proof for any tautology whose proof is not too long. Notice that there is actually only one open-ended step, which is working-forward step 4. If you systematically return to each such $∀$-sentence that you have deduced and repeatedly apply $∀$-elim on it on a different term, making sure not to miss any term (including those generated by $∃$-elim), it turns out that you will never fail to find a proof if there is one!

If you want to prove a theorem $C$ from some given set $T$ of axioms, note that it is equivalent to proving $A∧\cdots∧B ⇒ C$ for some (finitely many) $A,...,B∈T$. If $T$ is finite, you can just make a conjunction of all its axioms and go. If $T$ is infinite, then you have a second source of open-ended choice. Again, first try using the axioms that you think are most likely to be needed. It turns out that if you iteratively add an axiom from $T$, eventually adding all of them, to the sentences that you have deduced (in the global context), and apply the entire above guide to each newly added axiom, you will eventually find a proof if it exists!