1
$\begingroup$

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...

  • 0
    I guess you want a first-order theory whose models are $9 \times 9$ matrices of digits $\{ 1, \ldots, 9 \}$. This can be done – in fact, it can be done in _propositional_ logic – but it is probably not what you're really interested in.2012-07-12

1 Answers 1

2

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!

  • 0
    Got it now. Excellent. This is what I was looking for.2012-07-12