Predicate Logic

For predicate logic, we need several additional axioms and rules. The axioms are all fairly straightforward. We have, first of all, three axioms (actually axiom schemata) for identity:

$$x=x \textrm{ for each variable } x$$

$$[(x_1 = y_1) \wedge (x_2 = y_2) \wedge \dots \wedge (x_n = y_n)]\to (f(x_1,x_2,\ldots, x_n) = f(y_1, y_2, \ldots, y_n))$$

$$[(x_1 = y_1) \wedge (x_2 = y_2) \wedge \dots \wedge (x_n = y_n)]\to (R(x_1,x_2,\ldots, x_n) = R(y_1, y_2, \ldots, y_n))$$

Notice that the first axiom corresponds to B&E's rule of $=$Intro, and the other two axioms correspond to B&E's rule of $=$Elim. Given the way the quantifier rules work, we will be able to get from $x=x$ to $(\forall x)(x=x)$, and from there to $t=t$ for any term $t$ (subject to certain substitutability requirements), so the first axiom gives results as general as $=$Intro even though it only explicitly concerns variables. Similarly, the second and third axioms only explicitly allow substitution of variables, and then only into terms consisting of function symbols followed by terms, and into relation symbols followed by terms. In fact, however, the effect will be to allow substition of any term $t_2$ for any term $t_1$ if we have the identity statement $t_1 = t_2$, and to allow this in any formula.

We also have two quantifier axioms. These are also quite straightforward.

$$(\forall x \phi) \to \phi^x_t, \textrm{ if $t$ is substitutable for $x$ in $\phi$.}$$

$$\phi^x_t \to (\exists x \phi), \textrm{ if $t$ is substitutable for $x$ in $\phi$.}$$

The first of these quantifier axioms corresponds to the rule $\forall$Elim, and the second corresponds to the rule $\exists$Intro. You will recall that of the four quantifier rules in B&E, these are the two that have no restrictions and are easy to understand. To fully understand the axioms, we need to recall some definitions from Chapter 1. $\phi^x_t$ is the result of substituting $t$ for all free occurrences of $x$ in the formula $\phi$. $t$ is substitutable for $x$ provided that it does not contain any free variables that would be bound by quantifiers in $\phi$. (Here again we see how complicated everything needs to be in order to accommodate nonsentential formulas.) For instance, if $t$ is the term $y$, then it is not substitutable for $x$ in the formula $(\forall y)(\textrm{Large}(y) \to y \not= x)$. [Note to self: find a better example. Need a reasonable formula which would become unreasonable if the substitution were allowed. This one doesn't really qualify because it can't be true to start with, since free variables are essentially treated as though they were universally quantified.]

This leaves us with two quantifier rules of inference, which we may anticipate will correspond to $\forall$Intro and $\exists$Elim, the more complicated quantifier rules in B&E's system (as well as most others). And so they do, but at first glance they are a bit mysterious.

First, we have a rule corresponding to $\forall$Intro, namely the rule

$$\langle \{\psi \to \phi \}, \psi \to (\forall x \phi) \rangle$$

provided that $x$ is not free in $\psi$. (A minor point: $x$ can be any variable. So it might be better to say that, for any variable $v$, $\langle \{\psi \to \phi \}, \psi \to (\forall v \phi) \rangle$ is a rule of inference.)

We also have a rule corresponding to $\exists$Elim, namely this:

$$\langle \{\phi \to \psi \}, (\exists x \phi) \to \psi \rangle$$

provided, again, that $x$ is not free in $\psi$.

It requires some thought to see that these rules amount to $\forall$Intro and $\exists$Elim, and Leary really doesn't help all that much, as his entire discussion of these two rules consists of about half a page. (He also doesn't have any exercises that require using the rules!)

It may help to look at how these rules might actually be used in a deduction. Let's consider a couple of easy quantifier proofs and compare how they work in B&E's system and in Leary's system. [Actually I only had time to type one of these up for the time being.]

To begin with, suppose we want to prove, from the premises that $(\exists x)\textrm{Tet}(x)$ and $(\forall x)(\textrm{Tet}(x) \to \textrm{Large}(x))$, the conclusion $(\exists x)\textrm{Large}(x)$. This should be a fairly straightforward deduction. Here is a proof in B&E's system:

And now, for comparison, here is a proof in Leary's system:

$$\begin{array}{lll} 1. & (\exists x)\textrm{Tet}(x) & \textrm... ...ists x)\textrm{Large}(x) & \textrm{prop cons: 1, 7} \end{array}$$

That's all for now . . .