Set of axioms for finite subset of Natural Numbers I would like to get a set of Peano like first-order axioms for a finite subset of natural numbers $N'$ such that $0 \leq N' \leq Max$, with $Max$ denoting the upper-bound. (So my signature might be $(0,Max, suc, + , *)$ or only $(0,Max, suc)$. Is this possible to achieve by a limited set of axioms (by possibly tweaking Peano's set of axioms) or any other way?
 A: I played around with following axioms for finite arithmetic a while ago. I couldn't do much with them.  Maybe you will be able to do something with them:
Axioms


*

*$0\in N'$

*$Max\in N'$

*$\forall x\in N':[x\ne Max\implies S(a)\in N'] $ (a partial function)

*$\forall x\in N': S(x)\ne 0$

*$S(Max)\notin N'$

*$\forall x,y:[S(x)=S(y)\implies x=y]$

*$\forall P\subset N':[0\in P \land \forall x\in P:[S(x)\in N'\implies S(x)\in P] \implies N'\subset P]$
Will need to tweak that last one for a first-order representation. In that case, you will also need definitions of $+$ and $\times$ since you won't have set theory to construct them.
For addition:


*

*$\forall x\in N':x+0=x$

*$\forall x,y,z \in N':[S(y)\in N' \land S(z)\in N' \implies [x+y=z\implies x+S(y)=S(z)]$
Example
$N'=\{0,1,Max\}$
$S(0)=1$
$S(1)=Max$
$S(Max)$ is undefined.
$0+0=0$
$1+0=1$
$Max+0=Max$
$0+1=1$
$0+Max=Max$
$1+1=Max$
Other sums are undefined.
A: Finite structures can always be described completely. You haven't specified what the successor of $Max$ is, so I'm giving it the name $M$; $M$ has to be an element of your domain. For a number $k$, let $\langle k \rangle$ be $suc^{(k)}(0)$, that is the result of applying $suc$ to zero $k$ times. The axioms for $(0,Max,suc)$ are:


*

*$\forall x (x = \langle 0 \rangle) \lor (x = \langle 1 \rangle) \lor \cdots \lor (x = \langle Max \rangle)$.

*$\langle i \rangle \neq \langle j \rangle$ for all $0 \leq i < j \leq Max$.

*$suc(\langle Max \rangle) = \langle M \rangle$.
If you're adventurous, you can leave the last axiom out. It is still the case that the successor of $Max$ is some element in $0,\ldots,Max$, but we "don't know" which.
If you want to add more operators, you just add axioms describing them completely. For example, let $plus$ be some operation from the square of the domain to itself. Then you can add the axioms $\langle i \rangle + \langle j \rangle = \langle plus(i,j) \rangle$ for all $0 \leq i,j \leq Max$.
