The Mutilated Checkerboard in Set

Theory

John McCarthy Computer Science Department

Stanford University jmc@cs.stanford.edu

http://www-formal.stanford.edu/jmc/

September 13, 2004 An 8 by 8 checkerboard with two diagonally opposite squares removed cannot be covered by dominoes each of which covers two rectilinearly adjacent squares. We present a set theory description of the proposition and an informal proof that the covering is impossible. While no present system that I know of will accept either the formal description or the proof, I claim that both should be admitted in any heavy duty set theory.

We have the definitions

Board = Z8 × Z8,  (1)

mutilated-board = Board − {(0, 0), (7, 7)},  (2)

\begin{matrix}domino-on-board(x) ≡ (x ⊂ Board) ∧ card(x) = 2 \\ ∧(∀x1 x2)(x1 ≠ x2 ∧ x1 ∈ x ∧ x2 ∈ x \\ ⊃ adjacent(x1, x2)), \end{matrix}  (3)

\begin{matrix}adjacent(x1, x2) ≡ |c(x1, 1) − c(x2, 1)| = 1 \\ ∧c(x1, 2) = c(x2, 2) \\ ∨|c(x1, 2) − c(x2, 2)| = 1 ∧ c(x1, 1) = c(x2, 1), \end{matrix}  (4)

and

\begin{matrix}partial-covering(z) \\ ≡ (∀x)(x ∈ z ⊃ domino-on-board(x)) \\ ∧(∀x y)(x ∈ z ∧ y ∈ z ⊃ x = y ∨ x ∩ y = \{\}) \end{matrix}  (5)

Theorem:

¬(∃z)(partial-covering(z) ∧ ⋃ z = mutilated-board)  (6)

Proof: We define

x ∈ Board ⊃ color(x) = rem(c(x, 1) + c(x, 2), 2)  (7)

\begin{matrix}domino-on-board(x) ⊃ \\ (∃u v)(u ∈ x ∧ v ∈ x ∧ color(u) = 0 ∧ color(v) = 1), \end{matrix}  (8)

\begin{matrix}partial-covering(z) ⊃ \\ card(\{u ∈ ⋃ z|color(u) = 0\}) \\ = card(\{u ∈ ⋃ z|color(u) = 1\}), \end{matrix}  (9)

\begin{matrix}card(\{u ∈ mutilated-board|color(u) = 0\}) \\ ≠ card(\{u ∈ mutilated-board|color(u) = 1\}), \end{matrix}  (10)

and finally

¬(∃z)(partial-covering(z) ∧ mutilated-board = ⋃ z) (11)

Q.E.D.