CS 245 — Lecture 16

Natural Deduction for Predicate Logic

So now that we understand the semantics of predicate logic, it's time to tackle the last piece of the puzzle: proof systems for predicate logic. We will be extending natural deduction, the Gentzen-style proof system we know and love, to predicate logic. What this means is that all of the inference rules we have from before will stay the same and we will add new rules to cover quantifiers. You may have already guessed that this means there are four new inference rules to be defined: $\forall e, \forall i, \exists e, \exists i$. Since we are familiar with inference rules already, we will group the rules by how easy they are to use.

The easy rules

The rules that are easier to use are $\forall e$ and $\exists i$:

Definition 16.1. \begin{equation*} \frac{(\forall x \alpha)}{\alpha[t/x]} \forall e \quad \frac{\alpha[t/x]}{(\exists x \alpha)} \exists i \end{equation*}

So what exactly do these rules say? For $\forall$e, if we have a formula $(\forall x \alpha)$, then we can conclude that we can substitute anything for $x$ in $\alpha$. That is, since $\alpha$ holds for all values $x$, we should be able to replace $x$ with any term.

On the other hand, if we have some formula $\alpha$ that holds for some term $t$, we can conclude that there is at least one value such that $\alpha$ holds. In other words, we have shown that there exists some element for which $\alpha$ holds and therefore, $(\exists x \alpha)$.

The reason that these are so simple is that they are analogous to $\wedge e$ and $\vee i$. In the case of $\forall e$, if a formula is true for every value of $x$, we can take that formula and substitute any value we wish for $x$ and it will still be true. Similarly, if we have a formula that is true after substituting some value for a variable $x$, we can conclude that it is true for some value.

Example 16.2. We will show that $\{(\forall x P(x))\} \vdash (\exists y P(y))$.

This proof is not earthshattering, but the reasoning behind these rules was not groundbreaking either. We can reason this out quite simply: if $(\forall x P(x))$, then obviously, we can choose some arbitrary value $u$ to get $P(u)$. Since we have $P(u)$, we know that there is some value $u$ that gave us $P(u)$, and therefore, we can conclude that $(\exists y P(y))$.

Example 16.3. Here, we'll have a look at what we're allowed to do with these rules. We show $\{(\neg P(y))\} \vdash (\exists x (P(x) \rightarrow Q(y)))$.

A very quick reading of the inference rule $\exists$i may lead you to believe that its application should have resulted in $(\exists x (P(x) \rightarrow Q(x)))$ in the final line. However, we need to take a careful look at what the inference rule says: we can infer $(\exists x \alpha)$ if we have a formula $\alpha[t/x]$. Let's consider $\alpha$. If $\alpha = (P(x) \rightarrow Q(x))$, then we have $\alpha[y/x] = (P(y) \rightarrow Q(y))$, as expected. But if $\alpha = (P(x) \rightarrow Q(y))$, then $\alpha[y/x] = (P(y) \rightarrow Q(y))$ too!

Universal quantifier introduction

With the more complicated rules, we need to introduce a new notion dealing with subproofs. First, let's look at the rule for introducing a universal quantifier:

Definition 16.4. $$\frac{\boxed{\begin{matrix} \text{$u$ fresh} \\ \vdots \\ \alpha[u/x] \end{matrix}}}{(\forall x \alpha)} \forall i$$

The way to think about $\forall$i is to think about $\wedge$i. For $\wedge$i, we needed to make sure that we had the two formulas $\varphi$ and $\psi$ show up in our proof before we could apply $\wedge$i to make $(\varphi \wedge \psi)$. In other words, we need to somehow have $\alpha$ for every value $x$. Of course, this is a problem since there could be infinitely many values in our domain.

Let's step back for a second and think about how we might prove that something is true, say, for all natural numbers. We'd start the proof by saying something like "let $n$ be a natural number," and then proceed. Then once we prove whatever it is that we wanted to prove for $n$, we'd conclude that, since we just chose an arbitrary $n$, the property must hold for all natural numbers.

Now, let's go back to the inference rule. Here, "$u$ fresh" is a new notion that captures this idea of choosing some arbitrary $u$ to work with. Here, fresh means that the variable has never been used before in the proof. And because it opens a subproof, it will not be used once we're finished proving that $\alpha[u/x]$. Just like an assumption, $u$ is a local variable that only lives inside the box that it opens. The same subproof rules apply: if the box is open, we can use it, and if the box is closed, we can't reach in and grab something from it.

Example 16.5. We will show $\{(\forall x P(x))\} \vdash (\forall y P(y))$.

Again, this proof is kind of obvious and is meant to illustrate the reasoning behind the rules. Here, we are claiming that if we have an arbitrary new value $u$, then since $(\forall x P(x))$, we must have $P(u)$. However, since $u$ is fresh, in the sense that it is an arbitrary value, we may conclude that $(\forall y P(y))$.

Example 16.6. We will show $\{(\forall x(P(x) \vee Q(x))), (\forall x(\neg P(x)))\} \vdash (\forall x Q(x))$.

Example 16.7. Back when we were introducing the notions of predicate logic, we discussed how to express the very questionable claim that "no students love CS 245". We had either $(\neg (\exists x (S(x) \wedge L(x,c))))$ or $(\forall x (S(x) \rightarrow (\neg L(x,c))))$. We can now start to prove that these two formulas are equivalent using natural deduction.

First, we will show that $\{(\neg (\exists x (S(x) \wedge L(x,c))))\} \vdash (\forall x (S(x) \rightarrow (\neg L(x,c))))$.

We'll see how to prove the other direction once we introduce our final new rule...