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.^[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 running-time computational complexity of this decision problem is triply exponential.^[2]

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)
• AdicAbsDiff_n(p, a, b) := Prime(p) ∧ p | ab ∧ ∃P.∃Q.(InvAdicAbs(p, a, P) ∧ InvAdicAbs(p, b, Q) ∧ Q = pⁿP) for each integer n > 0.

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.∀n.(aⁿ = bⁿ → a = b) for each integer n > 0
7. ∀x.∃a.∃r.(x = arⁿ ∧ ∀b.∀s.(x = bsⁿ → a | b)) for each integer n > 0
8. ∀a.∃p.(Prime(p) ∧ ¬(p | a))
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))))
12. ∀p.∀n.∀m.(Prime(p) → ∃P.∃Q.(InvAdicAbs(p, n, P) ∧ InvAdicAbs(p, m, Q) ∧ InvAdicAbs(p, nm, PQ)))
13. ∀a.∀b.(∀p.(Prime(p) → ∃P.∃Q.(InvAdicAbs(p, a, P) ∧ InvAdicAbs(p, b, Q) ∧ P | Q)) → a | b)
14. ∀a.∀b.∃c.∀p(Prime(p) → (((p | a → ∃P.(InvAdicAbs(p, b, P) ∧ InvAdicAbs(p, c, P))) ∧ ((p | b) → (p | a))))
15. ∀a.∃b.∀p.(Prime(p) → (∃P.(InvAdicAbs(p, a, P) ∧ InvAdicAbs(p, b, pP))) ∧ (p | b → p | a)))
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 integer n > 0

Expressive power

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\ \Leftrightarrow \ \exists a.c=a\cdot b}$
• Greatest common divisor: ${\displaystyle d=\gcd(a,b)\ \Leftrightarrow \ d|a\land d|b\land \forall d'.(d'|a\land d'|b)\Rightarrow d'|d}$
• Least common multiple: ${\displaystyle m=\mathrm {lcm} (a,b)\ \Leftrightarrow \ a|m\land b|m\land \forall m'.(a|m'\land b|m')\Rightarrow m|m'}$
• the constant ${\displaystyle 1}$: ${\displaystyle \forall a.1|a}$
• Prime number: ${\displaystyle \mathrm {prime} (p)\ \Leftrightarrow \ p\neq 1\land \forall a.a|p\Rightarrow (a=1\lor a=p)}$
• Number ${\displaystyle b}$ is a product of ${\displaystyle k}$ primes (for a fixed ${\displaystyle k}$): ${\displaystyle \exists a_{1},...a_{k}.\ \mathrm {prime} (a_{1})\land \ldots \land \mathrm {prime} (a_{k})\land b=a_{1}\cdot \ldots \cdot a_{k}}$
• Number ${\displaystyle b}$ is a power of some prime: ${\displaystyle \mathrm {ppower} (b)\ \Leftrightarrow \ \exists p.\mathrm {prime} (p)\land \forall a.(a\neq 1\land a|b)\Rightarrow p|a}$
• Number ${\displaystyle b}$ is a product of exactly ${\displaystyle k}$ prime powers: ${\displaystyle \exists a_{1},...a_{k}.\ \mathrm {ppower} (a_{1})\land \ldots \land \mathrm {ppower} (a_{k})\land b=a_{1}\cdot \ldots \cdot a_{k}}$

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, 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},\ldots }$. Denote such sequences of non-negative integers by ${\displaystyle N^{*}}$.

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_{}}}$Zdroj:https://en.wikipedia.org?pojem=Skolem_arithmetic
Text je dostupný za podmienok Creative Commons Attribution/Share-Alike License 3.0 Unported; prípadne za ďalších podmienok. Podrobnejšie informácie nájdete na stránke Podmienky použitia.

---