Description of a matrix in first-order logic Assume a 9 by 9 matrix with variable elements that are natural numbers ranging from 1 to 9 (like a Sudoku puzzle). I want to describe the entire matrix in first-order logic, but I'm having trouble thinking of a way to do so that isn't too horribly verbose.
Anyone have ideas? In general, I guess I don't really understand well how to quantify objects in first-order logic...
 A: To do this you need some way to describe the relations between the numbers in the matrix. A standard one is using set theory, with the membership relation $\in$ as our only primitive relation. Using that, we first define some convenience notation:
\begin{align}
    x = \left\{ a, b \right\} :=& \forall{y} 
(y \in x \leftrightarrow y = a \vee y = b) \\\\
    x \in \left\{ a, b \right\} :=& (x = a \vee x = b).
\end{align}
This lets us define the notation for singletons as $\left\{ a \right\} := \left\{ a, a \right\}$. Now we can define an ordered pair using the usual Kuratowski definition:
$$\langle a, b \rangle := \left\{ \left\{ a \right\}, \left\{ a, b \right\} \right\}.$$
From ordered pairs we move to finite sequences $\langle a_0, a_1, \dotsc, a_n \rangle$ of length $n$. These we can define by recursion using ordered pairs. Let a sequence of $n$ elements be defined as follows
\begin{align}
    \langle a_1, a_2, \dotsc, a_n \rangle :=& \langle \langle a_1, a_2, \dotsc, a_{n - 1} \rangle, a_n \rangle
\end{align}
Then we can define an $n$ by $m$ matrix as a sequence of length $m$ of sequences of length $n$ of numbers. To get back a representation of a particular matrix in the language of set theory, $\mathcal{L}_\in$, just start with a matrix and replace recursively with the right-hand side of these definitions. Eventually you'll get a very long formula $\varphi$ in $\mathcal{L}_\in$. There is a reason we don't do this very often!
