Order Logic..

Quantifier elimination is a powerful property that aids in proving decidability,and has numerous applications. In the late 1920s, Tarski led a seminar on logic problems at the University of Warsaw, focusing on developing a method of quantifier elimination. Tarski and his students achieved significant results. One of his students, Mojżesz Presburger, succeeded in developing quantifier elimination procedure for the theory of additive integer numbers (Presburger Arithmetic). The foundational basis for this study lies in the classical results of mathematical logic and computability theory, notably articulated in the comprehensive text by Boolos, Burgess, and Jeffrey [1]. Foundational algebraic concepts, especially those relevant to universal algebra and logical structures, are drawn from Burris and Sankappanavar’s seminal work [2]. The decidability and model-theoretic properties of Boolean algebras are supported by Poizat’s developments in model theory [3] and the axiomatizability of the natural lattice as presented by Cégielski [4]. The results regarding complete theories of Boolean algebras and quantifier elimination stem from Ortiz’s analysis [5], while logical formalism is further contextualized by Leary and Kristiansen [6]. Philosophical and historical perspectives on logic, as examined by Prawitz and Westerståhl [7], complement the syntactical treatment of formal languages discussed by Dutilh [8]. The general approach to logic formalization aligns with the structure of Enderton’s textbook [9]. In formulating a rigorous axiomatization of multiplicative and divisibility structures, this study draws from the algebraic framework introduced by Givant and Halmos [10] and is deeply informed by Salehi’s earlier work on axiomatizability of multiplicative theories [11, 12]. The logical number theoretic aspects, particularly related to the structures of ⟨Z; ×⟩ and ⟨Q; |⟩, are situated within the framework developed by Smorynski [13]. Finally, set-theoretic insights and their connections to logic, relevant especially in the context of structural decidability, are considered from the recent work of Habič et al. [14].

A theory or structure in language L admits quantifier elimination if every formula φ in L is equivalent to a quantifier-free formula ψ in L. In this study, we explore the structures of integers, and rational numbers under the divisibility relation. Skolem initially claimed decidability for Th(N; ×, =) by employing a quantifier elimination technique [1]. However, Mostowski provided the first proof of decidability, relying on the notion of the weak (direct) powers of a structure, which allowed the reduction of Th(N; ×) to Th(N; +). Cegielski later axiomatized Th(N; ×) [4], and in this paper, we provide an explicit axiomatization for Th(Z; ×). The main focus of this study is the exploration of the decidability and axiomatizability of certain first-order mathematical structures, particularly those involving integers, and rational numbers under the divisibility relation. This research extends existing results on Th(N; |) [5]to Th(Z; |) and investigates the theory of divisibility in rational numbers, ⟨Q; |⟩. This work aims to provide a clear and comprehensive axiomatization of ⟨Q; |⟩, while also contributing to a deeper understanding of divisibility theory in other first-order structures. The results are expected to offer new insights into decidability in mathematical logic, with potential applications. The significance of this research lies in its potential to advance knowledge on the axiomatizability and decidability of first-order structures. By presenting explicit axiomatizations, this study may foster further theoretical developments and practical applications in fields where these structures are fundamental.

The multiplicative theory of integers, denoted Th(Z; ×), explores the properties of the structure ⟨Z; ×⟩, where Z represents the set of all integers and × denotes multiplication. This theory is analogous to the study of the multiplicative theory of natural numbers, Th(N; ×), which concerns tht properties of set N under multiplication. The study of the multiplicative theory of integers, Th(Z; ×), is intriguing because of its complexity, reflecting the multiplicative theory of natural numbers, Th(N; ×), but with additional in-tricacies due to the inclusion of negative integers.The structure ⟨Z; ×⟩, is decidable and thus axiomatizable [12,14].

Definition 1. p-adic valuation: The p-adic valuation of u, denoted by V , is defined as follows: For example, if

n m 0

u = p1 p2 p3 · · ·

then

V (p2, u) = p2 .

Definition 2. A number p is considered prime, denoted by P(p), if and only if:

p ̸= 1 ∧ ∀u (u | p → (u = 1 ∨ u = p)).

Definition 3. A number x is called a p-primary number, denoted by P R(p, x), if and only if:

1 v(n,p)

If n = p , then we might not explicitly define v(n, p) in the theory. However, we may denote it as n = V (n, p),

v(n,p)

where V (n, p) = p . For small v, we have v(p, a, b) = v(p, a) + v(p, b), whereas for large V , we have V (p, a · b) = V (p, a) · V (p, b). P(p) ∧ ∀q ((P(q) ∧ q ̸= p) → q ∤ x).

Corollary 1. (Axiomatizability of Th(Z; ×)) The following theory completely axiomatizes the structure ⟨Z; ×⟩.

(1) Associativity:

∀u∀v∀w, (u · (v · w) = (u · v) · w).

This axiom states that multiplication is associative, which is a fundamental property of the multiplication operation in the integers.

(2) Existence of Multiplicative Identity:

∃u such that ∀v, (u · v = v · u = v).

This axiom asserts the existence of a multiplicative identity (which is 1 for integers) such that multiplying any integer by this identity leaves the integer unchanged.

(3) Commutativity:

∀u∀v, (u · v = v · u).

This axiom states that multiplication is commutative, meaning the order in which two integers are multiplied does not matter.

(4) Cancellation Law:

∀u∀v∀w ̸= 0, (u · w = v · w → u = v).

This axiom indicates that if the product of two pairs of integers with the same multiplier is equal, then the integers themselves must be equal, provided the multiplier is not zero.

(5) Uniqueness of Multiplicative Inverse:

∀u, v ̸= 0, (u · v = 1 → u = v = 1 ∨ u = v = −1).

This axiom states that the only integers with a multiplicative inverse (under integer multiplication) are 1 and −1. This axiom is more restrictive, asserting that only 1 and −1 have this property in the context of this axiomatization.

(6) Unique Roots:

n n ∗

∀u∀v, (u = v → u = v) (n ∈ N ).

This axiom ensures that if two integers raised to the same positive integer power are equal, then the integers themselves must be equal. This is crucial for capturing the behavior of integers under exponentiation.

(7) Division Algorithm:

∀u∀n ∈ N , ∃v∃w, (u = n · v + w ∧ w < n ∧ w ̸= n).

This axiom captures the division algorithm, which states that any integer can be expressed as a quotient and a remainder when divided by a positive integer.

(8) Unique Factorization:

∀u, ∃v∃w, (u = v · w ∧ ∀v ´∀w, ´ (u = ´ v · w ´ → w | w ´)).

This axiom asserts that each integer can be factored uniquely into powers of integers and that these factors are unique up to multiplication by units.

(9) Existence of Prime Numbers:

∀u, ∃p, (P(p) ∧ p ∤ u).

This axiom ensures the existence of prime numbers and that for any integer, there exists a prime that does not divide it.

(10) Prime Divisibility:

∀p∀u∀v, ((P(p, u) ∧ P(p, v)) → u | v ∨ v | u).

This axiom states that if a prime number divides two integers, then one of those integers must divide the other.

(11) Prime Factorization:

∀u∀p, (P(p) → ∃v, (u = V (p, v))).

This axiom asserts the unique factorization of integers into prime factors.

(12) Equality of Prime Factor Representations:

u = v ↔ ∀p, (P(p) → ∃v, (V (p, u) = V (p, v))).

This axiom states that two integers are equal if and only if their prime factorizations are identical.

(13) Multiplication of Prime Factor Representations:

∀u∀v∀p, (P(p) → V (p, u · v) = V (p, u) · V (p, v)).

This axiom ensures that the prime factor representation of a product is the product of the prime factor representations.

(14) Divisibility in Terms of Prime Factors:

∀u∀v, (∀p, (P(p) → V (p, u) | V (p, v)) → u | v) .

This axiom relates the divisibility of integers to the divisibility of their prime factors.

(15) Existence of Prime Factors for Multiples:

∀u∀v, ∃w, ∀p, (P(p) → (p | u → V (p, w) = V (p, v)) ∧ (p ∤ u → V (p, w) = 1)) .

This axiom ensures the existence of a suitable integer w given u and v such that certain conditions involving prime factors are met.

(16) Prime Factor Behavior for Non-divisors:

∀u ∃v ∀p (P(p) → (p ∤ u → V (p, v) = 1) ∧ (p | u → V (p, v) = p · V (p, u))) .

This axiom describes the behavior of prime factors for integers that are not divisible by a given prime.

(17) Behavior of Prime Factors for Products:

∀u∀v ∃w ∀p (P(p) → (p | u · v ∧ V (p, u) ≡n V (p, v)) → V (p, w) = p) ∧

∧ (p ∤ u · v ∨ V (p, u) ̸≡n V (p, v) → V (p, w) = 1) , (n ∈ N).

This axiom ensures that every integer has an additive inverse, capturing the structure of integers under addition and subtraction.

In this section, we focus on axiomatizing the divisibility theory of integers and demonstrating its decidability. The divisibility relation, denoted as u | v, is the standard notation where u divides v, defined as:

u | v ↔ ∃w ∈ Z, ; u · w = v.

We recommend using this symbol consistently throughout our discussion. The structure ⟨Z , |⟩ is decidable and axiomatizable, where Z denotes the positive integers. The theory of divisibility in Z can be defined in terms of divisibility in N, specifically:

′ ′ ′ ′

z = −z ⇐⇒ z ̸= z and z | z and z | z.

Now, we proceed to axiomatize the divisibility theory of integers [2,12]. The following axioms completely axiomatizes the structure ⟨Z; |⟩:

• [D1]∀u (u | u): Every integer divides itself.

• [D2]∀u, v (u | v ∧ v | u → u = v): If an integer u divides v and v divides u, then u and v are equal.

• [D3]∀u, v, w (u | v ∧ v | w → u | w): If u divides v and v divides w, then u divides w.

• [D4]∀u, v ∃z (z | u, v ∧ ∀t (t | u, v → t | z) ; z = u ⊓ v): For any integers u and v, there exists an integer z (denoted as u ⊓ v) that is a common divisor of u and v, and any common divisor of u and v divides z.

• [D5]∀u, v ∃w (u, v | w ∧ ∀t (u, v | t → w | t) ; w = u ⊔ v): For any integers u and v, there exists an integer w (denoted as u ⊔ v) that is a common multiple of u and v, and w divides any common multiple of u and v.

• [D6]∀u (1 | u): 1 divides every integer.

• [D7]∀u, v [∀w (SI(w) → [w | u → w | v]) → u | v]: If for all strongly irreducible elements w, w divides u implies w divides v, then u divides v.

∗ ∗ ∗

• [D8]∀u, v, w (SI (u) ∧ SI (v) ∧ SI (w) ∧ [(u, v | w) ∨ (w | u, v)] → u | v ∨ v | u): If u, v, and w are strongly irreducible, and either u and v together divide w or w divides both u and v, then either u divides v or v divides u.

• [D9]∀u, a ([SI (a)∧a | u] → ∃b (SI(b)∧a | b | u∧ ∀c (SI(c)∧c | u, a) → c | b)): If a is strongly irreducible and divides u, then there exists a b such that a divides b, b divides u, and any strongly irreducible c that divides both u and a also divides b.

• [D10]∀u (u ̸= 0 → ∃a (P(a) ∧ a | u)): For any non-zero u, there exists a prime a that divides u.

• [D11]∀u (u ̸= 0 → ∃a (P(a) ∧ a ∤ u)): For any non-zero u, there exists a prime a that does not divide u.

• [D12]∀u ∃s ∀a (P(a) → [(V (a, u) ̸= 0 → V (a, s) ̸= a) ∧ (V (a, u) = 0 → V (a, s) = 0)]), where s = SUPP(u): For any u, there exists s (denoted as SUPP(u)) such that for any prime a, if V (a, u) ̸= 0, then V (a, s) ̸= a, and if V (a, u) = 0, then V (a, s) = 0.

• [D ]∀u, v ∃w ∀a (P(a) → [(a ∤ u → V (a, w) = V (a, v)) ∧ (a | u → V (a, w) = 0)]), where w = T ¯ (u, v):

For any u and v, there exists w (denoted as T ¯(u, v)) such that for any prime a, if a does not divide u, then V (a, w) = V (a, v), and if a divides u, then V (a, w) = 0.

• [D14]∀a, u (SI(a, u) → ∃v (SI(a, v) ∧ u | v ∧ v = ̸ u ∧ ∀w ((SI(a, w) ∧ u | w) → w | v))), where v = Sa(u):

If a and u are strongly irreducible, then there exists v (denoted as Sa(u)) such that u divides v, v is not equal to u, and any w that is strongly irreducible with a and u, and u divides w, then w divides v.

• [D15 ]∀a, u (SI(a, u) ∧ u = 0 ̸ → ∃v (SI(a, v) ∧ Sa(v) = u)): If a and u are strongly irreducible and u = 0 ̸ , then there exists v such that v is strongly irreducible with a and Sa(v) = u.

• [D15 ]∀u ∃v ∀a (P(a) → [(a ∤ u → V (a, v) = 0) ∧ (a | u → V (a, v) = SaV (a, u))]), where v = I(u): For any u, there exists v (denoted as I(u)) such that for any prime a, if a does not divide u, then V (a, v) = 0, and if a divides u, then V (a, v) = SaV (a, u).

• [D16]∀u, v ∃w ∀a (P(a) → [V (a, w) = 0 ∨ (a | w ∧ V (a, w) = a ↔ (a | u ∨ a | v) ∧ V (a, u) | V (a, v))]): For any u and v, there exists w such that for any prime a, V (a, w) = 0 or a divides w and V (a, w) = a if and only if a divides u or a divides v, and V (a, u) divides V (a, v).

This section focuses on atomless Boolean algebra. Boolean algebra was first introduced by Boole in 1854, but it was Alfred Tarski who established the decidability of the theory of Boolean algebra. The following formulas are in this section focusing on atomless Boolean algebra.

Lemma 1. Let L = ⟨0, 1, ∧, ∨, ¬⟩ be the language of Boolean algebras. The equivalence

(1) ∃u (ru = 0 ∧ su ¯ = 0 ∧ aiu ̸= 0 ∧ bju ¯ ̸= 0)

i=1 j=1

holds with

(2) (rs = 0 ∧ ∃v ( airv ¯ ̸= 0 ∧ bjs ¯v ¯ ̸= 0).

i=1 j=1

Proof : For the proof from (1) to (2): Assume there exists u such that

ru = 0 ∧ su = 0 ∧ aiu ̸= 0 ∧ bju ¯ ̸= 0.

i=1 j=1

Then, we have:

ru = 0 ∧ rsu ¯ = 0 ⇒ rs(u + ¯ u) = 0 ⇒ rs(1) = 0 ⇒ rs = 0.

And, aix ̸= 0 ⇒ aix(r + ¯ r) ̸= 0 ⇒ aiur + aiur ¯ ̸= 0 ⇒ aiur ¯ ̸= 0, which is equivalent to the following formula:

⇒ ∃u( airu ¯ ̸= 0 ∧ bjs ¯u ¯ ̸= 0).

i=1 j=1

For the other direction, let rs = 0. There exists v such that

airv ¯ ̸= 0 ∧ bjs ¯v ¯ ̸= 0.

i=1 j=1

Let us put u = ¯ r(s + v), u ¯ = r + ¯ sv ¯ = (r + ¯ s)(r + ¯ v) = ¯ s(r + ¯ v).

Then, aiu = air ¯(s + v) = airs ¯ + airv ¯ ⊇ airv ¯ ̸= 0, bju ¯ = bjs ¯(r + ¯ v) = bjsr ¯ + bjs ¯v ¯ ⊇ bjs ¯v ¯ ̸= 0.

In this way, we establish the following equivalence:

aiu ̸= 0 ∧ bju ¯ ̸= 0,

i=1 j=1

which implies the desired conclusion. □

Corollary 2. The theory of atomless Boolean algebras in the language L = {0, 1, ∧, ∨, ¬, =} admits quantifier elimination and is therefore decidable.

• [B1] u ∧ v = v ∧ u, u ∨ v = v ∨ u.

• [B2] u ∧ (v ∧ w) = (u ∧ v) ∧ w, u ∨ (v ∨ w) = (u ∨ v) ∨ w.

• [B3] (u ∧ v) ∨ v = v, (u ∨ v) ∧ v = v.

• [B4] u ∧ (v ∨ w) = (u ∧ v) ∨ (u ∧ w), u ∨ (v ∧ w) = (u ∨ v) ∧ (u ∨ w).

• [B5] u ∧ u = 0, u ∨ u = 1.

• [B6] ¬At(u)(At(u) is u ̸= 0 ∧ ¬∃v(v ̸= 0 ∧ u ∧ v = v)) ⇒ 0 ̸= 1.

Proof : By using B1, B2, B3, B4, B5, each term on x is equal to x · r + x · s. Thus, every atomic formula involving x is equal to x · r + x · s = 0. As a consequence, by using quantifier elimination (Lemma 4.4), it is sufficient to eliminate quantifiers of the following formulas:

∃x(rx = 0 ∧ sx ¯ = 0 ∧ uix ̸= 0 ∧ vjx ¯ ̸= 0). (1)

i=1 j=1

Thus, by Lemma (4.4) we show

≡ rs = 0 ∧ ∃y( uiry ¯ ̸= 0 ∧ vjs ¯y ¯ ̸= 0). (2)

i=1 j=1

It suffices to eliminate the quantifier of the formula:

∃y( aiy ̸= 0 ∧ bjy ¯ ̸= 0). (3)

i=1 j=1

This is equivalent to the following formula:

≡ ai ̸= 0 ∧ bj ̸= 0, (4)

i=1 j=1

which implies the desired conclusion.

We prove the theory of atomless Boolean algebra admits quantifier elimination. As for atomless Boolean algebras, its decidability follows from the decidability of the entire principle of Boolean algebras (TBA) demonstrated via Tarski and Ershov. It follows from the fact that any sentence A is true on all atomless Boolean algebras if and only if the theory of Boolean algebras proves the sentence “all elements are atomless" ⇒ A. □

The rational numbers Q can be seen as an extension of the integers Z by including ratios of integers. The theory of the structure ⟨Q ; |⟩ is decidable. The divisibility relation (but for 0 divides z, which is true if and only if z = 0); the theory ⟨Q ; |⟩ is hence interdefinable with the theory of an infinite set T h(Q; 0) in the language that just contains = and one constant 0. The axiomatization of the elementary T h(Q; |) such that (u|v is the standard notation for "u divides v"):

(1) ∃u (∀v(v|u) ∧ ∀v(v ̸= u → ∀w(w|v ↔ w ̸= u))) .

(2) ∃v0, ..., vn (1 ≤ n).

Here, axiom 1 asserts that there exists zero (an element with the desired divisibility properties), and axiom 2 asserts the existence of infinitely many distinct elements. It is trivial to show that (1). This list of axioms gives a countably categorical theory, and (2). All the axioms hold in (Q; |). Hence, it is indeed an axiomatization of T h(Q; |).

The T h(Q; |) such that p | q ↔ ∃m ∈ N (p · m = q) is axiomatizable. This structure falls under the category of algebraic structures.

D1 ∀u (u | u).

Every element divides itself.

D2 ∀u, v (u | v ∧ v | u → u = v).

If two elements divide each other, they are equal.

D3 ∀u, v, w (u | v ∧ v | w → u | w).

Divisibility is transitive.

D4 ∀u, v ∃z (z | u, v ∧ ∀t [t | u, v → t | z]), z = u ⊓ v.

There exists a greatest common divisor for any two elements.

D5 ∀u, v ∃w (u, v | w ∧ ∀t [u, v | t → w | t]), w = u ⊔ v.

There exists a least common multiple for any two elements.

D6 ∀u (1 | u).

The element 1 divides every element.

D7 ∀u, v [∀w (SI(w) → [w | u → w | v]) → u | v].

If for all simple elements w, w divides u implies w divides v, then u divides v.

∗ ∗ ∗

D8 ∀u, v, w (SI (u) ∧ SI (v) ∧ SI (w) ∧ [(u, v | w) ∨ (w | u, v)] → u | v ∨ v | u).

For any three simple elements, if they pairwise divide or are divided by a third element, then one divides the other.

D9 ∀u, a ([SI (a) ∧ a | u] → ∃b SI(b) ∧ a | b | u ∧ ∀c (SI(c) ∧ c | u, a) → c | b).

For any u and simple element a dividing u, there exists a simple element b such that a | b | u and any simple element c dividing both u and a divides b.

D10 ∀u (u ̸= 0 → ∃a (P(a) ∧ a | u)).

Every nonzero element has a prime divisor.

D11 ∀u (u ̸= 0 → ∃a (P(a) ∧ a ̸| u)).

Every nonzero element has a prime that does not divide it.

D12 ∀u ∃s ∀a (P(a) → (V (a, u) ̸= 0 → V (a, s) ̸= a) ∧ (V (a, u) = 0 → V (a, s) = 0))).

For every element u, there exists a unique element s, denoted SUPP(u), such that for every prime a, V (a, u) ̸= 0 implies V (a, s) ̸= a and V (a, u) = 0 implies V (a, s) = 0.

D13 ∀u, v ∃w ∀a (P(a) → ((a ̸| u → V (a, w) = V (a, v)) ∧ (a | u → V (a, w) = 0))).

For every u and v, there exists a unique w, denoted T ¯ (u, v), such that for every prime a, a ̸| u implies V (a, w) = V (a, v) and a | u implies V (a, w) = 0.

D14 ∀a, u (SI(a, u) → ∃v (SI(a, v) ∧ u | v ∧ v ̸= u ∧ ∀w (SI(a, w) ∧ u | w) → v | w))).

For any simple element a and any element u such that SI(a, u), there exists a unique element v, denoted Sa(u), such that SI(a, v), u | v, v ̸= u, and for all w, SI(a, w) ∧ u | w implies v | w.

D15 ∀a, u (SI(a, u) ∧ u ̸= 0) → ∃v (SI(a, v) ∧ Sa(v) = u).

For any simple element a and any nonzero element u such that SI(a, u), there exists a unique element v, denoted Pa(u), such that SI(a, v) and Sa(v) = u.

D15 ∀u ∃v ∀a (P(a) → ((a ̸| u → V (a, v) = 0) ∧ (a | u → V (a, v) = SaV (a, u)))).

For every element u, there exists a unique element v, denoted I(u), such that for every prime a, a ̸| u implies V (a, v) = 0 and a | u implies V (a, v) = SaV (a, u).

D16 ∀u ∀v ∃w ∀a (P(a) → (V (a, w) = 0 ∨ a ∧ V (a, w) = a ↔ (a | u ∨ a | v) ∧ V (a, u) | V (a, v))).

For every u and v, there exists a unique w such that for every prime a, V (a, w) = 0 or a and V (a, w) = a if and only if (a | u ∨ a | v) and V (a, u) | V (a, v).

D17 ∀u ∀v ∃w ∀a (P(a) → (V (a, w) = 0 ∨ a ∧ V (a, w) = a ↔ (a | u ∨ a | v) ∧ V (a, u) | V (a, v))).

For every u and v, there exists a unique w such that for every prime a, V (a, w) = 0 or a and V (a, w) = a if and only if (a | u ∨ a | v) and V (a, u) | V (a, v).

D18 u ⊓ v = v ⊓ u u ⊔ v = v ⊔ u.

The operations ⊓ and ⊔ are commutative.

u ⊓ (v ⊓ w) = (u ⊓ v) ⊓ w u ⊔ (v ⊔ w) = (u ⊔ v) ⊔ w.

The operations ⊓ and ⊔ are associative.

(u ⊓ v) ⊔ v = v (u ⊔ v) ⊓ v = v.

The operations ⊓ and ⊔ are idempotent.

u ⊓ (u ⊔ v) = u u ⊔ (u ⊓ v) = u.

Absorption laws for ⊓ and ⊔.

u ⊓ (v ⊔ w) = (u ⊓ v) ⊔ (u ⊓ w) u ⊔ (v ⊓ w) = (u ⊔ v) ⊓ (u ⊔ w.)

Distributive laws for ⊓ and ⊔.

u ⊓ u = 1 u ⊔ u = u

−1 −1

This axiom states that each element u has an inverse u such that u ⊓ u = 1 (where 1 is the identity element for ⊓) and u ⊔ u = u (where u remains unchanged under ⊔).

¬P(a)

This axiom states that a specific predicate P(a) is not true for element a.

∀u, v, w (u · (v · w) = (u · v) · w)

This is the associativity of multiplication. It states that the way in which elements are grouped in multiplication does not affect the result.

2n 2n

∀u, v (0 < u < v → ∃w (u < w < v ), n ≥ 1.)

This axiom ensures that for any u and v such that 0 < u < v, there exists an element w between u and v for some n ≥ 1. This is related to the density of elements in the structure.

n mk

∀ξ1, . . . , ξl ∃u ∀w (u · ξk ̸= w )

This axiom states that for any set of elements ξ1, . . . , ξl, there exists an element u such that for all

n mk

elements w, the products u · ξk are not equal to w for any k = 1, . . . , l. This relates to the existence of certain elements with specific properties in the structure.

Consider the theory of the rational numbers (Q ; |), where | denotes divisibility:

p | q ↔ ∃m(p · m = q) 5 7 5 7 7 For example, divides by the definition above (since × = ). The structure (Q ; |), where | is the 3 3 3 5 3 divisibility relation, is decidable. Notably, we have:

p | q ↔ ∃m(p · m = q) in Q (rational numbers) is equivalent to:

p = 0 → q = 0, Thus, all formulations in the language | can be translated into the same formulations of the language of the signature, which includes a single constant 0. Quantifier elimination for this language is known, and 0 = 0. It follows that:

T h(Q ; |) is decidable. However, p | q ↔ ∃m ∈ N (p · m = q) is not equivalent to p | q ↔ ∃m(p · m = q). Therefore, decidability for the theory of rational numbers (Q ; |), where:

p | q ↔ ∃m ∈ N (p · m = q) is false.

We now present a proof that the divisibility theory of rational numbers (Q; |) is decidable.

Proposition 1. The theory of rational numbers (Q; |), where divisibility is defined as p | q ⇔ ∃m(p · m = q), is decidable.

Proof : Let φ be any formula in the divisibility theory of rational numbers, we perform the following:

(1) We express φ in terms of prime factor decompositions of the rational numbers involved. Since every rational number has a unique factorization, the divisibility relations can be reduced to checking conditions on these factorizations.

(2) Apply quantifier elimination as outlined in the algorithm. This ensures that any existential quantifier (representing the existence of a divisor) is removed, leading to an equivalent quantifier-free formula.

(3) By known results from model theory, the quantifier-free fragment of the theory of (Q; |) is decidable.

Thus, for any input formula φ, we can determine whether φ is true or false in (Q; |).

Therefore, the theory of (Q; |) is decidable, as any formula can be reduced to a quantifier-free form which can be algorithmically checked for truth. □

In this paper, we provided explicit axiomatizations for the structures ⟨Z; |⟩, ⟨Z; ×⟩, and ⟨Q; |⟩, showing the intricate relationship between decidability, axiomatizability, and quantifier elimination. The results extend previous work on the divisibility theory of integers and rational numbers, contributing to the broader understanding of first-order structures in mathematical logic.

This study lays the groundwork for future investigations. In particular, we intend to explore the axiomatizability and decidability of structures arising in fractal geometry. Such work aims to understand whether logical frameworks developed for algebraic structures can be extended to more complex and self-similar mathematical systems.

The authors would like to express their sincere gratitude to the editors and anonymous reviewers for their invaluable comments and constructive feedback, which significantly contributed to the enhancement of this paper. In particular, we are deeply thankful to Dr. Davron Aslonqulovich Juraev for his insightful guidance and editorial support throughout the development of this work.