Georgian Mathematical Journal 1(1994), No. 5, 561-565

COMPLEXITY OF THE DECIDABILITY OF THE UNQUANTIFIED SET THEORY WITH A RANK OPERATOR

M. TETRUASHVILI

Abstract. The unquantified set theory MLSR containing the symbols ∪, \, =, ∈, R (R(x) is interpreted as a rank of x) is considered. It is proved that there exists an algorithm which for any formula Q of the MLSR theory decides whether Q is true or not using the space c|Q|^{3} (|Q| is the length of Q).

Let MLSR be an unquantified set theory whose language contains the symbols ∪, \, =, ∈, R, where R denotes a unary functional symbol and R(x) is interpreted as a rank of the set x in the sense of J.von Neumann. The decidability problem for the theory MLSR reduces readily to testing the satisfiability of conjunctions of literals of the following types:

(=) x = y ∪ z, x = y \ z, (∈) x ∈ y, (R) x = R(y)

(the literal x ∉ y is equivalent to the formula x ∈ z & z = z\y, while the literal x ≠ y to the formula [u ∈ x & u ∉ y] ∨ [u ∈ y & u ∉ x], where z, u are new variables). The conjunction Q of literals is sometimes treated as a set of its literals.

Let, further, MLS be an unquantified set theory whose language contains the symbols ∪, \, =, ∈.

Definition 1. The interpretation α of the MLS language is called the singleton model of a formula φ of this language if it associates a subset of the {∅} with each variable and φ is true in α.

Definition 2. The singleton model α of a set of all literals of the type (=) of the formula Q of the language of MLSR theory is called the place of the conjunction Q.

If α is the place of Q and y is the variable occurring in Q, then y(α) is the value of y in α.

561

1991 Mathematics Subject Classification. 03D15.

1072-947X/1994/0900-0561$07.00/0 \begin{matrix}c \\ ◯ \end{matrix} 1994 Plenum Publishing Corporation

Definition 3. Let y be the variable occurring in Q. The place α of the formula Q is called the place at y if

y(α) = \begin{cases}1, & when x ∈ y occurs in Q, \\ 0, & when x ∉ y occurs in Q. \end{cases}

D. Cantone et al. the following result have given in [1]:

Theorem 1. Let Q be the conjunction of literals of the types (=, ∈, R) and y_{1}, …, y_{m} be its pairwise-distinct variables occurring in Q. Then Q is satisfiable iff there exist

(i) a set Π = {α_{1}, …, α_{n}} of pairwise-distinct places of Q;

(ii) a function F : {1, …, m} → {1, …, n};

(iii) a set W ⊆ {1, …, m};

(iv) a sequence of integers 0 = r_{0} < r_{1} < ⋯ < r_{k} = n such that the following conditions are fulfilled:

(a) α_{F (i)} is the place at y_{i} for all i ∈ {1, …, m};

(b) If y_{i}∼_{Π}y_{j} (i.e., ∀α ∈ Π(y_{i}(α) = y_{j}(α))), then F (i) = F (j) (i, j ∈

{1, …, m});

(c) If y_{i}(α_{j}) = 1, then k_{j} < k_{F (i)} (i ∈ {1, …, m}, j ∈ {1, …, n}), where for every j ∈ {1, …, n} k_{j} denotes the number r_{s} such that r_{s−1} < j ≤ r_{s};

(d) If y_{j} = R(y_{i}) is a literal of Q, then j ∈ W;

(e) If y_{j} = R(y_{i}) is a literal of Q, then k_{i^{∗}} = k_{j^{∗}}, where h^{∗} = max{l : y_{h}(α_{l}) = 1}, h ∈ {1, …, m};

(f) ∀i ∈ W ∀j ∈ W (y_{i} ∼_{Π} y_{j} ⇒ y_{i}ˆ∈y_{j} ∨ y_{j} ˆ∈y_{i}), where y_{i}ˆ∈y_{j} denotes

y_{j}(α_{F (i)}) = 1;

(g) ∀i ∈ W ∀j ∈ W (y_{i}ˆ∈y_{j} ⇒ y_{i} ˆ⊆y_{j}), where y_{i} ˆ⊆y_{j} denotes ∀α ∈ Π (y_{i}(α) = 1 ⇒ y_{j}(α) = 1);

(h) If for i, j ∈ W there exists h ∈ {1, …, n} such that y_{i}(α_{h}) = 0 and y_{j}(α_{h}) = 1, then ∀r ∈ {1, …, n}(y_{i}(α_{r}) = 1 ⇒ k_{r} < k_{h}).

The proof of the necessity of this theorem makes essential use of the Venn diagram [2]. The construction of the set Π is based on the Venn diagram for m sets. Consequently the number n of places is, in general, of order 2^{m}. Therefore, despite the fact that Theorem 1 solves the decidability problem for the MLSR theory, the corresponding decision procedure has an exponential computational complexity (by space). Thus is of great interest to find an algorithm solving the decidability problem for the MLSR theory with a polynomial computational complexity (by space). The next theorem shows that such an algorithm can really be constructed.

Theorem 2. Let the conjunction Q of literals of the types (=, ∈, R) is satisfiable and y_{1}, …, y_{m} be all pairwise-distinct variables of Q. Then there exist:

(i) a set Π̄ = {β_{1}, …, βn̄} of pairwise-distinct places Q;

(ii) a function F̄ : {1, …, m} → {1, …, n̄};

(iii) a set W ⊆ {1, …, m};

(iv) a sequence 0 = r̄_{0} < r̄_{1} < ⋯ < r̄k̄ = n̄ of natural numbers such that all the conditions (a)–(h) of Theorem 1 are fulfilled and n̄ ≤ c|Q|^{2}, where |Q| is the length of Q.

Proof. Let Q be satisfiable. By virtue of Theorem 1 there exists: a set Π = {α_{1}, …, α_{n}}, a function F : {1, …, m} → {1, …, n}, a set W and a sequence r_{0}, r_{1}, …, r_{k}, satisfying the conditions (a)–(h) of this theorem.

Denote by Π^{F} a set {α_{F (i)} : i = 1, …, m} of places of Q. Π^{F} ⊆ Π. Let < i_{1}, j_{1} >, …, < i_{τ} , j_{τ} > be pairs of numbers from {1, …, m} such that i_{ν} < j_{ν} and F (i_{ν}) ≠ F (j_{ν}), ν = 1, …, τ. Then by the condition (b) of Theorem 1 y_{i_{ν}} ∼_{Π} y_{j_{ν}}, ν = 1, …, τ. Therefore for each pair < i_{ν}, j_{ν} >, ν = 1, …, τ, there exists a place α_{l_{ν}} ∈ Π with the lowest index l_{ν} such that y_{i_{ν}} (α_{l_{ν}}) ≠ y_{j_{ν}} (α_{l_{ν}}). Denote Π̃ = {α_{l_{ν}} : ν = 1, …, τ}. It is clear that τ ≤ m(m − 1)/2.

For each variable y_{i} of Q assume that α_{μ_{i}} is a place from Π with the highest index such that y_{i}(α_{μ_{i}}) = 1 (if such a place exists in Π). Denote by Π^{R} a set of all such places. Let Π_{0} = Π^{F} ∪ Π̃ ∪ Π^{R}. It is clear that card(Π_{0}) ≤ (m^{2} + m)/2.

Finally, denote by Π^{Δ} a set of places from the set Π which do not belong to the set Π_{0} but whose indices are the ends of intervals (r_{s−1}, r_{s}] containing the indices of places from the Π_{0}. Let Π̄ = Π_{0} ∪ Π^{Δ}. It is obvious that card(Π^{Δ}) ≤ card(Π_{0}) and therefore card(Π̄) ≤ m^{2} + m. Let n̄ = card(Π̄).

Let us now construct a new sequence of integers 0 = r̄_{0} < r̄_{1} < ⋯ < r̄k̄ = n̄. Identify each place with its index i. From the set Π̄ remove the integers which are not the indices of places from the set {1, …, n} and enumerate the elements of the set Π̄, preserving their order by the natural numbers 1, 2, …, n̄. Clearly, in this case all numbers r_{i} from the set Π̄ ⊆ Π will acquire the corresponding values from the set {1, …, n̄} which will form a new sequence 0 = r̄_{0} < r̄_{1} < ⋯ < r̄k̄ = n̄ of natural numbers.

Finally define the function F̄ : {1, …, m} → {1, …, n̄} as follows: F̄(i) is the natural number from [1, n̄] into which the number F (i) turns during the new enumeration of elements of the set Π̄ (F (i) is the index of a place from Π̄).

Let us check that the set Π̄ = {β_{1}, …, βn̄} of places of Q, the function F̄, the set W and the sequence 0 = r̄_{0} < r̄_{1} < ⋯ < r̄k̄ = n̄ satisfy all the conditions (a)–(h) of Theorem 1:

(a) β_{F̄(i)} is a place at y_{i}, i = 1, …, m, since β_{F̄(i)} = α_{F (i)};

(b) If y_{i}∼_{Π̄}y_{j}, then on account of Π̃ ⊆ Π_{0} ⊆ Π̄, we shall also have y_{i}∼_{Π}y_{j}.

But in that case F (i) = F (j). Therefore F̄(i) = F̄(j);

(c) Let y_{i}(β_{j}) = 1, i.e., y_{i}(α_{j′}) = 1, where j = 1, …, n. Then j and F (i) belong to different intervals (r_{s_{1}−1}, r_{s_{1}}] and (r_{s_{2}−1}, r_{s_{2}}], respectively, the first interval preceding the second one, and, since α_{F (i)} ∈ Π̄ and α_{j′} = β_{j} ∈ Π̄, the ends of both intervals belong to the set of indices of places from Π̄. But their order in the set {1, …, n} has remained unchanged during the new enumeration of elements of the set Π̄, the numbers j and F̄(i) belong to different new intervals corresponding to the sequence r̄_{0}, r̄_{1}, …, r̄k̄. Therefore k_{j} < k_{F̄(i)}, i ∈ {1, …, m}, j ∈ {1, …, n};

(d) It is obvious;

(e) Let y_{j} = R(y_{i}) be a literal of the conjunction Q. Then by Theorem 1 i^{∗} and j^{∗} belong to the same interval (r_{s−1}, r_{s}], s ≤ n. But Π^{R} ⊆ Π_{0} ⊆ Π and the intervals were not subdivided during the transformation. Therefore, after the new enumeration the equality k_{i^{∗}} = k_{j^{∗}} has also remained unchanged for the set Π̄;

(f) Let y_{i} ∼_{Π̄} y_{j}, i.e., ∃β ∈ Π̄[y_{i}(β) ≠ y_{j}(β)]. Since Π̄ ⊆ Π, we have

∃α ∈ Π[y_{i}(α) ≠ y_{j}(α)], i.e. y_{i} ∼_{Π} y_{j}. For example, y_{i}ˆ∈y_{j} is true by virtue of

Theorem 1 (the case when y_{j} ˆ∈y_{i} is true is considered in a similar manner), i.e. y_{j}(α_{F (i)}) = 1. But α_{F (i)} ∈ Π^{F} ⊆ Π̄ and α_{F (i)} = β_{F̄(i)}. Therefore y_{i}ˆ∈y_{j} is true in Π̄;

(g) Let y_{i}ˆ∈y_{j} hold in Π̄, i.e. y_{j}(β_{F̄(i)}) = 1. But β_{F̄(i)} = α_{F (i)}, i.e. y_{j}(α_{F (i)}) = 1. Therefore y_{i}ˆ∈y_{j} is true in Π. Then y_{i} ˆ⊆y_{j} is true in Π by virtue of Theorem 1, i.e. ∀α ∈ Π(y_{i}(α) = 1 ⇒ y_{j}(α) = 1). Since Π̄ ⊆ Π, the more so ∀α ∈ Π̄(y_{i}(α) = 1 ⇒ y_{j}(α) = 1), i.e., y_{i} ˆ⊆y_{j} is true in Π̄;

(h) Let i, j ∈ W and there exists h̄ ∈ {1, …, n̄} such that y_{i}(βh̄) = 0 and y_{j}(βh̄) = 1. But βh̄ = α_{h} for some h ∈ {1, …, n}, i.e. y_{i}(α_{h}) = 0, and by Theorem 1 ∀r ∈ {1, …, n}(y_{i}(α_{r}) = 1 ⇒ k_{r} < k_{h}). Let r̄ ∈ {1, …, n̄}. Then βr̄ = α_{r} for some r ∈ {1, …, n}. Therefore if y_{i}(βr̄) = 1, then y_{i}(α_{r}) = 1. Consequently, k_{r} < k_{h}, i.e. α_{r}, α_{h} ∈ Π̄, and r and h belong to different intervals (r_{s_{1}−1}, r_{s_{1}}] and (r_{s_{2}−1}, r_{s_{2}}], the first interval preceding the second one. The ends of these intervals were not removed from the set {1, …, n}. Therefore the inequality kr̄ < kh̄ has preserved. ■

Corrolary 1. There exists a Turing machine which for any formula Q of the MLSR theory decides whether Q is true or not, using the space c|Q|^{3}.

Let MLSO_{n} be an unquantified set theory whose language contains the symbols ∪, \, =, ∈ and a single-place predicate O_{n} (O_{n}(x) is interpreted as follows: x is an ordinal). Since O_{n}(x) iff x = R(x), we have

Corrolary 2. There exists a Turing machine which for any formula Q of the MLSO_{n} theory decides whether Q is true or not, using the space c|Q|^{3}.

References

1. D. Cantone et al., Decision procedures for elementary sublanguages of set theory IV. Comm. Pure and Appl. Math. 40(1987), 37–77.

2. A. Kuzichev, Venn diagram. (Russian) Nauka, Moscow, 1968.

(Received 04.05.1993)

Author’s address: I. Vekua Institute of Applied Mathematics of Tbilisi State University 2, University St., Tbilisi 380043 Republic of Georgia