Cardano and the Exclusive Club

Chapter 3, Problem 6 from [To Mock a Mockingbird]

Here is a [calculational solution] to this problem.

In a small village there is an Exclusive Club, consisting of every person who doesn't shave anyone who shaves him. There is also the local barber, Cardano, who boast that he shaves the Exclusive Club, the whole Exclusive Club, and nothing but the Exclusive Club. Prove that Cardano cannot be telling the truth.

Representation

We write x and y for arbitrary people in the village, and let c stand for Cardano. We use the following notations:

 xSy == "x shaves y"
 E.x == "x is a member of the Exclusive Club"

The definition of the Exclusive Club can be represented as

 (1)  (Ax|: E.x == (Ay| ySx: !xSy))

and Cardano's claim is

 (2)  (Ax|: cSx == E.x)

Solution

We will prove that (1) and (2) together lead to a contradiction. We start with (1): for every x,

   E.x == (Ay| ySx: !xSy)
==   "(2), which is the only thing known about E.x"
   cSx == (Ay| ySx: !xSy)
=>   "logic: weakening, so that we can substitute y:=c"
   cSx => (Ay| ySx: !xSy)
=>   "choose y:=c"
   cSx => (cSx => !xSc)
==   "logic: simplify"
   cSx => !xSc

This proves

 (3)  (Ax| cSx: !xSc)

Now there are two obvious things that we can do with this statement: we can substitute x:=c, or we can rewrite it so that definition (1) applies. We will do both.

First we calculate

   (Ax| cSx: !xSc)
==   "choose x:=c"
   cSc => !cSc
==   "logic: rewrite =>"
   !cSc \/ !cSc
==   "logic: simplify"
   !cSc

and then

   (Ax| cSx: !xSc)
==   "logic: exchange range and domain, to prepare for (1)"
   (Ax| xSc: !cSx)
==   "(1), after renaming x:=y"
   E.c
==   "(2)"
   cSc

So from (1) and (2) we've derived both that Cardano shaves himself, and that he doesn't, which is a contradiction. Therefore Cardano was lying.

This page is brought to you by Marnix Klooster, and is part of his home page. Feel free to e-mail me with comments on the form and content of this page.

Changes to calc/tmam-3-6.html:

Sat Oct 30 12:38:39 MEST 2004  Marnix Klooster
  * Move from CVS to darcs: do not show the CVS date anymore.

Thu Feb  7 19:43:35 MET 2002  marnix
  * Updated all files to use the m4 template

Fri Sep 14 19:28:49 MEST 2001  marnix
  * moved tmam-x-x to tmam-3-6