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.
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)
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 => !xScThis 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" !cScand then
(Ax| cSx: !xSc) == "logic: exchange range and domain, to prepare for (1)" (Ax| xSc: !cSx) == "(1), after renaming x:=y" E.c == "(2)" cScSo 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.
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