Logic Trees: How do I figure out which names to apply for the universal quantifier first?

Question

I'm trying to teach myself logic with Nicholas J.J. Smith's Logic: The Laws of Truth. Right now, I'm working through the chapter on General Predicate Logic, and am having a little bit of difficulty in working out trees that involve the universal quantifier. Here's problem 12.3.1.2.viii:

∀x∀y(∃z(Rzx ⋀ Rzy) → Rxy)
∀xRax
∴ ∀x∀yRxy

I got into 20-something steps three times before I gave up and checked Smith's answer key. His answer is neat and sensible. I don't have any difficulty understanding it as an explanation. What I'm finding difficult is figuring out how you know when to apply which name to the universal quantifier.

Here's how the tree starts:

1. ∀x∀y(∃z(Rzx ⋀ Rzy) → Rxy)
2. ∀xRax
3. ¬∀x∀yRxy
…
7. ¬Rbc (addressing the negation in 3, & then introducing names)

So far, no problem. I then did something a little differently from Smith, which seems harmless enough, which is that I applied the names a, b, & c to the universal quantifier in 2.

8. Raa
9. Rab
10. Rac

Smith does very nearly the same thing later. The change in order doesn't seem important. But what is important is how Smith treats the universal quantifier in 1: He begins by assigning it the name b, and never has to go any further.

11. ∀y(∃z(Rzb ⋀ Rzy) → Rby)

And then he assigns the name c to the universal quantifier in 11:

12. ∃z(Rzb ⋀ Rzc) → Rbc

Which allows then splits into two branches which very quickly close off.

My problem was that I went through and applied each name to each universal quantifier systematically, rapidly developing a fairly unwieldy tree. My question, then, is: How do you know where to begin in assigning universal quantifiers? Do you just develop a sense/an eye for what kinds of patterns might develop? Is this just a matter of experience? Or is there a method?

Answer 1

Mostly it's a matter of experience -- as well as a very important point which it looks like you're neglecting: The purpose of formal logic is to model ordinary prose mathematical reasoning of a kind you should already be familiar with. The best way to construct a formal proof is not to stare at the rules, but to think up an ordinary informal proof and then use your proof system to formalize that.

In this case the informal proof would be something like:

Theorem. Assume that we have a relation $\prec$ that satisfies

1. $\forall x\forall y\; (\forall z(z\prec x\land z\prec y))\to x\prec y $
   (that is, whenever there is something ($z$) that relates to both $x$ and $y$, then $x$ and $y$ relate to each other) and
2. $\forall x\; a\prec x$
   (the special element called $a$ relates to everything)

Then everything is related to everything.

Proof. Let $x$ and $y$ be arbitrary. Then since the $a$ from assumption (2) relates to everything, we have $a\prec x$ and $a\prec y$. But this means that $a$ can play the role of $z$ in the premise of (1), so we conclude that $x\prec y$. But since $x$ and $y$ were arbitrary, this means that everything relates to everything.

Formalizing this proof is then not a matter of knowing how to apply the rules in isolation, but of knowing how your rules can be used to represent each of the motifs in our informal proof.

The details of this depends on exactly how the textbook's system (which I don't know in detail) is set up. What you should now use the exercise for is try to map the formal proof in the solution key back to an informal prose proof, and compare their structure to get a feel for how the formal rules express the manipulations we take for granted when we write prose proofs.

For example, the part you quote sounds like Smith's system deals with the "Let $x$ and $y$ be arbitrary" motif by choosing new constant letters $c$ and $d$ to stand for $x$ and $y$ in the following proof steps, and then finally uses a generalization rule to swap the $b$ and $c$ out with $x$ and $y$ while getting the quantifier in place -- the "since $x$ and $y$ were arbitary" step.