Sunday, 23 November 2014

peano arithmetic - Naturally definable sets of natural numbers

In general, I consider this question interesting. But on the other hand - well, you don't specify what literals you accept in your formal System.



If you have $le$ for example, it is likely that you define $a < b$ by $a le b wedge aneq b$, so you implicitly get an $=$ into your formula, and hence, you also cant allow $x < n$ for fixed $n$. Same for $le$. So actually, I would consider it more reasonable to disallow explicit numbers in general. In fact, anything that depends on an explicitly given (and therefore exchangable) number doesnt seem "natural" to me.



(Also, being even doesnt really seem natural to me - it is divisibility by 2, why not divisibility by 3? But as soon as you have a $+$-Function, you cannot suppress this being natural.)



Lets assume we are in a classical setting. Then it is sufficient to have $wedge$, $vee$, $lnot$, $forall$ to express anything we want, and the relation symbols $=$, <, and the function symbols $S$, $+$, $cdot$ (normally, we could spare $S$ and add $0$ and $1$ if we have $+$, but since we dont want explicit numbers anyway, lets just add the successor-function and disallow $0$ and $1$ - so the "naturality" is a consequence rather than an enforcement).



Of course, we can express $mathbb{N}$ and $emptyset$ by $x=x$ and $x < x$, and conjunctions and disjunctions of it. We can express the set of even numbers by $lnotforall y lnot x=y+y$, and the set of all primes by $forall a,b,c,d . x=acdot d rightarrow x=bcdot d rightarrow x neq c cdot d$, and we can express finite intersections and unions.



And - we still can define predicates depending on explicit numbers, since $forall y (x < y vee x=y) leftrightarrow x=0$. So lets - additionally - disallow <. Then the atoms we have left are $=$-expressions between terms consisting of variables, $S$, $+$ and $cdot$. Trivially, every of these terms is equal to some polynomial with natural coefficients. On the other hand, we can express every polynomial with natural coefficients of at least degree 1 in every variable by these natural numbers. And thus, our atomic relationships between variables are equivalent to the relationships between polynomials with natural coefficients of at least degree 1, which can always be expressed as sets of roots of a polynomial with integer coefficients of at least degree 1. So what we get as atoms are relations describing sets of natural roots of polynomials with integer coefficients.



Anyway, enough of this, well, we can still get $0$ by saying $x+x=x$ and $1$ by saying $x*x=x wedge x+x neq x$.



Disallowing $+$ and $cdot$ would seem strange to me, as then you would only have the successor-function, which would only allow atomic relations equivalent to $x=y+n$ for fixed $n$ - and still, here you would be able to get $0$ by saying $forall y.x neq S(y)$.



Maybe you could also disallow negations instead, then you would get something similar to algebraic varieties. Or maybe you should take a look at Presburger Arithmetic.



I myself would just define a set of natural numbers as "natural" if it is decidable.

No comments:

Post a Comment