In
mathematical logic
Mathematical logic is the study of logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of for ...
, Skolem arithmetic is the
first-order theory
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantif ...
of the
natural number
In mathematics, the natural numbers are those numbers used for counting (as in "there are ''six'' coins on the table") and ordering (as in "this is the ''third'' largest city in the country").
Numbers used for counting are called ''Cardinal n ...
s with
multiplication
Multiplication (often denoted by the cross symbol , by the mid-line dot operator , by juxtaposition, or, on computers, by an asterisk ) is one of the four elementary mathematical operations of arithmetic, with the other ones being additi ...
, named in honor of
Thoralf Skolem
Thoralf Albert Skolem (; 23 May 1887 – 23 March 1963) was a Norwegian mathematician who worked in mathematical logic and set theory.
Life
Although Skolem's father was a primary school teacher, most of his extended family were farmers. Skolem ...
. The
signature
A signature (; from la, signare, "to sign") is a handwritten (and often stylized) depiction of someone's name, nickname, or even a simple "X" or other mark that a person writes on documents as a proof of identity and intent. The writer of a ...
of Skolem arithmetic contains only the multiplication operation and equality, omitting the addition operation entirely.
Skolem arithmetic is weaker than
Peano arithmetic
In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearly u ...
, 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
In computer science, the computational complexity or simply complexity of an algorithm is the amount of resources required to run it. Particular focus is given to computation time (generally measured by the number of needed elementary operations) ...
of this
decision problem
In computability theory and computational complexity theory, a decision problem is a computational problem that can be posed as a yes–no question of the input values. An example of a decision problem is deciding by means of an algorithm whethe ...
is triply exponential.
Expressive power
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:
* Divisibility:
*
Greatest common divisor
In mathematics, the greatest common divisor (GCD) of two or more integers, which are not all zero, is the largest positive integer that divides each of the integers. For two integers ''x'', ''y'', the greatest common divisor of ''x'' and ''y'' is ...
:
*
Least common multiple
In arithmetic and number theory, the least common multiple, lowest common multiple, or smallest common multiple of two integers ''a'' and ''b'', usually denoted by lcm(''a'', ''b''), is the smallest positive integer that is divisible by bot ...
:
* the constant
:
*
Prime number
A prime number (or a prime) is a natural number greater than 1 that is not a product of two smaller natural numbers. A natural number greater than 1 that is not prime is called a composite number. For example, 5 is prime because the only ways ...
:
* Number
is a product of
primes (for a fixed
):
* Number
is a power of some prime:
* Number
is a product of exactly
prime powers:
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
Feferman–Vaught theorem in model theory is a theorem by Solomon Feferman and Robert Lawson Vaught that shows how to reduce, in an algorithmic way, the first-order theory of a product of first-order structures to the first-order theory of elemen ...
that can be shown using
Quantifier elimination Quantifier elimination is a concept of simplification used in mathematical logic, model theory, and theoretical computer science. Informally, a quantified statement "\exists x such that \ldots" can be viewed as a question "When is there an x such t ...
. Another way of stating this is that first-order theory of positive integers is isomorphic to the first-order theory of finite
multiset
In mathematics, a multiset (or bag, or mset) is a modification of the concept of a set that, unlike a set, allows for multiple instances for each of its elements. The number of instances given for each element is called the multiplicity of that e ...
s 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
In mathematics, the fundamental theorem of arithmetic, also called the unique factorization theorem and prime factorization theorem, states that every integer greater than 1 can be represented uniquely as a product of prime numbers, up to the ord ...
, a positive integer
can be represented as a product of prime powers:
:
If a prime number
does not appear as a factor, we define its exponent
to be zero. Thus, only finitely many exponents are non-zero in the infinite sequence
. Denote such sequences of non-negative integers by
.
Now consider the decomposition of another positive number,
:
The multiplication
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
Feferman–Vaught theorem in model theory is a theorem by Solomon Feferman and Robert Lawson Vaught that shows how to reduce, in an algorithmic way, the first-order theory of a product of first-order structures to the first-order theory of elemen ...
for
first-order logic
First-order logic—also known as predicate logic, quantificational logic, and first-order predicate calculus—is a collection of formal systems used in mathematics, philosophy, linguistics, and computer science. First-order logic uses quantifie ...
, 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
Presburger arithmetic is the first-order theory of the natural numbers with addition, named in honor of Mojżesz Presburger, who introduced it in 1929. The signature of Presburger arithmetic contains only the addition operation and equality, omitti ...
. Because Presburger arithmetic is decidable, Skolem arithmetic is also decidable.
Complexity
establish, using
Ehrenfeucht–Fraïssé game In the mathematical discipline of model theory, the Ehrenfeucht–Fraïssé game (also called back-and-forth games)
is a technique based on game semantics for determining whether two structures
are elementarily equivalent. The main application of E ...
s, 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
, and thus of Skolem arithmetic.
proves that the
satisfiability
In mathematical logic, a formula is ''satisfiable'' if it is true under some assignment of values to its variables. For example, the formula x+3=y is satisfiable because it is true when x=3 and y=6, while the formula x+1=x is not satisfiable over ...
problem for the ''quantifier-free'' fragment of Skolem arithmetic belongs to the
NP complexity class.
Decidable Extensions
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
that is true if and only if
and
have the equal number of distinct prime factors:
:
For example,
because both sides denote a number that has two distinct prime factors.
If we add the relation
to Skolem arithmetic, it remains decidable. This is because the theory of sets of indices remains decidable in the presence of the
equinumerosity
In mathematics, two sets or classes ''A'' and ''B'' are equinumerous if there exists a one-to-one correspondence (or bijection) between them, that is, if there exists a function from ''A'' to ''B'' such that for every element ''y'' of ''B'', ther ...
operator on sets, as shown by the
Feferman–Vaught theorem
Feferman–Vaught theorem in model theory is a theorem by Solomon Feferman and Robert Lawson Vaught that shows how to reduce, in an algorithmic way, the first-order theory of a product of first-order structures to the first-order theory of elemen ...
.
Undecidable extensions
An extension of Skolem arithmetic with the successor predicate,
can define the addition relation using Tarski's identity:
:
and defining the relation
on positive integers by
:
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
by
:
so the extension with
is also undecidable.
See also
*
Presburger arithmetic
Presburger arithmetic is the first-order theory of the natural numbers with addition, named in honor of Mojżesz Presburger, who introduced it in 1929. The signature of Presburger arithmetic contains only the addition operation and equality, omitti ...
*
Robinson arithmetic
In mathematics, Robinson arithmetic is a finitely axiomatized fragment of first-order Peano arithmetic (PA), first set out by R. M. Robinson in 1950. It is usually denoted Q. Q is almost PA without the axiom schema of mathematical induction. Q is ...
*
Quantifier elimination Quantifier elimination is a concept of simplification used in mathematical logic, model theory, and theoretical computer science. Informally, a quantified statement "\exists x such that \ldots" can be viewed as a question "When is there an x such t ...
References
Bibliography
*
*
*
*
*
*
{{Refend
Formal theories of arithmetic