I want to axiomatize sudoku

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.
 PhysOrg.com science news on PhysOrg.com >> Galaxies fed by funnels of fuel>> The better to see you with: Scientists build record-setting metamaterial flat lens>> Google eyes emerging markets networks
 Blog Entries: 8 Recognitions: Gold Member Science Advisor Staff Emeritus 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 *...