=Paper=
{{Paper
|id=Vol-2756/paper5
|storemode=property
|title=From Hilbert's 10th Problem to slim, Undecidable Fragments of Set Theory
|pdfUrl=https://ceur-ws.org/Vol-2756/paper_5.pdf
|volume=Vol-2756
|authors=Domenico Cantone,Eugenio Omodeo,Mattia Panettiere
|dblpUrl=https://dblp.org/rec/conf/ictcs/CantoneOP20
}}
==From Hilbert's 10th Problem to slim, Undecidable Fragments of Set Theory
==
https://ceur-ws.org/Vol-2756/paper_5.pdf
From Hilbert’s 10th Problem to slim,
Undecidable Fragments of Set Theory?
Domenico Cantone[0000−0002−1306−1166]1 ,
Eugenio G. Omodeo[0000−0003−3917−1942]2 , and Mattia Panettiere1
1
Dept. of Mathematics and Computer Science, University of Catania, Italy
domenico.cantone@unict.it, mattia.panettiere@gmail.com
2
Dept. of Mathematics and Earth Sciences, University of Trieste, Italy
eomodeo@units.it
Abstract. We revisit, deepen, and make more systematic, the study—
undertaken ca. 1990—of reductions of Hilbert’s tenth problem to frag-
ments of set theory, whereby sublanguages of the Zermelo-Fraenkel ax-
iomatic theory are shown to have an undecidable satisfiability problem.
Key words: Hilbert’s 10th problem; Undecidability; ZF set theory; Sat-
isfiability problem; Cartesian product; (∀∃)0 formulas; Proof-checkers.
Introduction
We show that the satisfiability problems for various fragments of ZF—the
Zermelo-Fraenkel first-order set theory with regularity axiom—are undecidable.
To wit, if Φ is among those sublanguages of ZF, no algorithm can establish
whether or not any given formula ψ in Φ becomes true under suitable assign-
ments of sets to its free variables.
For each Φ taken into account, the undecidability result stems from a uniform
translation method which turns every instance D = 0 (with D ∈ Z[x1 , . . . , xm ])
of Hilbert’s 10th problem into a formula ψ of Φ so that ψ is satisfiable if and only
if the polynomial equation D(x1 , . . . , xm ) = 0 has natural solutions. Through
this translation, the algorithmic unsolvability of Hilbert’s 10th problem carries
over to the satisfiability problem for Φ.
Some of the undecidable Φ’s are slight extensions of a core language consist-
ing of all conjunctions of literals of the forms x = y ∪ z, x = y ⊗ z, x ∩ y = ∅, and
|x| = |y|, where x, y, z stand for variables, y ⊗ z is a variant of Cartesian prod-
uct consisting of singletons and unordered doubletons, and |x| = |y| designates
equinumerosity between x and y. Additional conjuncts entering into play can be,
e.g.: one literal of the form Finite(x), stating that x has finitely many elements,
?
Copyright c 2020 for this paper by its authors. Use permitted under Creative Com-
mons License Attribution 4.0 International (CC BY 4.0). We gratefully acknowledge
partial support from project “STORAGE—Università degli Studi di Catania, Piano
della Ricerca 2020/2022, Linea di intervento 2”, and from INdAM-GNCS 2019 and
2020 research funds.
2 D. Cantone, E.G. Omodeo, M. Panettiere
taken along with one literal of the form x 6= ∅. Another option would be to
extend the said syntactic core by allowing three negated equinumerosity literals
of the form |x| 6= |y| to appear in the conjunction. Our interest in these, and
similar, slim undecidable set-theoretic languages is increased by the fact that
they lie extremely close to fragments of ZF which are either known [3, Sec.11.1],
or conjectured [4, p. 239], to be decidable.
One can recast the undecidable fragments of ZF under study in a set-theoretic
language entirely devoid of function symbols (such as ∪, ⊗, etc.), which only in-
volves the relators ∈ and =, propositional connectives, and also the constructs
∀ x ∈ y ϕ and ∃ x ∈ y ϕ involving bounded quantifiers, subject to a very re-
strained use. The fact that somewhat sophisticated notions like “being an or-
dinal”, “being the first limit ordinal ω”, “having a finite cardinality”, “being a
hereditarily finite set”, can be specified inside this collection of formulas, dubbed
(∀∃)0 formulas, gives evidence of the high expressive power of bounded quantifi-
cation in the context of ZF.
In a full-fledged language for set theory, (∀∃)0 specifications are only seldom
used in order to define mathematical notions. Hence, to support the correct-
ness of the proposed (∀∃)0 -specifications of ω, equinumerosity, and finitude, we
have proved that they are equivalent to more direct and practical characteriza-
tions of the same notions. As we document at the http://aetnanova.units.
it/scenarios/SetTheoreticH10/, this formal accomplishment was carried out
with the aid of a proof-checker embodying a computational version of ZF.
1 From Hilbert’s 10th problem to unsolvable satisfiability
problems in set theory
1.1 How to flatten instances of Hilbert’s 10th problem
Consider a polynomial Diophantine equation
D(x1 , . . . , xm ) = 0
to be solved in N. By pulling out subterms of the polynomial D, we can flatten
this equation into a system (viz., a conjunction) of equations of the forms
x=y+z, x=y·z, x=1, x=y,
where x, y, z stand for variables, to be regarded—the new ones as well as the
original ones, x1 , . . . , xm —as unknowns in N (cf. [10,1]). We can then eliminate
each equation of the form x = y by rewriting it as x = y + ζ, where ζ is forced
to assume the value 0 (see equations (5) below).
The flattening process can easily enforce that x, y, z are distinct variables
when they appear together in the same equation x = y ? z (with ? ∈ {‘+’, ‘·’});
moreover, we will keep a sole equation, o = 1, involving 1. The equi-solvability
between the system ∆ so obtained and the original equation will be obvious.
From Hilbert’s 10th problem to undecidable fragments of set theory 3
Example 1. The equation (from [8, p. 4])
4 x31 x2 − 2 x21 x33 − 3 x22 x1 + 5 x3 = 0 (1)
can be flattened into the following system ∆1 consisting of 26 equations in 28
unknowns, 3 of which are x1 , x2 , x3 , namely the original unknowns of (1):
ζ = ζ1 + ζ2 , ζ1 = ζ2 + ζ , ζ2 = ζ + ζ1 ,
o=1, u2 = u1 + o , u4 = u3 + o ,
u1 = o + ζ , u3 = u2 + o , u5 = u4 + o ,
Px11 = x1 + ζ , Px21 = Px11 · x1 , Px31 = Px21 · x1 ,
Px12 = x2 + ζ , Px22 = Px12 · x2 ,
Px13 = x3 + ζ , Px23 = Px13 · x3 , Px33 = Px23 · x3 ,
M11 = u4 · Px31 , M1 = M11 · x2 , M4 = u5 · x3 ,
M21 = u2 · Px21 , M2 = M21 · Px33 , L = M1 + M4 ,
M31 = u3 · Px22 , M3 = M31 · x1 , L = M2 + M3 .
By then replacing the equation o = 1 in ∆1 by the constraints o 6= ζ and
o = o · o0 , o0 = o + ζ , (2)
(which are equisatisfiable with o = o2 & o 6= ζ ), we get a system ∆ which is
equisolvable—in N—with the initial equation (1) and consists of: 28 equations
in 29 unknowns, of the forms
x=y+z, x=y·z, (3)
(where all compound terms y ? z involve distinct variables) and one inequality
o 6= ζ . (4)
a
Definition 1. Systems that consist of flat equations of the forms (3) conjoined
with the equations
ζ = ζ1 + ζ2 , ζ1 = ζ2 + ζ , ζ2 = ζ + ζ1 (5)
and (2) and with the inequality (4), and inside which all terms of type y + z and
y · z involve distinct variables, are named canonical Diophantine systems.
Remark 1. One can also express multiplication in terms of the squaring oper-
ation (see [6, p. 230]). Notice, in fact, that any equation of the form x = y · z
is equisolvable in N with the flattened system of equations
p = y + z , x0 = x + ζ ,
q = p2 , f = y2 , g = z2 ,
0
k =x+x , h=f +g, q =k+h,
4 D. Cantone, E.G. Omodeo, M. Panettiere
as can be seen from the identity
q k h
z }| { z }| { z }| {
( y + z )2 = y · z + y · z + y 2 + |{z}
z2 .
| {z } |{z} |{z} |{z}
g
a
p x x0 f
From a canonical Diophantine systems ∆, we will next get a conjunction ∆
b
of set-theoretic constraints of the forms:
= ∪ union (ternary relation)
= × Cartesian product (ternary relation)
∩ = ∅ disjointness (dyadic relation)
| | = | | equinumerosity (dyadic relation)
Finite( ) finitude (property)
={ } singleton formation (dyadic relation)
6= ∅ non-emptyness (property)
| | 6= | | non-equinumerosity (dyadic relation)
Here, in light of the replaceability of multiplication by the squaring operation (as
pointed out in Remark 1), we might only employ Cartesian square y ×y, without
ever resorting to the product y × z with y distinct from z.
1.2 How to translate a canonical Diophantine system ∆ into
unquantified fragments of set theory
Let ∆ be a Diophantine canonical system.
We translate each conjunct of ∆ according to the following rules:
x=y+z uy,z = y ∪ z & y ∩ z = ∅ & | uy,z | = | x | ,
x=y·z wy,z = y × z & | wy,z | = | x | ,
o 6= ζ o 6= ∅ ,
where each uy,z and each wy,z is a new variable. By also adding, for each variable
u in ∆, the conjunct Finite(u) (meaning that | u | ∈ N), we obtain the set-theoretic
counterpart ∆ b of ∆.
Next we prove that the canonical system ∆ is satisfiable in N if and only if
its set-theoretic counterpart ∆b is satisfiable in the universe of all sets. In view
of the unsolvability of Hilbert’s Tenth problem (see [8, Chapter 5]), we readily
obtain the algorithmic unsolvability of the satisfiability problem for set-theoretic
conjunctions of positive literals of the forms
x=y∪z, x=y×z, x∩y =∅, |x| = |y| , Finite(x) ,
plus a single inequality of the form x 6= ∅ .
From Hilbert’s 10th problem to undecidable fragments of set theory 5
To carry out the first half of the proof, we observe that any set-assignment
v 7→ M v over the variables of ∆ b that satisfies ∆
b induces naturally the corre-
sponding N-assignment
v 7→ |M v| (6)
over the variables of ∆, and it is a simple matter to check that (6) satisfies ∆.
For instance, if x = y + z is in ∆, then the following conjuncts are in ∆
b
uy,z = y ∪ z , y∩z = ∅, | uy,z | = | x | ,
Finite(x) , Finite(y) , Finite(z) .
Hence, we have:
M uy,z = M y ∪ M z , My ∩ Mz = ∅ , | M uy,z | = | M x | ,
| Mx | ∈ N , | My | ∈ N , | Mz | ∈ N ,
so that
| M x | = | M uy,z | = | M y ∪ M z | = | M y | + | M z | ,
proving that the N-assignment (6) satisfies the equation x = y + z .
Similarly, one can show that the N-assignment (6) also satisfies all equations
of the form x = y · z in ∆ as well as the inequality o 6= 0.
For the converse proof, we will make use of the following notation, for every
k ∈ N and A ⊆ N:
[k] := {1, 2, . . . , k} and k + A := {k + a : a ∈ A} .
Suppose that v 7→ v is a solution to ∆ in N, and let v1 , v2 , . . . , v` be the
distinct variables in ∆, in any fixed order. We define a set-assignment over the
variables in ∆b by putting:
Pj−1
– M vj := kj + [vv j ], for j = 1, . . . , `, where kj := r=1 v r (so that k1 = 0);
y,z :=
– Mu M y ∪ M z , for every literal x = y + z in ∆ ;
– M wy,z := M y × M z , for every literal x = y · z in ∆ .
We prove that the set-assignment M so defined over the variables of ∆
b satisfies
all of the conjuncts of ∆ .
b
– Let x = y + z be in ∆. By the definition of M , we have
M uy,z = M y ∪ M z ,
so that M satisfies the conjunct uy,z = y ∪ z.
Let y and z be the variables vi and vj , respectively, where without loss of
generality we are assuming i < j. Also, let x be the variable vh . Preliminarily,
we show that
M vi ∩ M vj = ∅ . (7)
6 D. Cantone, E.G. Omodeo, M. Panettiere
If ∅ ∈ {M vi , M vj }, then (7) plainly holds. Otherwise, recalling that
M vi := ki + [vv i ] and M vj := kj + [vv j ] ,
we get
i−1
X i
X j−1
X
max M vi = ki + v i = vr + vi = vr 6 v r < min M vj ,
r=1 r=1 r=1
whence (7) follows in this case too. From (7), it follows that
| M uy,z | = | M y ∪ M z | = | M y | + | M z | = | M vi | + | M vj |
= v i + v j = v h = | M vh | = | M x | ,
proving that the set-assignment M satisfies the conjunct | M uy,z | = | M x |.
– It is even easier to prove that M satisfies also the literals in ∆
b of the forms
wy,z = y × z , | wy,z | = | x | ,
resulting from the translation of equations of the form x = y · z, and the
only literal of the form x 6= ∅ in ∆
b.
– To end, for each variable u in ∆, the assignment M also satisfies Finite(u) .
We have thus obtained that the set-assignment M satisfies the conjunction
b and hence conclude that the translation ∆ 7→ ∆
∆, b is satisfiability-preserving,
namely:
Theorem 1. A canonical Diophantine system ∆ is solvable in N if and only if
the corresponding conjunction ∆
b is satisfied by some set-assignment.
Consequently, from the undecidability of Hilbert’s tenth problem we get:
Lemma 1. The satisfiability problem for set-theoretic conjunctions of any num-
ber of positive literals of the forms
x=y∪z, x=y×z, x∩y =∅, |x| = |y| (‡)
and of the form Finite(x), plus one negative literal of the form x 6= ∅ , is algo-
rithmically unsolvable.
V
Since finitude is ⊆-hereditary, any conjunction i∈I Finite(xi ) of finitude
constraints canV be replaced, without affecting satisfiability, by the conjunction
Finite(F ) & i∈I F = F ∪ x i containing a single finitude constraint, where F
is a newly introduced variable. The preceding undecidability result can hence be
slightly strengthened into:
Lemma 2. The satisfiability problem for set-theoretic conjunctions of any num-
ber of positive literals of the forms (‡), plus one positive finitude literal, Finite(x) ,
and one negative literal of the form x 6= ∅ is algorithmically unsolvable.
From Hilbert’s 10th problem to undecidable fragments of set theory 7
A fortiori, we also have the following negative result:
Lemma 3. The satisfiability problem for set-theoretic conjunctions of any num-
ber of positive literals of the forms (‡), plus one positive finitude literal, Finite(x) ,
and one negative literal of the form | x | = 6 | y | is algorithmically unsolvable.
The following claim gives us a way of expressing the finitude of sets:
Proposition 1. A set with at least two members is finite if and only if it is the
union of two sets whose cardinalities differ from its own cardinality.
Proof. It suffices to note that, for an infinite set s and any decomposition s = s1 ∪
s2 , we have (independently of whether s1 ∩s2 = ∅ or not) | s | = max(| s1 | , | s2 |).
V
Thus, without affecting satisfiability, any conjunction i∈I Finite(xi ) of
finitude literals can be replaced by the conjunction
^
F = F1 ∪ F2 & | F1 | = 6 | F | & | F2 | = 6 |F | & F = F ∪ xi
i∈I
containing no finitude literal, where F, F1 , F2 are newly introduced variables.
In view of the preceding remark, Lemma 3 can be restated as follows.
Lemma 4. The satisfiability problem for set-theoretic conjunctions of any num-
ber of positive literals of the forms (‡), plus at most three negative literals of the
form | x | =
6 | y | , is algorithmically unsolvable.
One can express finitude also in the following way:
Proposition 2. A nonempty set is finite if and only if, by removing a member
from it, one obtains a set of different cardinality.
Therefore, we have:
Lemma 5. The satisfiability problem for set-theoretic conjunctions of any num-
ber of positive literals of the forms (‡), plus two positive literals of the form
x = { y } , and one negative literal of the form | x | =
6 | y | , is unsolvable.
Proof. In view of Lemma 2, it is enough to observe that:
– a negative literal of the form x 6= ∅ can be expressed via a conjunction of
the form y 0 = { x0 } & x = x ∪ y 0 where x0 , y 0 are brand new variables;
V
– any conjunction i∈I Finite(xi ) of finitude literals can be expressed by
means of the conjunction
^
F ∗ = { f ∗ } & F = F ∪F ∗ & F − = F \F ∗ & F − 6= | F | & F = F ∪xi
i∈I
containing no finitude literal, where F, F ∗ , F − are new variables;
– a literal of the form x = y \ z can be expressed by means of the conjunction
y = x ∪ x0 & x ∩ x0 = ∅ & x ∩ z = ∅ & x0 ∩ y = ∅ .
8 D. Cantone, E.G. Omodeo, M. Panettiere
1.3 Undecidability results regarding unordered Cartesian product
Much the same reductions can be carried out when the operation ⊗ defined by
s ⊗ t := {u, v} : u ∈ s, v ∈ t .
(for sets s, t whatsoever) supersedes the standard Cartesian product operator ×.
In order that Lemmas 1, 2, 3, 4, and 5 retain their validity with this unordered
product operator ⊗ in place of ×, it suffices that the above-proposed translation
rule for arithmetical constraints of the form x = y · z gets retouched as follows:
x=y·z wy,z = y ⊗ z & y ∩ z = ∅ & | wy,z | = | x | .
2 Undecidability of a restrained collection of
bounded-quantifier formulas in set theory
So far we have been designating various set-theoretic operations (e.g., dyadic
union, Cartesian product, cardinality) and properties and relations (finitude,
disjointness, etc.) by means of ad hoc signs ( ∪ , × , Finite( ), ∩ = ∅ , etc.)
which, if adopted beforehand as primitives in the language supporting set theory,
would make the undecidable fragments reviewed in Sec. 1 devoid of quantifiers.
Most often, set theories get formalized in a first-order language devoid of
constants and function symbols, whose only relators are ∈ and =. How complex
then becomes the syntactic structure of the formulas lying in the undecidable
fragments? As we will see next, a very modest usage of quantification is needed
to state them: only bounded quantifiers, and just one quantifier alternation are
needed, with (bounded) universal quantifiers in leading position.
2.1 The syntax of (∀∃)0 formulas
Consider the first-order language L∈ endowed with:
– an infinite supply ν0 , ν1 , ν2 , . . . of set variables;
– dyadic relators ∈, = designating membership and equality;
– the familiar propositional connectives ¬ (monadic) and & , ∨ , →, ↔ (dyadic);
– associated with each set variable νi , the familiar quantifiers ∀ νi and ∃ νi .
We enhance the usual syntax of formulas with two handy shortening devices:
Definition 2. Universal and existential bounded quantifiers are introduced
as follows:
(∀ x ∈ y)ϕ ↔Def (∀ x)(x ∈ y → ϕ) ;
(∃ x ∈ y)ϕ ↔Def (∃ x)(x ∈ y & ϕ) .
From Hilbert’s 10th problem to undecidable fragments of set theory 9
Definition 3. We dub (∀∃)0 -formula any conjunction Φ of the form
M
^
0 0
(∀yj1 ∈ yj1 ) · · · (∀yjpj ∈ yjpj
) (∃xj1 ∈ x0j1 ) · · · (∃xjqj ∈ x0jqj ) ϕj
j=0
where, for each j, the formula ϕj is devoid of quantifiers and either pj > 0,
qj > 0 or pj = qj = 0 holds.
2.2 (∀∃)0 specifications
Definition 4. We dub (∀∃)0 specification of an m-place relationship R over
sets a (∀∃)0 formula Φ with free variables a1 , . . . , am , x1 , . . . , xκ (where κ > 0)
such that, under the axioms of set theory (see below), one can prove:
R(a1 , . . . , am ) ↔ (∃ x1 , . . . , xκ ) Φ .
E.g., the right-hand sides of
a = b \ c ↔ (∀t ∈ a)(t ∈ b & t ∈
/ c) & (∀t ∈ b)(t ∈ c ∨ t ∈ a) ,
Sngl(a) ↔ (∃ x) x ∈ a & (∀y ∈ a)(y = x)
are (∀∃)0 specifications of the 3-place relationship a = b \ c and, respectively, of
the property “being a singleton set”.
In the ongoing, our set-theoretic framework will be the theory ZF, axiom of
regularity included. First, in order to design a (∀∃)0 specification of the property
“being a finite set” (see Sec. 2.4), we will extend temporarily the signature of L∈
with a constant ω which is meant to designate the first limit ordinal; then we will
figure out a (∀∃)0 specification of the property “being the first limit ordinal” (see
Sec. 2.5), thus ending in an impeccable (∀∃)0 specification of finitude. Along the
way, we will also specify the important equinumerosity predicate, which relates
two sets when they have the same cardinality (see Sec. 2.4).
2.3 (∀∃)0 specifications referring to disjointness, unionset, and
weak Cartesian product
x ∩ y = ∅ ↔ (∀ v ∈ x) v ∈/y ,
x ⊆ ∪y ↔ (∀ x0 ∈ x)(∃ y 0 ∈ y) x0 ∈ y 0 ,
∪f ⊆ v ↔ (∀p ∈ f )(∀w ∈ p)(w ∈ v) ,
Mapw (f ) ↔ (∀p ∈ f )(∀x1 , x2 , x3 ∈ p) x1 = x2 ∨ x2 = x3 ∨ x3 = x1 ,
f ⊆ x ⊗ y ↔ Mapw (f ) &
(∀p ∈ f )(∃x0 ∈ x)(∃y 0 ∈ y) x0 ∈ p & y 0 ∈ p ) &
(∀p ∈ f )(∀w ∈ p) w ∈ x ∨ w ∈ y ) .
The explanation of the last of these is straightforward; here it is:
10 D. Cantone, E.G. Omodeo, M. Panettiere
No member of f has more than two members: (∀p ∈ f ) |p| 6 2 ,
where
|p| 6 2 ↔ (∀x1 , x2 , x3 ∈ p) x1 = x2 ∨ x2 = x3 ∨ x3 = x1 .
Each member of f has the form {x0 , y 0 } with x0 ∈ x and y 0 ∈ y:
(∀p ∈ f )(∃x0 ∈ x)(∃y 0 ∈ y) x0 ∈ p & y 0 ∈ p ) .
No member of a member of f lies outside x ∪ y: ∪f ⊆ x ∪ y .
2.4 (∀∃)0 specifications of equinumerosity, squaring, and finitude
1-1w (x, f, y) ↔ x ∩ y = ∅ & f ⊆ x ⊗ y & x ⊆ ∪f & y ⊆ ∪f &
(∀p , q ∈ f )(∀v ∈ p) v ∈ q → p = q .
Meaning:
1-1w (x, f, y) can only hold if x and y are disjoint sets, in which case f models
a one-to-one mapping between x and y by means of unordered pairs, in the
sense that:
f consists of doubletons proper;
each doubleton in f pairs up a member of x with one of y;
f pairs up exactly one member of y with each member of x;
f pairs up exactly one member of x with each member of y.
Stating that sets x, y are of the same cardinality amounts to the statement
that there is a set y 0 such that
y 0 can be put in one-to-one correspondence with x,
y 0 can be put in one-to-one correspondence with y,
y 0 and x are disjoint, and y 0 and y are disjoint.
Summing up, we have:
|x| = |y| ↔ (∃ y 0 , g , h ) 1-1w (x, g, y 0 ) & 1-1w (y, h, y 0 ) .
Clue: One way of concretizing y 0 , here, is by putting y 0 = y ⊗ {y ∪ x}.
2
Likewise, stating that the cardinalities |x| , |y| are such that |x| = |y| amounts
to the statement that there are sets y 0 , x0 such that
y 0 can be put in one-to-one correspondence with y,
x0 = y ⊗ y 0 and x0 can be put in one-to-one correspondence with x,
x0 and x are disjoint, and y 0 and y are disjoint.
From Hilbert’s 10th problem to undecidable fragments of set theory 11
Summing up, we have:
2
|x| = |y| ↔ (∃ x0 , y 0 , g , h ) Mapw (x0 ) & 1-1w (x0 , g, x) &
1-1w (y 0 , h, y) &
0 0
(∀p ∈ x )(∃u ∈ y)(∃v ∈ y )( u ∈ p & v ∈ p ) &
(∀u ∈ y)(∀v ∈ y 0 )(∃p ∈ x0 )( u ∈ p & v ∈ p ) .
Clue: The equality x0 = y⊗y 0 follows from the conjunction of Mapw (x0 ) with the
last two conditions, thanks to the disjointness constraint y 0 ∩y = ∅ hidden inside
1-1w (y 0 , h, y). A convenient way to instantiate y 0 is, again, to put y 0 = y ⊗{y ∪x}.
A finite set is one that can be put in one-to-one correspondence with a
cardinal preceding (i.e., belonging to) the first infinite ordinal, ω :
Finite(x) ↔ (∃ o) o ∈ ω & |x| = |o| .
More explicitly:
Finite(x) ↔ (∃ o , x0 , g , h) o ∈ ω & 1-1w (x0 , g, x) & 1-1w (x0 , h, o) .
2.5 (∀∃)0 specification of ordinals and of the first limit ordinal
A set t is said to be transitive if t ⊆ P(t); equivalently, if ∪ t ⊆ t . After John
von Neumann and Raphael M. Robinson, ordinal numbers are those transitive
sets within which any two different elements can be compared by membership:
Ord(o) ↔ (∀y ∈ o)(∀y 0 ∈ y) y 0 ∈ o &
(∀o1 ∈ o)(∀o2 ∈ o)(o1 = o2 ∨ o1 ∈ o2 ∨ o2 ∈ o1 )
Those ordinal numbers o such that o 6= ∅ and o = ∪o are called limit ordinals.
Plainly, the property “being a limit ordinal” is (∀∃)0 -specifiable.
To characterize uniquely the first limit ordinal, ω, among all sets, it will
suffice to conjoin together the following conditions, where Z , a, and s are meant
to represent, respectively: ω itself, an element of ω, and the successor function
(modeled as a set of doubletons, each one implicitly ordered by membership):
Z is a non-null ordinal:
a ∈ Z & Ord(Z ) (8)
No member of s has more than two members:
Mapw (s) (9)
Each member of s is a doubleton {x, y} with x ∈ y ∈ Z :
(∀p ∈ s)(∃x, y ∈ p) x ∈ y & y ∈ Z (10)
12 D. Cantone, E.G. Omodeo, M. Panettiere
s is single-valued:
(∀p, q ∈ s)(∀x, y ∈ p)(∀y 0 ∈ q) (x ∈ y & x ∈ y 0 & x ∈ q) → p = q
(11)
The domain of s includes Z :
(∀x ∈ Z )(∃p ∈ s)(∃y ∈ p) x ∈ p & x ∈ y (12)
The multi-image of s includes Z \ {∅}:
(∀y ∈ Z )(∀e ∈ y)(∃p ∈ s)(∃x ∈ p) y ∈ p & x ∈ y (13)
Thus, one can prove (in ZF with regularity):
(∀Z ) Z = ω ↔ (∃a)(∃s) (8) & · · · & (13) .
In fact:
by (10) and (12), the domain of s equals Z ;
(12) and (13) yield that Z has no largest element;
consequently, by (8), Z is an ordinal such that Z ∈/ ω;
if Z were such that ω ∈ Z then, by (13), there should exist some x ∈ Z such
that {x, ω} ∈ s,
which is untenable: for, since s represents an increasing function, the imme-
diate successor x ∪ {x} of x would not be in the multi-image of s. From
Z ∈
/ ω and ω ∈ / Z , we get Z = ω.
Concluding remarks and open problems
We have revisited, deepened, and made more systematic, the study undertaken
long ago with [2] (see also [3, pp. 161–165]).
Can we do more along the directions envisioned in the following excerpt from
a historical paper?
[· · · ]the translation of a theorem of the appropriate form in some part of math-
ematics shows that the corresponding Diophantine equation has no solution.
Hence whatever methods went into proving the theorem can in fact be used
to show that a particular Diophantine equation has no solution. It is possible
that the same methods can be used to show that a class of equations includ-
ing perhaps an equation of interest in itself are unsolvable. Such an example
providing a new tool for solving Diophantine equations would be a consider-
able breakthrough. In any case, any mathematical method that has been used to
prove a theorem of the appropriate form has in fact been used to show that a
particular Diophantine equation has no solution. Thus all mathematical meth-
ods can be tools in the theory of Diophantine equations and perhaps we should
consciously attempt to exploit them. ” [5, pp. 338–339]
The quest is open. . . It may be rewarding to:
From Hilbert’s 10th problem to undecidable fragments of set theory 13
– translate back into number theory decidability results regarding fragments
of set theory;
– mimic the proofs of the theorems, dubbed DPR and DPRM in [7], concern-
ing the exponential Diophantine representability and the polynomial Dio-
phantine representability of any r.e. set, directly inside set theory (possibly
making some technical aspects of those proofs more transparent).
Open problems
Let BSTC⊗ (Boolean Set Theory with Cardinality comparison and the unordered
Cartesian product) be the collection of conjunctions of any number of positive
literals of the forms
x = y ∪ z , x = y ⊗ z , x ∩ y = ∅ , |x| = |y| .
In sight of the still in progress decidability result for MLS⊗ (multilevel syllo-
gistic with the unordered Cartesian product), concerning a positive solution to
the satisfiability problem for conjunctions of literals of the forms
x=y∪z, x=y⊗z, x∩y =∅, x∈y,
to precisely locate the boundary between decidability and undecidability, one
should attempt to find the decidability status of the satisfiability problem for
the following collections of equalities:
– BSTC⊗-conjunctions plus one negative literal of the form x 6= ∅ ,
– BSTC⊗-conjunctions plus two literals of any of the following forms:
|x| =
6 |y| and x = {y} .
Acknowledgements
We are grateful to Martin Davis for his encouragement. We thank the anonymous
referees for their careful comments.
References
1. J.L. Britton. Integer solutions of systems of quadratic equations. Mathematical
Proceedings of the Cambridge Philosophical Society, 86(3):385–389, 1979.
2. D. Cantone, Vincenzo Cutello, and Alberto Policriti. Set-theoretic reductions of
Hilbert’s tenth problem. In Egon Börger, Hans Kleine Büning, and Michael M.
Richter, editors, CSL ’89, 3rd Workshop on Computer Science Logic, Kaiser-
slautern, Germany, October 2-6, 1989, Proceedings, volume 440 of Lecture Notes
in Computer Science, pages 65–75. Springer, 1990.
3. D. Cantone, E. G. Omodeo, and A. Policriti. Set Theory for Computing. From De-
cision Procedures to Declarative Programming with Sets. Monographs in Computer
Science. Springer, 2001.
4. Domenico Cantone and Pietro Ursino. Formative processes with applications to
the decision problem in set theory: II. Powerset and singleton operators, finiteness
predicate. Information and Computation, 237:215–242, 2014.
5. Martin Davis, Yuri Matijasevič, and Julia Robinson. Hilbert’s tenth problem. Dio-
phantine equations: positive aspects of a negative solution. In Mathematical Devel-
opments Arising From Hilbert Problems, volume 28 of Proceedings of Symposia in
Pure Mathematics, pages 323–378, Providence, RI, 1976. American Mathematical
Society. Reprinted in [9, p. 269ff.].
14 D. Cantone, E.G. Omodeo, M. Panettiere
6. Yu. Matiyasevich. Existential arithmetization of Diophantine equations. Annals
of Pure and Applied Logic, 253(2-3):225–233, 2009.
7. Yu. V. Matiyasevich. Martin Davis and Hilbert’s tenth problem. In Eugenio G.
Omodeo and Alberto Policriti, editors, Martin Davis on Computability, Computa-
tional Logic, and Mathematical Foundations, volume 10 of Outstanding Contribu-
tions to Logic, pages 35–54. Springer, 2016.
8. Yuri Vladimirovich Matiyasevich. Hilbert’s tenth problem. The MIT Press, Cam-
bridge (MA) and London, 1993.
9. Julia Robinson. The collected works of Julia Robinson, volume 6 of Collected
Works. American Mathematical Society, Providence, RI, 1996. ISBN 0-8218-
0575-4. With an introduction by Constance Reid. Edited and with a foreword by
Solomon Feferman. xliv+338 pp.
10. Thoralf Skolem. Über die Nicht-charakterisierbarkeit der Zahlenreihe mittels
endlich oder abzählbar unendlich vieler Aussagen mit ausschliesslich Zahlenvari-
ablen. Fundamenta Mathematicae, 23:150–161, 1934.