Subsection 5.1.7 New Rules for Instantiating and Generalizing Quantifiers
So now our proof toolkit includes all of the Boolean identities and inference rules. And we have just added two new identities, the two Quantifier Exchange rules.
The last thing we need is some new inference rules that will allow us to reason with quantified expressions. To see why, consider the following argument that we should surely be allowed to make:
 ∀x (Student(x) → Person(x)) All students are people.
 ∀x (Person(x) → Breathes(x)) All people breathe.
 ∀x (Student(x) → Breathes(x)) All students breathe.
An argument with this structure is called a syllogism. Syllogisms have formed the core of classical logic since the days of Aristotle. We have no problem writing syllogisms in Boolean logic. In fact, the inference rule that lets us write them is called Hypothetical Syllogism:
From p → q and q → r, infer p → r.
We’ve already seen that we can treat a predicate logic statement (i.e., an entire expression that has a truth value) as a single proposition and then reason with it just as we would have done in Boolean logic.
But this won’t solve the problem of writing syllogisms like the Breathes one. To do that, we need to reach inside quantified expressions. We want to match the (nonstatement) wff Person(x) on the right hand side of the implication in  with the same (nonstatement) wff on the left hand side of the implication in  so that we can chain the two statements together. We don’t yet have a way to do that. We’ll present one soon.
But, first, let’s see why we can’t just wing it.
Assume the following premises:
 All students are creatures.
 All zebras are creatures.
 All creatures are mortal unless they are mythological.
 All mythological creatures have stripes.
 There are no striped students.
 Not all zebras have stripes.
Can we conclude:
 All students are mortal.
 All zebras are mortal.
The answer is yes for  and no for . And this time, it’s much less obvious how we can reason correctly and not make mistakes.
To guarantee that we continue to use only inference rules that we know are sound, we need to formalize the ways that we can work with quantified statements.
For each of the following arguments, indicate whether or not it is a syllogism:
(a) All great desserts are chocolate.
Brownies are chocolate.
∴ Brownies are great desserts.
(b) All unicorns have stripes.
All striped things are happy.
∴ All unicorns are happy.
(c) All wooly things are warm.
All sheep are wooly.
∴ All sheep are warm.