Set of axioms for finite subset of Natural Numbers

Question

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?

Answer 1

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:

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

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

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

Answer 2

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

1. $0\in N'$

2. $Max\in N'$

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

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

5. $S(Max)\notin N'$

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

7. $\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:

1. $\forall x\in N':x+0=x$

2. $\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.