How to Generate Theorems for an Abstract System like Sudoku?

[TylerH]

For an exercise, I want to axiomatize sudoku.

I've came up with the definition of the sudoku puzzle in mathematical terms, as well as the definition of a solved puzzle. I'm have trouble going from there to draw theorems from my newly defined system. How does one generate theorems about an abstract system like this?

My definition:

Generalizing for an n^2 x n^2 sudoku puzzle:

Let there be a matrix, A, of deminsions, n x n, such that each element is a matrix of deminsions, n x n.
Let there be a set, S = {x exists in N, 1 <= x <= n^2}.

The puzzle is solved iff every element of A contains exactly one of each member of S and for every i from 1 to n, the set of elements in A(i, j) for j from 1 to n contains exactly one of each member of S.

Any suggestions on changes to the definition are also appreciated.

 

[micromass]

With a sudoku puzzle, we can associate a operation * as:

$$*:\{1,...,n\}\times\{1,...,n\}\rightarrow \{1,...,n\}$$

such that k*l is the number in row k, column l. Thus the Cayley multiplication table of this operation is our Sudoku puzzle.

An interesting thing to find out is what properties our * satisfies. For example, you can show that * is cancelative, that is:

$$a*b=a*c~\Rightarrow~b=c$$

That's a theorem you can prove. Maybe you can search some other things that hold for our *...