In mathematical logic, Skolem arithmetic is the first-order theory of the natural numbers with multiplication, named in honor of Thoralf Skolem. The signature of Skolem arithmetic contains only the multiplication operation and equality, omitting the addition operation entirely.

Skolem arithmetic is weaker than Peano arithmetic, which includes both addition and multiplication operations. Unlike Peano arithmetic, Skolem arithmetic is a decidable 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-time computational complexity of this decision problem is triply exponential.

Axioms

We define the following abbreviations.

In plain English:

• holds if and only if exactly.

  holds if and only if the p-adic valuation.

The axioms of Skolem arithmetic are:

Expressive power

. Using this relation and equality, we can define the following relations on positive integers:

• Greatest common divisor

• Least common multiple

• Prime number

Idea of decidability

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 can be represented as a product of prime powers:

.

Now consider the decomposition of another positive number,

corresponds point-wise addition of the exponents:

Define the corresponding point-wise addition on sequences by:

.

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. Because Presburger arithmetic is decidable, Skolem arithmetic is also decidable.

Complexity

establish, using Ehrenfeucht–Fraïssé games, and thus of Skolem arithmetic.

proves that the satisfiability problem for the quantifier-free fragment of Skolem arithmetic belongs to the NP complexity class.

Decidable extensions

have the equal number of distinct prime factors:

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.

Undecidable extensions

can define the addition relation using Tarski's identity:

on positive integers by

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

by

is also undecidable.

See also

• Presburger arithmetic

• Robinson arithmetic

• Quantifier elimination

Notes and references

Bibliography