=Paper=
{{Paper
|id=Vol-2199/paper1
|storemode=property
|title=Encoding Sets as Real Numbers
|pdfUrl=https://ceur-ws.org/Vol-2199/paper1.pdf
|volume=Vol-2199
|authors=Domenico Cantone,Alberto Policriti
|dblpUrl=https://dblp.org/rec/conf/zum/CantoneP18
}}
==Encoding Sets as Real Numbers==
https://ceur-ws.org/Vol-2199/paper1.pdf
Encoding Sets as Real Numbers
Domenico Cantone1 and Alberto Policriti2
1
Dept. of Mathematics and Computer Science, University of Catania, Italy
2
Dept. of Mathematics, Computer Science, and Physics, University of Udine, Italy
Abstract. We study a variant of the Ackermann encoding NA (x) :=
P NA (y)
y∈x 2 of the hereditarily finite sets by the natural numbers, appli-
cable to the larger collection HF1/2 of the hereditarily finite hypersets.
The proposed variation is obtained by simply placing a ‘minus’ sign be-
fore each P exponent in the definition of NA , resulting in the expression
RA (x) := y∈x 2−RA (y) . By a careful analysis, we prove that the encod-
ing RA is well-defined over the whole collection HF1/2 , as it allows one
to univocally assign a real-valued code to each hyperset in it. We also
address some preliminary cases of the injectivity problem for RA .
1 Introduction
In 1937, W. Ackermann proposed the following recursive encoding of hereditarily
finite sets by natural numbers:
X
NA (x) := 2NA (y) . (1)
y∈x
The encoding NA is simple, elegant, and highly expressive for a number of rea-
sons. On the one hand, it builds a strong bridge between two foundational mathe-
matical structures: (hereditarily finite) sets and (natural) numbers. On the other
hand, it enables the representation of the characteristic function of hereditarily
finite sets in terms of the usual notation for natural numbers as sequences of
binary digits. That is: y belongs to x if and only if the NA (y)-th digit in the
binary expansion of NA (x) is equal to 1. As one would expect, the string of 0’s
and 1’s representing NA (x) is nothing but (a representation of) the characteristic
function of x.
In this paper we study a very simple variation of the encoding NA , originally
proposed in [Pol13] and discussed in [DOPT15] and [OPT17], applicable to a
larger collection of sets. The proposed variation is obtained by simply placing a
minus sign before each exponent in (1), resulting in the expression:
X
RA (x) := 2−RA (y) .
y∈x
As opposed to the encoding NA , the range of RA is not contained in the set N
of the natural numbers, but it extends to the set R of real numbers. In addition,
the domain of RA can be expanded so as to include also the non-well-founded
hereditarily finite sets, namely, the sets defined by (finite) systems of equations
of the following form
ς1 = {ς1,1 , . . . , ς1,m1 }
.. (2)
.
ςn = {ςn,1 , . . . , ςn,mn },
with bisimilarity as equality criterion (see [Acz88] and [BM96], where the term
hyperset is also used). For instance, the special case of the single set equation
ς = {ς}, resulting into the equation (in real numbers) x = 2−x , is illustrated
in Section 3 and provides the code of the unique (under bisimilarity) hyperset
Ω = {Ω}.3
While the encoding NA is defined inductively (and this is perfectly in line with
our intuition of the very basic properties of the collections of natural numbers
N and of hereditarily finite sets HF—called HF0 in [BM96]), the definition of
RA , instead, is not inductive when extended to non-well-founded sets, and thus
it requires a more careful analysis, as it must be proved that it univocally (and
possibly injectively) associates (real) numbers to sets.
The injectivity of RA on the collection of well-founded and non-well-founded
hereditarily finite sets—henceforth, to be referred to as HF1/2 , see [BM96]—was
conjectured in [Pol13] and is still an open problem. Here we prove that, given any
finite collection ~1 , . . . , ~n of pairwise distinct sets in HF1/2 satisfying a system
of set-theoretic equations of the form (2) in n unknowns, one can univocally
determine real numbers RA (~1 ), . . . , RA (~n ) satisfying the following system of
equations:
Pm1 −RA (~1,k )
RA (~1 ) = k=1 2
..
.
Pmn −RA (~n,k )
RA (~n ) = k=1 2 .
This preliminary result shows that the definition of RA is well-given, as it
associates a unique (real) number to each hereditarily finite hyperset in HF1/2 .
This extends to HF1/2 the first of the properties that the encoding NA enjoys
with respect to HF. Should RA also enjoy the injectivity property, the proposed
adaptation of NA would be completely satisfiying, and RA could be coherently
dubbed an encoding for HF1/2 .
In the course of our proof, we shall also present a procedure that drives us
to the real numbers RA (~1 ), . . . , RA (~n ) mentioned above by way of successive
approximations. In the well-founded case, our procedure will converge in a finite
number of steps, whereas infinitely many steps will be required for convergence
in the non-well-founded case. In the last section of the paper, we shall also briefly
hint at the injectivity problem for RA .
3
Notice that the solution to the equation x = e−x is the so-called omega constant,
introduced by Lambert in [Lam58] and studied also by Euler in [Eul83].
2 Basics
Let N be the set of natural numbers and let P(·) denote the powerset operator.
S
Definition 1 (Hereditarily finite sets). HF := n∈N HFn is the collection of
all hereditarily finite sets, where
(
HF0 := ∅,
HFn+1 := P(HFn ), for n ∈ N.
In this paper we shall introduce and study a variation of the following map
introduced by Ackermann in 1937 (see [Ack37]):
Definition 2 (Ackermann encoding).
X 0
NA (h) := 2NA (h ) , for h ∈ HF.
h0 ∈h
It is easy to see that the map NA is a bijection between HF.
From now on, we denote by hi the element of HF whose NA -code is i, so that
NA (hi ) = i, for i ∈ N. Using the iterated-singleton notation
{x}0 := x
{x}n+1 := {x}n , for n ∈ N,
we plainly have:
h0 = ∅, h1 = {∅}, h2 = {∅}2 , h3 = {{∅}, ∅}, h4 = {∅}3 , etc.
In addition, for j ∈ N we have:
h0 ∈ hj iff j is odd, (3)
h2j = {hj } and h2j −1 = {h0 , h1 , . . . , hj−1 } . (4)
The map NA induces a total ordering ≺ among the elements of HF (that we shall
call Ackermann ordering) such that, for h, h0 ∈ HF:
h ≺ h0 iff NA (h) < NA (h0 ) .
Thus, hi is the i-th element of HF in the Ackermann ordering and, for i, j ∈ N,
we plainly have:
hi ≺ hj iff i < j.
The following proposition can be read as a restating of the bitwise comparison
between natural numbers in set-theoretic terms.
Proposition 1. For hi , hj ∈ HF, the following equivalence holds:
hi ≺ hj iff hi 6= hj and max(hi ∆ hj ) ∈ hj ,
≺
where ∆ is the symmetric difference operator A ∆ B := (A \ B) ∪ (B \ A).
It is also useful to define the following map low : N → N which, for i ∈ N,
computes the smallest code j of a set hj not present in hi (or, equivalently, the
position of the lowest bit set to 0 in the binary expansion of i):
low(i) := min{j | hj ∈
/ hi } .
The following elementary properties, whose proof is left to the reader, will
be used in the last section of the paper.
Lemma 1. For i ∈ N, we have:
(i) low(i) = 0 iff i is even,
(ii) hlow(i) ∈ / hi ,
(iii) {h0 , . . . , hlow(i)−1 } ⊆ hi ,
(iv) hi+1 = hi \ {h0 , . . . , hlow(i)−1 } ∪ {hlow(i) }.
Finally, we briefly recall that hypersets satisfy all axioms of ZFC, but the ax-
iom of regularity, which forbids both membership cycles and infinite descending
chains of memberships. In the hypersets realm of our interest, based on the Forti-
Honsell axiomatization [FH83] as popularized by P. Aczel [Acz88], the axiom
of regularity is replaced by the anti-foundation axiom (AFA). Roughly speak-
ing, AFA states that every conceivable hyperset, described in terms of a graph
specification modelling its internal membership structure, actually exists and is
univocally determined, regardless of the presence of cycles or infinite descending
paths in its graph specification. To be slightly more precise, a graph specification
(or membership graph) is a directed graph with a distinguished node (point),
where nodes are intended to represent hypersets, edges model membership re-
lationships among the node/hypersets, and the distinguished node denotes the
hyperset of interest among all the hypersets represented by the nodes of the
graph. However, extensionality needs to be strengthened so as structurally in-
distinguishable pointed graphs are always realized by the same hyperset. More
specifically, we say that two pointed graphs G = (V, E, p) and G0 = (V 0 , E 0 , p0 ),
where p ∈ V and p0 ∈ V 0 are the ‘points’ of G and G0 , respectively, are struc-
turally indistinguishable if the points p and p0 are bisimilar, namely, if there
exists a relation R over V × V 0 such that the following three properties hold, for
all v ∈ V and v 0 ∈ V 0 :
(B1) (∀w ∈ V )(∃w0 ∈ V 0 ) (v R v 0 ∧ (v, w) ∈ E) → ((v 0 , w0 ) ∈ E 0 ∧ w R w0 );
(B2) (∀w0 ∈ V 0 )(∃w ∈ V ) (v R v 0 ∧ (v 0 , w0 ) ∈ E 0 ) → ((v, w) ∈ E ∧ w R w0 ) ;
(B3) p R p0 .
Any relation R0 ⊆ V × V 0 satisfying properties (B1) and (B2) above is called a
bisimulation over V × V 0 .
In this paper, we are interested in those hypersets that admit a representation
as a finite pointed graph: these are the hereditarily finite hypersets in HF1/2 .
Given a (finite) pointed graph G = (V, E, p) whose nodes are all reachable
from its point p, the collection of hypersets represented by all its nodes form the
transitive closure of {~}, denoted trCl ({~}), where ~ is the hyperset correspond-
ing to the point p.
3 The real-valued map RA
Consider the following map RA obtained from NA by simply placing a minus
sign before each exponent in (1):
X
RA (x) := 2−RA (y) . (5)
y∈x
From (5) it follows immediately that all (valid) RA -codes are nonnegative.
For instance, we have:
1
RA (∅) = 0, RA ({∅}) = 1, RA ({∅}2 ) = ,
2
1
1 − √12
−√
RA ({∅}3 ) = √ , RA ({∅}4 ) = 2 RA ({∅}5 ) = 2−2
2
, , etc.
2
The definition of RA bears a strong formal similarity with NA , but calls into
play real numbers. As a further example, from the definition of RA , it follows
that the hyperset defined by the set equation ς = {ς} yields the equation in R
x = 2−x . (6)
It is easy to see that the equation (6) has a unique solution in R, since the
functions x and 2−x are, respectively, strictly increasing and strictly decreasing,
so that the function x − 2−x is strictly increasing. In addition, we have:
1 1 1
x − 2−x |x= 12 = − √ < 0 < 1 − = x − 2−x |x=1 .
2 2 2
Thus, the solution Ω of (6) over R, namely, the code of the hyperset defined
by the set equation x = {x}, satisfies 21 < Ω < 1. Furthermore, much by the
√
same argument used by the Pythagoreans to prove the irrationality of 2, it can
easily be shown that Ω is irrational. In fact, Ω is transcendental. This follows
from the Gelfond-Schneider theorem (see [Gel34]), which states that every real
number of the form ab is transcendental, provided that a and b are algebraic
numbers such that 0 6= a 6= 1, and b is irrational.4 Indeed, if Ω were algebraic, so
would be −Ω and therefore, by the Gelfond-Schneider theorem, 2−Ω = Ω would
be transcendental, contradicting the assumed algebraicity of Ω. Thus, √
Ω must
−1/ 2
be transcendental after all. As is easy to check, the RA -code 2 of {∅}4 is
transcendental as well.
Much as for NA , the encoding RA is easily seen to be well-defined over HF. As
a consequence of the results to be proved in Section 4, we shall see that (5) allows
one to associate univocally a code to each non-well-founded hereditarily finite
set as well, thus showing that RA is also well-defined over the whole collection
HF1/2 of hereditarily finite hypersets.
4
We recall that the Gelfond-Schneider theorem, obtained independently in 1934 by
A. O. Gelfond and Th. Schneider, solves completely the seventh in a well-celebrated
list of twenty-three problems posed by David Hilbert at the International Congress
of Mathematicians held in Paris, 1900 (see [Hil02]).
Remark 1 For every singleton {h0 } ∈ HF, definition (5) gives RA ({h0 }) =
0
2−RA (h ) . Thus, for every h ∈ HF, we have
n n
X 0 X
RA (h) = 2−RA (h ) = RA ({h0 }) . (7)
h0 ∈h h0 ∈h
Once we prove that RA is well-defined over HF1/2 , equation (7) can be im-
mediately generalized to HF1/2 as well.
As the following proposition shows, the codes of hereditarily finite sets can
grow arbitrarily large.
Proposition 2. For any n ∈ N, there exists an i ∈ N such that RA (hi ) > n.
Proof. Notice that for any odd natural number j, we have ∅ ∈ hj . Thus, by
(7), we have RA (hj ) > R({∅}) = 1, RA ({hj }) = 2−RA (hj ) 6 2−1 = 12 , and
RA ({{hj }}) = 2−RA ({hj }) > 2−1/2 > 12 .
Let k = 4n and consider the hereditarily finite set h := {hk0 } : k 0 6 k .
Then, we have:
k k
X X 1 k
RA (h) = RA ({{hk0 }}) > RA ({{hk0 }}) > · = n.
2 2
k0 =0 k0 =0
k0 is odd
4 RA on Hereditarily Finite Hypersets
The fully general case corresponds to considering systems of set-theoretic equa-
tions such as the ones introduced by the following definition (see also [Acz88]).
Definition 3 (Set systems). A set system S (ς1 , . . . , ςn ) in the set unknowns
ς1 , . . . , ςn is a collection of set-theoretic equations of the form:
ς1 = {ς1,1 , . . . , ς1,m1 }
.. (8)
.
ςn = {ςn,1 , . . . , ςn,mn },
with mi > 0 for i ∈ {1, . . . , n}, and where each unknown ςi,u , for i ∈ {1, . . . , n}
and u ∈ {1, . . . , mi }, occurs among the unknowns ς1 , . . . , ςn .5
The index map IS of S (ς1 , . . . , ςn ) is the map
n
[
IS : {hi, vi | 1 6 v 6 mi } → {1, . . . , n}
i=1
such that IS (i, v) is the index of the unknown ςi,v in the list ς1 , . . . , ςn , for i ∈
{1, . . . , n} and v ∈ {1, . . . , mi }, namely, ςIS (i,v) ≡ ςi,v .
5
When mi = 0, the expression {ςi,1 , . . . , ςi,mi } reduces to the empty set {}.
A set system S (ς1 , . . . , ςn ) is normal if there exist n pairwise distinct (i.e.,
non bisimilar) hypersets ~1 , . . . , ~n ∈ HF1/2 such that the assignment ςi 7→ ~i
satisfies all the set equations of S (ς1 , . . . , ςn ).
Observe that, by the anti-foundation axiom, the assignment ςi 7→ ~i satisfying
the equations of a given normal set system S (ς1 , . . . , ςn ) is plainly unique.
From now on, we shall write ~, with or without subscripts and/or super-
scripts, to denote a generic (possibly well-founded) hyperset in HF1/2 .
Having in mind the definition (5) of RA , to each normal set system we asso-
ciate a system of equations in R, called code system, as follows.
Definition 4 (Code systems). Let S (ς1 , . . . , ςn ) be a normal set system of
the form
ς1 = {ς1,1 , . . . , ς1,m1 }
..
.
ςn = {ςn,1 , . . . , ςn,mn },
with index map IS . The code system associated with S (ς1 , . . . , ςn ) is the follow-
ing system C (x1 , . . . , xn ) of equations in the real unknowns x1 , . . . , xn :
−x1,1
+ · · · + 2−x1,m1
x1 = 2
.. (9)
.
xn = 2−xn,1 + · · · + 2−xn,mn ,
where xi,u is a shorthand for xIS (i,u) , for i ∈ {1, . . . , n} and u ∈ {1, . . . , mi }.
Normal set systems characterise all possible elements of HF1/2 and we shall
see that the corresponding code systems characterise their RA -codes. In fact,
we shall prove that every code system admits a unique solution which can be
computed as the limit of suitable sequences of real numbers. Terms in such se-
quences approximate the final solution alternatively from above and from below.
In case of non-well-founded sets, such approximating sequences are infinite and
convergent (to the codes of the non-well-founded sets); additionally, its terms
eventually become codes of certain well-founded hereditarily finite sets which
can be seen as approximations of the corresponding non-well-founded set.
We begin by formally defining the set and multi-set approximating sequences
(of the solution) of set systems.
Definition 5 (Hereditarily finite multi-sets). Hereditarily finite multi-sets
are collection of elements—themselves multi-sets—that can occur with finite mul-
tiplicities.
Hereditarily finite multi-sets will be denoted by specifying their elements in
square brackets, in any order, where elements are repeated according to their
multiplicities. For instance, the set a occurs in the multi-set [b, a, b, b] with mul-
tiplicity 1, whereas b occurs with multiplicity 3.
Remark 2 A natural embedding of the hereditarily finite sets in the hereditarily
finite multi-sets is the following: a multi-set µ can be regarded as a set if and
only if each of its elements has multiplicity 1 and, recursively, can be regarded
as a set. Thus, in particular, ∅ is both a set and a multi-set.
Definition 6. Let S (ς1 , . . . , ςn ) be a (normal) set system of the form (8), and
let IS be its index map. The set-approximating sequence for (the solution of )
S (ς1 , . . . , ςn ) is the sequence h~ji | 1 6 i 6 ni j∈N of the n-tuples of well-
founded hereditarily finite sets defined by
h∅ | 1 6 i 6 ni if j = 0
h~ji | 1 6 i 6 ni :=
h{~j−1 j−1
i,1 , . . . , ~i,mi } | 1 6 i 6 ni if j > 0 ,
where ~j−1 j−1
i,u is a shorthand for ~IS (i,u) , for i ∈ {1, . . . , n} and u ∈ {1, . . . , mi }.
approximating sequence for (the solution of ) S (ς1 , . . . , ςn ) is
The multi-set
the sequence hµji | 1 6 i 6 n}i j∈N of the n-tuples of well-founded hereditarily
finite multi-sets defined by
h∅ | 1 6 i 6 ni if j = 0
hµji | 1 6 i 6 ni :=
j−1
h[µi,1 , . . . , µj−1
i,mi ] | 1 6 i 6 ni if j > 0 ,
where µj−1 j−1
i,u is a shorthand for µIS (i,u) , for i ∈ {1, . . . , n} and u ∈ {1, . . . , mi }.
Given a (normal) set system S (ς1 , . . . , ςn ), we say that two unknowns ςi
and ςi0 , with i, i0 ∈ {1,. . . , n}, are distinguished at step k > 0 by the set-
approximating sequence h~ji | 1 6 i 6 ni j∈N for S (ς1 , . . . , ςn ) (resp., multi-set
approximating sequence hµji | 1 6 i 6 ni j∈N for S (ς1 , . . . , ςn )) if ~ki 6= ~ki0
(resp., µki 6= µki0 ). Further, we shall refer to ~ji (resp., µji ) as the (j-th) set-
approximation value (resp., multi-set approximation value) of ςi at step j.
Example 1. Consider the following normal set system:
ς1 = {ς2 , ς3 }
ς2 = {}
S (ς1 , ς2 , ς3 , ς4 ) =
ς3 = {ς3 }
ς4 = {ς2 } .
In this case, we have: m1 = 2, m2 = 0, m3 = 1, and m4 = 1; in addition, ς1,1 , ς1,2 ,
ς3,1 , and ς4,1 are ς2 , ς3 , ς3 , and ς2 , respectively, so that IS (1, 1) = 2, IS (1, 2) = 3,
IS (3, 1) = 3, and IS (4, 1) = 2.
The first four elements of the set-approximating sequence for S are:
~01 , ~02 , ~03 , ~04 = h∅, ∅, ∅, ∅i
~11 , ~12 , ~13 , ~14 = h{∅}, ∅, {∅}, {∅}i
~21 , ~22 , ~23 , ~24 = h{∅, {∅}}, ∅, {{∅}}, {∅}i
~31 , ~32 , ~33 , ~34 = h{∅, {{∅}}}, ∅, {{{∅}}}, {∅}i .
Notice that, for j = 2 and j = 3, all the ~ji ’s are pairwise distinct. In fact, as
a consequence of the next lemma, this is true also for all j > 3.
The first four tuples of the multi-set approximating sequence of S are:
µ01 , µ02 , µ03 , µ04 = h∅, ∅, ∅, ∅i
µ11 , µ12 , µ13 , µ14 = h[∅, ∅], ∅, [∅], [∅]i
µ21 , µ22 , µ23 , µ24 = h[∅, [∅]], ∅, [[∅]], [∅]i
µ31 , µ32 , µ33 , µ34 = h[∅, [[∅]]], ∅, [[[∅]]], [∅]i .
Also in this case, for j = 2 and j = 3, all the µji ’s are pairwise distinct and
this holds also for j > 3. Observe that the unknowns ςi and ςj are distinguished
by the multi-set approximating sequence before than by the set-approximating
sequence: indeed, µ11 6= µ31 , whereas ~11 = ~31 .
All sets in the tuples of a set-approximating system are well-founded hered-
itarily finite sets. The initial tuples of a multi-set approximating sequence may
contain proper multi-sets (as in the above example). However, as a consequence
of the following lemma (whose proof can be found in the extended version [CP18]
of this paper), after at most n steps all pairs of distinct unknowns are distin-
guished and each tuple contains only proper sets.
Lemma 2. Let S (ς1 , . . . , ςn ) be a normal set-system, and let h~ji | 1 6 i 6
j
n}i j∈N and hµi | 1 6 i 6 ni j∈N be its set- and multi-set approximating
sequences, respectively. The following conditions hold:
(a) for i, i0 ∈ {1, . . . , n} and j, k > 0, we have
~ji 6= ~ji0 =⇒ (~j+k+1
i 6= ~j+k+1
i0 ∧ µji 6= µji0 )
(namely, if at step j > 0 two unknowns are distinguished by the set-approx-
imating sequence, then they are also distinguished by the multi-set approx-
imating sequence; in addition, they remain distinguished in all subsequent
steps);
(b) for j, k > 0 and i ∈ {1, . . . , n}, we have
~ji = ~j+1
i =⇒ ~ji = ~j+k+2
i
(namely, as soon as ~ji = ~j+1 i holds for some j > 0, the set-approximation
value of ςi remains unchanged for all subsequent steps);
(c) for i, i0 ∈ {1, . . . n} and j > n, we have
(i 6= i0 =⇒ ~ji 6= ~ji0 ) ∧ hµji | 1 6 i 6 ni = h~ji | 1 6 i 6 ni
(namely, starting from step n, all pairs of distinct unknowns are distinguished
and the set- and multi-set approximating sequences coincide).
Point a) in the above lemma suggests that even though set and multi-set
approximating sequences will eventually “separate” all solutions of a set sys-
tem, multi-set can introduce inequalities first. This is our first motivation for
extending the notion of RA -code to multi-sets and use such code-extension to
approximate regular RA -codes. The second motivation is given in Remark 3.
Definition 7. Given a normal set system S (ς1 , . . . , ςn ) and its multi-set ap-
proximating sequence hµji | 1 6 i 6 n}i j∈N , we define the corresponding code
approximating sequence hRµA (µji ) | 1 6 i 6 n}i j∈N by recursively putting, for
i ∈ {1, . . . , n} and j ∈ N:
(
RµA (µ0i ) := 0
Pmi −Rµ (µj ) (10)
RµA (µj+1
i ) := u=1 2 A i,u .
We also define the corresponding code increment sequence hδij | 1 6 i 6 ni j∈N
by putting, for i ∈ {1, . . . , n} and j ∈ N:
δij := RµA (µj+1
i ) − RµA (µji ) . (11)
Plainly, RµA (µji ) > 0, for all i ∈ {1, . . . , n} and j ∈ N.
Remark 3 Consider a normal set system S (ς1 , . . . , ςn ) and its solutions
~1 , . . . , ~n . The values RµA (µ1i ) and RµA (µ1i0 ) are equal if and only if |~i | = |~i0 |.
The values RµA (µ2i ) and RµA (µ2i0 ) are equal if and only if the multi-sets of the
cardinalities of elements in ~i and ~i0 are equal. The values RµA (µ3i ) and RµA (µ3i0 )
are equal if and only if the multi-sets of multi-sets of the cardinalities of elements
of elements in ~i and ~i0 are equal, and so on.
In preparation for the proof of the existence and uniqueness of a solution to
the code system associated with any normal set system, we state the technical
properties contained in the following lemma, whose proof can be found in the
extended version [CP18] of this paper.
Lemma 3. Let S (ς1 , . . . , ςn ) be a normal set system of the form
ς1 = {ς1,1 , . . . , ς1,m1 }
..
.
ςn = {ςn,1 , . . . , ςn,mn },
with index map IS , code approximating sequence hRµA (µji ) | 1 6 i 6 n}i j∈N ,
and code increment sequence hδij | 1 6 i 6 n}i j∈N . Then, for i ∈ {1, . . . , n}
and j ∈ N, the following facts hold:
(i) RµA (µj+1
i ) = δi0 + · · · + δij ,
0
(ii) δi = mi ,
Pmi −Rµ (µj ) j
(iii) δij+1 = u=1 2 A i,u · (2−δi,u − 1),
(iv) δi2j+1 6 0 6 δi2j ,
(v) |δij+1 | 6 |δij |, and
(vi) limj→∞ δij = 0.
We are now ready to prove the main result of the paper.
Theorem 4. For any given normal set system, the corresponding code system
admits always a unique solution.
Proof.
µ Let S (ς1 , . . . , ςn ) be a normal set system of the form (8), and let
hRA (µji ) | 1 6 i 6 n}i j∈N and hδij | 1 6 i 6 n}i j∈N be its code approximat-
ing sequence and code increment sequence, respectively. Also, let C (x1 , . . . , xn )
be the code system
x1 = 2−x1,1 + · · · + 2−x1,m1
..
.
xn = 2−xn,1 + · · · + 2−xn,mn ,
associated with S (ς1 , . . . , ςn ).
We first exhibit a solution of the system C (x1 , . . . , xn ) and then prove its
uniqueness.
Existence: By Lemma 3(i),(iv),(vi), using the Leibniz criterion for alternating
series, it follows that each of the sequences {RµA (µji )}j∈N is convergent, for i ∈
{1, . . . , n}. Let us put αi := limj→∞ RµA (µji ), for i ∈ {1, . . . , n}. From (10), we
have
mi
X µ j
µ j+1
RA (µi ) = 2−RA (µi,u ) , for j ∈ N .
u=1
Then, by taking the limit of both sides as j approaches infinity, it follows that
mi
X
αi = 2−αi,u ,
u=1
for i ∈ {1, . . . , n}, where αi,u is a shorthand for αIS (i,u) , with IS the index map
of S (ς1 , . . . , ςn ), proving that the n-tuple hα1 , . . . , αn i is a solution of the code
system C (x1 , . . . , xn ).
Uniqueness: Next we prove that the solution hα1 , . . . , αn i is unique. Let
hα10 , . . . , αn0 i be any solution of the code system C (x1 , . . . , xn ). To show that
hα10 , . . . , αn0 i = hα1 , . . . , αn i it is enough to prove that
RµA µ2j 6 αi0 6 RµA µ2j+1
i i , for j ∈ N and i ∈ {1, . . . , n}, (12)
holds. Indeed, from (12), it follows immediately
αi = lim RµA µ2j 6 αi0 6 lim RµA µ2j+1
i i = αi ,
j→∞ j→∞
for every i ∈ {1, . . . , n}, showing that hα10 , . . . , αn0 i = hα1 , . . . , αn i.
We prove (12) by induction on j, for all i ∈ {1, . . . , n}.
Pmi −α0
For the base case j = 0, we observe that since αi0 = u=1 2 i,u (where, as
0
usual, αi,u stands for αI0S (i,u) ), then
RµA µ0i = 0 6 αi0 6 mi = RµA µ1i ,
for i ∈ {1, . . . , n}.
For the inductive step, let us assume that
RµA µ2j 6 αi0 6 RµA µ2j+1
i i , for i ∈ {1, . . . , n}, (13)
holds for some j ∈ N, and prove that it holds for j + 1 as well. From (13)
Pmi −α0
and recalling that αi0 = u=1 2 i,u , the following inequalities hold, for every
i ∈ {1, . . . , n} and u ∈ {1, . . . , mi }:
RµA µ2j 0 µ 2j+1
i,u 6 αi,u 6 RA µi,u
µ 2j+1 0 µ 2j
2−RA (µi,u ) 6 2−αi,u 6 2−RA (µi,u )
mi mi mi
µ 2j+1 0 µ 2j
2−RA (µi,u ) 6 2−RA (µi,u )
X X X
2−αi,u 6
u=1 u=1 u=1
RµA 2j+2
6 αi0 6 RµA µ2j+1
µi i .
The inequalities on the last line (for i ∈ {1, . . . , n}) imply in particular that we
have
RµA µ2j+2 0
6 RµA µ2j+1
i,u 6 αi,u i,u ,
for every i ∈ {1, . . . , n} and u ∈ {1, . . . , mi }. Hence, by repeating the very same
steps as above, one can deduce also the inequalities
2(j+1) 2(j+1)+1
RµA µi = RµA µ2j+2 6 αi0 6 RµA µ2j+3 = RµA µi
i i ,
for i ∈ {1, . . . , n}, proving that (13) holds for j + 1 too. This completes the
induction, and also the proof of the theorem.
Remark 5 To show that the code RA is well-defined over the whole HF1/2 , we
proceed as follows. Given a hereditarily finite hyperset ~ ∈ HF1/2 , let ~1 , . . . , ~n
be the distinct elements of the transitive closure trCl ({~}) of {~}, where ~1 = ~.
Then we have
~1 = {~1,1 , . . . , ~1,m1 }
.. (14)
.
~n = {~n,1 , . . . , ~n,mn }
for suitable hypersets ~i,j ∈ {~1 , . . . , ~n }, with i ∈ {1, . . . , n} and j ∈ {1, . . . , mi }.
Consider the set system S (ς1 , . . . , ςn )
ς1 = {ς1,1 , . . . , ς1,m1 }
..
.
ςn = {ςn,1 , . . . , ςn,mn },
associated with (14), where ςi,j = ς` iff ~i,j = ~` , for all i, ` ∈ {1, . . . , n} and
j ∈ {1, . . . , mi }. Plainly, S (ς1 , . . . , ςn ) is normal and ~1 , . . . , ~n is its solution.
By Theorem 4, let α1 , . . . , αn be the solution to the code system associated with
S (ς1 , . . . , ςn ). Then RA (~i ) = αi , for i ∈ {1, . . . , n}, and, in particular, RA (~) =
RA (~1 ) = α1 . Further, it is immediate to check that, for every normal set system
S 0 (x01 , . . . , x0m ) containing ~ in its solution, say at position k̄ ∈ {1, . . . , m}, if
α10 , . . . , αm
0
is the solution to the corresponding code system, then αk̄0 = α1 . In
other words, the value RA (~) computed by the above procedure is independent of
the normal set system used. By the arbitrariness of ~, it follows that RA (~) is
defined for every hyperset ~ ∈ HF1/2 .
5 A first step towards injectivity
As already remarked, the problem of establishing the injectivity of the map
RA is still open. As an initial example, we provide here a very partial result.
However, the arguments used in the proof below do not seem to easily generalize
even to the narrower task of proving the injectivity of RA over the well-founded
hereditarily finite sets only.
Lemma 4. For all i ∈ N, we have:
(a) RA (hi ) 6= RA (hi+1 ), and
(b) RA (hi ) 6= RA (hi+2 ),
where hj is the j-th element of HF in the Ackermann ordering.
Proof. Let i ∈ N. From (iii) and (iv) of Lemma 1 and from (4), we have
RA (hi+1 ) = RA (hi ) − RA (h2low(i) −1 ) + RA (h2low(i) ) . (15)
If i is even, then low(i) = 0, and therefore
RA (h2low(i) −1 ) = 0 6= 1 = RA (h2low(i) ) .
On the other hand, if i is odd, then low(i) 6= 0, and so, by (3):
RA (h2low(i) ) < 1 = RA ({h0 }) 6 RA (h2low(i) −1 ) .
In any case, we have RA (h2low(i) ) − RA (h2low(i) −1 ) 6= 0, proving (a), by (15).
Concerning (b), we begin by putting
∆j := RA (h2j ) − RA (h2j −1 ) ,
for j ∈ N. Let us show that ∆j 6= −1, for all j ∈ N. To begin with, for j = 0, 1, 2,
we have:
∆0 = RA (h1 ) − RA (h0 ) = 1 6= −1
1
∆1 = RA (h2 ) − RA (h1 ) = RA ({h1 }) − RA (h1 ) = 2−1 − 1 = − 6= −1
2
∆2 = RA (h4 ) − RA (h3 ) = RA ({h2 }) − RA ({h0 , h1 })
−1 1 1 3
= 2−2 − 1 + = √ − 6= −1 .
2 2 2
In addition, for j > 2, we have {h0 , h1 , h2 } ⊆ h2j −1 , and therefore:
RA (h2j −1 ) > RA ({h0 , h1 , h2 }) = 2−RA (h0 ) + 2−RA (h1 ) + 2−RA (h2 )
= 2−0 + 2−1 + 2−2
1 1
= 1 + + √ > 2.
2 2
Hence, we have ∆j 6= −1 also for j > 2, since RA (h2j ) = 2−RA (hj ) < 1. But
then, from (15), we have, for every i ∈ N:
RA (hi+2 ) − R(hi ) = RA (hi+2 ) − R(hi+1 ) + RA (hi+1 ) − R(hi )
= ∆low(i+1) + ∆low(i) 6= 0 ,
since either i or i + 1 is even and so either ∆low(i) = 1 or ∆low(i+1) = 1, whereas,
as we proved above, ∆low(i) 6= −1 6= ∆low(i+1) . This proves (b), completing the
proof of the lemma.
Remark 6 While the value of RA µ0i is 0 for any i ∈ {1, . . . , n}, the value
of RA µ1i —first approximation of RA (µi )—is the cardinality of µi , and the
subsequent approximations oscillate within the interval [0, |µi |].
Conclusions
By turning labels into sets, the encoding proposed in this paper can be used on
a variety of structures, going from labelled graphs to Kripke models. This can be
done in many different ways and in [DPP04,PP04] the reader can find a rather
general—albeit non optimised—technique to carry out this label elimination
task. A label elimination performed to optimise code computation (or its form)
is under study.
The algorithmic side of RA is also under study. A possible direction towards
its usage—for example in bisimulation computation—starts from the observation
that only the computation of a bounded number of digits is actually necessary
to realise all the inequalities in any given set system.
Acknowledgements
The authors thank Eugenio Omodeo for very pleasant and fruitful conversations,
and an anonymous reviewer for his/her comments.
References
[Ack37] W. Ackermann, Die Widerspruchfreiheit der allgemeinen Mengenlehre,
Mathematische Annalen 114 (1937), 305–315.
[Acz88] P. Aczel, Non-well-founded sets, vol. 14 of CSLI Lecture Notes, Stanford,
CA, 1988.
[BM96] J. Barwise and L. S. Moss, Vicious circles, CSLI Lecture Notes, Stanford,
CA, 1996.
[CP18] D. Cantone and A. Policriti, Encoding sets as real numbers (Extended ver-
sion), Tech. Report arXiv:1806.09329 [cs], June 2018.
[DOPT15] Giovanna D’Agostino, Eugenio G. Omodeo, Alberto Policriti, and Alexan-
dru I. Tomescu, Mapping sets and hypersets into numbers, Fundam. Inform.
140 (2015), no. 3-4, 307–328.
[DPP04] A. Dovier, C. Piazza, and A. Policriti, An efficient algorithm for computing
bisimulation equivalence, Theor. Comput. Sci. 311 (2004), no. 1-3, 221–256.
[Eul83] L. Euler, De serie Lambertina Plurimisque eius insignibus proprietatibus.,
Acta Acad. Scient. Petropol. 2 (1783), 29–51, reprinted in Euler, L. Opera
Omnia, Series Prima, Vol. 6: Commentationes Algebraicae. Leipzig, Ger-
many: Teubner, pp. 350–369, 1921.
[FH83] M. Forti and F. Honsell, Set theory with free construction principles, Annali
Scuola Normale Superiore di Pisa, Classe di Scienze IV (1983), no. 10, 493–
522.
[Gel34] Aleksandr Gelfond, Sur le septième Problème de Hilbert, Bulletin de
l’Académie des Sciences de l’URSS. VII (1934), no. 4, 62–634.
[Hil02] D. Hilbert, Mathematical problems, Bulletin of the American Mathematical
Society 8 (1902), no. 10, 437–479.
[Lam58] J.H. Lambert, Observations variae in Mathesin Puram, Acta Helvitica,
physico-mathematico-anatomico-botanico-medica 3 (1758), 128–168.
[OPT17] Eugenio G. Omodeo, Alberto Policriti, and Alexandru I. Tomescu, On sets
and graphs. perspectives on logic and combinatorics, Springer, 2017.
[Pol13] A. Policriti, Encodings of sets and hypersets, Proc. of the 28th Italian Con-
ference on Computational Logic, Catania, Italy, September 25-27, 2013.
(D. Cantone and M. Nicolosi Asmundo, eds.), vol. 1068, CEUR Workshop
Proceedings, ISSN 1613-0073, 2013, pp. 235–240.
[PP04] C. Piazza and A. Policriti, Ackermann Encoding, Bisimulations, and OB-
DDs, Theory and Practice of Logic Programming 4 (2004), no. 5-6, 695–718.