Skip to main content

Subsection 5.1.3 Review – Natural Deduction Proofs

Boolean logic gives us two quite different-looking ways to build proofs:

  • Truth tables

  • Natural deduction

Of course, we proved (using truth tables) that our natural deduction rules are sound. So, at a logical level, these two techniques are equivalent. Sometimes one is more convenient than the other.

Unfortunately, we cannot, in general, use truth tables to construct proofs in predicate logic. Why not? Because a truth table is a finite list of possible interpretations (combinations of truth values of the primitive objects). But predicate logic lets us quantify over domains that may be genuinely infinite or ones whose members we don’t know enough about to enumerate.

Here’s an example where we have an infinite domain:

We can say that every positive integer has a successor:

\(\forall\) x (PositiveInteger(x) \(\rightarrow\) HasSucessor(x))

Here are a couple of examples where the domain is formally finite but we can’t, as a practical matter, enumerate it:

We can say that every citizen must pay taxes:

\(\forall\) x (Citizen(x) \(\rightarrow\) MustPayTaxes(x))

Or we can say that all people have birthdays:

\(\forall\) x (Person(x) \(\rightarrow\) HasBirthday(x))

Clearly, if there are infinitely many things for which we would have to consider truth values, we can’t enter them into a table of finite size. And, if there are finitely many things but we’re unable to make a list of all them, we can’t put them into a table either. So truth tables won’t work.

But Boolean natural deduction does generalize to predicate logic. Proofs will have the same structure that they did in Boolean logic. Recall that a proof starts with a set of premises (or axioms). Then we apply rules of inference to create new statements. Any statement derived in this way is called a theorem.

To refresh our memory, here’s a simple Boolean logic natural deduction proof:

  1. p Premise

  2. p \(\rightarrow \) q Premise

  3. (q \(\wedge \) s) \(\rightarrow \) r Premise

  4. q Modus Ponens [1], [2]

  5. q \(\vee \) s Addition [4]

  6. r Modus Ponens [3], [5]

To generalize natural deduction to predicate logic, we will need to add some new inference rules. As before, we must assure that all of our inference rules are sound (truth-preserving). In other words, if they’re applied to a set of premises, they can derive only conclusions that are entailed by those premises. Said another way, they can derive only conclusions that must be true in every interpretation in which the premises are true.