In mathematical logic, Skolem arithmetic is the first-order theory of the natural numbers with multiplication, named in honor of Thoralf Skolem.
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-time computational complexity of this decision problem is triply exponential.
The axioms of Skolem arithmetic are:[3] First-order logic with equality and multiplication of positive integers can express the relation
Using this relation and equality, we can define the following relations on positive integers: 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 the Feferman–Vaught theorem that can be shown using quantifier elimination.
Another way of stating this is that first-order theory of positive integers is isomorphic to the first-order theory of finite multisets 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 the fundamental theorem of arithmetic, a positive integer
Thus, only finitely many exponents are non-zero in the infinite sequence
corresponds point-wise addition of the exponents: Define the corresponding point-wise addition on sequences by: Thus we have an isomorphism between the structure of positive integers with multiplication,
and of point-wise addition of the sequences of non-negative integers in which only finitely many elements are non-zero,
From Feferman–Vaught theorem for first-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, is Presburger arithmetic.
Ferrante & Rackoff (1979, Chapter 5) establish, using Ehrenfeucht–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
Grädel (1989, Section 5) proves that the satisfiability problem for the quantifier-free fragment of Skolem arithmetic belongs to the NP 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.
have the equal number of distinct prime factors: For example,
because both sides denote a number that has two distinct prime factors.
to Skolem arithmetic, it remains decidable.
This is because the theory of sets of indices remains decidable in the presence of the equinumerosity operator on sets, as shown by the Feferman–Vaught theorem.
An extension of Skolem arithmetic with the successor predicate,
on positive integers by Because it can express both multiplication and addition, the resulting theory is undecidable.