Good Math

All in the Family

Now let’s move on and try something more interesting. We’re going to go back to the family-relationships example from the previous chapter and prove that if two people are cousins, then they have a common grandparent.

In our family relations, we need to define what cousins are in logical terms: we’ll say that two people are cousins if they each have a parent who’s a sibling of one of the other’s parents. In FOPL, that’s this: ∀ a: ∀ b: Cousin(a, b) ⇔ ∃ m: ∃ n: Sibling(m, n) ∧ Parent(m, a) ∧ Parent(n, b).

We want to prove that ∀ d: ∀ e: Cousin(d, e) ⇔ ∃ g: Grandparent(g, d) ∧ Grandparent(g, e).

Like the proof of the excluded middle, we can do this without branching the tree. The proof does have a fair bit of jumping around. ...