The Mutilated Checkerboard in Set Theory

John McCarthy Computer Science Department Stanford University jmc@cs.stanford.edu http://www-formal.stanford.edu/jmc/

April 27, 2001

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.^{1}

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)(x = \{x1, x2\} → adjacent(x1, x2)) \end{matrix}  (3)

and

\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)

If we are willing to be slightly tricky, we can write more compactly

adjacent(x1, x2) ≡ |c(x1, 1) − c(x2, 1)| + |c(x1, 2) − c(x2, 2)| = 1, (5)

but then the proof might not be so obvious to the program.

Next we have.

1The Mizar proof checker accepts the definitions essentially as they are, but the first proof in Mizar is 400 lines.

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

Theorem:

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

Proof:

We define

x ∈ Board → color(x) = rem(c(x, 1) + c(x, 2), 2)  (8)

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

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

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

and finally

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

Q.E.D.