In mathematical logic, Skolem arithmetic is the firstorder 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.^{[1]} 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 runningtime computational complexity of this decision problem is triply exponential.^{[2]}
YouTube Encyclopedic

1/5Views:1 5772 3935 5348971 185

Math 557 – The LöwenheimSkolem Theorems

Skolemization using Skolem Function

Example of Skolemization

Skolemization using Skolem Constant

Mathematical Logic, part 3: Löwenheim–Skolem theorem
Transcription
Axioms
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 of p dividing n]
 AdicAbsDiff_{n}(p, a, b) := Prime(p) ∧ p  ab ∧ ∃P.∃Q.(InvAdicAbs(p, a, P) ∧ InvAdicAbs(p, b, Q) ∧ Q = p^{n}P) for each integer n > 0. [The largest power of p dividing b is p^{n} times the largest power of p dividing a]
The axioms of Skolem arithmetic are:^{[3]}
 ∀a.∀b.(ab = ba)
 ∀a.∀b.∀c.((ab)c = a(bc))
 ∃e.One(e)
 ∀a.∀b.(One(ab) → One(a) ∨ One(b))
 ∀a.∀b.∀c.(ac = bc → a = b)
 ∀a.∀b.∀n.(a^{n} = b^{n} → a = b) for each integer n > 0
 ∀x.∃a.∃r.(x = ar^{n} ∧ ∀b.∀s.(x = bs^{n} → a  b)) for each integer n > 0
 ∀a.∃p.(Prime(p) ∧ ¬(p  a)) [Infinitude of primes]
 ∀p.∀P.∀Q.((PrimePower(p, P) ∧ PrimePower(p, Q)) → (P  Q ∨ Q  P))
 ∀p.∀n.(Prime(p) → ∃P.InvAdicAbs(p,n,P))
 ∀n.∀m.(n = m ↔ ∀p.(Prime(p) → ∃P.(InvAdicAbs(p, n, P) ∧ InvAdicAbs(p, m, P)))) [Unique factorization]
 ∀p.∀n.∀m.(Prime(p) → ∃P.∃Q.(InvAdicAbs(p, n, P) ∧ InvAdicAbs(p, m, Q) ∧ InvAdicAbs(p, nm, PQ))) [padic absolute value is multiplicative]
 ∀a.∀b.(∀p.(Prime(p) → ∃P.∃Q.(InvAdicAbs(p, a, P) ∧ InvAdicAbs(p, b, Q) ∧ P  Q)) → a  b) [If the padic valuation of a is less than that of b for every prime p, then a  b]
 ∀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 of b all primes not dividing a]
 ∀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 of a by 1]
 ∀a.∀b.∃c.∀p.(Prime(p) → ((AdicAbsDiff_{n}(p, a, b) → InvAdicAbs(p, c, p)) ∧ (p  c → AdicAbsDiff_{n}(p, a, b))) for each integer n > 0 [Product of those primes p such that the largest power of p dividing b is p^{n} times the largest power of p dividing a]
Expressive power
Firstorder 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:
 Least common multiple:
 the constant :
 Prime number:
 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 nonnegative integers constituting their prime factor decomposition, with multiplication becoming pointwise 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 firstorder theory of positive integers is isomorphic to the firstorder theory of finite multisets of nonnegative 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 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 nonzero in the infinite sequence . Denote such sequences of nonnegative integers by .
Now consider the decomposition of another positive number,
The multiplication corresponds pointwise addition of the exponents:
Define the corresponding pointwise addition on sequences by:
Thus we have an isomorphism between the structure of positive integers with multiplication, and of pointwise addition of the sequences of nonnegative integers in which only finitely many elements are nonzero, .
From Feferman–Vaught theorem for firstorder logic, the truth value of a firstorder 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
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 , and thus of Skolem arithmetic.
Grädel (1989, Section 5) proves that the satisfiability problem for the quantifierfree fragment of Skolem arithmetic belongs to the NP complexity class.
Decidable extensions
Thanks to the above reduction using Feferman–Vaught theorem, we can obtain firstorder 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 operator on sets, as shown by the Feferman–Vaught theorem.
Undecidable extensions
An extension of Skolem arithmetic with the successor predicate, can define the addition relation using Tarski's identity:^{[4]}^{[5]}
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
References
 ^ Nadel 1981.
 ^ Ferrante & Rackoff 1979, p. 135.
 ^ Cegielski 1981.
 ^ Robinson 1949, p. 100.
 ^ Bès & Richard 1998.
Bibliography
 Bès, Alexis (2001). "A Survey of Arithmetical Definability" (PDF). In Crabbé, Marcel; Point, Françoise; Michaux, Christian (eds.). A Tribute to Maurice Boffa. Brussels: Societé mathématique de Belgique. pp. 1–54.
 Bès, Alexis; Richard, Denis (1998). "Undecidable Extensions of Skolem Arithmetic". Journal of Symbolic Logic. 63 (2): 379–401. CiteSeerX 10.1.1.2.1139. doi:10.2307/2586837. JSTOR 2586837. S2CID 14566619.
 Cegielski, Patrick (1981), "Théorie élémentaire de la multiplication des entiers naturels", in Berline, Chantal; McAloon, Kenneth; Ressayre, JeanPierre (eds.), Model Theory and Arithmetic, Berlin: Springer, pp. 44–89.
 Ferrante, Jeanne; Rackoff, Charles W. (1979). The Computational Complexity of Logical Theories. Berlin Heidelberg New York: SpringerVerlag. doi:10.1007/BFb0062837. ISBN 3540095012.
 Grädel, Erich (June 1989). "Dominoes and the complexity of subclasses of logical theories". Annals of Pure and Applied Logic. 43 (1): 1–30. doi:10.1016/01680072(89)900237.
 Nadel, Mark E. (1981). "The completeness of Peano multiplication". Israel Journal of Mathematics. 39 (3): 225–233. doi:10.1007/bf02760851. Retrieved 20220908.
 Robinson, Julia Hall Bowman (1949). "Definability and Decision Problems in Arithmetic" (PDF). Journal of Symbolic Logic. 14 (2): 98–114. doi:10.2307/2266510. JSTOR 2266510. S2CID 40861592. Retrieved 20220905.