\documentstyle[11pt]{article}
%\usepackage[]{}
 
\begin{document}
 
        \title{
        The Mutilated Checkerboard in Set Theory\\
}
\author{
        John McCarthy\\
\\Computer Science Department\\Stanford University\\jmc@cs.
stanford.edu
        \\http://www-formal.stanford.edu/jmc/   % insert author(s) here
}
\date{}   % optional
 
\maketitle
 
 
        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
{\em heavy duty set theory}.\footnote{The Mizar theorem prover
  essentially accepts the definitions, but seems to be far from
  providing a proof.}
 
We have the definitions
 
\begin{equation}
        Board = Z8 \times Z8,
        \label{board}
\end{equation}
 
\begin{equation}
        mutilated\mbox{-}board = Board - \{(0,0),(7,7)\},
        \label{mutilated1}
\end{equation}
 
 
\begin{equation}
        \begin{array}{l}
                domino\mbox{-}on\mbox{-}board(x) \equiv (x \subset Board) \land
card(x) =2  \\
                \land (\forall x1\ x2)(x1 \not= x2 \land x1 \in x \land x2 \in x
 \\
                \supset adjacent(x1,x2))
        \end{array}
        \label{domino}
\end{equation}
%
and
 
\begin{equation}
        \begin{array}{l}
                adjacent(x1,x2) \equiv |c(x1,1) - c(x2,1)| =1 \\
                 \land c(x1,2) = c(x2,2) \\
                \lor |c(x1,2) - c(x2,2)| =1 \land c(x1,1) = c(x2,1).
        \end{array}
        \label{adjacent}
\end{equation}
%
If we are willing to be slightly tricky, we can write more compactly
 
\begin{equation}
      adjacent(x1,x2) \equiv |c(x1,1) - c(x2,1)| + |c(x1,2) - c(x2,2)| = 1,
        \label{adjacent1}
\end{equation}
%
but then the proof might not be so obvious to the program.
 
 
Next we have
 
\begin{equation}
\begin{array}{l}
                partial\mbox{-}covering(z)  \\
                 \equiv (\forall x)(x \in z \supset
        domino\mbox{-}on\mbox{-}board(x))
  \\
        \land (\forall x\ y)(x \in z \land y \in z \supset x = y \lor x \cap
        y = \{\})
\end{array}
        \label{covering}
\end{equation}
 
 
                                        \noindent {\bf Theorem}:
\begin{equation}
        \lnot (\exists z)(partial\mbox{-}covering(z) \land \bigcup z
        = mutilated\mbox{-}board)
        \label{theorem}
\end{equation}
 
\noindent {\bf Proof:}
 
We define
 
\begin{equation}
        x \in Board \supset color(x) = rem(c(x,1) + c(x,2),2)
        \label{color}
\end{equation}
 
 
 
\begin{equation}
\begin{array}{l}
        domino\mbox{-}on\mbox{-}board (x) \supset \\
         (\exists u\ v)(u \in x
        \land v \in x \land color(u) = 0 \land color(v) = 1),
\end{array}
        \label{colordomino}
\end{equation}
 
\begin{equation}
        \begin{array}{l}
                partial\mbox{-}covering(z) \supset  \\
                card(\{u \in \bigcup z|color(u) =0\}) \\
                =       card(\{u \in \bigcup z|color(u) =1\}),
        \end{array}
                \label{eqcolor}
\end{equation}
 
 
\begin{equation}
\begin{array}{l}
         card(\{u \in mutilated\mbox{-}board|color(u) = 0\}) \\
        \not= card(\{u \in mutilated\mbox{-}board|color(u) = 1\}),
\end{array}
        \label{mutilated}
\end{equation}
%
and finally
 
\begin{equation}
        \lnot (\exists z)(partial\mbox{-}covering(z)\ \ \land\ \
        mutilated\mbox{-}board = \bigcup z)
        \label{theorem-again}
\end{equation}
 
\noindent {\bf Q.E.D.}
 
 
\end{document}