Is Skolem arithmetic effectively axiomatizable?

Question

Skolem arithmetic

I found nothing via Google about its axioms. Wikipedia says nothing about whether it has ever been effectively axiomatized. If it has, then what do its effective axioms look like?

Answer 1

It actually says on the page you linked

Skolem arithmetic is the first-order theory of the natural numbers with multiplication, ...

So in notation this would be $(\mathbb{N}, \cdot)$ or $\operatorname{Th}(\mathbb{N}, \cdot)$. That is, our language consists of just the multiplication symbol (and equality of course, as always) and we take all the sentences in this language that are true in the natural numbers.

Edit: after the question was edited it now asks for an effective axiomatisation. As another answer already mentions, Skolem arithmetic is decidable (as can be found on the same Wikipedia page), so in particular it is effectively axiomatisable (i.e. the set of axioms is recursively enumerable).

Answer 2

The theory of $(\Bbb N, \times)$ is decidable (there is an algorithm that decides the truth value of a given formula in $\Bbb N$), so yes, Skolem arithmetic is effectively axiomatisable, because you can enumerate first-order formulas in the language $\times$ and keep the ones that are true in $\Bbb N$. Sure, you will get a whole lot of redundant axioms but that still is an effective set of axioms.

Some examples (I omit the multiplication symbol because it would get cluttered) :

$\exists x\, \forall y \; xy=x$
$\exists x\, \forall y \; xy=y$
$\forall x\, \forall y \; xy=yx$
$\forall x\, \forall y \, \forall z\; x(yz)= (xy)z$
$\forall x\; ((\exists y \; xy \neq x) \implies \forall y\,\forall z \; (xy = xz \implies y=z))$
$\exists x\, \forall y \; x \neq yy$

Answer 3

In my initial comment to the OP, I wrote:

A better question would be: "What is an explicit axiomatization of Skolem arithmetic"? Which probably can be best answered by reading the reference for Wikipedia's claim that this theory is decidable.

I finally took my own advice on this. Wikipedia's reference is to A Survey of Arithmetical Definability by Bès. Here one can read that Skolem arithmetic was axiomatized by Cegielski in the paper Theorie elementaire de la multiplication des entiers naturels. One can find a summary of Cegielski's results in (in English) in Chapter III.5 of Logical Number Theory I by Smorynski. I'll give a further summary of what I read in Smorynski's book here.

Let's agree to axiomatize the complete theory of $(\mathbb{N}_+,\cdot)$ here (where $\mathbb{N}_+ = \mathbb{N}\setminus 0$). If you want to include $0$, it's easy to obtain an axiomatization of $(\mathbb{N},\cdot)$ from this by asserting the existence of $0$ ($\exists x \forall y (xy = x\land yx = x)$) noting it must be unique, and then restricting all the quantifiers in the axioms below to the non-zero elements.

Let's introduce some abbreviations:

• $x|y$ is an abbreviation for $\exists z(xz = y)$. It means "$x$ divides $y$".
• $x|_n y$ is an abbreviation for $\exists z(xz^n = y)$. It means "$x$ divides $y$ and the quotient is an $n^{\text{th}}$ power". We say "$x$ $n$-divides $y$". Note $0$-dividing is equality and $1$-dividing is ordinary dividing.
• $O(x)$ is an abbreviation for $\forall y\, (xy = y)$. It means "$x = 1$".
• $P(x)$ is an abbreviation for $\lnot O(x)\land \forall y(y|x\rightarrow (O(y)\lor y = x))$. It means "$x$ is prime".
• $PP(x,y)$ is an abbreviation for $P(x)\land x|y\land \forall z((P(z)\land z\neq x\rightarrow \lnot (z|y))$. It means "$x$ is prime and $y$ is a power of $x$".
• $V(x,y,z)$ is an abbreviation for $PP(x,z)\land z|y \land \forall w((PP(x,w)\land w|y)\rightarrow w|z)$. It means "$z$ is the highest power of the prime $x$ which divides $y$".
• $T(x,y,z)$ is an abbreviation for $\forall p(P(p)\rightarrow ((p|x\rightarrow \exists w(V(p,y,w) \land V(p,z,w)))\land (\lnot p|x\rightarrow \lnot p|z)))$. It means "$z$ is the number obtained by deleting from the prime factorization of $y$ all primes not dividing $x$".
• $I(x,y)$ is an abbreviation for $\forall p(P(p)\rightarrow ((p|x\rightarrow \exists w(V(p,x,w)\land V(p,y,pw))\land (\lnot p|x\rightarrow \lnot p|y))$. It means "$y$ is the number obtained by increasing each prime exponent appearing in the prime factorization of $x$ by $1$".
• $S_n(p,x,y)$ is an abbreviation for $P(p)\land p|xy\land \exists z\exists w(V(p,x,z)\land V(p,y,w)\land z|_n w)$. It means "$p$ is a prime which divides $xy$, and the highest power of $p$ dividing $x$ $n$-divides the highest power of $p$ dividing $y$.
• For $n\geq 0$, $SP_n(x,y,z)$ is an abbreviation for $\forall p(P(p)\rightarrow ((S_n(p,x,y)\rightarrow V(p,z,p))\land (\lnot S_n(p,x,y)\rightarrow \lnot (p|z)))$. It means "$z$ is the product of those primes which divide $xy$ and for which the highest power of $p$ dividing $x$ $n$-divides the highest power of $p$ dividing $y$." You should think of this as a kind of comprehension/separation condition. If we think of an element as coding a (multi)set of primes (its prime factors), then $z$ codes the set of primes $p$ for which a certain modular arithmetic condition holds between the exponent of $p$ in the prime factorizations of $x$ and $y$.

Now we can give our axioms:

• $\forall x\forall y\forall z((xy)z = x(yz))$
• $\forall x\forall y(xy = yx)$
• $\exists x (O(x))$ [Note that uniqueness of $x$ follows from the previous axioms.]
• $\forall x\forall y\forall z(xz = yz\rightarrow x = y)$
• $\forall x\forall y(O(xy)\rightarrow (O(x)\lor O(y)))$
• $\forall x\forall y(x^n = y^n \rightarrow x = y)$ for each natural number $n>0$
• $\forall x\exists y\exists z(x = y^nz\land \forall y'\forall z'(x = (y')^nz'\rightarrow z|z'))$ for each natural number $n>0$
• $\forall x\exists p (P(p)\land \lnot p|x)$
• $\forall x\forall y\forall z((PP(x,y)\land PP(x,z))\rightarrow (y|z\lor z|y))$
• $\forall p\forall x(P(p)\rightarrow \exists y(V(p,x,y)))$ [Note that uniqueness of $y$ follows from the previous axioms.]
• $\forall x\forall y(x = y\leftrightarrow \forall p(P(p)\rightarrow \exists z(V(p,x,z)\land V(p,y,z))))$
• $\forall p\forall x\forall y(P(p)\rightarrow (\exists z\exists w (V(p,x,z)\land V(p,y,w)\land V(p,xy,zw))))$
• $\forall x\forall y(\forall p(P(p)\rightarrow \exists z\exists w(V(p,x,z)\land V(p,y,w)\land z|w))\rightarrow x|y)$
• $\forall x\forall y\exists z(T(x,y,z))$ [Note that uniqueness of $z$ follows from the previous axioms.]
• $\forall x\exists y(I(x,y))$ [Note that uniqueness of $y$ follows from the previous axioms.]
• $\forall x\forall y\exists z(SP_n(x,y,z))$ for each natural number $n\geq 0$ [Note that uniqueness of $z$ follows from the previous axioms.]

Further, this theory has quantifier elimination in the definable expansion $\{\cdot,1,t,i,(sp_n)_{n\geq0},(E_n)_{n>0}\}$ where $1$ is a constant symbol defined by $O$ above, $t$ is a binary function symbol defined by $T(x,y,z)$ above, $i$ is a unary function symbol defined by $I(x,y)$ above, $sp_n$ is a binary function symbol for each $n\geq 0$ defined by $SP_n(x,y,z)$ above, and $E_n(x)$ is a unary relation symbol for each $n>0$ defined by $$\exists p_1\dots\exists p_n(\bigwedge_{1\leq i < j \leq n} (p_i\neq p_j) \land \bigwedge_{1\leq i \leq n} (P(p_i)\land p_i|x)).$$

Disclaimer: I have not read Cegielski's proofs, only the summary of results in Smorynski. Some errors may have arisen in the "game of telephone" by which I summarized Smorynski's summary of Cegielski. But writing out the axiomatization here has given me some intuition for the kinds of complexities that arise in Skolem arithmetic - I hope it does the same for you!