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?
$\begingroup$
$\endgroup$
Add a comment
|
2 Answers
$\begingroup$
$\endgroup$
7
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$.
answered Apr 10, 2015 at 4:48
-
$\begingroup$ 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. $\endgroup$ Apr 10, 2015 at 4:55
-
$\begingroup$ @RossMillikan I don't have to remove it since I never included it. $\endgroup$ Apr 10, 2015 at 4:56
-
$\begingroup$ 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. $\endgroup$ Apr 10, 2015 at 5:01
-
1$\begingroup$ @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. $\endgroup$ Apr 10, 2015 at 5:37
-
1$\begingroup$ @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$). $\endgroup$ Apr 10, 2015 at 6:09
$\begingroup$
$\endgroup$
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
$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.
answered Apr 10, 2015 at 4:23
-
$\begingroup$ 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? $\endgroup$– qartalApr 11, 2015 at 20:45
-
$\begingroup$ 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. $\endgroup$ Apr 11, 2015 at 22:09