First-order tableaux

Just like our first-order syntax and semantics is an extension of zeroth-order syntax and semantics, our first-order tableau system will be an extension of our zeroth-order one. In particular, and again paralleling the syntactic and semantic treatment, the only additional rules we need to introduce for our system are the ones which will allow us to deal with quantified sentences.

Our tableau system only deals with first-order sentences, that is, closed formulas. Accordingly, open formulas will not occur at any part of any of the deductions to follow.

Accordingly, we still have the same rules for the connectives as introduced for zeroth-order tableau. In particular, we have:

1. the premise rule Pr;

2. the double negation rule $\neg \neg$;

3. the conjunctiom rule $\wedge$ and the negated conjunction rule $\neg \wedge$;

4. the disjunction rule $\vee$ and the negated disjunction rule $\neg \vee$;

5. the conditional rule $\rightarrow$ and the negated conditional rule $\neg \rightarrow$.

We also retain the general approach to how we construct our trees. So in particular, if we want to show that $\{X_1, X_2, …\} \vdash Y$, we put the formula $\neg Y$ (the negation of $Y$) as the starting point. Then, if the argument is indeed syntactically valid, we should be able to close each branch of the tree (sooner or later) by finding some formula $Z$ and its negation $\neg Z$ for each branch.

Again, the only change is that we need rules to deal with certain additional formula forms. In particular:

1. a rule $\forall$ for universally quantified sentences of form $\forall x Y$;

2. a rule $\neg \forall$ for negated universally quantified sentences of form $\neg \forall x Y$;

3. a rule $\exists$ for existentially quantified sentences of form $\exists x Y$;

4. a rule $\neg \exists$ for negated existentially quantified sentences of form $\neg \exists x Y$.

Accordingly, our definition of what it means for something to constitute a proof of validity is as follows:

The rule $\forall$

We start with the simplest first-order tableau rule, $\forall$. What the rule $\forall$ captures, in semantic terms, is that if for some structure $\mathbf{S}$, $\mathbf{S} \models \forall x Y$, then if we take $Y$ by itself and replace each variable $x$ originally bound by the quantifier $\forall$ in front of the formula with an arbitrary name $a$, then the resulting sentence will also be true in the structure. Remember that we have a particular notation for this. Namely, what we claim is that if $\mathbf{S} \models \forall x Y$, then for any name $a$, we have that $\mathbf{S} \models Y(a/x)$. Unsurprisingly, this is a semantically valid inference in first-order logic. Moreover, it is intuitively quite simple.

For example, it is true of every natural number that it is either less than or equal 5, or larger than 5. That is, $\forall x (x\leq 5 \vee x >5)$. But then we can substitute for $x$ any specific number, and the resulting sentence will also be true. For example, it is true that $4 \leq 5 \vee 4 >5$, since $4 \leq 5$. But it is also true that $7 \leq 5 \vee 7 >5$, since $7>5$. And the sentence will also be true if we substitute $45$, $2$, or $83574634$ for $x$ in $\forall x (x\leq 5 \vee x >5)$.

Accordingly, we get the following non-branching rule:

The following example is an application of the $\forall$ rule:

As you can see, we simply took the universally quantified sentence $\forall x \exists y (R(x, y) \wedge \exists z R(x, z))$, and using the $\forall$ rule, derived from it the sentence $\exists y (R(a, y) \wedge \exists z R(a, z))$, which results from taking off the quantifier expression $\forall x$ and substituting the name $a$ for every occurrence of $x$ bound by $\forall$. And since the rule works with any name whatsoever, we could also use it like this:

Of course, in practice, which name we choose is not quite this arbitrary, since we are always aiming to close the branches of the tree. And this is usually only possible with some specific choice for a name to be substituted in.

For example, take $\{\forall x (P(x) \rightarrow Q(x)), P(b)\} \vdash Q(b)$. We can prove this as follows:

As you can see, the only reason we were able to close the branches of the tree is because we substituted $b$ for $x$ when applying $\forall$ on line $3$. If we substituted any other name for $x$, the branches would not have closed. Thus, when you are using the rule $\forall$, you need to be mindful which name you choose. Remember that the goal is always to be able to close each branch of the tree.

The rule $\neg \exists$

Just like the rules $\wedge$ and $\neg \vee$ function similarly, the $\forall$ rule functions similar to the $\neg \exists$ rule. This is no accident given the negation push-through result we showed earlier. In particular, if $\mathbf{S} \models \neg \exists x Y(x)$, then $\mathbf{S} \models \forall x \neg Y(x)$. And as noted above, from $\mathbf{S} \models \forall x \neg Y(x)$, it follows that $\mathbf{S} \models \neg Y(a/x)$ for any name $a$. So from $\neg \exists xY(x)$, we should be able to immediately derive $\neg Y(a/x)$.

Again, intuitively, this is easy to see. For example, it is true at this point in time at least that there is no one taller than 10 feet. From this, it follows that everyone is not taller than 10 feet. So substituting any person’s name, it will also be true that, e.g., ‘Dwayne Johnson is not taller than 10 feet’, ‘Donald Trump is not taller than 10 feet’, and ‘Beyonce is not taller than 10 feet’. In symbols, from $\neg \exists x T(x)$, it follows that $\forall x \neg T(x)$, from which it follows that $\forall x \neg T(a)$ for any name $a$. This is precisely the type of reasoning the $\neg \exists$ rule codifies.

For example, take $\neg \exists x (P(x) \rightarrow Q(x)) \vdash \neg Q(d) \wedge P(d)$. We can prove this as follows:

Once again, it was important when using the rule $\neg \exists$ that we substituted $d$ for $x$, since it was $d$ that occurred in the conclusion, and hence was necessary to close both branches of the tree.

The rule $\exists$

The rule $\exists$ comes with an important caveat that you should always keep in mind. Semantically speaking, a sentence like $\exists x P(x)$ gives us some information, but in some sense, that information is quite limited. Namely, it tells us that there exists an $x$ such that it is $P$, but it does not tell us which thing is the one that is $P$. Accordingly, unlike with $\forall$, you cannot just substitute any name for $x$ in $P(x)$ to get a sentence that is true. In fact, you cannot be sure that you can substitute any name for $x$ in $P(x)$, for it might be the case that the object that makes $\exists x P(x)$ true does not have a name (that is, no name is interpreted such that its value is the object that is $P$).

For example, suppose you are in a classroom the first day of classes at your college, and there are 20 other students with you. However, you only know two of them by name, your friends Jade and Ali. Then, the professor tells you: ‘There is a senior in this classroom’. Can you infer that ‘Jade is a senior’, or that ‘Ali is the senior’, based on this information alone? The answer is ‘no’, since you do not know who the senior is, only that there is one. And the situation is not much better if the professor gives you the names of every person in the room, for again, you still do not know which name is the name of the senior.

However, sometimes you do want to have a name for an object in the domain that makes an existential statement true, and to then reason about that specific object. For example, the professor might tell you later on that every person who received an A was a senior, from which you can reason that the person who is a senior got an A. Now what you can do in this case is simple; introduce a new name with the explicit intention that it refer to that specific object. In the above example, we could introduce a new name like ‘Senior’, and say that that person is a senior. The important thing is that ‘Senior’ must be an entirely new name, not shared by anyone in the class. Then, you can infer that ‘Senior is a senior’, and from then, that ‘Senior got an A’, and so on.

Based on the above, our $\exists$ rule is specified as follows:

We are now in the position to show Proposition 8.7 syntactically, namely, that $$\{\forall x (P (x) \rightarrow Q(x)), \exists y P(y)\} \vdash \exists y Q(y)$$

The proof goes like this:

Notice the interplay between our three rules, $\exists$, $\forall$, and $\neg \exists$ above. First, we used the $\exists$ rule on $\exists y P(y)$. For this, we needed to find a new name that did not occur on any of the branches or in the premise set. This was trivial, since no name occurred in either. So we chose a random one, $e$. So we deduced that $e$ is $P$. Next, we considered $\forall x (P(x) \rightarrow Q(x))$. With $\forall$, we can substitute for $x$ any name whatsoever, but of course, we chose $e$ specifically. So we got that if $e$ is $P$, then $e$ must be $Q$. With $\rightarrow$, this left us two options: either $e$ is not $P$, or $e$ must be $Q$. But we already knew that $e$ is $P$, so that branch closed. Moreover, from $\neg\exists y Q(y)$, with the rule $\neg \exists$, we can substitute for $y$ any name whatsoever. So in particular, we again substituted $e$ for $y$, getting $\neg Q(e)$, and closed the other branch.

The rule $\neg\forall$

Given the above, it is now easy to understand the rule $\neg\forall$. First, we can again refer to negation push-through. In particular, semantically, if $\mathbf{S} \models \neg \forall x Y(x)$, then $\mathbf{S}\models \exists x \neg Y(x)$. That is, if it is not true of everything that $Y$, then there is something for which it is false that $Y$. But then again, we can use the reasoning we provided for the rule $\exists$, and derive from $\exists x \neg Y(x)$ the sentence $\neg Y(a/x)$ provided $a$ is a new name introduced specifically for the object that makes $\exists x \neg Y(x)$ true. Thus, we simply have:

Here is an illustration of how this works in practice. Take the following: $${\neg\forall x Q(x), \exists y S(y) \rightarrow \forall z Q(z)} \vdash \neg \exists u S(u)$$

We can show that this is indeed the case as follows:

Notice something extremely important above. As noted, the name introduced with either $\exists$ or $\neg\forall$ must always be one that does not occur in the premise set or on the branch that we are working on. On line 4, we introduced the name $e$, using $\neg\forall$ on $\neg\forall x Q(x)$. Then, on the left branch, at line 6, we came across $\exists u S(u)$. This meant that we needed a new name to apply $\exists$. But now there was a name already occurring on the branch, namely, the name $e$. So $e$ was off limits, and we needed to find a new one. So we chose $d$. Notice also that when it came to $\neg\exists$ and $\forall$, we chose the names $d$ and $e$, respectively. There is no mystery here. We could have chosen any name whatsoever, including the inverse selection. But since we wanted to close both branches, we chose the names in accordance with that goal.

Exercise 8.8. Show that the following hold in first-order logic:

1. $\neg \forall x P(x) \vdash \exists x \neg P(x)$

2. $\exists x \neg P(x) \vdash \neg \forall x P(x)$

3. $\neg \exists x P(x) \vdash \forall x \neg P(x)$

4. $\forall x \neg P(x) \vdash \neg \forall x P(x)$

5. $\neg \forall x \neg Q(x) \vdash \exists x Q(x)$

6. $\exists x Q(x) \vdash \neg \forall x \neg Q(x)$

7. $\neg \exists x \neg Q(x) \vdash \forall x Q(x)$

8. $\forall x Q(x) \vdash \neg \exists x \neg Q(x)$

Here is the first one:

Exercise 8.9. Show that the following hold in first-order logic:

1. $\forall x \exists y L(x, y) \vdash \exists z L(a, z)$

2. $\exists x \forall y L(y, x) \vdash \forall x \exists y L(x, y)$

3. $\forall x \neg L(a, x) \vdash \exists x \exists y \neg L(x, y)$

4. $\{\forall x (L(a, x) \rightarrow P(x)), \neg P(b)\} \vdash \neg L(a, b)$

5. $\{\forall x (L(a, x) \vee \exists y (L(a, y) \wedge L(y, x)))\} \vdash L(a, b) \vee \exists x (L(a, x) \wedge L(x, b))$

6. $\{\forall x L(x, b) \vee \forall x \neg L(x, b), L(a, b)\}\vdash L(c, b)$

7. $\{\forall x L(j, x) \wedge \neg \exists y L(b, y)\} \vdash L(j, b) \wedge \neg L(b, j)$

8. $\{\forall x(L(j, x) \rightarrow \forall y L(y, x)), \neg L(a, b)\} \vdash \neg L(j, b)$

9. $\{\forall x (\exists y L(y, x) \rightarrow \exists y L(x, y))\} \vdash \neg \exists x L(a, x) \rightarrow \neg L(c, a)$

10. $\{\neg L(a, a), \forall x \forall y(L(x, y) \rightarrow L(y, y))\} \vdash \neg \exists x L(x, a)$