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?

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

• You have to remove the Peano axiom $suc(x)=suc(y) \implies x=y$ because that (along with nothing has $0$ for a successor) forces the domain to be infinite. – Ross Millikan Apr 10 '15 at 4:55
• @RossMillikan I don't have to remove it since I never included it. – Yuval Filmus Apr 10 '15 at 4:56
• True, but because the OP said Peano-like I thought the default was to include them. Certainly you are correct that finite structures can be defined completely. – Ross Millikan Apr 10 '15 at 5:01
• @qartal You're confusing the language with the metalanguage. The second axiom is a collection of $\binom{Max+1}{2}$ axioms of the form $\langle i \rangle \neq \langle j \rangle$ or, if you prefer, a single axiom which is the conjunction of these $\binom{Max+1}{2}$ statements. – Yuval Filmus Apr 10 '15 at 5:37
• @qartal I think you are missing the point of my answer. Finite structures are "boring" from many perspectives, because you can prove any true statement by just checking all cases. You can probably come up with a more succinct set of axioms – probably $(\log Max)^{O(1)}$ is enough, compared to my $Max^{O(1)}$. But these are just encoding tricks. What you should really do is work over the natural numbers with the usual axioms, and just relativize all your statements to $\{0,\ldots,Max\}$ (i.e. replace every quantifier $Qx$ with $Qx \leq Max$). – Yuval Filmus Apr 10 '15 at 6:09

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.

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.

• What do you mean you couldn't do much: Does it mean they are not complete/correct yet; or you could not find an application for this way of representation? – qartal Apr 11 '15 at 20:45
• I meant that I couldn't do something as simple as proving the associativity and commutativity of addition. All the conditions you have to test seemed to make it impractical if not impossible. Maybe you can find a way around this. – Dan Christensen Apr 11 '15 at 22:09