Subsection 5.1.8 Our Approach – Back and Forth to Boolean Logic
So we need a way to reach inside quantified expressions to reason with them.
To solve this problem, we’ll propose a bigger picture plan:
We observe that we have very flexible inference rules for Boolean logic.
So, to work in predicate logic, we will define a set of rules that allow us to:
Transform predicate logic expressions into Boolean ones,
Reason in the Boolean world, and finally
Transform the Boolean expressions back into predicate logic.
Of course, we must do that in a way that is sound.
Here’s the key idea we’ll use:
In Boolean logic we reason about individuals one at a time.
But quantified statements, like ∀x (P(x)) or ∃x (Q(x)), let us reason about entire groups of individuals all at once.
So what we need is a way to transform quantified statements into statements about particular individuals. Then we can reason with them.
And finally we need a way to transform back into generalized (quantified) statements.
With this idea in mind, let’s return to the Nonmythological Students example:
 All students are creatures.
 All creatures are mortal unless they are mythological.
 All mythological creatures have stripes.
 There are no striped students.
We’ll reason as follows. Consider any student. (Now we’re not talking about all students. We’re talking about just one student but (s)he’s an arbitrary one. We don’t know anything special about him/her.) We do know (s)he must be a creature (from ) and that (s)he is not striped (from ). Thus (s)he cannot be mythological (from ). So (s)he must be mortal (from ). And so we can conclude, that if an arbitrary student must be mortal, all students are mortal. We’ve thus proved:
 All students are mortal.
The set of steps that we just did is what we now must formalize.