Ideas for modelling the rules to Sudoku using first-order logic? I'm trying to model the rules to sudoku using first order logic. I've got the first two rules down: 
(The notation I use is $a_{x,y,v} $, where $v$ is the digit and $x,y$ is the coordinates of the cell that $v$ is in.)
$\forall x_1, \forall x_2, \forall y, \forall v,( a_{x_1, y, v} \land x_1 \ne x_2 \implies \overline{a_{x_2, y, v}}) $, (same digit once per line)
$\forall x, \forall y_1, \forall y_2, \forall v,( a_{x, y_1, v} \land y_1 \ne y_2 \implies \overline{a_{y_2, y, v}}) $, (same digit once per column) $\\$ $\\$
However, I'm having a hard time finding a clever way to formalize the rule of not having the same digit more than once per sub-gird (the 3x3 ones)?
I was considering making a relation $S^{r,2}$ such that $S(x,y)$ means x and y are in the same grid, in the hopes of simplifying the modelization, but I'm not sure if that would be rigorous enough.
On the other hand, writing everything seems like it would be overcomplicated.
I'm rather new to first-order logic, but I decided to formalize the rules this way and not with propositional logic because I thought it would be easier and cleaner. And help or advice is appreciated. Thanks!
 A: Remember that first-order logic has no idea what a 'digit' is, so you'll need to specify that:
$\forall x (x=1 \lor x=2 \lor x=3 \lor x=4 \lor x=5 \lor x=6 \lor x=7 \lor x=8 \lor x = 9)$
In fact, even that is not enough, since just because you have different symbols does not mean that they should denote different objects. So, you'll actually have to specify that these are all different, i.e. you need:
$1 \not = 2$, $1 \not = 3$, etc.
Even then, first-order has no idea that $1$ is 'next' to $2$, etc. ... but you'll need that knowledge to indicate the blocks .. or at least that $1$,$2$, and $3$ go together, and same for $4$, $5$, $6$, and for $7$, $8$, $9$
So, maybe have a two-place $b$ relation to indicate that:
$b_{1,2}$, $b_{2,3}$, $b_{4,5}$, $b_{5,6}$, $b_{7,8}$, $b_{8,9}$ 
and take its symmetric and transitive closure:
$\forall z_1 \forall z_2 (b_{z_1,z_2} \to b_{z_2,z_1})$
$\forall z_1 \forall z_2 \forall z_3 ((b_{z_1,z_2} \land b_{z_2,z_3})\to b_{z_1,z_3})$
And now you can specify that there cannot be two of the same digits in the same block:
$\forall x_1 \forall x_2 \forall y_1 \forall y_2 \forall v ((a_{x_1,y_1,v} \land \neg (x_1 = x_2 \land y_1 = y_2) \land b_{x_1,x_2} \land b_{y_1,y_2}) \to \neg a_{x_2,y_2,v})$ 
Oh, and finally, make sure to say that every square needs a digit!
$\forall x \forall y \exists v \ a_{x,y,v}$
