Inmathematical logic,Skolem arithmetic is thefirst-order theory of thenatural numbers withmultiplication, named in honor ofThoralf Skolem. Thesignature of Skolem arithmetic contains only the multiplication operation and equality, omitting the addition operation entirely.

Skolem arithmetic is weaker thanPeano arithmetic, which includes both addition and multiplication operations.^[1] Unlike Peano arithmetic, Skolem arithmetic is adecidable theory. This means it is possible to effectively determine, for any sentence in the language of Skolem arithmetic, whether that sentence is provable from the axioms of Skolem arithmetic. The asymptotic running-timecomputational complexity of thisdecision problem is triply exponential.^[2]

We define the following abbreviations.

• a |b := ∃n.(an =b)
• One(e) := ∀n.(ne =n)
• Prime(p) := ¬One(p) ∧ ∀a.(a |p → (One(a) ∨a =p))
• PrimePower(p,P) := Prime(p) ∧p |P ∧ ∀q.(Prime(q) ∧ ¬(q =p) → ¬(q |P))
• InvAdicAbs(p,n,P) := PrimePower(p,P) ∧P |n ∧ ∀Q.((PrimePower(p,Q) ∧Q |n) →Q |P) [P is the largest power ofp dividingn]
• AdicAbsDiff_n(p,a,b) := Prime(p) ∧p |ab ∧ ∃P.∃Q.(InvAdicAbs(p,a,P) ∧ InvAdicAbs(p,b,Q) ∧Q =pⁿP) for each integern > 0. [The largest power ofp dividingb ispⁿ times the largest power ofp dividinga]

The axioms of Skolem arithmetic are:^[3]

1. ∀a.∀b.(ab =ba)
2. ∀a.∀b.∀c.((ab)c =a(bc))
3. ∃e.One(e)
4. ∀a.∀b.(One(ab) → One(a) ∨ One(b))
5. ∀a.∀b.∀c.(ac =bc →a =b)
6. ∀a.∀b.(aⁿ =bⁿ →a =b) for each integern > 0
7. ∀x.∃a.∃r.(x =arⁿ ∧ ∀b.∀s.(x =bsⁿ →a |b)) for each integern > 0
8. ∀a.∃p.(Prime(p) ∧ ¬(p |a)) [Infinitude of primes]
9. ∀p.∀P.∀Q.((PrimePower(p,P) ∧ PrimePower(p,Q)) → (P |Q ∨Q |P))
10. ∀p.∀n.(Prime(p) → ∃P.InvAdicAbs(p,n,P))
11. ∀n.∀m.(n =m ↔ ∀p.(Prime(p) → ∃P.(InvAdicAbs(p,n,P) ∧ InvAdicAbs(p,m,P)))) [Unique factorization]
12. ∀p.∀n.∀m.(Prime(p) → ∃P.∃Q.(InvAdicAbs(p,n,P) ∧ InvAdicAbs(p,m,Q) ∧ InvAdicAbs(p,nm,PQ))) [p-adic absolute value is multiplicative]
13. ∀a.∀b.(∀p.(Prime(p) → ∃P.∃Q.(InvAdicAbs(p,a,P) ∧ InvAdicAbs(p,b,Q) ∧P |Q)) →a |b) [If thep-adic valuation ofa is less than that ofb for every primep, thena |b]
14. ∀a.∀b.∃c.∀p(Prime(p) → (((p |a → ∃P.(InvAdicAbs(p,b,P) ∧ InvAdicAbs(p,c,P))) ∧ ((p |b) → (p |a)))) [Deleting from the prime factorization ofb all primes not dividinga]
15. ∀a.∃b.∀p.(Prime(p) → (∃P.(InvAdicAbs(p,a,P) ∧ InvAdicAbs(p,b,pP))) ∧ (p |b →p |a))) [Increasing each exponent in the prime factorization ofa by 1]
16. ∀a.∀b.∃c.∀p.(Prime(p) → ((AdicAbsDiff_n(p,a,b) → InvAdicAbs(p,c,p)) ∧ (p |c → AdicAbsDiff_n(p,a,b))) for each integern > 0 [Product of those primesp such that the largest power ofp dividingb ispⁿ times the largest power ofp dividinga]

First-order logic with equality and multiplication of positive integers can express the relation${\displaystyle c=a\cdot b}$. Using this relation and equality, we can define the following relations on positive integers:

• Divisibility:${\displaystyle b|c\iff \mathrm{\exists }a.c=a\cdot b}$
• Greatest common divisor:${\displaystyle d=gcd(a,b)\iff d|a\wedge d|b\wedge \mathrm{\forall }{d}^{\prime }.(d^{\prime }|a\wedge d^{\prime }|b)\Rightarrow d^{\prime }|d}$
• Least common multiple:${\displaystyle m=\mathrm{l}\mathrm{c}\mathrm{m}(a,b)\iff a|m\wedge b|m\wedge \mathrm{\forall }{m}^{\prime }.(a|m^{\prime }\wedge b|m^{\prime })\Rightarrow m|m^{\prime }}$
• the constant${\displaystyle 1}$:${\displaystyle \mathrm{\forall }a.1|a}$
• Prime number:${\displaystyle \mathrm{p}\mathrm{r}\mathrm{i}\mathrm{m}\mathrm{e}(p)\iff p\ne 1\wedge \mathrm{\forall }a.a|p\Rightarrow (a=1\vee a=p)}$
• Number${\displaystyle b}$ is a product of${\displaystyle k}$ primes (for a fixed${\displaystyle k}$):${\displaystyle \mathrm{\exists }{a}_1,...a_k.\mathrm{p}\mathrm{r}\mathrm{i}\mathrm{m}\mathrm{e}(a_1)\wedge \dots \wedge \mathrm{p}\mathrm{r}\mathrm{i}\mathrm{m}\mathrm{e}(a_k)\wedge b=a_1\cdot \dots \cdot a_k}$
• Number${\displaystyle b}$ is a power of some prime:${\displaystyle \mathrm{p}\mathrm{p}\mathrm{o}\mathrm{w}\mathrm{e}\mathrm{r}(b)\iff \mathrm{\exists }p.\mathrm{p}\mathrm{r}\mathrm{i}\mathrm{m}\mathrm{e}(p)\wedge \mathrm{\forall }a.(a\ne 1\wedge a|b)\Rightarrow p|a}$
• Number${\displaystyle b}$ is a product of exactly${\displaystyle k}$ prime powers:${\displaystyle \mathrm{\exists }{a}_1,...a_k.\mathrm{p}\mathrm{p}\mathrm{o}\mathrm{w}\mathrm{e}\mathrm{r}(a_1)\wedge \dots \wedge \mathrm{p}\mathrm{p}\mathrm{o}\mathrm{w}\mathrm{e}\mathrm{r}(a_k)\wedge b=a_1\cdot \dots \cdot a_k}$

The truth value of formulas of Skolem arithmetic can be reduced to the truth value of sequences of non-negative integers constituting their prime factor decomposition, with multiplication becoming point-wise addition of sequences. The decidability then follows from theFeferman–Vaught theorem that can be shown usingquantifier elimination. Another way of stating this is that first-order theory of positive integers is isomorphic to the first-order theory of finitemultisets of non-negative integers with the multiset sum operation, whose decidability reduces to the decidability of the theory of elements.

In more detail, according to thefundamental theorem of arithmetic, a positive integer${\displaystyle a>1}$ can be represented as a product of prime powers:

${\displaystyle a=p_1^{a_1}{p}_2^{a_2}\cdots }$

If a prime number${\displaystyle p_k}$ does not appear as a factor, we define its exponent${\displaystyle a_k}$ to be zero. Thus, only finitely many exponents are non-zero in the infinite sequence${\displaystyle a_1,a_2,\dots }$. Denote such sequences of non-negative integers by${\displaystyle N^{\ast }}$.

Now consider the decomposition of another positive number,

${\displaystyle b=p_1^{b_1}{p}_2^{b_2}\cdots }$

The multiplication${\displaystyle ab}$ corresponds point-wise addition of the exponents:

${\displaystyle ab=p_1^{a_1+b_1}{p}_2^{a_2+b_2}\cdots }$

Define the corresponding point-wise addition on sequences by:

${\displaystyle (a_1,a_2,\dots )\overline{+}(b_1,b_2,\dots )=(a_1+b_1,a_2+b_2,\dots )}$

Thus we have an isomorphism between the structure of positive integers with multiplication,${\displaystyle (N,\cdot )}$ and of point-wise addition of the sequences of non-negative integers in which only finitely many elements are non-zero,${\displaystyle (N^{\ast },\overline{+})}$.

FromFeferman–Vaught theorem forfirst-order logic, the truth value of a first-order logic formula over sequences and pointwise addition on them reduces, in an algorithmic way, to the truth value of formulas in the theory of elements of the sequence with addition, which, in this case, isPresburger arithmetic. Because Presburger arithmetic is decidable, Skolem arithmetic is also decidable.

Ferrante & Rackoff (1979, Chapter 5) establish, usingEhrenfeucht–Fraïssé games, a method to prove upper bounds on decision problem complexity of weak direct powers of theories. They apply this method to obtain triply exponential space complexity for${\displaystyle (N^{\ast },\overline{+})}$, and thus of Skolem arithmetic.

Grädel (1989, Section 5) proves that thesatisfiability problem for thequantifier-free fragment of Skolem arithmetic belongs to theNP complexity class.

Thanks to the above reduction using Feferman–Vaught theorem, we can obtain first-order theories whose open formulas define a larger set of relations if we strengthen the theory of multisets of prime factors. For example, consider the relation${\displaystyle a\sim b}$ that is true if and only if${\displaystyle a}$ and${\displaystyle b}$ have the equal number of distinct prime factors:

${\displaystyle |\{p\mid \mathrm{p}\mathrm{r}\mathrm{i}\mathrm{m}\mathrm{e}(p)\wedge (p|a)\}|=|\{p\mid \mathrm{p}\mathrm{r}\mathrm{i}\mathrm{m}\mathrm{e}(p)\wedge (p|b)\}|}$

For example,${\displaystyle 2^{10}\cdot 3^{100}\sim 5^8\cdot {19}^9}$ because both sides denote a number that has two distinct prime factors.

If we add the relation${\displaystyle \sim }$ to Skolem arithmetic, it remains decidable. This is because the theory of sets of indices remains decidable in the presence of theequinumerosity operator on sets, as shown by theFeferman–Vaught theorem.

An extension of Skolem arithmetic with the successor predicate,${\displaystyle succ(n)=n+1}$ can define the addition relation using Tarski's identity:^[4][5]

${\displaystyle (c=0\vee c=a+b)\iff (ac+1)(bc+1)=c^2(ab+1)+1}$

and defining the relation${\displaystyle c=a+b}$ on positive integers by

${\displaystyle \mathrm{s}\mathrm{u}\mathrm{c}\mathrm{c}(ac)\mathrm{s}\mathrm{u}\mathrm{c}\mathrm{c}(bc)=\mathrm{s}\mathrm{u}\mathrm{c}\mathrm{c}(c^2\mathrm{s}\mathrm{u}\mathrm{c}\mathrm{c}(ab))}$

Because it can express both multiplication and addition, the resulting theory is undecidable.

If we have an ordering predicate on natural numbers (less than,), we can express${\displaystyle \mathrm{s}\mathrm{u}\mathrm{c}\mathrm{c}}$ by

so the extension with is also undecidable.

• Presburger arithmetic
• Robinson arithmetic
• Quantifier elimination

• Formal theories of arithmetic

• Articles with short description
• Short description is different from Wikidata