# Flow: the Axiom of Choice is independent from the Partition Principle in ZFU

Adonai S. Sant’Anna  Renato Brodzinski  Marcio P. P. de França  Otávio Bueno

<EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS><EMAIL_ADDRESS>
###### Abstract

We introduce a formal theory called Flow where the intended interpretation of
its terms is that of function. We prove ZF, ZFC and ZFU (ZF with atoms) can be
immersed within Flow as natural consequences from our framework. Our first
important application is the introduction of a model of ZFU where the
Partition Principle holds but the Axiom of Choice fails, if Flow is
consistent. So, our framework allows us to address the oldest open problem in
set theory: if the Partition Principle entails the Axiom of Choice.

This is a fully revised version of a previous preprint about Flow and its
applications.

###### Contents

  1. 1 Introduction
  2. 2 Flow theory
    1. 2.1 The very basic
    2. 2.2 Emergent functions
    3. 2.3 More about restrictions
    4. 2.4 Ordinals
    5. 2.5 ZF-sets
    6. 2.6 Atoms
    7. 2.7 Interpreting ZFU
    8. 2.8 The model
  3. 3 ZFU is immersed in Flow
    1. 3.1 ZFU
    2. 3.2 Lévy model
    3. 3.3 Other models
  4. 4 On the consistency of Flow
  5. 5 Final remarks
  6. 6 Acknowledgements

##  1 Introduction

It is rather difficult to determine when functions were born, since
mathematics itself significantly evolves along history. Specially nowadays we
find different formal concepts associated to the label function. But an
educated guess could point towards Sharaf al-Dīn al-Tūsī who, in the 12th
century, not only introduced a ‘dynamical’ concept which could be interpreted
as some notion of function, but also studied how to determine the maxima of
such functions [13].

All usual mathematical approaches for physical theories are based on either
differential equations or systems of differential equations whose solutions
(when they exist) are either functions or classes of functions (see, e.g.,
[29]). In pure mathematics the situation is no different. Continuous
functions, linear transformations, homomorphisms, and homeomorphisms, for
example, play a fundamental role in topology, linear algebra, group theory,
and differential geometry, respectively. Category theory [20] emphasizes such
a role in a very clear, elegant, and comprehensive way. As remarked by Marquis
[21], category theory allows us to distinguish between canonical and
noncanonical maps, in a way which is not usually achieved within purely
extensional set theories, like ZFC. And canonical maps “constitute the highway
system of mathematical concepts”. Concepts of symmetry are essential in pure
and applied mathematics, and they are stated by means of group transformations
[32].

Some authors suggest that functions are supposed to play a strategic role into
the foundations of mathematics [35] and even mathematics teaching [17], rather
than sets. The irony of such perspective starts in the historical roots of set
theories. Georg Cantor’s seminal works on sets were strongly motivated by
Bernard Bolzano’s manuscripts on infinite multitudes called Menge [34]. Those
collections were supposed to be conceived in a way such that the arrangement
of their components is unimportant. However, Bolzano insisted on an Euclidian
view that the whole should be greater than a part, while Cantor proposed a
quite different approach: to compare infinite quantities we should consider a
one-to-one correspondence between collections. Cantor’s concept of collection
(in his famous Mengenlehre) was strongly committed to the idea of function.
Subsequent formalizations of Cantor’s “theory” were developed in a way such
that all strategic terms were associated to an intended interpretation of
collection. The result of that effort is a strange phenomenon from the point
of view of theories of definition: Padoa’s principle allows us to show domains
of functions are definable from functions themselves [4] [5] [27]. Thus, even
in extensional set theories functions seem to play a more fundamental role
than sets.

Nevertheless, there is another crucial role that functions (in a broader
intuitive sense) play in the study of set theories and cannot be ignored,
namely, those questions regarding the use of $\in$-automorphisms [15] and non-
trivial elementary embeddings of a universe into itself [16], among other
examples. Some questions regarding set theories cannot be answered by means of
the use of their axioms alone. That is where model theory provides
metamathematical tools to answer to some of those questions [33]. Non-trivial
elementary embeddings and $\in$-automorphisms are examples of ‘functions’
which are not formalized into standard set theories but which are very useful
to evaluate questions regarding independence of formulas like the Axiom of
Choice, the Continuum Hypothesis and the existence of inaccessible cardinals.
Within this context, the formal theory we introduce here is supposed to
provide a framework where at least some of those ‘very large functions’ can be
precisely defined.

This paper was initially motivated by von Neumann’s original ideas [35] and a
variation of them [27], and related papers as well ([4] [5]). In [27] it was
provided a reformulation of von Neumann’s ‘functions’ theory (termed
$\mathcal{N}$ theory). Nevertheless, we develop here a whole new approach
called Flow.

String diagrams [7] (whose edges and vertices can eventually be interpreted as
morphisms in a monoidal category) introduce some ideas which seem to intersect
with our own. A remarkable feature of string diagrams is that edges need not
be connected to vertices at both ends. More than that, unconnected ends can be
interpreted as inputs and outputs of a string diagram (with important
applications in computer science). But within our framework no function has
any domain whatsoever. Besides, the usual way to cope with string diagrams is
by means of a discrete and finitary framework, while in Flow (our framework)
we do not impose such restrictions.

A more radical proposal where functions play a fundamental role is the Theory
of Autocategories [10]. Autocategories are developed with the aid of
autographs, where arrows (which work as morphisms) are drawn between arrows
with no need of objects. Thus, once more we see a powerful idea concerning
functions is naturally emerging in different places nowadays.

When Ernst Zermelo introduced AC, his motivation was the Partition Principle
[2], which is usually stated by means of functions. Indeed, AC entails PP. But
since 1904 (when Zermelo introduced AC) it is unknown whether PP implies AC.
For a review about the subject see, e.g., [2] [12] [14] [26]. Our answer is
that AC is independent from PP, at least within ZFU if Flow is consistent. Our
point is that ZF, ZFC, all their variants, and almost all their respective
models (with a few exceptions like those in [1] and [6]) are somehow committed
to a methodological and epistemological character which forces us to see sets
as collections of some sort. Within Flow that does not happen, since our
framework drives us to see sets as special cases of terms whose intended
interpretation correspond to an intuitive notion of function. All sets in Flow
are restrictions of $\underline{\mathfrak{1}}$, a function which works as some
sort of ‘universal’ identity in the sense that for any $x$ we have
$\underline{\mathfrak{1}}(x)=x$. Nevertheless, functions who are no
restrictions of $\underline{\mathfrak{1}}$ play an important role with
consequences over sets. An analogous situation takes place with the well known
Reflexion Principle in model theory [31]: some features of the von Neumann
Universe motivate mathematicians to look for new axioms which grant the
existence of strongly inaccessible cardinals. Flow, however, provides a new
way for coping with the metamathematics of ZF and its variants.

As a final remark before we start, it is worth to observe we freely employ the
term ‘Flow’ in this paper. Within a more general viewpoint, ‘Flow’ refers to
any first order theory (i) whose objects are supposed to be interpreted as
functions; (ii) which grants the existence of functions
$\underline{\mathfrak{0}}$ and $\underline{\mathfrak{1}}$, in the sense that
$\forall
x(\underline{\mathfrak{1}}(x)=x\wedge\underline{\mathfrak{0}}(x)=\underline{\mathfrak{0}})$
and $\underline{\mathfrak{0}}\neq\underline{\mathfrak{1}}$, as it follows in
the next Section; and (iii) which allows a nontrivial composition among any
functions at all, whether such a composition is associative or not. In this
first paper about Flow, however, we explore one specific formal framework who
is able to replicate ZF, ZFC, and ZFU. Our goal here is to suggest another way
to construct models of set theories.

##  2 Flow theory

Our first Flow theory is a first-order theory $\mathfrak{F}$ with identity
[22], where $x=y$ reads ‘$x$ is equal to $y$’, and $\neg(x=y)$ is abbreviated
as $x\neq y$. From now on we use Flow and $\mathfrak{F}$ as synonyms. Flow has
one functional letter $f_{1}^{2}$ (termed evaluation), where $f_{1}^{2}(f,x)$
is a term, if $f$ and $x$ are terms. If $y=f_{1}^{2}(f,x)$, we abbreviate this
by $f(x)=y$, and read ‘$y$ is the image of $x$ by $f$’. All terms are called
functions. Such a terminology seems to be adequate under the light of our
intended interpretation: functions are supposed to be terms which ‘transform’
terms into other terms. Since we are assuming identity, our functions cannot
play the role of non-trivial relations. Suppose, for example, $f(x)=y$ and
$f(x)=y^{\prime}$, which are abbreviations for $f_{1}^{2}(f,x)=y$ and
$f_{1}^{2}(f,x)=y^{\prime}$, respectively. From transitivity of identity, we
have $y=y^{\prime}$. So, for any $f$ and any $x$, there is one single $y$ such
that $f(x)=y$.

Lowercase Latin and Greek letters denote functions, with the sole exception of
two specific functions to appear in the next pages, namely,
$\underline{\mathfrak{0}}$ and $\underline{\mathfrak{1}}$. Uppercase Latin
letters are used to denote formulas or predicates (which are eventually
defined). Any explicit definition in Flow is an abbreviative one, in the sense
that for a given formula $F$, the definiendum is a metalinguistic abbreviation
for the definiens given by $F$. Eventually we use bounded quantifiers. If $P$
is a predicate defined by a formula $F$, we abbreviate $\forall
x(P(x)\Rightarrow G(x))$ and $\exists x(P(x)\wedge G(x))$ as
$\forall_{P}x(G(x))$ and $\exists_{P}x(G(x))$, respectively; where $G$ is a
formula. Finally, $\exists!x(G(x))$ is a metalinguistic abbreviation for
$\exists x\forall y(G(y)\Leftrightarrow y=x)$.

Postulates F1$\sim$F11 of $\mathfrak{F}$ are as follows.

###  2.1 The very basic

F1 - Weak Extensionality

$\forall f\forall g(((f(g)=f\wedge g(f)=g)\vee(f(g)=g\wedge
g(f)=f))\Rightarrow f=g))$.

If $f(g)=f$ we say $f$ is rigid with $g$. If $f(g)=g$ we say $f$ is flexible
with $g$. If both $f$ and $g$ are rigid (flexible) with each other, then
$f=g$.

F2 - Self-Reference

$\forall f(f(f)=f)$.

Any $f$ is flexible and rigid with itself. That may sound a strong limitation
if we compare our framework, e.g., to lambda calculus [3]. But that feature is
quite useful for our purposes. One task for the future is to admit some
variations of Flow where F2 is no axiom.

###### Observation 1

Let $y$ be a function such that $\forall x(y(x)=r\Leftrightarrow x(x)\neq r)$.
What about $y(y)$? If $x=y$, then $y(y)=r\Leftrightarrow y(y)\neq r$
(Russell’s paradox). But that entails $y(y)\neq y(y)$, another contradiction.
However, our Self-Reference postulate does not allow us to define such an $y$,
since $x(x)=x$ for any $x$. That is not the only way to avoid such an
inconsistency. Our Restriction axiom (some pages below) does the same work.
That opens the possibility of variations of Flow where Self-Reference is not a
theorem.

Our first theorem states any $f$ can be identified by its images $f(x)$.

###### Theorem 1

$\forall f\forall g(f=g\Leftrightarrow\forall x(f(x)=g(x)))$.

Proof

From substitutivity of identity in $f(x)=f(x)$, proof of the $\Rightarrow$
part is straightforward: if $f=g$, then $f(x)=g(x)$, for any $x$. For the
$\Leftarrow$ part, suppose, for any $x$, $f(x)=g(x)$. If $x=f$, $f(f)=g(f)$;
if $x=g$, $f(g)=g(g)$. From F2, $f(f)=f$ and $g(g)=g$. So, $g(f)=f$ and
$f(g)=g$. F1 entails $f=g$.

Axioms F1 and F2 could be rewritten as one single formula:

F1’ - Alternative Weak Extensionality

$\forall f\forall g(((f(g)=f\wedge g(f)=g)\vee(f(g)=g\wedge
g(f)=f))\Leftrightarrow f=g))$.

F2 is a consequence from F1’. Ultimately, $f=g$ entails $f(g)=f$ (from F1’).
And substitutivity of identity entails $f(f)=f$. But we prefer to keep axioms
F1 and F2 (instead of F1’) to smooth away some discussions. From F1 and F2, we
can analogously see that F1’ is a nontrivial theorem.

F3 - Identity

$\exists f\forall x(f(x)=x)$.

There is at least one $f$ such that, for any $x$, we have $f(x)=x$. Any
function $f$ which satisfies F3 is said to be an identity function.

###### Theorem 2

Identity function is unique.

Proof

Suppose both $f$ and $g$ satisfy F3. Then, for any $x$, $f(x)=x$ and $g(x)=x$.
Thus, $f(g)=g$ and $g(f)=f$. Hence, according to F1, $f=g$.

In other words, there is one single $f$ which is flexible to every term. In
that case we simply say $f$ is flexible. That means “flexible” and “identity”
are synonyms.

F4 - Rigidness

$\exists f\forall x(f(x)=f)$.

There is at least one $f$ which is rigid with any function. Observe the
symmetry between F3 and F4! Any $f$ which satisfies last postulate is said to
be rigid.

###### Theorem 3

The rigid function is unique.

Proof

Let $f$ and $g$ satisfy axiom F4. Then, for any $x$, $f(x)=f$ and $g(x)=g$.
Thus, $f(g(x))=f(g)=f$ and $g(f(x))=g(f)=g$. From F1, $f=g$.

Now we are able to introduce new terminology. Term $\underline{\mathfrak{1}}$
is the identity (flexible) function, while $\underline{\mathfrak{0}}$ is the
rigid function, since we proved they are both unique. So,

$\forall
x(\underline{\mathfrak{1}}(x)=x\;\;\wedge\;\;\underline{\mathfrak{0}}(x)=\underline{\mathfrak{0}}).$

Since $f(x)=y$ says $f_{1}^{2}(f,x)=y$, F3 states there is an $f$ such that,
for any $x$, $f_{1}^{2}(f,x)=x$, while F4 says there is $f$ where
$f_{1}^{2}(f,x)=f$. If we do not grant the existence of other functions, it
seems rather difficult to prove
$\underline{\mathfrak{0}}\neq\underline{\mathfrak{1}}$.

###### Theorem 4

$\underline{\mathfrak{0}}$ is the only function which is rigid with
$\underline{\mathfrak{0}}$.

Proof

This theorem says $\forall x(x\neq\underline{\mathfrak{0}}\Rightarrow
x(\underline{\mathfrak{0}})\neq x)$, i.e., $\forall
x(x(\underline{\mathfrak{0}})=x\Rightarrow x=\underline{\mathfrak{0}})$. But
$\underline{\mathfrak{0}}(x)=\underline{\mathfrak{0}}$. So, if
$x(\underline{\mathfrak{0}})=x\wedge\underline{\mathfrak{0}}(x)=\underline{\mathfrak{0}}$,
then $x=\underline{\mathfrak{0}}$ (F1).

###### Theorem 5

$\underline{\mathfrak{1}}$ is the only function which is flexible with
$\underline{\mathfrak{1}}$.

Proof

This theorem says $\forall x(x\neq\underline{\mathfrak{1}}\Rightarrow
x(\underline{\mathfrak{1}})\neq\underline{\mathfrak{1}})$, i.e., $\forall
x(x(\underline{\mathfrak{1}})=\underline{\mathfrak{1}}\Rightarrow
x=\underline{\mathfrak{1}})$. But $\underline{\mathfrak{1}}(x)=x$. So, if
$x(\underline{\mathfrak{1}})=\underline{\mathfrak{1}}\wedge\underline{\mathfrak{1}}(x)=x$,
then $x=\underline{\mathfrak{1}}$ (F1).

For more details about $x(\underline{\mathfrak{0}})$ and
$x(\underline{\mathfrak{1}})$, for any $x$, see Theorems 10 and 13.

###### Definition 1

$f[t]$ iff $t\neq f\wedge f(t)\neq\underline{\mathfrak{0}}$. We read $f[t]$ as
‘$f$ acts on $t$’.

Whereas $f(t)$ is a term, $f[t]$ abbreviates a formula. No $f$ acts on itself.
The intuitive idea is to allow us to talk about what a function $f$ does. For
example, $\underline{\mathfrak{0}}$ does nothing whatsoever, since there is no
$t$ on which it acts.

Next definition is a pedagogical move to write postulate F5 in a simple and
direct way. If the reader is not comfortable with that, all you have to do is
to rewrite $h=f\circ g$ in F5 (next postulate) as the conjunction of all five
formulas in the next definition.

###### Definition 2

Given $f$ and $g$, the $\mathfrak{F}$-composition $h=f\circ g$, if it exists,
must satisfy the next conditions:

(i) $h\neq\underline{\mathfrak{0}}$; (ii) $\forall x((x\neq f\wedge x\neq
g\wedge x\neq h)\Rightarrow h(x)=f(g(x)))$;
(iii) $h\neq f\Rightarrow h(f)=\underline{\mathfrak{0}}$; (iv) $h\neq
g\Rightarrow h(g)=\underline{\mathfrak{0}}$;
(v) $(g\neq h\wedge f\neq h\wedge g\neq\underline{\mathfrak{1}}\wedge
f\neq\underline{\mathfrak{1}})\Rightarrow(f(g(h))=\underline{\mathfrak{0}}\vee
g(h)=\underline{\mathfrak{0}})$

So, (i) No $\mathfrak{F}$-composition is $\underline{\mathfrak{0}}$. (ii)
$\mathfrak{F}$-composition behaves like standard notions of composition
between functions up to self-reference. Nevertheless, contrary to usual
practice in standard set theories, we can define $\mathfrak{F}$-composition
between any two functions. (iii and iv) No $\mathfrak{F}$-composition
$h=f\circ g$ acts on any of its factors $f$ or $g$. Finally, item (v) is a
technical constraint to avoid ambiguities in the calculation of $f\circ g$.
Either $g$ does not act on the $\mathfrak{F}$-composition $h$ or, if it acts,
then $f$ does not act on $g(h)$.

F5 - $\mathfrak{F}$-Composition

$\forall f\forall g(\exists!h(h=f\circ g))$.

We never calculate $(f\circ g)(f\circ g)$ as $f(g(f\circ g))$, since $(f\circ
g)(f\circ g)$ is $f\circ g$, according to F2. Given $f$ and $g$, we can
‘build’ $f\circ g$ through a three-step process: (i) First we establish a
label $h$ for $f\circ g$; (ii) Next we evaluate $f(g(x))$ for any $x$ which is
different of $f$ and $g$. By doing that we are assuming those $x$ are
different of $h$. Thus, if such a choice of $x$ entails $f(g(x))=y$ for a
given $y$, then $h(x)=y$; (iii) Next we evaluate the following possibilities:
is $h$ equal to either $f$, $g$ or something else? If $h\neq g$, then $h(g)$
is supposed to be $\underline{\mathfrak{0}}$. If
$h(g)=\underline{\mathfrak{0}}$ entails a contradiction, then $h$ is simply
$g$. An analogous method is used for assessing if $h$ is $f$. Eventually, $h$
is neither $f$ nor $g$, as we can see in the next theorems.

It is worth to remark that $\mathfrak{F}$-composition plays a crucial role in
our main result (Theorems 67 and 68).

###### Theorem 6

There is a unique $h$ such that $h\neq\underline{\mathfrak{0}}$ but
$h(x)=\underline{\mathfrak{0}}$ for any $x\neq h$.

Proof

From Definition 2 and F5,
$\underline{\mathfrak{0}}\circ\underline{\mathfrak{0}}$ is a unique
$h\neq\underline{\mathfrak{0}}$ such that, for any $x$ where
$x\neq\underline{\mathfrak{0}}$ and $x\neq h$,
$h(x)=\underline{\mathfrak{0}}(\underline{\mathfrak{0}}(x))=\underline{\mathfrak{0}}(\underline{\mathfrak{0}})=\underline{\mathfrak{0}}$.
Since $h\neq\underline{\mathfrak{0}}$, then F5 entails
$h(\underline{\mathfrak{0}})=\underline{\mathfrak{0}}$. Thus, $h(x)$ is
$\underline{\mathfrak{0}}$ for any $x\neq h$, while $h$ itself is different of
$\underline{\mathfrak{0}}$.

Such $h$ of last theorem (which does not conflict neither with Theorem 3 nor
with Theorem 4) is labeled with a special symbol, namely, $\varphi_{0}$. So,
$\underline{\mathfrak{0}}\circ\underline{\mathfrak{0}}=\varphi_{0}$, where
$\varphi_{0}\neq\underline{\mathfrak{0}}$. If the reader is intrigued by the
subscript 0 in $\varphi_{0}$, our answer is ‘yes, we intend to introduce
ordinals, where $\varphi_{0}$ is the first one’.

Let $f$, $g$, $a$, and $c$ be pairwise distinct functions where: (i)$f(a)=g$,
$f(g)=c$, $f(c)=c$, $f(f)=f$, and $f(r)=\underline{\mathfrak{0}}$ for the
remaining values $r$; (ii) $g(a)=a$, $g(g)=g$, and
$g(r)=\underline{\mathfrak{0}}$ for the remaining values $r$; (iii) $a$ and
$c$ are arbitrary, as long they are neither $\underline{\mathfrak{0}}$ nor
$\underline{\mathfrak{1}}$. Then, $(f\circ g)\circ f=\varphi_{0}$, while
$f\circ(g\circ f)=l$, where $l(a)=c$, $l(l)=l$, and
$l(r)=\underline{\mathfrak{0}}$ for the remaining values $r$. Thus,
$\mathfrak{F}$-composition among functions which act on each other (observe in
this example $f[g]$, since $f\neq g$ and
$f(g)=c\neq\underline{\mathfrak{0}}$), if they exist, is not necessarily
associative.

###### Theorem 7

Let $f$, $g$, and $h$ be terms such that neither one of them acts on the
remaining ones. Then $\mathfrak{F}$-Composition is associative among $f$, $g$,
and $h$.

Proof

Both $f\circ(g\circ h)=p$ and $(f\circ g)\circ h=q$ correspond (Definition 2)
to $y=f(g(h(x)))$, if $x$ is different of $f$, $g$, $h$, $p$, and $q$. So,
$f\circ(g\circ h)=(f\circ g)\circ h$ for those values of $x$. But $f$, $g$,
and $h$ do not act on $f$, $g$, or $h$; and no $\mathfrak{F}$-composition acts
on any of its factors. So, $f\circ(g\circ h)=(f\circ g)\circ h=f(g(h(x)))$.

Evaluation $f_{1}^{2}$ is not associative as well. Consider, e.g.,
$x(\underline{\mathfrak{1}}(x))$, for $x$ different of
$\underline{\mathfrak{0}}$ and different of $\underline{\mathfrak{1}}$, and
such that $x(\underline{\mathfrak{1}})=\underline{\mathfrak{0}}$ (functions
like that do exist, as we can see later on). Thus,
$x(\underline{\mathfrak{1}}(x))=x(x)=x$. If evaluation was associative, we
would have
$x(\underline{\mathfrak{1}}(x))=x(\underline{\mathfrak{1}})(x)=\underline{\mathfrak{0}}(x)=\underline{\mathfrak{0}}$;
a contradiction, since we assumed $x\neq\underline{\mathfrak{0}}$! Of course
this rationale works only if we prove the existence of a function like $x$ and
that $\underline{\mathfrak{0}}\neq\underline{\mathfrak{1}}$. Both claims are
the subject of the next two theorems.

It is good news that evaluation is not associative. According to F2, for all
$t$, $g(t)=(g(g))(t)$, since $g(g)=g$. If evaluation was associative, we would
have $g(t)=g(g(t))$ and, thus, $g=g\circ g$. So, $\mathfrak{F}$-composition
would be idempotent, a useless feature for our purposes.

###### Theorem 8

$\underline{\mathfrak{0}}\neq\underline{\mathfrak{1}}$.

Proof

$\underline{\mathfrak{0}}\circ\underline{\mathfrak{0}}=\varphi_{0}\neq\underline{\mathfrak{0}}$
(Theorem 6). But
$\underline{\mathfrak{0}}(\varphi_{0})=\underline{\mathfrak{0}}$, while
$\underline{\mathfrak{1}}(\varphi_{0})=\varphi_{0}$. Thus, from Theorem 1,
$\underline{\mathfrak{0}}\neq\underline{\mathfrak{1}}$.

###### Theorem 9

For any $x$ we have $\underline{\mathfrak{0}}\circ
x=x\circ\underline{\mathfrak{0}}=\varphi_{0}$

Proof

First we prove $\underline{\mathfrak{0}}\circ x=\varphi_{0}$. From Definition
2 and axiom F5, $(\underline{\mathfrak{0}}\circ
x)(t)=\underline{\mathfrak{0}}(x(t))=\underline{\mathfrak{0}}$ for any
$t\neq\underline{\mathfrak{0}}$ and $t\neq x$. But F5 demands
$\underline{\mathfrak{0}}\circ x$ is different of $\underline{\mathfrak{0}}$.
Hence, $(\underline{\mathfrak{0}}\circ
x)(\underline{\mathfrak{0}})=\underline{\mathfrak{0}}$. Regarding $x$, there
are three possibilities: (i) $x=\underline{\mathfrak{0}}$; (ii)
$x=\varphi_{0}$; (iii) $x$ is neither $\underline{\mathfrak{0}}$ nor
$\varphi_{0}$. The first case corresponds to Theorem 6, which entails
$\underline{\mathfrak{0}}\circ x=\varphi_{0}$. In the second case, if
$\underline{\mathfrak{0}}\circ x$ is different of $x=\varphi_{0}$, then
$(\underline{\mathfrak{0}}\circ x)(\varphi_{0})=\underline{\mathfrak{0}}$. But
that would entail $(\underline{\mathfrak{0}}\circ
x)(t)=\underline{\mathfrak{0}}$ for any $t\neq\underline{\mathfrak{0}}\circ
x$, which corresponds exactly to function $\varphi_{0}$ proven in Theorem 6, a
contradiction. So, $\underline{\mathfrak{0}}\circ x$ is indeed $\varphi_{0}$,
when $x=\varphi_{0}$. Concerning last case, since
$x\neq\underline{\mathfrak{0}}$ and $x\neq\varphi_{0}$, then (Theorem 1) there
is $t\neq\varphi_{0}$ such that $x(t)\neq\underline{\mathfrak{0}}$ for $x\neq
t$. From F5, $(\underline{\mathfrak{0}}\circ x)(t)=\underline{\mathfrak{0}}$
for such value of $t$. But once again we have a function
$\underline{\mathfrak{0}}\circ x$ such that $(\underline{\mathfrak{0}}\circ
x)(t)=\underline{\mathfrak{0}}$ for any $t\neq\underline{\mathfrak{0}}$, which
corresponds to $\varphi_{0}$ from Theorem 6. Concerning the identity
$x\circ\underline{\mathfrak{0}}=\varphi_{0}$, the proof is analogous. If
$h=x\circ\underline{\mathfrak{0}}$, then $h\neq\underline{\mathfrak{0}}$ (from
F5). Besides, for any $x$, $x\neq h$ entails $h(x)=\underline{\mathfrak{0}}$.
Hence, $h=\varphi_{0}$.

###### Theorem 10

$\forall x(x(\underline{\mathfrak{0}})=\underline{\mathfrak{0}})$.

Proof

$x\circ\underline{\mathfrak{0}}=\varphi_{0}$ (Theorem 9). Hence, for any $t$,
$(t\neq x\wedge t\neq\underline{\mathfrak{0}}\wedge
t\neq\varphi_{0})\Rightarrow\varphi_{0}(t)=x(\underline{\mathfrak{0}}(t))=x(\underline{\mathfrak{0}})$.
But $\varphi_{0}(t)=\underline{\mathfrak{0}}$ for any $t\neq\varphi_{0}$.
Thus, $x(\underline{\mathfrak{0}})=\underline{\mathfrak{0}}$.

###### Theorem 11

$\underline{\mathfrak{1}}\circ\underline{\mathfrak{1}}=\underline{\mathfrak{1}}$.

Proof

From F5, $h=\underline{\mathfrak{1}}\circ\underline{\mathfrak{1}}$ entails
$h(x)=x$ for any $x\neq\underline{\mathfrak{1}}$. Since the
$\mathfrak{F}$-composition is unique and $\underline{\mathfrak{1}}$ guarantees
all demanded conditions, then $h=\underline{\mathfrak{1}}$.

###### Theorem 12

$\forall x\forall y(x\circ
y=\underline{\mathfrak{1}}\Rightarrow(x=\underline{\mathfrak{1}}\wedge
y=\underline{\mathfrak{1}}))$.

Proof

Let $x\neq\underline{\mathfrak{1}}$. Then
$\underline{\mathfrak{1}}(x)=\underline{\mathfrak{0}}$, according to F5. But
that happens only for $x=\underline{\mathfrak{0}}$. And
$\underline{\mathfrak{0}}\circ y\neq\underline{\mathfrak{1}}$. Analogous
argument holds for $y\neq\underline{\mathfrak{1}}$.

There can be no functions different of $\underline{\mathfrak{1}}$ such that
their composition is $\underline{\mathfrak{1}}$.

Next theorem is important for a better understanding about F1, although its
proof does not demand the use of such a postulate.

###### Theorem 13

$\forall x((x\neq\underline{\mathfrak{0}}\wedge
x(\underline{\mathfrak{1}})=\underline{\mathfrak{0}})\Leftrightarrow(\underline{\mathfrak{1}}\circ
x=x\wedge x\circ\underline{\mathfrak{1}}=x\wedge
x\neq\underline{\mathfrak{1}}))$.

Proof

The $\Rightarrow$ part. If
$x(\underline{\mathfrak{1}})=\underline{\mathfrak{0}}$, then
$x\neq\underline{\mathfrak{1}}$, since
$\underline{\mathfrak{1}}(\underline{\mathfrak{1}})=\underline{\mathfrak{1}}$.
If $x\circ\underline{\mathfrak{1}}=h$, then, for any $t$ different of $x$,
$\underline{\mathfrak{1}}$, and $h$, we have
$h(t)=x(\underline{\mathfrak{1}}(t))=x(t)$. If $h=x$, then $h$ satisfies all
conditions from F5, since $x\neq\underline{\mathfrak{1}}$,
$h(\underline{\mathfrak{1}})=x(\underline{\mathfrak{1}})=\underline{\mathfrak{0}}$,
and $h(t)=x(t)$ for any $t\neq h$. Since F5 demands $h$ to be unique, then
$h=x$. If $\underline{\mathfrak{1}}\circ x=h$, we use an analogous argument.
For the $\Leftarrow$ part, $\underline{\mathfrak{1}}\circ
x=x\circ\underline{\mathfrak{1}}=x$ entails $x\neq\underline{\mathfrak{0}}$
(Theorem 9). Since $x\neq\underline{\mathfrak{1}}$, then F5 demands for the
$\mathfrak{F}$-composition $x$ that
$x(\underline{\mathfrak{1}})=\underline{\mathfrak{0}}$.

###### Observation 2

If it wasn’t for the uniqueness of $\mathfrak{F}$-compositions in F5, Flow
would be consistent with the existence of many functions, like $x$ and $h$
(from the proof of Theorem 13), which “do” the same thing. We refer to such
functions as clones. For a brief investigation about clones see Definition 12
and its subsequent discussion. Clones are meant to be different functions $x$
and $h$ which share the same images $x(t)$ and $h(t)$ for any $t$ different of
both $x$ and $h$, and such that $x(h)=\underline{\mathfrak{0}}$ and
$h(x)=\underline{\mathfrak{0}}$. From Theorem 1, $x\neq h$ (recall F2). We use
this opportunity to prove Theorem 6, since
$\underline{\mathfrak{0}}\circ\underline{\mathfrak{0}}=\varphi_{0}$, where
$\varphi_{0}$ and $\underline{\mathfrak{0}}$ are clones. But we cease using
clones when we talk about other functions. That is why we refer to F1 as “weak
extensionality”. A strong extensionality postulate would demand that other
clones besides $\underline{\mathfrak{0}}$ and $\varphi_{0}$ cannot exist. We
do something like that in some remaining postulates where we use the
quantifier $\exists!$.

###### Definition 3

Given a term $f$, $g$ is the $\mathfrak{F}$-successor of $f$, and we denote
this by $\Sigma(f,g)$, iff $f(g)=\underline{\mathfrak{0}}\wedge\forall x(x\neq
g\Rightarrow g(x)=f(x))$.

For example, let $f$ be given by $f(a)=b$, $f(b)=c$, $f(c)=c$, $f(f)=f$, and
$f(r)=\underline{\mathfrak{0}}$ for the remaining values $r$. Now let $g$ be
given by $g(a)=b$, $g(b)=c$, $g(c)=c$, $g(f)=f$, $g(g)=g$, and
$g(r)=\underline{\mathfrak{0}}$ for the remaining values $r$, where $g\neq f$.
In that case, $\Sigma(f,g)$, if functions like those exist. Observe this has
nothing to do with our previous discussion about clones.

F6 - $\mathfrak{F}$-Successor Function

$\exists!\sigma(\sigma\neq\underline{\mathfrak{0}}\wedge\forall
f((f\neq\sigma\wedge f\neq\underline{\mathfrak{0}})\Rightarrow\\\ (\exists
g(\Sigma(f,g)\Leftrightarrow\sigma(f)=g)\vee(\forall
h(\neg\Sigma(f,h))\Leftrightarrow\sigma(f)=\underline{\mathfrak{0}}))))$.

This last axiom states the existence and uniqueness of a special function
$\sigma$. From now on we write mostly $\sigma_{f}$ for $\sigma(f)$. Every time
we use the symbol $\sigma$ we are referring to the same term from F6: the only
one such that $\sigma_{f}=g\neq\underline{\mathfrak{0}}$ is equivalent to
$\Sigma(f,g)$, and $\sigma_{f}=\underline{\mathfrak{0}}$ is equivalent to
$\forall h(\neg\Sigma(f,h))$, as long $f$ is neither $\sigma$ nor
$\underline{\mathfrak{0}}$. Thus, $\sigma$ successfully ‘signals’
$\mathfrak{F}$-successors, when they exist, for all functions, except when $f$
is either $\underline{\mathfrak{0}}$ or $\sigma$. In those cases, we have
$\Sigma(\underline{\mathfrak{0}},\varphi_{0})$ and
$\sigma_{\underline{\mathfrak{0}}}=\underline{\mathfrak{0}}$ (Theorem 10),
while $\forall h(\neg\Sigma(\sigma,h))$ and $\sigma_{\sigma}=\sigma$ (F2).

Next we want to grant the existence of $\mathfrak{F}$-successors for many
other terms. As previously announced, this axiom states the existence of an
hierarchy of functions, where $\varphi_{0}$ is the first one.

F7 - Infinity

$\exists i((\forall t(i(t)=t\vee
i(t)=\underline{\mathfrak{0}}))\wedge\sigma_{i}\neq\underline{\mathfrak{0}}\wedge(i(\varphi_{0})=\varphi_{0}\wedge\forall
x((x\neq\underline{\mathfrak{0}}\wedge
i(x)=x)\Rightarrow(i(\sigma_{x})=\sigma_{x}\wedge\sigma_{x}\neq\underline{\mathfrak{0}}))))$.

###### Definition 4

Any $i$ which satisfies F7 is said to be inductive.

Since the existence of $\varphi_{0}$ is granted by F5, we can use $\sigma$ and
F7 to grant the existence of $\varphi_{1}=\sigma_{\varphi_{0}}$ such that
$\varphi_{1}(\varphi_{1})=\varphi_{1}$,
$\varphi_{1}(\varphi_{0})=\varphi_{0}$, and for the remaining values $r$
(those who are neither $\varphi_{0}$ nor $\varphi_{1}$) we have
$\varphi_{1}(r)=\underline{\mathfrak{0}}$. That happens because F7 states the
existence of at least one other function $i$ and infinitely many other
functions. It says $i(\varphi_{0})=\varphi_{0}$. Besides, there is a
non-$\underline{\mathfrak{0}}$ $\mathfrak{F}$-successor of $\varphi_{0}$ such
that $i(\sigma_{\varphi_{0}})=\sigma_{\varphi_{0}}$. More than that, if $x$
admits a non-$\underline{\mathfrak{0}}$ $\mathfrak{F}$-successor $\sigma_{x}$
(where $i(x)=x$), then $i(\sigma_{x})=\sigma_{x}$, where
$\sigma_{x}\neq\underline{\mathfrak{0}}$. Thus,
$\varphi_{0}\neq\underline{\mathfrak{0}}$ and
$\sigma_{\varphi_{0}}=\varphi_{1}$, where $\varphi_{1}\neq\varphi_{0}$ and
$\varphi_{1}\neq\underline{\mathfrak{0}}$. Analogously we can get
$\varphi_{2}$, $\varphi_{3}$, and so on. Along with those terms $\varphi_{n}$,
F7 says any inductive function $i$ admits its own
non-$\underline{\mathfrak{0}}$ $\mathfrak{F}$-successor $\sigma_{i}$.

Subscripts $0$, $1$, $2$, $3$, etc., are metalinguistic symbols based on an
alphabet of ten symbols (the usual decimal numeral system) which follows the
lexicographic order $\prec$, where $0\prec 1\prec 2\prec\cdots\prec 8\prec 9$.
If $n$ is a subscript, then $n+1$ corresponds to the next subscript, in
accordance to the lexicographic order. In that case, we write $n\prec n+1$.
$n+m$ is an abbreviation for $(...(...((n+1)+1)+...1)...)$ with $m$
occurrences of $+$ and $m$ occurrences of pairs of parentheses. Again we have
$n\prec n+m$. Besides, $\prec$ is a strict total order. That fact allows us to
talk about a minimum value between subscripts $m$ and $n$:
$\mbox{min}\\{m,n\\}$ is $m$ iff $m\prec n$, it is $n$ iff $n\prec m$, and it
is either one of them if $m=n$. Of course, $m=n$ iff $\neg(m\prec
n)\wedge\neg(n\prec m)$. If $m\prec n\vee m=n$, we denote this by $m\preceq
n$. Such a vocabulary of ten symbols endowed with $\prec$ is called here
(meta) language $\mathcal{L}$.

F7 provides us some sort of “recursive definition” for functions
$\varphi_{n}$, while it allows as well to guarantee the existence of inductive
functions: (i) $\varphi_{0}$ is such that $\varphi_{0}(x)$ is $\varphi_{0}$ if
$x=\varphi_{0}$ and $\underline{\mathfrak{0}}$ otherwise; (ii) $\varphi_{n+1}$
is such that $\varphi_{n+1}(\varphi_{n+1})=\varphi_{n+1}$,
$\varphi_{n+1}\neq\varphi_{n}$, and $\varphi_{n+1}(x)=\varphi_{n}(x)$ for any
$x$ different of $\varphi_{n+1}$.

Observe that
$\varphi_{n+1}(\varphi_{n})=\varphi_{n}(\varphi_{n})=\varphi_{n}$, while
$\varphi_{n}(\varphi_{n+1})=\underline{\mathfrak{0}}$. Moreover,
$\varphi_{n+2}(\varphi_{n+1})=\varphi_{n+1}$, and
$\varphi_{n+2}(\varphi_{n})=\varphi_{n+1}(\varphi_{n})=\varphi_{n}$; while
$\varphi_{n}(\varphi_{n+2})=\underline{\mathfrak{0}}$.

Figure 1 illustrates how to represent some functions $f$ in a quite intuitive
way. A diagram of $f$ is formed by a rectangle. On the left top corner inside
the rectangle we find label $f$. The remaining labels refer to terms $x$ such
that either $f(x)\neq\underline{\mathfrak{0}}$ ($f$ acts on $x$) or there is
$t$ such that $f(t)=x\neq\underline{\mathfrak{0}}$. Term
$\underline{\mathfrak{0}}$ never occurs in any diagram. For each $x$ inside
the rectangle there is a unique corresponding arrow which indicates the image
of $x$ by $f$, as long $x$ is not $f$ itself. Due to self-reference, label $f$
at the left top corner inside the rectangle does not need to be attached to
any arrow, to avoid redundancy.

From left to right, the first diagram in Figure 1 refers to $\varphi_{0}$. It
says, for any $x$, $\varphi_{0}(x)$ is $\underline{\mathfrak{0}}$, except for
$\varphi_{0}$ itself. The second diagram says
$\varphi_{1}(\varphi_{1})=\varphi_{1}$, and
$\varphi_{1}(\varphi_{0})=\varphi_{0}$. The circular arrow associated to
$\varphi_{0}$ in the second diagram says
$\varphi_{1}(\varphi_{0})=\varphi_{0}$ ($\varphi_{1}[\varphi_{0}]$). The third
diagram says $\varphi_{2}(\varphi_{2})=\varphi_{2}$,
$\varphi_{2}(\varphi_{1})=\varphi_{1}$, and
$\varphi_{2}(\varphi_{0})=\varphi_{0}$. Finally, for the sake of illustration,
the last diagram corresponds to an $f$ such that $f(a)=b$, $f(b)=c$, and
$f(c)=\underline{\mathfrak{0}}$. That is why there is no arrow ‘starting’ at
$c$. In those cases we represent $c$ outside the rectangle. The existence of
functions like that is granted by F10α some pages below. The diagrams of
$\underline{\mathfrak{0}}$ and $\underline{\mathfrak{1}}$ are, respectively, a
blank rectangle and a filled in black rectangle. Other examples are provided
in the next paragraphs.

\begin{picture}(60.0,50.0)\par\put(3.0,13.0){\framebox(50.0,40.0)[]{}}
\par\par\put(10.0,43.0){$\varphi_{0}$}
\par\par\put(63.0,13.0){\framebox(50.0,40.0)[]{}}
\par\par\put(70.0,43.0){$\varphi_{1}$}
\par\put(70.0,26.0){$\boldmath\curvearrowleft$}
\par\put(70.0,20.0){$\varphi_{0}$}
\par\par\put(123.0,13.0){\framebox(50.0,40.0)[]{}}
\par\par\put(130.0,43.0){$\varphi_{2}$}
\par\put(130.0,26.0){$\boldmath\curvearrowleft$}
\par\put(130.0,20.0){$\varphi_{0}$}
\par\put(160.0,26.0){$\boldmath\curvearrowleft$}
\par\put(160.0,20.0){$\varphi_{1}$} \par\put(190.0,30.0){$\cdots$}
\par\put(250.0,13.0){\framebox(50.0,40.0)[]{}} \par\put(255.0,43.0){$f$}
\par\put(255.0,23.0){$a$} \par\put(275.0,23.0){$b$} \par\put(315.0,23.0){$c$}
\par\put(282.0,26.0){\vector(2,0){30.0}}
\par\put(262.0,26.0){\vector(2,0){10.0}} \par\end{picture}

$\varphi_{0}$

$\varphi_{1}$

$\boldmath\curvearrowleft$

$\varphi_{0}$

$\varphi_{2}$

$\boldmath\curvearrowleft$

$\varphi_{0}$

$\boldmath\curvearrowleft$

$\varphi_{1}$

$\cdots$

$f$

$a$

$b$

$c$

Figure 1: From left to right, diagrams of $\varphi_{0}$, $\varphi_{1}$,
$\varphi_{2}$, and an arbitrary $f$.

Observe that $\varphi_{m+n}(\varphi_{n})=\varphi_{n}$, for any $m$ and $n$ of
$\mathcal{L}$.

###### Theorem 14

$\underline{\mathfrak{0}}$ and $\varphi_{0}$ are the only functions who do not
act on any $t$.

Proof

If $f$ does not act on any $t$, then $\forall t(t=f\vee
f(t)=\underline{\mathfrak{0}})$. Suppose $f$ is neither
$\underline{\mathfrak{0}}$ nor $\varphi_{0}$. Then there is $t$ such that
$t\neq f\wedge f(t)\neq\underline{\mathfrak{0}}$. But that entails $f[t]$
(Definition 1). So, the only functions which do not act on any $t$ are
$\underline{\mathfrak{0}}$ and $\varphi_{0}$.

###### Theorem 15

$\sigma_{\underline{\mathfrak{1}}}=\underline{\mathfrak{0}}$.

Proof

$\sigma_{\underline{\mathfrak{1}}}\neq\underline{\mathfrak{0}}\Rightarrow\underline{\mathfrak{1}}(\sigma_{\underline{\mathfrak{1}}})=\underline{\mathfrak{0}}$
(Definition 3). That happens only if
$\sigma_{\underline{\mathfrak{1}}}=\underline{\mathfrak{0}}$.

###### Theorem 16

For any $g$, $\sigma_{g}\neq\underline{\mathfrak{1}}$

Proof

Suppose there is $g$ such that $\sigma_{g}=\underline{\mathfrak{1}}$. Since
$\underline{\mathfrak{1}}\neq\underline{\mathfrak{0}}$, then
$g(\underline{\mathfrak{1}})=\underline{\mathfrak{0}}$ and
$\underline{\mathfrak{1}}(g)=g$, according to Definition 3. So,
$g\neq\underline{\mathfrak{1}}$. Once again from Definition 3,
$g(x)=\underline{\mathfrak{1}}(x)$ for any $x\neq\underline{\mathfrak{1}}$.
But those are the same conditions for
$\underline{\mathfrak{1}}\circ\underline{\mathfrak{1}}=g$, according to F5.
Since any $\mathfrak{F}$-composition is unique, then
$g=\underline{\mathfrak{1}}$ (Theorem 11), which contradicts the assumption
$g\neq\underline{\mathfrak{1}}$. So, there is no such $g$.

In other words, the existence of some ‘functions’ in Flow is forbidden.

###### Definition 5

For any function $f$, a restriction $g$ of $f$ is defined as

$g\subseteq f\;\;\mbox{iff}\;\;g\neq\underline{\mathfrak{0}}\wedge\forall
x((g[x]\Rightarrow f[x])\wedge((g[x]\wedge f[x])\Rightarrow f(x)=g(x))),$

Proper restrictions are defined as $g\subset f\;\;\mbox{iff}\;\;g\subseteq
f\wedge g\neq f$. We abbreviate $\neg(g\subseteq f)$ and $\neg(g\subset f)$
as, respectively, $g\not\subseteq f$ and $g\not\subset f$. For example,
$\varphi_{1}\subseteq\varphi_{3}$, $\varphi_{1}\subset\varphi_{3}$, and
$\varphi_{3}\not\subseteq\varphi_{1}$.

###### Theorem 17

$\forall f\forall g(g\subset f\Rightarrow g(f)=\underline{\mathfrak{0}})$.

Proof

Suppose $g(f)\neq\underline{\mathfrak{0}}$. Since $g\neq f$, then $g[f]$. But
for any $f$ we have $\neg f[f]$. In other words, $\neg(g[f]\Rightarrow f[f])$.
Hence, $g\not\subseteq f$.

Some of the most useful restrictions are obtained from a given formula $F$, in
a way which resembles the well known Separation Scheme in ZF. That is achieved
thanks to careful considerations regarding the $\mathfrak{F}$-successor
function $\sigma$. But before that, we need more concepts, since we are
interested on a vast number of situations.

###### Definition 6

A term $f$ is comprehensive iff there is $g$ such that
$g\neq\underline{\mathfrak{0}}$, $g\subseteq f$, and
$\sigma_{g}=\underline{\mathfrak{0}}$; and we denote that by $\mathbb{C}(f)$.
Otherwise, $f$ is uncomprehensive.

Comprehensive functions are supposed to describe “huge” functions who act on
“many terms”, and they are partially regulated by some of the the next axioms.
If $f$ itself is such that $\sigma_{f}=\underline{\mathfrak{0}}$, then $f$ is
comprehensive, except when $f=\underline{\mathfrak{0}}$. Besides, it is easy
to see that $\underline{\mathfrak{1}}$ is comprehensive and
$\underline{\mathfrak{0}}$ is uncomprehensive. On the other hand, there are
other comprehensive functions which, by the way, play an important role within
our proposal for building a model of ZFU. But for now we are mostly interested
on uncomprehensive functions, as it follows in the next Subsection.

###### Theorem 18

If $f\subseteq g$ and $f$ is comprehensive, then $g$ is comprehensive.

Proof

If $f$ is comprehensive, then there is $h$ such that
$h\neq\underline{\mathfrak{0}}$, $h\subseteq f$, and
$\sigma_{h}=\underline{\mathfrak{0}}$. Since $h\subseteq f\subseteq g$, then
$h\subseteq g$. Thus, $g$ is comprehensive.

###  2.2 Emergent functions

###### Definition 7

$\mathbb{E}(f)$ iff (i) $f\neq\sigma$; (ii)
$\sigma_{f}\neq\underline{\mathfrak{0}}$; (iii) $\forall
x(f[x]\Rightarrow\sigma_{x}\neq\underline{\mathfrak{0}})$; (iv) $\forall
y((\exists x(f(x)=y\wedge
y\neq\underline{\mathfrak{0}}))\Rightarrow\sigma_{y}\neq\underline{\mathfrak{0}})$.

We read $\mathbb{E}(f)$ as ‘$f$ is emergent’. $\varphi_{0}$ is vacuously
emergent. That entails $\varphi_{1}$ is emergent. Emergent functions are
supposed to be uncomprehensive terms who act only on uncomprehensive terms.
The behavior of emergent functions is regulated by the next axiom, F8.

###### Definition 8

$g\trianglelefteq f$ iff $g\neq\underline{\mathfrak{0}}\wedge\forall
x(g[x]\Rightarrow((f[x]\vee\exists a(f(a)=x))\wedge(f[g(x)]\vee\exists
b(f(b)=g(x)))))$. If $g\trianglelefteq f$, we say $g$ lurks $f$. Besides,
$g\triangleleft f$ iff $g\trianglelefteq f$ and $g\neq f$. In that case we say
$g$ properly lurks $f$. Finally, $\neg(g\trianglelefteq f)$ and
$\neg(g\triangleleft f)$ are abbreviated as $g\ntrianglelefteq f$ and
$g\ntriangleleft f$, respectively.

Last definition is a generalization of restriction, as it follows in the next
theorem. Besides, if $f$ is a function such that $f(f)=f$,
$f(\varphi_{0})=\varphi_{1}$, $f(\varphi_{1})=\varphi_{0}$ and
$f(r)=\underline{\mathfrak{0}}$ for the remaining values, then
$f\trianglelefteq\varphi_{2}$, $\varphi_{2}\trianglelefteq f$,
$f\trianglelefteq\varphi_{3}$, $\varphi_{3}\ntrianglelefteq f$.

###### Theorem 19

If $g\subseteq f$ and $g\neq\underline{\mathfrak{0}}$, then $g\trianglelefteq
f$.

The proof is straightforward. The converse is obviously not a theorem.

###### Definition 9

$h=\mathfrak{p}(f)$ iff $\forall x(h[x]\Leftrightarrow x\trianglelefteq f)$.
$h$ is the full power of $f$.

The full power $\mathfrak{p}(f)$ of $f$ acts on all terms $x$ who lurk $f$.

###### Theorem 20

If $f\subset\underline{\mathfrak{1}}$ acts on $n$ terms, then
$\mathfrak{p}(f)$ acts on $(n+1)^{n}$ terms.

Proof

If $f$ acts on $n$ terms $x_{i}$ and $g$ lurks $f$, each $x_{i}$ may
correspond to any $x_{j}$ (where eventually $x_{j}=x_{i}$) in the sense we may
have $g(x_{i})=x_{j}$. On the other hand, we may have
$g(x_{i})=\underline{\mathfrak{0}}$ as well. Thus, for each $x_{i}$ ($n$
possible values) there are $n+1$ possible images. So, there are $(n+1)^{n}$
terms who lurk $f$.

F8 - Cohesion

$\forall f(\mathbb{E}(f)\Rightarrow(\forall g((g\trianglelefteq
f\Rightarrow\sigma_{g}\neq\underline{\mathfrak{0}})\wedge\forall
h((h[g]\Leftrightarrow g\trianglelefteq
f)\Rightarrow\sigma_{h}\neq\underline{\mathfrak{0}}))\wedge\forall i(\forall
t(i[t]\Rightarrow\exists x(x[t]\wedge
f[x])))\Rightarrow\sigma_{i}\neq\underline{\mathfrak{0}})\wedge\mathbb{E}(\sigma_{f}))$.

If $f$ is emergent, then any $g$ (if it exists) who lurks $f$ has a
non-$\underline{\mathfrak{0}}$ $\mathfrak{F}$-successor. Function $h$ at F8
refers to the full power of $f$, if it exists. Term $i$ is useful for dealing
with arbitrary union, if we are able to define it. Finally, if $f$ is
emergent, so it is $\sigma_{f}$.

Observe F8 is an existence postulate. For understanding this, recall F6, which
provides necessary and sufficient conditions for knowing if
$\sigma_{f}\neq\underline{\mathfrak{0}}$: there must be a $g$ different of $f$
such that certain conditions are met. The point here is that F8 grants the
existence of certain terms which are $\mathfrak{F}$-successors of others, as
long some conditions are met. When we say, as above, that
$\sigma_{g}\neq\underline{\mathfrak{0}}$, we state there is a function
$z\neq\underline{\mathfrak{0}}$ such that $\sigma_{g}=z$. The same happens to
$\sigma_{h}$ and $\sigma_{i}$.

###  2.3 More about restrictions

###### Definition 10

Let $f$ be a function and $F(t)$ be a formula where all occurrences of $t$ are
free. We say $g$ is restriction of $f$ under $F(t)$, and denote this by
$g=f\big{|}_{F(t)}$, iff: (i) $g\neq\underline{\mathfrak{0}}$; (ii)
$f(\sigma_{g})=\underline{\mathfrak{0}}\vee\neg F(g)$; (iii) $g\neq
f\Rightarrow g(f)=\underline{\mathfrak{0}}$; (iv) $\forall t((t\neq f\wedge
t\neq g)\Rightarrow((g(t)=f(t)\wedge F(t)\wedge
f[t])\vee(g(t)=\underline{\mathfrak{0}}\wedge(\neg F(t)\vee\neg f[t]))))$.

Formula $g=f\big{|}_{F(t)}$ is somehow equivalent to $g\subseteq f$, as we see
in the next two theorems.

###### Theorem 21

If $g\subseteq f$, then it is possible to state a formula $F$ where
$g=f\big{|}_{F}$.

Proof

If $g\subseteq f$, assume as formula $F(t)$ the next one: $g[t]$. Item (i) of
Definition 10 is a consequence from Definition 5. Item (ii) of the same
definition is granted thanks to the fact that $\neg g[g]$ ($\neg F(g)$) for
any $g$. Item (iii) is due to Theorem 17. Finally, item (iv) is granted from
Definition 5.

###### Theorem 22

If $g=f\big{|}_{F}$, then $g\subseteq f$.

Proof

If $g=f\big{|}_{F}$, then either $g=\varphi_{0}$ or $g\neq\varphi_{0}$. In the
first case, the proof is immediate by vacuity ($\varphi_{0}$ does not act on
any term). If $g\neq\varphi_{0}$, then item (iv) of Definition 10 demands, for
any $t$, $g[t]\Rightarrow(f[t]\wedge g(t)=f(t))$. Thus, $g\subseteq f$.

A natural way of getting some restrictions $g$ of $f$ is through F9E below.
Observe as well item (iv) of Definition 10 takes into account the self-
reference postulate, since we demand $t\neq f\wedge t\neq g$. Now, if $F(t)$
is a formula (abbreviated by $F$) where all occurrences of $t$ are free, then
the following is an axiom.

F9E \- $\mathbb{E}$-Restriction

$\forall f\forall
x((F(x)\Rightarrow\mathbb{E}(x))\Rightarrow\exists!g(g=f\big{|}_{F}))$.

Subscript E highlights a strong commitment to emergent functions, although
there is no need of $f$ to be emergent. Many restrictions due to this last
postulate grant the existence of emergent functions. Next theorem, for
example, shows we do not need $\mathfrak{F}$-composition to prove there is
$\varphi_{0}$.

###### Theorem 23

$\underline{\mathfrak{0}}\big{|}_{F(x)}=\varphi_{0}$ if $\forall
x(F(x)\Rightarrow\mathbb{E}(x))$.

Proof

Immediate, since $\underline{\mathfrak{0}}$ does not act on any term and no
restriction can be $\underline{\mathfrak{0}}$.

###### Theorem 24

For any emergent $f$ we have: (i) $f\big{|}_{x\neq x}=\varphi_{0}$; (ii)
$f\big{|}_{x=x}=f$; (iii) $f\big{|}_{x\neq f}=f$; (iv)
$f\big{|}_{x=f}=\varphi_{0}$.

Proof

Item (i) is proven by vacuity. (ii) takes into account all terms where $f$
acts. Observe F8 grants any emergent function who acts on any term, acts on
emergent functions. About (iii) and (iv), recall $f$ plays no role into the
calculation of its restriction. All that matters are the terms where $f$ acts.

From F9E, there are four possible restrictions $g$ of $\varphi_{2}$. If $F(x)$
is, for example, “$x=\varphi_{0}$”, then $g=\varphi_{1}$. Accordingly, assume
$f=\varphi_{2}$ in F9E. So, consider, e.g., $x=\varphi_{0}$. Such a value for
$x$ is different of $\varphi_{2}$. Besides, $F(\varphi_{0})$. That implies
$g(\varphi_{0})=\varphi_{2}(\varphi_{0})=\varphi_{0}$. For all remaining
values $x\neq\varphi_{0}$, we know $g$ does not act on $x$. That means $g$
acts solely on $\varphi_{0}$. And according to F7, that function is supposed
to be $\varphi_{1}$. Observe $\varphi_{1}$ is allowed to have a free
occurrence in $F(x)$, according to our Restriction Axiom. Nevertheless $g$
does not act on $\varphi_{1}$ in our first example. That means either
$g(\varphi_{1})=\underline{\mathfrak{0}}$ or $g=\varphi_{1}$. In this case, we
have $g=\varphi_{1}$. Later on we define a membership relationship $\in$
(Definition 24) where $x\in f$ iff $f[x]$ and some conditions are imposed over
$f$. That entails we can guarantee that in a translation of ZF’s Separation
Scheme into Flow’s language, any free occurrence of $g$ in $F(x)$ will have no
impact (in a precise sense). After all, in this first example $F(x)$ is
$x=\varphi_{0}$, while $g$ is $\varphi_{1}$. For more details see Section 3.

Resuming the discussion about restrictions of $\varphi_{2}$, if $F(x)$ is the
formula “$x=\varphi_{0}\vee x=\varphi_{1}$”, then $g=\varphi_{2}$. If $F(x)$
is “$x=x$”, then again $g=\varphi_{2}$. If $F(x)$ is “$x\neq x$”, then
$g=\varphi_{0}$. The novelty here, however, happens with the formula $F(x)$
given by “$x=\varphi_{1}$”. In that case we have a proper restriction $\gamma$
such that $\gamma\neq\varphi_{1}$, $\gamma(\gamma)=\gamma$,
$\gamma(\varphi_{1})=\varphi_{1}$, and $\gamma(r)=\underline{\mathfrak{0}}$
for any remaining $r$ different of $\varphi_{1}$ and $\gamma$ itself. Thus,
$\gamma$ is a new function whose existence is granted thanks to F9E and no
other previous postulate. Besides, F8 grants $\gamma$ is emergent. Hence,
$\sigma_{\gamma}\neq\underline{\mathfrak{0}}$.

###### Definition 11

$z$ is the restricted power of $f\neq\underline{\mathfrak{0}}$ iff $\forall
x((x\neq z\wedge
x\neq\underline{\mathfrak{0}})\Rightarrow((z(x)=x\Leftrightarrow x\subseteq
f)\wedge(z(x)=\underline{\mathfrak{0}}\Leftrightarrow x\not\subseteq f)))$. We
denote $z$ as $\wp(f)$. We adopt the convention
$\wp(\underline{\mathfrak{0}})=\varphi_{0}$.

For example, $\wp(\varphi_{0})=\varphi_{1}$, $\wp(\varphi_{1})=\varphi_{2}$,
and $\wp(\varphi_{2})=f$, where $f(\varphi_{0})=\varphi_{0}$,
$f(\varphi_{1})=\varphi_{1}$, $f(\varphi_{2})=\varphi_{2}$,
$f(\gamma)=\gamma$, $f(f)=f$, and $f(x)=\underline{\mathfrak{0}}$ for the
remaining values $x$. Recall $\gamma$ acts only on $\varphi_{1}$ and
$\gamma(\varphi_{1})=\varphi_{1}$.

Observe $z=\wp(f)$ is a restriction of $\underline{\mathfrak{1}}$, even if $f$
is not. Besides, $\wp$ is not a function, but a metalinguistic symbol which
helps us to abbreviate the formula $z=\wp(f)$ given by the definition above.
Observe as well $\wp(f)\subseteq\mathfrak{p}(f)$, for any $f$. While
$\mathfrak{p}(f)$ refers to a function who acts on all terms that lurk $f$,
$\wp(f)$ acts on all terms that lurk $f$ as long they are restrictions of $f$.

###### Observation 3

In a sense, F9E is similar to the Separation Scheme in ZFC, since it states
the existence of a unique $g$ obtained from a given $f$ and a formula $F(x)$.
Nevertheless, the role of Separation Scheme in ZFC is not limited to grant the
existence of subsets of a given set. Thanks to that postulate, ZFC avoids
antinomies like Russell’s paradox. In our case those antinomies are avoided by
means of the simple use of Self-Reference (Observation 1). That is one of the
reasons why we do not prohibit free occurrences of $g$ in $F(x)$ (like what
happens in ZFC). Actually, if we demanded no free occurrences of $g$ in
$F(x)$, we would be unable to obtain some useful restrictions, as we can see
in the examples below. Nevertheless, we demand $\forall x((x\neq g\wedge x\neq
f)\Rightarrow((f(x)=g(x)\wedge
F(x))\vee(g(x)=\underline{\mathfrak{0}}\wedge\neg F(x)))$ (Definition 10),
which is a weaker condition than the prohibition of occurrences of $g$ in
$F(x)$. If we recall Observation 1, we can easily see that, for any $y$ and
any $r$, neither $y\big{|}_{x(x)\neq y}$ nor $y\big{|}_{x(x)\neq r}$ allow us
to get any contradiction in the style of Russell’s paradox. Finally, if anyone
tries to “define” a function $f$ from a formula $F(x)$ without using F9E, it
is perfectly possible to get a contradiction. For example, we can “define” a
function $f$ as it follows: $\forall x(f(x)=\varphi_{0})$. Since no $f$ acts
on $\underline{\mathfrak{0}}$, we have a contradiction, namely,
$f(\underline{\mathfrak{0}})=\varphi_{0}$. Nevertheless, that would not be a
definition at all, but simply a new postulate which is inconsistent with our
axioms. Definitions are supposed to be conservative, in the sense of not
allowing new theorems [4].

###### Definition 12

$f\sim g$ iff $\forall t((f[t]\Leftrightarrow g[t])\wedge((t\neq f\wedge t\neq
g)\Rightarrow f(t)=g(t)))$.

If $f\sim g$ but $f\neq g$, we say $f$ and $g$ are clones, as discussed in
Observation 2. Regarding their images, clones $f$ and $g$ differ solely on $f$
and $g$: $f(g)=\underline{\mathfrak{0}}$, while $g(g)=g$, and
$g(f)=\underline{\mathfrak{0}}$, while $f(f)=f$. It is easy to see that $\sim$
is reflexive.

###### Theorem 25

Let $f$ be emergent. Then, for any $h\neq\underline{\mathfrak{0}}$, $h\sim f$
entails $h=f$.

Proof

From Theorem 24, $f=f\big{|}_{t=t}$. Since $h\sim f$, $h=f\big{|}_{t=t}$ as
well. But F9E says any restriction is unique. Thus, $h=f$.

This last theorem grants $\underline{\mathfrak{0}}$ and $\varphi_{0}$ are the
only clones in Flow, at least among emergent functions.

###### Theorem 26

$\forall f(\varphi_{0}\subseteq f).$

Proof

Theorem 14 states $\varphi_{0}$ is the only function different of
$\underline{\mathfrak{0}}$ who do not act on any term. Thus, Definition 5
grants formula above is proven by vacuity.

###### Theorem 27

For any $x$ and $y$, $x\subset y$ entails $y\not\subset x$.

Proof

If $x$ and $y$ are, respectively, $\varphi_{0}$ and
$\underline{\mathfrak{0}}$, the proof is straightforward, since
$\underline{\mathfrak{0}}$ is never any restriction, according to F9E and
Definition 5. For the remaining cases, $x\subset y$ entails $x\neq y$ and, for
any $t$, $x[t]\Rightarrow(y[t]\wedge x(t)=y(t))$. So, there is $t^{\prime}$
where $y[t^{\prime}]\wedge\neg x[t^{\prime}]$ or $y[t^{\prime}]\wedge
x[t^{\prime}]\wedge x(t^{\prime})\neq y(t^{\prime})$. In anyone of those cases
we have $y\not\subset x$.

###### Theorem 28

$\sigma$ and $\underline{\mathfrak{0}}$ are the only functions $f$ such that
$\sigma_{f}=f$.

Proof

We already know $\sigma_{\sigma}=\sigma$ (F2) and
$\sigma_{\underline{\mathfrak{0}}}=\underline{\mathfrak{0}}$ (Theorem 10). If
$f\neq\underline{\mathfrak{0}}$ and $\sigma_{f}=\underline{\mathfrak{0}}$,
then $\sigma_{f}\neq f$. If $f\neq\sigma$, $f\neq\underline{\mathfrak{0}}$ and
$\sigma_{f}\neq\underline{\mathfrak{0}}$, then F6 and Definition 3 demand
$\sigma_{f}\neq f$. Observe as well there is no clone of $\sigma$, according
to F6, although $\sigma$ is not emergent.

###### Theorem 29

$\forall f(\mathbb{E}(f)\Rightarrow f=\sigma_{f}\big{|}_{x\neq f})$.

Proof

$\mathbb{E}(f)$ entails $\sigma_{f}\neq\underline{\mathfrak{0}}$. So,
$\sigma_{f}$ acts on all terms where $f$ acts. But $\sigma_{f}$ acts on just
one more term: $f$ itself. Since formula $F(x)$ in the restriction above is
“$x\neq f$” (observe we follow all demands for $F(x)$ in F9E), then
$\sigma_{f}\big{|}_{x\neq f\wedge}$ acts exactly on all terms where $f$ acts.
Besides, they share all their images, according to F9E. So,
$\sigma_{f}\big{|}_{x\neq f}=f$, since $f[x]\Rightarrow x\neq f$.

###### Definition 13

Let $f$ be a restriction of $\underline{\mathfrak{1}}$ where $\forall g\forall
t((f[g]\wedge g[t])\Rightarrow\mathbb{E}(t))$. The arbitrary union of all
terms $g$ where $f$ acts (or arbitrary union of $f$, for short) is defined as
$u=\bigcup_{f[g]}g=\underline{\mathfrak{1}}\big{|}_{\exists g(f[g]\wedge
g[t])}$.

The idea of arbitrary union is as it follows. If $f$ acts on any $g$ which
acts on any $x$, then $u$ acts on that very same $x$; and if no $g$ acts on a
given $x$, then $u$ does not act on that $x$. Particularly, we write $u=g\cup
h$ for the case where $f$ acts at most on $g$ and $h$.

###### Definition 14

Let $f$ be a restriction of $\underline{\mathfrak{1}}$ where $\forall g\forall
t((f[g]\wedge g[t])\Rightarrow\mathbb{E}(t))$. Then the arbitrary intersection
of $f$ is given by $\bigcap_{f[g]}g=\underline{\mathfrak{1}}\big{|}_{\forall
g(f[g]\Rightarrow g[t])}.$

Observe the definition above is equivalent to
$\bigcap_{f[g]}g=\left(\bigcup_{f[g]}g\right)\big{|}_{\forall
g(f[g]\Rightarrow g[t])}$. If $f$ acts only on $g$ and $h$, the arbitrary
intersection may be written as $g\cap h$. In particular, for any $m$ and $n$
from language $\mathcal{L}$,
$\varphi_{m}\cap\varphi_{n}=\varphi_{m}\circ\varphi_{n}$.

###### Theorem 30

$\bigcup_{\underline{\mathfrak{0}}[g]}=\bigcup_{\varphi_{0}[g]}=\bigcup_{\varphi_{1}[g]}=\varphi_{0}$.

Proof is straightforward. Last identity from last theorem illustrates our
previous claim that it is possible the union $u$ be one of the terms where $f$
does act: $\varphi_{1}$ acts on $\varphi_{0}$, and
$\bigcup_{\varphi_{1}[g]}=\varphi_{0}$.

###  2.4 Ordinals

###### Definition 15

Let $F(t)$ be the formula
$t\subseteq\underline{\mathfrak{1}}\wedge\mathbb{E}(t)\wedge\forall
r(t[r]\Rightarrow r\subseteq t)\wedge\forall r\forall s((t[r]\wedge
t[s])\Rightarrow(r=s\vee r[s]\vee s[r]))\wedge\forall r((r\subseteq
t\wedge\exists s(r[s]))\Rightarrow\exists m(r[m]\wedge\forall
x(r[x]\Rightarrow\neg m[x])))$. Then,
$\varpi=\underline{\mathfrak{1}}\big{|}_{F(t)}$ is called the ordinal
function. Moreover, if $\varpi[t]$, we say $t$ is an ordinal.

The ordinal function $\varpi$ is defined from a conjunction of five formulas:
any ordinal is supposed to be a restriction of $\underline{\mathfrak{1}}$ and
emergent and transitive and totaly ordered by actions and well-ordered by
actions (term $m$ above is the least element with respect to actions). The
first two formulas are obviously satisfied by $\varphi_{0}$. The remaining
ones are satisfied by vacuity. Thus, $\varphi_{0}$ is an ordinal. That fact
entails any $\varphi_{n}$ is an ordinal. In order to grant we are talking
about ordinals in an usual sense, we prove the next theorems.

###### Theorem 31

Every ordinal acts only on ordinals.

Proof

All we have to prove is $\forall r(\forall t(\varpi[t]\wedge
t[r])\Rightarrow\varpi[r])$. Formula $F(t)$ from Definition 15 is a
conjunction of five formulas. So, this proof is divided into five parts, where
we assume $t$ is an ordinal: (i) we know $(\varpi[t]\wedge t[r])\Rightarrow
r\subseteq t$. Since $t\subseteq\underline{\mathfrak{1}}$, then
$r\subseteq\underline{\mathfrak{1}}$. That means the first formula in the five
factors conjunction $F(t)$ is satisfied when we replace $t$ by $r$. (ii)
According to F8, any restriction $r$ of an emergent function $t$ is emergent.
Thus, since $t[r]\Rightarrow r\subseteq t$, then $\mathbb{E}(r)$. That settles
the second condition from $F(t)$. (iii) We know $(\varpi[t]\wedge
t[r])\Rightarrow r\subseteq t$. Thus, if $r[s]$, then $t[s]$. That entails
$s\subseteq t$. Now, suppose $s\not\subseteq r$. Then, $\exists
y(s[y]\wedge\neg r[y])$. Since $t[r]\wedge t[y]$, then $r=y\vee y[r]\vee
r[y]$. Nevertheless, the possibilities $r[y]$ and $r=y$ cannot take place. So,
we must have $y[r]$. Therefore, $r[s]\wedge s[y]\wedge y[r]$, where $t$ acts
on all of them: $r$, $s$, and $y$. Now, let $m$ be a restriction of $t$ who
acts only on $r$, $s$, and $y$. Therefore, last formula of the five factor
conjunction $F(t)$ cannot be satisfied for $m$ (there is no least term with
respect to actions of $m$ on $r$, $s$, and $y$). In other words, our
hypothesis $s\not\subseteq r$ leads to a contradiction. Thus, $s\subseteq r$.
(iv) We know $(\varpi[t]\wedge t[r])\Rightarrow r\subseteq t$. Thus,
$(r[u]\wedge r[v])\Rightarrow(t[u]\wedge t[v])$. So, from the definition of
$\varpi$, $u=v\vee u[v]\vee v[u]$. (v) We know $(\varpi[t]\wedge
t[r])\Rightarrow r\subseteq t$. If $u\subseteq r$, then $u\subseteq t$. So, if
$u$ acts on at least one term, then last condition of $F(t)$ is satisfied when
we replace $t$ by $r$.

###### Theorem 32

If $t$ is an ordinal, then $\sigma_{t}$ is an ordinal.

Proof

Analogously to last theorem, we split this proof into five parts. (i) If $t$
is an ordinal, then it is emergent. According to F8, the
$\mathfrak{F}$-successor of any emergent function is emergent. That entails
$\sigma_{t}\neq\underline{\mathfrak{0}}$. (ii) If
$t\subseteq\underline{\mathfrak{1}}$, then
$\sigma_{t}\subseteq\underline{\mathfrak{1}}$. (iii) Since
$\sigma_{t}\neq\underline{\mathfrak{0}}$, then $\sigma_{t}[t]$ and $\forall
r(\sigma_{t}[r]\Rightarrow r\subseteq\sigma_{t})$. Last two parts are
straightforward.

###### Theorem 33

The ordinal function $\varpi$ is comprehensive.

Proof

Suppose $\sigma_{\varpi}\neq\underline{\mathfrak{0}}$. If $F(t)$ is the
formula used in the definition of $\varpi$, then $F(\varpi)$. But according to
item (ii) of Definition 10, that entails
$\underline{\mathfrak{1}}(\sigma_{\varpi})=\underline{\mathfrak{0}}$. Such a
condition is satisfied only for $\sigma_{\varpi}=\underline{\mathfrak{0}}$, a
contradiction. Therefore, $\varpi$ cannot be emergent, although it acts only
on emergent terms.

###### Definition 16

An ordinal $t$ is a limit ordinal iff $\nexists r(\sigma_{r}=t)$.

In particular, $\varphi_{0}$ is a limit ordinal.

###### Theorem 34

Any ordinal is well-ordered with respect to actions.

Proof

We adopt the next convention: if $r$ and $s$ are ordinals, $r$ is lesser than
$s$ iff $s[r]$. Trichotomy, transitivity, and the existence of a least element
(with respect to actions) are straightforward consequences from Definition 15.

###### Definition 17

The least limit ordinal who acts on $\varphi_{0}$ is denoted by $\omega$. We
say $r$ is a finite ordinal iff $\omega[r]$.

###### Theorem 35

If $r$ is an ordinal, then there is a limit ordinal $s$ such that $s[r]$.

Proof

Analogous to standard literature [15].

###  2.5 ZF-sets

It is convenient to introduce the next concepts.

###### Definition 18

If $\mathbb{E}(f)$ and $f$ acts solely on emergent functions,
$Dom_{f}^{\mathfrak{F}}=\underline{\mathfrak{1}}\big{|}_{f[t]}$ and
$Im_{f}^{\mathfrak{F}}=\underline{\mathfrak{1}}\big{|}_{\exists x(f[x]\wedge
f(x)=t)}$ are, respectively, the $\mathfrak{F}$-domain and the
$\mathfrak{F}$-image of $f$. We denote $f$ as $f:Dom_{f}^{\mathfrak{F}}\to
Im_{f}^{\mathfrak{F}}$.

When we write $f:x\to y$, that means $x=Dom_{f}^{\mathfrak{F}}$ and
$y=Im_{f}^{\mathfrak{F}}$, as long $f$ is emergent. We write
$Dom^{\mathfrak{F}}_{f}$ and $Im^{\mathfrak{F}}_{f}$ instead of $Dom_{f}$ and
$Im_{f}$ due to the fact we want to compare $\mathfrak{F}$-domain and
$\mathfrak{F}$-image with the usual notions of domain and image (range) of a
function in a theory like ZFU, for example. Details in Subsection 2.8.

Now, let $\alpha(x,y)$ be a formula where there is at least one occurrence of
$x$, one occurrence of $y$, and all of them are free. Then, next formula is an
axiom.

F10α \- Creation

$\forall x\exists!y(\alpha(x,y))\Rightarrow\forall
f(\mathbb{E}(f)\Rightarrow\exists!g(\forall x\forall y((\alpha(x,y)\wedge
x\neq g)\Rightarrow((f[x]\Rightarrow g(x)=y)\wedge(\neg f[x]\Rightarrow
g(x)=\underline{\mathfrak{0}})))\wedge\sigma(g)\neq\underline{\mathfrak{0}}\wedge\sigma(Im_{g}^{\mathfrak{F}})\neq\underline{\mathfrak{0}}\wedge(f[g]\Rightarrow\neg\alpha(g,f(g)))))$.

We employed the notation $\sigma(g)$ instead of $\sigma_{g}$ due to
limitations in the LaTeX editor of this text, particularly for the case of
$\mathfrak{F}$-successor of the $\mathfrak{F}$-image of $g$.

Last postulate is supposed to define functions $g$ from certain formulas
$\alpha$ and any $f$, as long $f$ is emergent. We say $g$ is created by $f$
and $\alpha(x,y)$, and denote this by $g=f\big{|}^{\alpha(x,y)}$ or, simply,
$g=f\big{|}^{\alpha}$. Besides, $g$ is emergent, as well as its
$\mathfrak{F}$-image (and consequently its $\mathfrak{F}$-domain). Last
conjunction in F10α avoids ambiguities in the calculation of $g$. Postulate
F10α motivates us to employ an alternative notation for functions. When we see
fit to do so, we may eventually write $a\stackrel{{\scriptstyle
f}}{{{}_{\longmapsto}}}b$ meaning $f(a)=b$. One obvious advantage of this
notation $a\stackrel{{\scriptstyle x}}{{{}_{\longmapsto}}}b$ is that it can be
used to easily write down strings like $a_{1}\stackrel{{\scriptstyle
f}}{{{}_{\longmapsto}}}a_{2}\stackrel{{\scriptstyle
f}}{{{}_{\longmapsto}}}a_{3}\stackrel{{\scriptstyle
f}}{{{}_{\longmapsto}}}\cdot\cdot\cdot$, meaning $f(a_{1})=a_{2}$,
$f(a_{2})=a_{3}$, and so on. We adopt the next convention: every time we state
a finite sequence like either $a_{1}\stackrel{{\scriptstyle
f}}{{{}_{\longmapsto}}}a_{2}\stackrel{{\scriptstyle
f}}{{{}_{\longmapsto}}}a_{3}\stackrel{{\scriptstyle
f}}{{{}_{\longmapsto}}}\cdot\cdot\cdot\stackrel{{\scriptstyle
f}}{{{}_{\longmapsto}}}a_{n}\stackrel{{\scriptstyle
f}}{{{}_{\longmapsto}}}\underline{\mathfrak{0}}$ or
$a_{1}\stackrel{{\scriptstyle
f}}{{{}_{\longmapsto}}}a_{2}\stackrel{{\scriptstyle
f}}{{{}_{\longmapsto}}}a_{3}\stackrel{{\scriptstyle
f}}{{{}_{\longmapsto}}}\cdot\cdot\cdot\stackrel{{\scriptstyle
f}}{{{}_{\longmapsto}}}a_{n}\stackrel{{\scriptstyle
f}}{{{}_{\longmapsto}}}a_{i}$ ($i$ is any value among terms from $1$ to $n$),
we assume $f(f)=f$ and $f(r)=\underline{\mathfrak{0}}$ if $r$ is different of
all previous terms already stated.

F10α allows us to get restrictions by other means besides F9E. For example,
from F10α there is a $g$ such that $\varphi_{1}\stackrel{{\scriptstyle
g}}{{{}_{\longmapsto}}}\varphi_{2}\stackrel{{\scriptstyle
g}}{{{}_{\longmapsto}}}\varphi_{3}\stackrel{{\scriptstyle
g}}{{{}_{\longmapsto}}}\underline{\mathfrak{0}}$. In that case
$g\subset\sigma$. Function $g$ could be created from, e.g., $\varphi_{4}$ and
an appropriate formula $\alpha$.

With the aid of F10α it is quite easy to show $\mathfrak{F}$-composition is
not commutative. As an example, consider $f$ as a function given by
$\varphi_{1}\stackrel{{\scriptstyle
f}}{{{}_{\longmapsto}}}\varphi_{2}\stackrel{{\scriptstyle
f}}{{{}_{\longmapsto}}}\varphi_{2}$ and $g$ given by
$\varphi_{2}\stackrel{{\scriptstyle
g}}{{{}_{\longmapsto}}}\varphi_{3}\stackrel{{\scriptstyle
g}}{{{}_{\longmapsto}}}\varphi_{3}$. In that case $g\circ f$ is given by
$\varphi_{1}\stackrel{{\scriptstyle g\circ
f}}{{{}_{\longmapsto}}}\varphi_{3}\stackrel{{\scriptstyle g\circ
f}}{{{}_{\longmapsto}}}\underline{\mathfrak{0}}$ and
$\varphi_{2}\stackrel{{\scriptstyle g\circ
f}}{{{}_{\longmapsto}}}\varphi_{3}\stackrel{{\scriptstyle g\circ
f}}{{{}_{\longmapsto}}}\underline{\mathfrak{0}}$, while $f\circ g$ is simply
$\varphi_{0}$ (which is obviously different of $g\circ f$).

It is worth to remark there are some functions which cannot exist (besides
those already discussed), as we can see in the next theorem.

###### Theorem 36

There is no $x$ where, for a given $t\neq\underline{\mathfrak{1}}$,
$t\stackrel{{\scriptstyle
x}}{{{}_{\longmapsto}}}\underline{\mathfrak{1}}\stackrel{{\scriptstyle
x}}{{{}_{\longmapsto}}}t$.

Proof

Suppose there is such a function $x$. Then, from F5, $x\circ x$ is given by
$t\stackrel{{\scriptstyle x\circ x}}{{{}_{\longmapsto}}}t$ and
$\underline{\mathfrak{1}}\stackrel{{\scriptstyle x\circ
x}}{{{}_{\longmapsto}}}\underline{\mathfrak{1}}$. But from Theorem 5 we have
that any function $h$ such that
$h(\underline{\mathfrak{1}})=\underline{\mathfrak{1}}$ entails
$h=\underline{\mathfrak{1}}$. Thus, $x\circ x$ is supposed to be
$\underline{\mathfrak{1}}$. But since $x$ is different of
$\underline{\mathfrak{1}}$, then $x\circ x$ cannot be
$\underline{\mathfrak{1}}$, according to Theorem 12. That is a contradiction!

###### Theorem 37

$\forall f(\mathbb{E}(f)\Rightarrow\exists!g(g=f\big{|}_{F}))$.

Proof

Since $f$ is emergent, we can use F10α. Let $\alpha(x,y)$ be the next formula:
$(F(x)\Rightarrow f(x)=y)\wedge(\neg F(x)\Rightarrow
y=\underline{\mathfrak{0}})$. In that case,
$f\big{|}^{\alpha}=f\big{|}_{F}=g$. Concerning the uniqueness of $g$, that is
granted by F10α.

Next we use the axioms of Creation and Restriction to define ZF-sets, who are
supposed to play the same role sets play in ZF set theory.

###### Definition 19

Let $\alpha(u,v)$ be a formula recursively defined as it follows:

i

$\alpha(\varphi_{0},\varphi_{0})$;

ii

$\forall u\forall
v(\varpi[u]\Rightarrow(\alpha(u,v)\Rightarrow\alpha(\sigma_{u},\wp(v))))$;

iii

$\forall u((\varpi[u]\wedge\nexists
x(\sigma_{x}=u))\Rightarrow\alpha(u,\underline{\mathfrak{1}}\big{|}_{\exists
r\exists v(u[r]\wedge\alpha(r,v)\wedge v[t])}))$;

iv

$\forall u((\neg\varpi[u])\Leftrightarrow\alpha(u,\underline{\mathfrak{0}}))$.

v

$\forall u\forall v\forall w((\alpha(u,v)\wedge\alpha(u,w))\Rightarrow v=w)$.

If $\eta=r\big{|}^{\alpha}$, where $r$ is an ordinal, we say $\eta$ is a von
Neumann function with rank $r$. For the sake of abbreviation, any von Neumann
function with rank $r$ is denoted by $\eta_{r}$.

As an example consider $\eta_{\varphi_{4}}$. That is a function given by
$\varphi_{0}\stackrel{{\scriptstyle\eta_{\varphi_{4}}}}{{{}_{\longmapsto}}}\varphi_{0}$,
$\varphi_{1}\stackrel{{\scriptstyle\eta_{\varphi_{4}}}}{{{}_{\longmapsto}}}\varphi_{1}$,
$\varphi_{2}\stackrel{{\scriptstyle\eta_{\varphi_{4}}}}{{{}_{\longmapsto}}}\varphi_{2}$,
$\varphi_{3}\stackrel{{\scriptstyle\eta_{\varphi_{4}}}}{{{}_{\longmapsto}}}\wp(\varphi_{2})$,
where $\wp(\varphi_{0})=\varphi_{1}$, $\wp(\varphi_{1})=\varphi_{2}$, and
$\wp(\varphi_{2})$ is a restriction of $\underline{\mathfrak{1}}$ who acts
only on $\varphi_{0}$, $\varphi_{1}$, $\varphi_{2}$ and $\gamma$, where
$\gamma$ acts only on $\varphi_{1}$.

###### Theorem 38

For any ordinal $r$ and any $t$ such that $r[t]$, $\eta_{r}(t)$ is emergent
and a restriction of $\underline{\mathfrak{1}}$.

Proof

Observe we are not saying that any $\eta_{r}$ is a restriction of
$\underline{\mathfrak{1}}$, but only their $\mathfrak{F}$-images. We prove
this by transfinite induction. Let $\alpha$ be the formula from Definition 19.
The first ordinal $r$ is $\varphi_{0}$. F10α trivially says
$\varphi_{0}\big{|}^{\alpha}=\varphi_{0}$. That entails
$\eta_{\varphi_{0}}=\varphi_{0}$. Since $\varphi_{0}$ does not act on any
term, then it satisfies the theorem by vacuity. For the sake of argument, next
ordinal $\varphi_{1}$ is the first one who acts on some term. In that case,
$\eta_{\varphi_{1}}=\varphi_{1}$. The only term where $\varphi_{1}$ acts is
$\varphi_{0}$. Besides, $\varphi_{1}(\varphi_{0})=\varphi_{0}$. And
$\varphi_{0}$ is emergent and a restriction of $\underline{\mathfrak{1}}$.
Now, suppose all non-$\underline{\mathfrak{0}}$ images of a given $\eta_{r}$
are emergent and restrictions of $\underline{\mathfrak{1}}$. As we could see,
that takes place with the first two ordinals. Since $r$ is an ordinal and any
ordinal acts only on ordinals (Theorem 31), then,
$\eta_{r}(\sigma_{t})=\wp(\eta_{r}(t))$, for any ordinal $t$ where $r$ acts,
as long $r$ acts on $\sigma_{t}$ besides $t$. From F8 (see function $h$ in
that axiom), $\wp(\eta_{r}(t))$ is emergent. Besides, from the very definition
of restricted power (Definition 11), $\wp(\eta_{r}(t))$ is a restriction of
$\underline{\mathfrak{1}}$. An analogous result holds for $\eta_{\sigma_{r}}$,
since $\sigma_{r}$ acts on all terms where $r$ acts and on $r$ itself. In the
case where $u$ is a limit ordinal (item iii of Definition 19), then
$\eta_{\sigma_{u}}(u)=\underline{\mathfrak{1}}\big{|}_{\exists r\exists
v(u[r]\wedge\alpha(r,v)\wedge v[t])}$. But, according to F8 (see function $i$
in that postulate), that last term is emergent. Besides, it is trivially a
restriction of $\underline{\mathfrak{1}}$.

###### Definition 20

(i) $\nu=\underline{\mathfrak{1}}\big{|}_{\exists
r(\varpi[r]\wedge\eta_{\sigma_{r}}(r)=t)}$ is the von Neumann universe; (ii)
$\forall u(\mathbb{Z}(u)\Leftrightarrow\exists t(\nu[t]\wedge t[u]))$; we read
$\mathbb{Z}(u)$ as ‘$u$ is a ZF-set’.

###### Theorem 39

Every ordinal is a ZF-set.

Proof

For any ordinal $r$, $\eta_{\sigma_{\sigma_{r}}}(\sigma_{r})$ acts on $r$
(although it may act on other terms as well), according to Definition 19. So,
from Definition 20, $\mathbb{Z}(r)$.

###### Theorem 40

If $\nu$ is the von Neumann universe, then
$\sigma_{\nu}=\underline{\mathfrak{0}}$.

Proof

From Theorem 39, $\varpi\subset\nu$. From Theorem 33,
$\sigma_{\varpi}=\underline{\mathfrak{0}}$. So, from Theorem 18, $\nu$ is
comprehensive. Suppose $\sigma_{\nu}\neq\underline{\mathfrak{0}}$. Then, $\nu$
is emergent, since it acts only on terms with non-$\underline{\mathfrak{0}}$
$\mathfrak{F}$-successor. Thus, from F8, every restriction of $\nu$ has a
non-$\underline{\mathfrak{0}}$ $\mathfrak{F}$-successor. But $\varpi$ is a
restriction of $\nu$ and $\sigma_{\varpi}=\underline{\mathfrak{0}}$, a
contradiction. Therefore, $\sigma_{\nu}=\underline{\mathfrak{0}}$.

###### Theorem 41

$\forall u(\mathbb{Z}(u)\Leftrightarrow\exists r(\varpi[r]\wedge
u\subseteq\eta_{\sigma_{r}}(r)))$.

Proof

From Definition 20, $\mathbb{Z}(u)\Leftrightarrow\exists r\exists
t(\varpi[r]\wedge\eta_{\sigma_{r}}(r)[t]\wedge t[u])$. From Definition 19,
item (ii), $\eta_{\sigma_{\sigma_{r}}}(\sigma_{r})=\wp(\eta_{\sigma_{r}}(r))$.
Hence, for any $x$, $\eta_{\sigma_{\sigma_{r}}}(\sigma_{r})[x]\Leftrightarrow
x\subseteq\eta_{\sigma_{r}}(r)$.

###### Definition 21

The rank of a ZF-set $u$ is the least ordinal $r$ such that
$u\subseteq\eta_{\sigma_{r}}(r)$. We denote this by $r=\mathtt{rank}(u)$.

As an example, consider a function $a$ such that $b\stackrel{{\scriptstyle
a}}{{{}_{\longmapsto}}}b$, where $\varphi_{1}\stackrel{{\scriptstyle
b}}{{{}_{\longmapsto}}}\varphi_{1}$. The rank of $a$ is $\varphi_{3}$, while
the rank of $b$ is $\varphi_{2}$, and the rank of $\varphi_{1}$ is
$\varphi_{1}$.

###### Theorem 42

$\forall u(\mathbb{Z}(u)\Rightarrow\forall
x(u[x]\Rightarrow\mathtt{rank}(u)[\mathtt{rank}(x)]))$.

Proof

Straightforward from Theorem 41 and the definition of rank of a ZF-set.

Last theorem, in a sense, resembles the definition of rank of a set in [23].

###### Theorem 43

$\forall
f(\mathbb{Z}(f)\Leftrightarrow(\sigma_{f}\neq\underline{\mathfrak{0}}\wedge
f\subseteq\underline{\mathfrak{1}}\wedge\forall
x(f[x]\Rightarrow\mathbb{Z}(x)))$.

Proof

The $\Rightarrow$ part is a direct consequence from Theorem 38 and Definition
20. For the $\Leftarrow$ part, we already know $f$ is emergent, since
$\sigma_{f}\neq\underline{\mathfrak{0}}$ and $f$ acts only on ZF-sets. That
entails we can use F10α to create a function $g$ from $f$, if an adequate
formula $\beta$ is used. For that purpose, consider formula $\beta(x,y)$ given
by “$(f[x]\Rightarrow y=\mathtt{rank}(x))\wedge(\neg f[x]\Rightarrow
y=\underline{\mathfrak{0}})$”. According to F10α,
$\sigma(Im_{g}^{\mathfrak{F}})\neq\underline{\mathfrak{0}}$. On the other
hand, $Im_{g}^{\mathfrak{F}}$ is a restriction of $\varpi$. Therefore,
$Im_{g}^{\mathfrak{F}}$ is a ZF-set (Theorem 39). Now, let
$r=\mathtt{rank}(Im_{g}^{\mathfrak{F}})$. That entails $r$ acts on the rank of
any term $x$ where $f$ acts, i.e., $\forall x(f[x]\Rightarrow
r[\mathtt{rank}(x)])$. Now, suppose $f$ is no restriction of
$\eta_{\sigma_{r}}(r)$ (see Theorem 41). That entails there is $u$ such that
$f[u]\wedge\neg\eta_{\sigma_{r}}(r)[u]$ (remember $u$ is supposed to be a ZF-
set). Since $\neg\eta_{\sigma_{r}}(r)[u]$, then $\mathtt{rank}(u)[r]$, which
entails $\neg r[\mathtt{rank}(u)]$. That contradicts the fact that $\forall
x(f[x]\Rightarrow r[\mathtt{rank}(x)])$. Thus, indeed
$f\subseteq\eta_{\sigma_{r}}(r)$. From Theorem 41, $f$ is a ZF-set.

###### Theorem 44

$u=\underline{\mathfrak{1}}\big{|}_{\mathbb{Z}(t)}$ is comprehensive.

Proof

Suppose $\sigma_{u}\neq\underline{\mathfrak{0}}$. Then, according to Theorem
43, $u$ is a ZF-set. Thus, $\sigma_{u}=u$, a contradiction.

###### Definition 22

$f$ is an ordered pair $(a,b)$, with both values $a$ and $b$ different of
$\underline{\mathfrak{0}}$, iff there are $\alpha$ and $\beta$ such that
$\alpha\neq f$, $\beta\neq f$, $\alpha\neq a$, $\beta\neq b$ and

$f(x)=\left\\{\begin{array}[]{cl}\alpha&\mbox{if}\;x=\alpha\\\
\beta&\mbox{if}\;x=\beta\\\ \underline{\mathfrak{0}}&\mbox{if}\;x\neq f\wedge
x\neq\alpha\wedge x\neq\beta\end{array}\right.$

where $\alpha(a)=a$, $\alpha(x)=\underline{\mathfrak{0}}$ if $x$ is neither
$a$ nor $\alpha$, $\beta(a)=a$, $\beta(b)=b$,
$\beta(x)=\underline{\mathfrak{0}}$ if $x$ is neither $a$ nor $b$ or $\beta$.

We have two kinds of ordered pairs: those where $\alpha\neq b$ (first kind)
and those where $\alpha=b$ (second kind). Their respective diagrams are as it
follows:

\begin{picture}(60.0,65.0)\par\put(3.0,25.0){\framebox(100.0,30.0)[]{}}
\par\par\put(10.0,45.0){$f$} \par\put(10.0,11.0){\framebox(40.0,30.0)[]{}}
\par\put(40.0,43.0){$\boldmath\curvearrowleft$} \par\put(15.0,32.0){$\alpha$}
\par\put(55.0,11.0){\framebox(40.0,30.0)[]{}}
\par\put(85.0,43.0){$\boldmath\curvearrowleft$} \par\put(60.0,31.0){$\beta$}
\par\put(60.0,12.0){$a$} \par\put(58.0,16.0){$\boldmath\curvearrowleft$}
\par\put(13.0,16.0){$\boldmath\curvearrowleft$}
\par\put(77.0,17.0){$\boldmath\curvearrowleft$} \par\put(80.0,12.0){$b$}
\par\put(15.0,12.0){$a$} \par\put(203.0,23.0){\framebox(100.0,40.0)[]{}}
\par\par\put(210.0,53.0){$g$} \par\put(220.0,5.0){\framebox(75.0,45.0)[]{}}
\par\put(240.0,8.0){\framebox(50.0,30.0)[]{}}
\par\put(280.0,40.0){$\boldmath\curvearrowleft$}
\par\put(285.0,51.0){$\boldmath\curvearrowleft$} \par\put(225.0,39.0){$\beta$}
\par\put(244.0,28.0){$\alpha=b$} \par\put(280.0,10.0){$a$}
\par\put(278.0,15.0){$\boldmath\curvearrowleft$} \par\end{picture}

$f$

$\boldmath\curvearrowleft$

$\alpha$

$\boldmath\curvearrowleft$

$\beta$

$a$

$\boldmath\curvearrowleft$

$\boldmath\curvearrowleft$

$\boldmath\curvearrowleft$

$b$

$a$

$g$

$\boldmath\curvearrowleft$

$\boldmath\curvearrowleft$

$\beta$

$\alpha=b$

$a$

$\boldmath\curvearrowleft$

Figure 2: Diagrams of $f=(a,b)$ and $g=(a,b)$ of the first and second kind.

Left diagram above concerns the case where $f$ acts only on $\alpha$ and
$\beta$, while $\alpha$ acts only on $a$, and $\beta$ acts only on $a$ and
$b$. In the particular case where $a=b$, we have $\alpha=\beta$, and the
ordered pair $f$ is $(a,a)$. So, $(a,a)$ is a function $f$ which acts solely
on $\alpha$, while $\alpha$ acts solely on $a$. Observe that
$f(a)=f(b)=\underline{\mathfrak{0}}$ ($f$ never acts neither on $a$ nor on
$b$) if $f$ is an ordered pair of the first kind. Thus, $f$ is $(a,b)$ iff $f$
acts only on $\alpha$ and $\beta$, which act, respectively, only on $a$ and
only on $a$ and $b$. To get $(b,a)$, all we have to do is to exchange $\alpha$
by a function $\alpha^{\prime}$ which acts only on $b$. Our definition is
obviously inspired on the standard notion due to Kuratowski. In standard set
theory $(a,b)$ is a set $\\{\\{a\\},\\{a,b\\}\\}$ such that neither $a$ nor
$b$ belong to $(a,b)$. In Flow, on the other hand, an ordered pair $(a,b)$ of
the first kind is a function which does not act neither on $a$ nor on $b$.

Nevertheless, the second kind of ordered pair shows our approach is not
equivalent to Kuratowki’s. In the case where $\alpha=b$, we have the diagram
to the right of Figure 2. This non-Kuratowskian ordered pair $g=(a,b)$ acts on
$b$, although it does not act on $a$. And no Kuratowskian ordered pair $(a,b)$
ever acts on either $a$ or $b$. So, in the general case, no ordered pair
$(a,b)$ ever acts on $a$. That means:

###### Theorem 45

Any ordered pair $(a,a)$ is Kuratowskian.

The proof is straightforward. Since any ordered pair $(a,b)$ is a function,
for the sake of abbreviation we write $x(a,b)$ for $x((a,b))$, for a given
function $x$.

The reader can observe, from Figure 2, that in a non-Kuratowskian ordered pair
$f$, $\beta$ is the non-$\underline{\mathfrak{0}}$ $\mathfrak{F}$-successor of
$\alpha$. In other words:

###### Theorem 46

$f=(a,b)$ is a non-Kuratowskian ordered pair iff $f$ acts only on a function
$\alpha$ \- which, in its turn, acts on one single term $a$ \- and on its
$\mathfrak{F}$-successor $\sigma_{\alpha}$, where
$\sigma_{\alpha}\neq\underline{\mathfrak{0}}$.

Proof

If $f=(a,b)$, then $f$ acts at most on $\alpha$ and $\beta$, where $\alpha$
acts only on $a$, and $\beta$ acts only on $a$ and $b$. Suppose $f=(a,b)$ is
non-Kuratowskian. Then, $a\neq b$ (Theorem 45); and $f=(a,\alpha)$, since
$\alpha=b$. But $a\neq b$ entails $a\neq\alpha$. And since $\alpha$ acts on
$a$, then $\beta$ acts on two terms: $\alpha$ and $a$. But that is the
condition given for granting $\beta=\sigma_{\alpha}$, where
$\sigma_{\alpha}\neq\underline{\mathfrak{0}}$. Finally, if $f$ acts only on
$\alpha$ and $\sigma_{\alpha}$, where $\alpha$ acts only on $a$ and
$\sigma_{\alpha}\neq\underline{\mathfrak{0}}$, then $f=(a,\alpha)$ is non-
Kuratowskian.

Suppose $f=\underline{\mathfrak{1}}\big{|}_{x=\varphi_{3}\vee x=\varphi_{4}}$.
In that case $f$ acts on $\varphi_{3}$ and on its $\mathfrak{F}$-successor
$\varphi_{4}$. Nevertheless, $\varphi_{3}$ does not act on just one single
term. Thus, such an $f$ is not an ordered pair, let alone a non-Kuratowskian
ordered pair.

###### Theorem 47

$(a,b)=(c,d)$ iff $a=c$ and $b=d$.

Proof

Straightforward from Definition 22 and F9E.

###### Theorem 48

If $a$ and $b$ are both emergent, then there is $f=(a,b)$.

Proof

From F9E we define the proper restriction $\beta$ of
$\underline{\mathfrak{1}}$ for “$t=a\vee t=b$” as formula $F(t)$. So,
$\beta(a)=a$, $\beta(b)=b$, $\beta(\beta)=\beta$, and
$\beta(x)=\underline{\mathfrak{0}}$ for all remaining values of $x$.
Analogously, the proper restriction $\alpha$ of $\underline{\mathfrak{1}}$ for
“$t=a$”gives us $\alpha(a)=a$, $\alpha(\alpha)=\alpha$, and
$\alpha(x)=\underline{\mathfrak{0}}$ for the remaining values of $x$. And,
from F9E, we have $\alpha\neq a$. Analogously, we have $\beta\neq a$ and
$\beta\neq b$. Finally, the proper restriction $f$ of
$\underline{\mathfrak{1}}$ for “$t=\alpha\vee t=\beta$ gives us
$f(\alpha)=\alpha$, $f(\beta)=\beta$, $f(f)=f$, and
$f(x)=\underline{\mathfrak{0}}$ for all the remaining values of $x$. Besides,
$f\neq\alpha$ and $f\neq\beta$. But function $f$ is exactly that one in
Definition 22. Hence, $f=(a,b)$.

To get an ordered pair $(\underline{\mathfrak{0}},\underline{\mathfrak{0}})$,
all we have to do is to consider $\varphi_{1}$, which acts only on
$\varphi_{0}$. So,
$\varphi_{1}=_{def}(\underline{\mathfrak{0}},\underline{\mathfrak{0}})$. If
$f$ acts only on $\alpha$ and $\varphi_{0}$, where $\alpha$ acts only on
$a\neq\underline{\mathfrak{0}}$, then we adopt the convention
$f=(a,\underline{\mathfrak{0}})$. For example, $\varphi_{2}$ is the ordered
pair $(\varphi_{0},\underline{\mathfrak{0}})$. There are no ordered pairs of
the form $(\underline{\mathfrak{0}},b)$, where
$b\neq\underline{\mathfrak{0}}$.

###### Theorem 49

If $f$ is a ZF-set, then $\wp(f)$ is a ZF-set.

Proof

If $f$ is a ZF-set, then it is emergent. So, $f$ acts only on emergent
functions and F8 says any $t$ who lurks $f$ is emergent. Now, let
$h=\underline{\mathfrak{1}}\big{|}_{t\trianglelefteq f}$. Then,
$h[t]\Leftrightarrow t\trianglelefteq f$. So, $h=\mathfrak{p}(f)$ (Definition
9). But F8 also says such an $h$ is emergent. From Definition 11,
$p=\wp(f)=\underline{\mathfrak{1}}\big{|}_{t\subseteq f}$. But $p$ lurks $h$.
So, once again from F8, $\sigma_{p}\neq\underline{\mathfrak{0}}$.

###### Definition 23

$f$ is injective iff $\forall r\forall s((f[r]\wedge f[s]\wedge r\neq
s)\Rightarrow f(r)\neq f(s))$. We denote this by $\mathbb{I}(f)$.

For example, any $\varphi_{n}$ is injective.

###### Definition 24

$x\in_{\mathbb{Z}}f$ iff
$f\subset\underline{\mathfrak{1}}\wedge\mathbb{Z}(x)\wedge f[x]$.

The negation of formula $x\in_{\mathbb{Z}}f$ is abbreviated as
$x\not\in_{\mathbb{Z}}f$. We read $x\in_{\mathbb{Z}}f$ as ‘$x$
$\mathbb{Z}$-belongs to $f$’ or ‘$x$ is a $\mathbb{Z}$-member of $f$’. The
symbol $\in_{\mathbb{Z}}$ is called $\mathbb{Z}$-membership relation.

###### Theorem 50

(i) $\forall x(x\not\in_{\mathbb{Z}}x)$; (ii) $\forall
x(\underline{\mathfrak{0}}\not\in_{\mathbb{Z}}x)$; (iii) $\forall
x(\underline{\mathfrak{1}}\not\in_{\mathbb{Z}}x)$.

Proof

Item (i) is consequence from F2, since no $x$ acts on itself. Item (ii) is
consequence from Theorem 10: no $x$ acts on $\underline{\mathfrak{0}}$. Item
(iii) is immediate, since $\underline{\mathfrak{1}}$ is not a ZF-set.

At first glance, item (i) looks like an evidence that Flow is well-founded.
Nevertheless, the issue of regularity is a little more subtle than that, as we
can see later on.

$\\{f,g\\}=_{def}\underline{\mathfrak{1}}\big{|}_{x=f\vee x=g}$, where
$\mathbb{E}(f)\wedge\mathbb{E}(g)$. So, a pair $\\{f,g\\}$ is a restriction of
$\underline{\mathfrak{1}}$ which acts only on $f$ and $g$, as long they are
both emergent.

###### Theorem 51

Let $\mathbb{E}(f)\wedge\mathbb{E}(g)$. If $u=\\{f,g\\}$ is a pair, then
$\mathbb{E}(u)$.

Proof

Let $h=\varphi_{2}\big{|}^{\alpha(x,y)}$ be defined from F10α by formula
$\alpha(x,y)$ given by $(x=\varphi_{0}\Rightarrow
y=f)\wedge(x=\varphi_{1}\Rightarrow y=g)\wedge((x\neq\varphi_{0}\wedge
x\neq\varphi_{1})\Rightarrow y=\underline{\mathfrak{0}})$. According to F10α,
$\sigma_{h}\neq\underline{\mathfrak{0}}$. Since $h$ acts on emergent
functions, then $h$ is emergent. Now, let
$u=\underline{\mathfrak{1}}\big{|}_{t=g(\varphi_{0})\vee t=g(\varphi_{1})}$.
That entails $u$ lurks $h$. And axiom F8 grants
$\sigma_{u}\neq\underline{\mathfrak{0}}$. Hence, $u$ is emergent.

In particular, any pair of ZF-sets is a ZF-set.

On the left side of the image below we find a Venn diagram of a set $f$ (in
the sense of ZF), with its elements $g$, $h$, and $i$. On the right side there
is a diagram of a ZF-set $f$ (in the sense of Flow) which acts on $g$, $h$,
and $i$. One of the main differences between both pictorial representations is
the absence of arrows in the Venn diagram. Venn diagrams do not emphasize the
full role of the Extensionality Axiom from ZF: a set is defined either by its
elements or by those terms who do not belong to it as well. Within Flow,
however, it is explicitly emphasized that anything which is not inside the
rectangle of a diagram has an image $\underline{\mathfrak{0}}$. Thus, in a
sense, Flow diagrams were always somehow implicit within Venn diagrams. At the
end, standard extensional set theories, like ZFC, are simply particular cases
of a general theory of functions, as we can formally check in Subsection 3.2.

\begin{picture}(60.0,45.0)\par\put(33.0,20.0){\circle{200.0}}
\par\put(13.0,35.0){$f$} \par\put(23.0,22.0){$g$} \par\put(40.0,22.0){$h$}
\par\put(32.0,7.0){$i$} \par\put(153.0,5.0){\framebox(100.0,30.0)[]{}}
\par\put(160.0,25.0){$f$} \par\put(172.0,10.0){$g$}
\par\put(170.0,16.0){$\boldmath\curvearrowleft$}
\par\put(200.0,16.0){$\boldmath\curvearrowleft$}
\par\put(230.0,16.0){$\boldmath\curvearrowleft$} \par\put(202.0,10.0){$h$}
\par\put(232.0,10.0){$i$} \par\end{picture}

$f$

$g$

$h$

$i$

$f$

$g$

$\boldmath\curvearrowleft$

$\boldmath\curvearrowleft$

$\boldmath\curvearrowleft$

$h$

$i$

Figure 3: Comparison between Venn diagrams and Flow diagrams.

###### Theorem 52

Any inductive function which acts only on ZF-sets is a ZF-set.

Proof

Immediate from the definitions of inductive function and ZF-set.

###### Definition 25

$f$ is a proper class iff $\forall
x(f[x]\Rightarrow\mathbb{Z}(x))\wedge\mathbb{C}(f)$.

In other words, no proper class is a ZF-set.

###### Theorem 53

There is one single ZF-set $f$ such that for any $x$, we have
$x\not\in_{\mathbb{Z}}f$.

Proof

$f=\varphi_{0}$. From F6, $\varphi_{0}$ is unique. From Theorem 14,
$\varphi_{0}$ is the only term different of $\underline{\mathfrak{0}}$ (recall
$\underline{\mathfrak{0}}$ is not a ZF-set) which satisfies the condition
given above. In other words, $\varphi_{0}$ is the empty ZF-set, which can be
denoted by $\emptyset$.

###  2.6 Atoms

Next we introduce a generalization of ZF-sets which is quite helpful for us.

###### Definition 26

i

$\mathbb{Z}_{\varphi_{0}}(f)$ iff $\mathbb{Z}(f)$;

ii

$\mathbb{Z}_{\varphi_{1}}(f)$ iff
$f\not\subseteq\underline{\mathfrak{1}}\wedge\mathbb{E}(f)\wedge\forall
x(f[x]\Rightarrow(\mathbb{Z}_{\varphi_{0}}(x)\wedge\mathbb{Z}_{\varphi_{0}}(f(x))))$;

iii

$\mathbb{Z}_{\sigma_{r}}(f)$ iff $\varpi[r]\wedge
r[\varphi_{0}]\wedge\mathbb{E}(f)\wedge\exists
x(f[x]\wedge(\mathbb{Z}_{r}(x)\vee\mathbb{Z}_{r}(f(x))))\wedge\forall
y((f[y]\wedge\neg\mathbb{Z}_{r}(y))\Rightarrow\exists s\exists t(r[s]\wedge
r[t]\wedge\mathbb{Z}_{s}(y)\wedge(\mathbb{Z}_{t}(f(y))\vee\mathbb{Z}_{r}(f(y)))))$.

iv

Let $s$ be a limit ordinal different of $\varphi_{0}$. Then,
$\mathbb{Z}_{s}(f)$ iff $\mathbb{E}(f)\wedge\forall x(f[x]\Rightarrow\exists
r\exists t(s[r]\wedge
s[t]\wedge\mathbb{Z}_{r}(x)\wedge\mathbb{Z}_{t}(f(x))\wedge\exists u\exists
y(u[r]\wedge u[t]\wedge s[u]\wedge f[y]\wedge\mathbb{Z}_{u}(y))))$.

If $r$ is an ordinal, we read $\mathbb{Z}_{r}(f)$ as ‘$f$ is a ZF-emergent
function of degree $r$’ or, simply, ‘ZF-emergent’, if the degree $r$ is
irrelevant.

The only ZF-emergent functions which are required to be no restrictions of
$\underline{\mathfrak{1}}$ are those with degree $\varphi_{1}$. Nevertheless,
for our purposes in this Subsection, we are mostly interested on ZF-emergent
functions which are no restrictions of $\underline{\mathfrak{1}}$, regardless
of their degree, according to next definition.

###### Definition 27

$\mathbb{A}(f)$ iff $\exists r(\varpi[r]\wedge\mathbb{Z}_{r}(f)\wedge
f\not\subseteq\underline{\mathfrak{1}})$. We read $\mathbb{A}(f)$ as ‘$f$ is
an atom’.

In other words, atoms are ZF-emergent functions who are no restriction of
$\underline{\mathfrak{1}}$.

###### Definition 28

Let $a\neq\varphi_{0}$ be an emergent function who acts only on atoms and such
that $a\subset\underline{\mathfrak{1}}$. In that case we say $a$ is a brick of
atoms, and denote this by $\mathbb{B}(a)$. If we change item i of Definition
19 to $\alpha(\varphi_{0},a)$, while keeping all remaining items, then
$\eta^{a}_{r}=r\big{|}^{\alpha}$ is an atomic von Neumann function, where $r$
is an ordinal. Besides, $\nu^{a}=\underline{\mathfrak{1}}\big{|}_{\exists
r(\varpi[r]\wedge\eta^{a}_{\sigma_{r}}(r)=t)}$ is an atomic von Neumann
universe. Furthermore, $\forall u(\mathbb{M}_{a}(u)\Leftrightarrow\exists
t(\nu^{a}[t]\wedge t[u]))$; we read $\mathbb{M}_{a}(u)$ as ‘$u$ is a Menge in
$\nu^{a}$’ or simply ‘$u$ is a Menge’ if there is no risk of confusion.

Obviously, the name Menge was borrowed from Cantor’s Mengenlehre. Observe no
Menge is an atom and no atom is a Menge. Besides, function $a$ of last
definition works, for all practical purposes, as the set of all atoms within
the context of our atomic von Neumann universe.

###### Theorem 54

For any brick of atoms $a$,
$\sigma(\nu^{a})=\sigma\left(\underline{\mathfrak{1}}\big{|}_{\mathbb{M}_{a}(t)}\right)=\underline{\mathfrak{0}}$.

Proof

Analogous to the proofs of Theorems 40 and 44.

###### Theorem 55

$\forall a\forall
f((\mathbb{B}(a)\wedge\mathbb{Z}(f))\Rightarrow\mathbb{M}_{a}(f))$.

The proof of last theorem is trivial. It means every ZF-set is a Menge in any
atomic von Neumann universe. Obviously there may be a Menge who is not a ZF-
set (recall every ZF-set is a ZF-emergent of degree $\varphi_{0}$).

Our atoms are supposed to mimic Urelemente from a theory in the style of ZFU
(ZF with Urelemente), while certain ZF-emergent functions $f$ such that
$f\subset\underline{\mathfrak{1}}$ are supposed to play the role of
‘collections’ or ‘sets’. In order to do that we need to introduce a
specialized concept of ‘membership’ which grants all atoms are empty. Thus:

###### Definition 29

(i) $x\in y$ iff $\mathbb{M}_{a}(y)\wedge y[x]$, if $a$ is a brick of atoms;
(ii) $x\not\in y$ iff $\neg(x\in y)$. We read $x\in y$ as ‘$x$ is an element
of $y$’ or ‘$x$ belongs to $y$’.

In other words, $x\in y$ iff $y$ is a Menge and $x$ is either an atom or a ZF-
set such that $y[x]$ or a Menge such that $y[x]$ and so on. After all, any
Menge who acts on some term, acts either on an atom or on a ZF-set or on
another Menge. Since no atom is a Menge, then every atom $y$ is empty, in the
sense that, for any $x$, we have $x\not\in y$. That means our ZF-sets
correspond to pure sets.

From an intuitive point of view, although our atoms are empty (with respect to
$\in$), they are not ontologically equivalent to the classical notion of
Urelemente. Urelemente, from German, are supposed to be primordial elements,
i.e., ‘unbreakable into minor parts’. However, our atoms have some sort of
‘inner structure’, since they are functions who act on other functions. For
example, if $x$ is a function such that $\varphi_{0}\stackrel{{\scriptstyle
x}}{{{}_{\longmapsto}}}\varphi_{1}\stackrel{{\scriptstyle
x}}{{{}_{\longmapsto}}}\varphi_{2}\stackrel{{\scriptstyle
x}}{{{}_{\longmapsto}}}\underline{\mathfrak{0}}$, and $y$ is given by
$\varphi_{2}\stackrel{{\scriptstyle
y}}{{{}_{\longmapsto}}}\varphi_{1}\stackrel{{\scriptstyle
y}}{{{}_{\longmapsto}}}\varphi_{0}\stackrel{{\scriptstyle
y}}{{{}_{\longmapsto}}}\underline{\mathfrak{0}}$, they are both atoms. But
$x\circ y$ is a ZF-set whose only elements are the ZF-sets $\varphi_{1}$ and
$\varphi_{2}$. No version of ZFU in literature suggests the possibility of
compositions among atoms who are able to produce ‘pure sets’. Besides, our
atoms may be ‘ranked’ by means of degrees: the degree of an atom $a$ is the
least ordinal $r$ such that $\mathbb{Z}_{r}(a)$. That is why we prefer to
avoid the terms ‘Urelement’ and ‘Urelemente’ for describing empty terms who
are not Menge. On the other hand, the term ‘atom’ is not appropriate either,
since its etymology is attached to the notion of indivisibility. Nevertheless,
for our purposes in this paper, we refer to our empty terms as atoms, as long
they are not Menge but can be elements of a Menge.

If $x$ is a ZF-emergent of degree $\varphi_{0}$, then it is a Menge in any von
Neumann universe (Theorem 55). If $x$ is a ZF-emergent of degree
$\varphi_{1}$, then it is an atom. Therefore, it is an atom in any atomic von
Neumann universe $\nu^{a}$ where $a$ acts on $x$. If $x$ is a ZF-emergent of
degree greater than $\varphi_{1}$, then either
$x\not\subset\underline{\mathfrak{1}}$ or $x\subset\underline{\mathfrak{1}}$.
In the first case, $x$ is an atom in $\nu^{a}$, for any $a$ which acts on $x$.
Finally, if $x\subset\underline{\mathfrak{1}}$, then $\forall
t(x[t]\Rightarrow(t\subset\underline{\mathfrak{1}}\vee
t\not\subset\underline{\mathfrak{1}}))$. Thus, either
$b=x\big{|}_{t\not\subseteq\underline{\mathfrak{1}}}$ is a brick of atoms or
$b=\varphi_{0}$. In the first case $b$ is a Menge in $\nu^{c}$ for any $c$
such that $b\subseteq c$. In the second case Theorem 55 once again grants
$\varphi_{0}$ is a Menge in any atomic von Neumann universe. All of this
points to an interesting phenomenon, namely, ZF-emergent functions of degree
$\varphi_{1}$ constitute some sort of frontier between collections with atoms
and collections without atoms.

###  2.7 Interpreting ZFU

Our main goal here is to introduce a minimum set of ingredients to build a
model of ZF set theory with atoms (ZFU) where we have PP but not AC. It is
well known that permutation models of ZFU are easily capable of violating the
Axiom of Choice thanks to one single fact: the axioms of ZFU cannot
distinguish among atoms, in the sense that there are non-trivial
$\in$-automorphisms on the universe of ZFU. Although Definition 27 allows the
existence of a vast number of atoms, we are interested only on a specific
range of them. But first we need a new concept.

###### Definition 30

Let $x$ be any function. The kernel of $x$ is given by
$\mathcal{K}(x)=\underline{\mathfrak{1}}\big{|}_{\mathbb{Z}(t)\wedge(x[t]\vee\exists
r(x(r)=t))}$.

Last definition is sound, since every ZF-set is emergent. Thus, F9F is
applicable.

###### Theorem 56

Let $\nu^{a}$ be an atomic von Neumann universe. Then,
$\mathcal{K}(\nu^{a})=\nu$, where $\nu$ is the von Neumann universe.

Proof

Straightforward from Theorem 55.

Thus, we have here a generalization of the usual concept of kernel [15] which
is applicable in a nontrivial way to atoms as well, as we can see in the next
Observation.

###### Observation 4

According to our previous discussions we have a lot of options for choosing a
brick $a$ of atoms for defining any atomic von Neumann universe $\nu^{a}$.
That is why we now introduce some simple examples for the sake of
illustration. Let $\mu$ be a function obtained from
$\varpi\big{|}_{t=\omega\vee t=\sigma_{\omega}}$ and F10α as it follows, where
$\omega$ is the limit ordinal who acts only on finite ordinals (Definition
17):
$\omega\stackrel{{\scriptstyle\mu}}{{{}_{\longmapsto}}}\sigma_{\omega}\stackrel{{\scriptstyle\mu}}{{{}_{\longmapsto}}}\omega$.
Let $\mu^{\prime}$ be obtained from $\varpi\big{|}_{t=\sigma_{\omega}\vee
t=\sigma_{\sigma_{\omega}}}$ and F10α as it follows:
$\sigma_{\omega}\stackrel{{\scriptstyle\mu^{\prime}}}{{{}_{\longmapsto}}}\sigma_{\sigma_{\omega}}\stackrel{{\scriptstyle\mu^{\prime}}}{{{}_{\longmapsto}}}\sigma_{\omega}$.
Obviously, $\mu\neq\mu^{\prime}$. Let $p$ be a function obtained from
$\varphi_{3}$ and F10α as it follows: $\varphi_{0}\stackrel{{\scriptstyle
p}}{{{}_{\longmapsto}}}\varphi_{1}\stackrel{{\scriptstyle
p}}{{{}_{\longmapsto}}}\varphi_{2}\stackrel{{\scriptstyle
p}}{{{}_{\longmapsto}}}\varphi_{0}$. Using once again F10α over $p$ we can
obtain the next function $g$ given by $\varphi_{1}\stackrel{{\scriptstyle
g}}{{{}_{\longmapsto}}}\varphi_{0}\stackrel{{\scriptstyle
g}}{{{}_{\longmapsto}}}\mu\stackrel{{\scriptstyle
g}}{{{}_{\longmapsto}}}\underline{\mathfrak{0}}$ and
$\varphi_{2}\stackrel{{\scriptstyle
g}}{{{}_{\longmapsto}}}\mu^{\prime}\stackrel{{\scriptstyle
g}}{{{}_{\longmapsto}}}\underline{\mathfrak{0}}$. Analogously there is an $h$
such that $\mu\stackrel{{\scriptstyle
h}}{{{}_{\longmapsto}}}\varphi_{0}\stackrel{{\scriptstyle
h}}{{{}_{\longmapsto}}}\varphi_{1}\stackrel{{\scriptstyle
h}}{{{}_{\longmapsto}}}\underline{\mathfrak{0}}$ and
$\mu^{\prime}\stackrel{{\scriptstyle
h}}{{{}_{\longmapsto}}}\varphi_{2}\stackrel{{\scriptstyle
h}}{{{}_{\longmapsto}}}\underline{\mathfrak{0}}$. Hence, there is a function
$a_{\varphi_{0}}$ where $\mu\stackrel{{\scriptstyle
a_{\varphi_{0}}}}{{{}_{\longmapsto}}}\varphi_{0}\stackrel{{\scriptstyle
a_{\varphi_{0}}}}{{{}_{\longmapsto}}}\mu^{\prime}\stackrel{{\scriptstyle
a_{\varphi_{0}}}}{{{}_{\longmapsto}}}\mu$. By using analogous arguments we
introduce the next atom $\overline{a_{\varphi_{0}}}$:
$\mu\stackrel{{\scriptstyle\overline{a_{\varphi_{0}}}}}{{{}_{\longmapsto}}}\mu^{\prime}\stackrel{{\scriptstyle\overline{a_{\varphi_{0}}}}}{{{}_{\longmapsto}}}\varphi_{0}\stackrel{{\scriptstyle\overline{a_{\varphi_{0}}}}}{{{}_{\longmapsto}}}\mu$.
Observe $a_{\varphi_{0}}\neq\overline{a_{\varphi_{0}}}$. Besides,
$a_{\varphi_{0}}\circ a_{\varphi_{0}}=\overline{a_{\varphi_{0}}}$,
$\overline{a_{\varphi_{0}}}\circ\overline{a_{\varphi_{0}}}=a_{\varphi_{0}}$,
but
$\mathcal{K}(a_{\varphi_{0}})=\mathcal{K}(\overline{a_{\varphi_{0}}})=\mathcal{K}(a_{\varphi_{0}}\circ
a_{\varphi_{0}})=\mathcal{K}(\overline{a_{\varphi_{0}}}\circ\overline{a_{\varphi_{0}}})=\mathcal{K}(a_{\varphi_{0}}\circ\overline{a_{\varphi_{0}}})=\mathcal{K}(\overline{a_{\varphi_{0}}}\circ
a_{\varphi_{0}})=\varphi_{1}$. Although both atoms $a_{\varphi_{0}}$ and
$\overline{a_{\varphi_{0}}}$ are empty (there is no $t$ such that $t$ belongs
to either one of them), their kernels are $\varphi_{1}$, a non-empty ZF-set.
We say $a_{\varphi_{0}}$ and $\overline{a_{\varphi_{0}}}$ are conjugates of
each other, in the sense that they cannot be distinguished from each other
neither by means of their kernels nor by means of the kernels of their
$\mathfrak{F}$-compositions. So, yes, we are inspired on the original ideas by
Abraham A. Fraenkel [8], despite the fact that his seminal paper has some well
known mistakes [24]. Nevertheless we use an analogous technique to introduce
atoms which can be distinguished from $a_{\varphi_{0}}$ and
$\overline{a_{\varphi_{0}}}$. That is a key point for our main result.

###### Definition 31

The rank of a Menge $u$ in an atomic von Neumann universe $\nu^{a}$ is the
least ordinal $r$ such that $u\subseteq\eta_{\sigma_{r}}^{a}(r)$. We denote
this by $r=\mathtt{rank}(u)$. The rank of any atom in an atomic von Neumann
universe is $\varphi_{0}$.

Observe this last concept of rank of a Menge in $\nu^{a}$ is independent from
the notion of degree of any atom where $a$ acts. Next we introduce the concept
of transitive closure, which is a copy from the usual notion in set theory.

###### Definition 32

Let $\mathbb{M}_{a}(x)$, i.e., $x$ is a Menge from an atomic von Neumann
universe $\nu^{a}$. Then: (i) $x_{\varphi_{0}}=x$; (ii)
$x_{\sigma_{r}}=\bigcup_{x_{r}[t]}t$, where $r$ is a finite ordinal; (iii)
$\mbox{TC}(x)=\bigcup_{\omega[r]}x_{r}$. We read $\mbox{TC}(x)$ as the
‘transitive closure’ of $x$.

###### Definition 33

Let $a$ be a brick of atoms such that $\forall
x(a[x]\Rightarrow\exists!y(a[y]\wedge x\neq
y\wedge\mathcal{K}(x)=\mathcal{K}(y)\wedge\mathcal{K}(x\circ
y)=\mathcal{K}(y\circ x)))$. Then, in the corresponding atomic von Neumann
universe $\nu^{a}$, we have:

i

If $\mathbb{Z}(x)$ and $y$ is any term, then $x\equiv y$ iff $x=y$;

ii

If $a[x]\wedge a[y]$, then $x\equiv y$ iff
$\mathcal{K}(x)=\mathcal{K}(y)\wedge\mathcal{K}(x\circ y)=\mathcal{K}(y\circ
x)$;

iii

Let $x=\underline{\mathfrak{1}}\big{|}_{t=r\vee t=s}$, where $a[r]\wedge
a[s]\wedge r\neq s\wedge r\equiv s$; then $\forall y(y\equiv x\Leftrightarrow
y=x)$;

iv

Let $f=\\{r\\}_{x}$ be an abbreviation for the formula $x\subseteq a\wedge
a[r]\wedge\forall s(f[s]\Leftrightarrow(x[s]\wedge s\equiv r))$; now, let
$x\subseteq a\wedge y\subseteq a$, then $x\equiv y$ iff $\forall
u(x[u]\Rightarrow\exists!v(v=\\{u\\}_{x}\wedge v\equiv\\{u\\}_{y}))$;

v

Let $\mathbb{M}_{a}(x)\wedge\mathbb{M}_{a}(y)$, then $x\equiv y$ iff
$\mathtt{rank}(x)=\mathtt{rank}(y)\wedge\forall r\forall
s((\varpi[r]\wedge\varpi[s])\Rightarrow\mbox{TC}(x\big{|}_{\mathtt{rank}(t)=r\vee\mathtt{rank}(t)=s})\big{|}_{a[m]}\equiv\mbox{TC}(y\big{|}_{\mathtt{rank}(t)=r\vee\mathtt{rank}(t)=s})\big{|}_{a[m]})$,
where all occurrences of $m$ in formula $a[m]$ are free;

vi

$\forall x\forall y(x\equiv y\Leftrightarrow y\equiv x)$;

vii

If $a[x]\wedge\mathbb{M}_{a}(y)$, then $\neg(x\equiv y)$.

We read $x\equiv y$ as ‘$x$ is indistinguishable of $y$’ or ‘$x$ is
indiscernible of $y$’. $x\not\equiv y$ abbreviates $\neg(x\equiv y)$, and we
read it as ‘$x$ is distinguishable of $y$’ or ‘$x$ is discernible of $y$’.

Obviously, any $x$ of $\nu^{a}$ (i.e., either $a[x]$ or $\mathbb{M}_{a}(x)$)
is indistinguishable of itself.

The same criteria used for indiscernible atoms (item ii) could be used to ZF-
sets. After all, if both $x$ and $y$ are ZF-sets, then $x\circ y=y\circ x$ is
simply the intersection between $x$ and $y$. In that case indistinguishability
$\equiv$ is simply identity $=$, since $\mathcal{K}(x)=x$, $\mathcal{K}(y)=y$,
$\mathcal{K}(x\circ y)=x\circ y$, and $\mathcal{K}(y\circ x)=y\circ x$.
Nevertheless, there may exist different atoms which are indistinguishable,
like $a_{\varphi_{0}}$ and $\overline{a_{\varphi_{0}}}$ in Observation 4. That
is a key feature we intend to use in our proof of independence of AC from the
Partition Principle within ZFU.

Item iv of last definition introduces classes of indiscernible atoms. For
instance, let $a_{\varphi_{0}}$ be the atom $\mu\stackrel{{\scriptstyle
a_{\varphi_{0}}}}{{{}_{\longmapsto}}}\varphi_{0}\stackrel{{\scriptstyle
a_{\varphi_{0}}}}{{{}_{\longmapsto}}}\mu^{\prime}\stackrel{{\scriptstyle
a_{\varphi_{0}}}}{{{}_{\longmapsto}}}\mu$. Let $\overline{a_{\varphi_{0}}}$ be
the atom
$\mu\stackrel{{\scriptstyle\overline{a_{\varphi_{0}}}}}{{{}_{\longmapsto}}}\mu^{\prime}\stackrel{{\scriptstyle\overline{a_{\varphi_{0}}}}}{{{}_{\longmapsto}}}\varphi_{0}\stackrel{{\scriptstyle\overline{a_{\varphi_{0}}}}}{{{}_{\longmapsto}}}\mu$.
Those are the same ones from Observation 4. Now, let $a_{\varphi_{1}}$ be the
atom $\mu\stackrel{{\scriptstyle
a_{\varphi_{1}}}}{{{}_{\longmapsto}}}\varphi_{1}\stackrel{{\scriptstyle
a_{\varphi_{1}}}}{{{}_{\longmapsto}}}\mu^{\prime}\stackrel{{\scriptstyle
a_{\varphi_{1}}}}{{{}_{\longmapsto}}}\mu$, and $\overline{a_{\varphi_{1}}}$ be
the atom
$\mu\stackrel{{\scriptstyle\overline{a_{\varphi_{1}}}}}{{{}_{\longmapsto}}}\mu^{\prime}\stackrel{{\scriptstyle\overline{a_{\varphi_{1}}}}}{{{}_{\longmapsto}}}\varphi_{1}\stackrel{{\scriptstyle\overline{a_{\varphi_{1}}}}}{{{}_{\longmapsto}}}\mu$.
Observe $a_{\varphi_{0}}\not\equiv a_{\varphi_{1}}$. If $x$ is a Menge who
acts only on $a_{\varphi_{0}}$, $\overline{a_{\varphi_{0}}}$, and
$a_{\varphi_{1}}$, then
$\\{a_{\varphi_{0}}\\}_{x}=\\{a_{\overline{\varphi_{0}}}\\}_{x}$, namely, a
Menge who acts only on $a_{\varphi_{0}}$ and $\overline{a_{\varphi_{0}}}$. On
the other hand,
$\\{a_{\varphi_{1}}\\}_{x}=\\{a_{\overline{\varphi_{1}}}\\}_{x}$, namely, a
Menge who acts solely on $a_{\varphi_{1}}$. If $a_{\varphi_{2}}$ is defined in
a similar fashion, then $\\{a_{\varphi_{2}}\\}_{x}=\varphi_{0}$.

Bricks of atoms in the sense of last Definition provide necessary but not
sufficient conditions for achieving our goals. That is why we need the next
concept. We introduce below our Appropriate Brick of Atoms which is used in
our main result of this paper.

###### Definition 34

For any finite ordinal $r$, let $\alpha_{r}$ be the atom
$r\stackrel{{\scriptstyle\alpha_{r}}}{{{}_{\longmapsto}}}\mu\stackrel{{\scriptstyle\alpha_{r}}}{{{}_{\longmapsto}}}\mu^{\prime}\stackrel{{\scriptstyle\alpha_{r}}}{{{}_{\longmapsto}}}r$
and $\overline{\alpha_{r}}$ be the atom
$r\stackrel{{\scriptstyle\alpha_{r}}}{{{}_{\longmapsto}}}\mu^{\prime}\stackrel{{\scriptstyle\alpha_{r}}}{{{}_{\longmapsto}}}\mu\stackrel{{\scriptstyle\alpha_{r}}}{{{}_{\longmapsto}}}r$,
where $\mu$ and $\mu^{\prime}$ are the same functions introduced in
Observation 4. Then, $\mathfrak{a}=\underline{\mathfrak{1}}\big{|}_{\exists
r(\omega[r]\Rightarrow(t=\alpha_{r}\vee t=\overline{\alpha_{r}}))}$ is the
Appropriate Brick of Atoms, where $\omega$ is the limit ordinal who acts only
on all finite ordinals (Definition 17), i.e., all $\varphi_{n}$. Any $t$ where
$\mathfrak{a}$ acts is an appropriate atom. Within this context,
$\nu^{\mathfrak{a}}$ is the Appropriate Atomic von Neumann Universe, or
Appropriate Universe, for short.

That means the Appropriate Brick of Atoms $\mathfrak{a}$ is a Menge in
$\nu^{\mathfrak{a}}$. From now on we use the same notation of last definition
for appropriate atoms, i.e., anytime we write either $\alpha_{r}$ or
$\overline{\alpha_{r}}$ we mean both are appropriate atoms. Next theorem is
quite important, although its proof is a simple exercise.

###### Theorem 57

For any finite ordinals $r$ and $s$, such that $r\neq s$, we have: (i)
$\mathcal{K}(\alpha_{r})=\mathcal{K}(\overline{\alpha_{r}})=\mathcal{K}(\alpha_{r}\circ\alpha_{r})=\mathcal{K}(\overline{\alpha_{r}}\circ\overline{\alpha_{r}})=\mathcal{K}(\alpha_{r}\circ\overline{\alpha_{r}})=\mathcal{K}(\overline{\alpha_{r}}\circ\alpha_{r})=\gamma$,
where $\gamma$ is given by
$r\stackrel{{\scriptstyle\gamma}}{{{}_{\longmapsto}}}r$; (ii)
$\mathcal{K}(\alpha_{r}\circ\alpha_{s})=\mathcal{K}(\overline{\alpha_{r}}\circ\alpha_{s})=\mathcal{K}(\alpha_{r}\circ\overline{\alpha_{s}})=\mathcal{K}(\overline{\alpha_{r}}\circ\overline{\alpha_{s}})=\gamma^{\prime}$,
where $\gamma^{\prime}$ is given by
$r\stackrel{{\scriptstyle\gamma^{\prime}}}{{{}_{\longmapsto}}}r$ and
$s\stackrel{{\scriptstyle\gamma^{\prime}}}{{{}_{\longmapsto}}}s$.

Proof

Just a bunch of boring calculations.

###### Theorem 58

For any finite ordinals $r$ and $s$, such that $r\neq s$, we have: (i)
$\alpha_{r}\equiv\overline{\alpha_{r}}$; (ii)
$\alpha_{r}\not\equiv\alpha_{s}$; (iii)
$\alpha_{r}\not\equiv\overline{\alpha_{s}}$; (iv)
$\overline{\alpha_{r}}\not\equiv\alpha_{s}$; (v)
$\overline{\alpha_{r}}\not\equiv\overline{\alpha_{s}}$.

Proof

For any finite ordinal $r$ we have
$\mathcal{K}(\alpha_{r})=\mathcal{K}(\overline{\alpha_{r}})=\mathcal{K}(\alpha_{r}\circ\overline{\alpha_{r}})=\mathcal{K}(\overline{\alpha_{r}}\circ\alpha_{r})=\gamma$,
where $\gamma$ is given by
$r\stackrel{{\scriptstyle\gamma}}{{{}_{\longmapsto}}}r$. That settles item i.
For the remaining items observe that
$\mathcal{K}(\alpha_{s})=\mathcal{K}(\overline{\alpha_{s}})=\gamma^{\prime}$,
where $r\stackrel{{\scriptstyle\gamma^{\prime}}}{{{}_{\longmapsto}}}r$ and
$s\stackrel{{\scriptstyle\gamma^{\prime}}}{{{}_{\longmapsto}}}s$. Since $r\neq
s$, then $\gamma\neq\gamma^{\prime}$.

###### Theorem 59

$\forall
f(\mathbb{M}_{\mathfrak{a}}(f)\Leftrightarrow(\sigma_{f}\neq\underline{\mathfrak{0}}\wedge
f\subseteq\underline{\mathfrak{1}}\wedge\forall
x(f[x]\Rightarrow(\mathfrak{a}[x]\vee\mathbb{M}_{\mathfrak{a}}(x)))))$.

Proof

Analogous to the proof of Theorem 43, since any Menge in $\nu^{\mathfrak{a}}$
can be ranked.

Next we follow a maneuver somehow inspired on Cantor-Schröder-Bernstein
theorem [18].

###### Definition 35

$g$ and $h$ are equipotent, denoted by $g\cong h$, iff there is $\tau$ where,
for any $t$: (i) $\tau[t]\Rightarrow\tau(\tau(t))=t$; (ii)
$g[t]\Rightarrow(\tau[t]\wedge h[\tau(t)])$; (iii)
$h[t]\Rightarrow(\tau[t]\wedge g[\tau(t)])$; (iv) $\tau[t]\Rightarrow(g[t]\vee
h[t])$. We call function $\tau$ a connector of $g/h$.

For example, any $\varphi_{n}$ is equipotent to itself. And a connector of
$\varphi_{n}/\varphi_{n}$ is $\varphi_{n}$.

###### Definition 36

$g$ is Dedekind-finite iff $\exists h(g\cong h\wedge\tau\not\cong g)$, where
$\tau$ is a connector of $g/h$ (Definition 35); and $g$ is Dedekind-infinite
iff it is not Dedekind-finite.

As an example, $h=\varphi_{5}\big{|}_{t=\varphi_{3}\vee t=\varphi_{4}}$ acts
only on $\varphi_{3}$ and $\varphi_{4}$. So, if we prove the existence of
$\tau$ such that $\tau(\varphi_{0})=\varphi_{3}$,
$\tau(\varphi_{3})=\varphi_{0}$, $\tau(\varphi_{1})=\varphi_{4}$, and
$\tau(\varphi_{4})=\varphi_{1}$, then $h\cong\varphi_{2}$ with connector
$\tau$. Besides, $\tau\not\cong\varphi_{2}\wedge\tau\not\cong h$, since $\tau$
acts on four terms, while $\varphi_{2}$ and $h$ act on two terms each. To
prove the existence of such a $\tau$ we use F10α.

###### Theorem 60

$\cong$ is reflexive among emergent functions.

Proof

If $f$ is $\varphi_{0}$, assume $\underline{\mathfrak{0}}$ as connector,
according to Definition 35. For the remaining cases, make
$\tau=\underline{\mathfrak{1}}\big{|}_{f[x]}$ as a connector of $f/f$.

###### Theorem 61

$\forall f\forall g((\mathbb{Z}(f)\wedge\mathbb{Z}(g)\wedge f\cong
g)\Rightarrow\sigma_{f}\cong\sigma_{g})$.

Proof

If $f$ and $g$ are ZF-sets, then $f\cup g$ is a ZF-set. That means
$\sigma_{f}\neq\underline{\mathfrak{0}}$,
$\sigma_{g}\neq\underline{\mathfrak{0}}$, and $\sigma_{f\cup
g}\neq\underline{\mathfrak{0}}$. If $f\cong g$, then there is a connector
$\tau$ of $f/g$. Since $f\cup g$ is uncomprehensive, we can apply axiom F10α
over $f\cup g$, where formula $\alpha(x,y)$ is $\tau(x)=y$. That entails, from
F10α, that $\sigma_{\tau}\neq\underline{\mathfrak{0}}$. Besides, $\sigma_{f}$,
$\sigma_{g}$, and $\sigma_{f\cup g}$ are uncomprehensive and ZF-sets. That
entails we can define a new connector $\tau^{\prime}$ for
$\sigma_{f}/\sigma_{g}$. All we have to do is to apply F10α over
$\sigma_{f}\cup\sigma_{g}$ with formula $\alpha^{\prime}(x,y)$ given by
$\alpha(x,y)$ when $x\neq f$ and $x\neq g$, and such that
$\alpha^{\prime}(f,g)$ and $\alpha^{\prime}(g,f)$. Hence,
$\sigma_{f}\cong\sigma_{g}$, where $\tau^{\prime}$ is the connector of
$\sigma_{f}/\sigma_{g}$.

###### Definition 37

$g$ is infinite iff there is no finite ordinal $r$ such that $r\cong g$.
Otherwise, we say $g$ is finite.

If we recall that $\mathbb{E}$ (emergent), $\mathbb{I}$ (injective), and
$\mathbb{B}$ (brick of atoms) are given, respectively, in Definitions 7, 23,
and 28, next formula is our last axiom of this first version of Flow.

F11 - $\mathfrak{F}$-Partition

$\forall f\forall
a((\mathbb{B}(a)\wedge\mathbb{E}(f)\wedge\mathbb{M}_{a}(Dom_{f}^{\mathfrak{F}})\wedge\mathbb{M}_{a}(Im_{f}^{\mathfrak{F}}))\Rightarrow\exists
c(Dom_{c}^{\mathfrak{F}}=Im_{f}^{\mathfrak{F}}\wedge
Im_{c}^{\mathfrak{F}}\subseteq Dom_{f}^{\mathfrak{F}}\wedge\mathbb{I}(c)))$.

###  2.8 The model

Next we prove that if $a=\mathfrak{a}$, then we are able to introduce a model
of ZFU where the Partition Principle holds but the Axiom of Choice fails.

###### Definition 38

Let $a$ be a brick of atoms. A function $f$ is a ZFU-function in an atomic von
Neumann universe $\nu^{a}$ iff:

i

$\mathbb{M}_{a}(f)$;

ii

$\forall t(f[t]\Rightarrow\exists u\exists v((a[u]\vee
a[v]\vee\mathbb{M}_{a}(u)\vee\mathbb{M}_{a}(v))\wedge t=(u,v)))$;

iii

$\forall u\forall v\forall w((f[(u,v)]\wedge f[(u,w)])\Rightarrow v=w)$.

Observe the concept of ZFU-function corresponds to the usual notion of
function in a theory like ZFU: a specific set of ordered pairs $(u,v)$ where
$u$ and $v$ are either atoms or sets.

###### Theorem 62

Let $a$ be a brick of atoms and $f:x\to y$ (Definition 18) be a function such
that both $x$ and $y$ are Mengen of $\nu^{a}$. Then there is one single ZFU-
function $f^{\prime}$ such that $\forall u\forall v(f[u]\wedge
f(u)=v)\Leftrightarrow(f^{\prime}[(u,v)]\wedge f^{\prime}((u,v))=(u,v))$.
Conversely, if $f^{\prime}$ is a ZFU-function in $\nu^{a}$, then there is a
single $f:x\to y$ such that $\mathbb{M}_{a}(x)\wedge\mathbb{M}_{a}(y)$ and
$\forall u\forall v(f[u]\wedge f(u)=v)\Leftrightarrow(f^{\prime}[(u,v)]\wedge
f^{\prime}((u,v))=(u,v))$.

Proof

First part. Let $f:x\to y$ be a function such that $\mathbb{M}_{a}(x)$ and
$\mathbb{M}_{a}(y)$. Then, $\forall r(f[r]\Rightarrow\exists s(y[s]\wedge
f(r)=s))$. Now, let $\alpha(r,t)$ be the next formula: $(f[r]\Rightarrow
t=(r,f(r)))\wedge(\neg f[r]\Rightarrow t=\underline{\mathfrak{0}})$. Then,
$h=f\big{|}^{\alpha}$ is a function whose non-$\underline{\mathfrak{0}}$
images $h(r)$ are just ordered pairs $(r,s)$ such that $f(r)=s$. Besides, F10α
entails $\sigma(Im_{h}^{\mathfrak{F}})\neq\underline{\mathfrak{0}}$. Another
way to write this is
$f^{\prime}=Im_{h}^{\mathfrak{F}}=\underline{\mathfrak{1}}\big{|}_{\forall
a\forall b(t=(a,b)\Leftrightarrow(f[a]\wedge f(a)=b))}$. So, $f^{\prime}$ is a
ZFU-function, whose uniqueness is granted by F9E. Theorem 59 grants
$f^{\prime}$ is a Menge in $\nu^{a}$, since any ordered pair $(r,s)$ of either
atoms or Mengen has a non-$\underline{\mathfrak{0}}$ $\mathfrak{F}$-successor.
Second part. Let $f^{\prime}$ be a ZFU-function in $\nu^{a}$. Then $\forall
u\forall v\forall w((f^{\prime}[(u,v)]\wedge f^{\prime}[(u,w)])\Rightarrow
v=w)$. Now, let $x=\underline{\mathfrak{1}}\big{|}_{\forall
u(t=u\Leftrightarrow\exists v(f^{\prime}[(u,v)]))}$. By analogous arguments
used in the first part, $\sigma_{x}\neq\underline{\mathfrak{0}}$. Next, let
$\alpha(r,s)$ be the formula $(x[r]\Rightarrow\forall
t(f^{\prime}[(r,t)]\Leftrightarrow t=s))\wedge(\neg x[r]\Rightarrow
s=\underline{\mathfrak{0}})$. The definition of ZFU-function grants $\forall
r\exists!s(\alpha(r,s))$. That means we can use F10α. Thus,
$f=x\big{|}^{\alpha}$ is a function $f:x\to y$ such that $\forall
r(f[r]\Rightarrow\exists s(y[s]\wedge f(r)=s))$. Besides,
$\sigma_{y}\neq\underline{\mathfrak{0}}$. The uniqueness of $f$ is granted by
F10α. Theorem 59 grants $x$ and $y$ are Mengen in $\nu^{a}$.

Last theorem could be rewritten in terms of an injective function
$\mathfrak{f}$ from the ‘space’ of all ZFU-functions of $\nu^{a}$ to the
‘space’ of all functions $f:x\to y$ where $x$ and $y$ are Mengen of $\nu^{a}$.

###### Definition 39

We say $f:x\to y$ is in correspondence to a ZFU-function $f^{\prime}$ in a
given $\nu^{a}$ iff $\forall u\forall v(f[u]\wedge
f(u)=v)\Leftrightarrow(f^{\prime}[(u,v)]\wedge f^{\prime}((u,v))=(u,v))$,
where $x$, $y$, and $f^{\prime}$ are Mengen in $\nu^{a}$.

###### Definition 40

Let $f^{\prime}$ be a ZFU-function. Then, the domain of $f^{\prime}$ is
$Dom_{f^{\prime}}=\underline{\mathfrak{1}}\big{|}_{\forall
u(t=u\Leftrightarrow\exists v(f^{\prime}[(u,v)]))}$, and the range of
$f^{\prime}$ is $Im_{f^{\prime}}=\underline{\mathfrak{1}}\big{|}_{\forall
v(t=v\Leftrightarrow\exists u(f^{\prime}[(u,v)]))}$.

###### Theorem 63

If $f:x\to y$ is in correspondence to a ZFU-function $f^{\prime}$, then
$Dom^{\mathfrak{F}}_{f}=Dom_{f^{\prime}}=x$ and
$Im^{\mathfrak{F}}_{f}=Im_{f^{\prime}}=y$. Besides, $f\neq f^{\prime}$.

Proof

See the proof of Theorem 62.

Next definition provides all necessary and sufficient conditions to introduce
the universe of our main model.

###### Definition 41

Let $F(t)$ be the formula $\exists v(\nu^{\mathfrak{a}}[v]\wedge
v[t]\wedge\forall r(\mbox{TC}(t)\big{|}_{\mathfrak{a}[m]}[r]\Rightarrow\exists
s(r\equiv s\wedge r\neq s\wedge\mbox{TC}(t)\big{|}_{\mathfrak{a}[m]}[s])))$.
Then, $\nu^{\mathfrak{a}}_{\dagger}=\nu^{\mathfrak{a}}\big{|}_{F(t)}$ is the
Azriel Lévy universe or Lévy universe, for short. If $x$ is a Menge in
$\nu^{\mathfrak{a}}_{\dagger}$, we denote this by
$\mathbb{M}_{\mathfrak{a}}^{\dagger}(x)$.

The Lévy universe is a restricted appropriate atomic von Neumann universe in
the sense that $\nu^{\mathfrak{a}}_{\dagger}\subset\nu^{\mathfrak{a}}$. Last
definition grants there is no Menge $f$ in $\nu^{\mathfrak{a}}_{\dagger}$
which acts on a single $u$ if there is any $v$ in $\nu^{\mathfrak{a}}$ where
$v\equiv u$ and $v\neq u$. For example, Flow allows us to define a Menge $f$
in $\nu^{\mathfrak{a}}$ such that $\alpha_{r}\stackrel{{\scriptstyle
f}}{{{}_{\longmapsto}}}\alpha_{r}$, where $\alpha_{r}$ is an appropriate atom.
Nevertheless, $\nu^{\mathfrak{a}}_{\dagger}$ does not act on any $t$ such that
$t$ acts on that $f$. If $g$ is a Menge in $\nu^{\mathfrak{a}}_{\dagger}$ who
acts on any $\alpha_{r}$, then $g$ acts on $\overline{\alpha_{r}}$ as well,
since $\overline{\alpha_{r}}$ is indiscernible from $\alpha_{r}$ (although
$\alpha_{r}\neq\overline{\alpha_{r}}$).

###### Theorem 64

$\forall x\forall
y((\mathbb{M}_{\mathfrak{a}}^{\dagger}(x)\wedge\mathbb{M}_{\mathfrak{a}}^{\dagger}(y)\wedge
x\equiv y)\Rightarrow x=y)$.

Proof

For any $x$, $\mathbb{Z}(x)\Rightarrow\mathbb{M}_{\mathfrak{a}}^{\dagger}(x)$
(from Theorem 55 and the fact that
$\nu^{\mathfrak{a}}_{\dagger}\subset\nu^{\mathfrak{a}}$). But, from item i of
Definition 33, for any ZF-set $x$ and any $y$, $x\equiv y\Leftrightarrow x=y$.
Now, let $x$ be a Menge who is not a ZF-set, recalling $\mathfrak{a}$
satisfies all conditions imposed in Definition 33. First we consider the case
where $x$ acts only on atoms. Since no Menge $x$ in
$\nu^{\mathfrak{a}}_{\dagger}$ acts on any atom $r$ without acting on $s$ when
$r\equiv s$, then item iii of Definition 33 grants $x\equiv y\Leftrightarrow
x=y$. Finally, if $x$ and $y$ are any Mengen in
$\nu^{\mathfrak{a}}_{\dagger}$, then
$\mbox{TC}(x\big{|}_{\mathtt{rank}(t)=r\vee\mathtt{rank}(t)=s})\big{|}_{\mathfrak{a}[m]}\equiv\mbox{TC}(y\big{|}_{\mathtt{rank}(t)=r\vee\mathtt{rank}(t)=s})\big{|}_{\mathfrak{a}[m]}$
iff
$\mbox{TC}(x\big{|}_{\mathtt{rank}(t)=r\vee\mathtt{rank}(t)=s})\big{|}_{\mathfrak{a}[m]}=\mbox{TC}(y\big{|}_{\mathtt{rank}(t)=r\vee\mathtt{rank}(t)=s})\big{|}_{\mathfrak{a}[m]}$,
where all occurrences of $m$ in formula $\mathfrak{a}[m]$ are free. So, item v
from Definition 33 grants $x\equiv y\Leftrightarrow x=y$.

###### Theorem 65

$\forall
f(\mathbb{M}_{\mathfrak{a}}^{\dagger}(f)\Leftrightarrow(\sigma_{f}\neq\underline{\mathfrak{0}}\wedge
f\subseteq\underline{\mathfrak{1}}\wedge\forall x(f[x]\Rightarrow(\forall
t(t\equiv x\Rightarrow
f[t])\wedge(\mathfrak{a}[x]\vee\mathbb{M}_{\mathfrak{a}}^{\dagger}(x))))))$.

Proof

Analogous to the proof of Theorem 43 and a special case of Theorem 59.

Next theorem is a key result.

###### Theorem 66

Any $f:x\to y$, such that $\mathbb{M}_{\mathfrak{a}}^{\dagger}(x)$ and
$\mathbb{M}_{\mathfrak{a}}^{\dagger}(y)$, corresponds to a ZFU-function
$f^{\prime}$ where $\mathbb{M}_{\mathfrak{a}}^{\dagger}(f^{\prime})$ iff
neither $x$ nor $y$ acts on any atom.

Proof

From Theorem 62 and Definition 39 we know any $f:x\to y$, such that
$\mathbb{M}_{\mathfrak{a}}^{\dagger}(x)$ and
$\mathbb{M}_{\mathfrak{a}}^{\dagger}(y)$, corresponds to a ZFU-function where
$Dom^{\mathfrak{F}}_{f}=Dom_{f^{\prime}}=x$ and
$Im^{\mathfrak{F}}_{f}=Im_{f^{\prime}}=y$ (Theorem 63) and
$\mathbb{M}_{\mathfrak{a}}(f^{\prime})$. The question is whether
$\mathbb{M}_{\mathfrak{a}}^{\dagger}(f^{\prime})$ or not. For the $\Leftarrow$
part, suppose $x$ acts on an atom $u$ from $\mathfrak{a}$. That entails
$f(u)=v$ for some $v\neq\underline{\mathfrak{0}}$. But $f$ is in
correspondence to a ZFU-function $f^{\prime}$ iff $\forall u\forall
v(f[u]\wedge f(u)=v)\Leftrightarrow(f^{\prime}[(u,v)]\wedge
f^{\prime}((u,v))=(u,v))$, where $x$, $y$, and $f^{\prime}$ are Mengen in
$\nu^{\mathfrak{a}}_{\dagger}$. Thus, any ordered pair $(u,v)$ is supposed to
be a Menge in $\nu^{\mathfrak{a}}_{\dagger}$, where $f^{\prime}$ acts.
Nevertheless, according to Definition 22, $(u,v)$ is a function such that
$\alpha\stackrel{{\scriptstyle(u,v)}}{{{}_{\longmapsto}}}\alpha$ and
$\beta\stackrel{{\scriptstyle(u,v)}}{{{}_{\longmapsto}}}\beta$, where
$u\stackrel{{\scriptstyle\alpha}}{{{}_{\longmapsto}}}u$, and
$u\stackrel{{\scriptstyle\beta}}{{{}_{\longmapsto}}}u$ and
$v\stackrel{{\scriptstyle\beta}}{{{}_{\longmapsto}}}v$. Although $\alpha$ is a
Menge in $\nu^{\mathfrak{a}}$, it is no Menge in
$\nu^{\mathfrak{a}}_{\dagger}$. After all, any Menge from
$\nu^{\mathfrak{a}}_{\dagger}$ who acts on any atom $u$ is supposed to act on
$u^{\prime}$ as well, where $u\equiv u^{\prime}$. Since any atom $u$ in
$\mathfrak{a}$ admits an $u^{\prime}$ such that $u\neq u^{\prime}$ and
$u\equiv u^{\prime}$, then $\neg\mathbb{M}_{\mathfrak{a}}^{\dagger}(\alpha)$.
Therefore, $\neg\mathbb{M}_{\mathfrak{a}}^{\dagger}(f^{\prime})$. An analogous
rationale holds for the case where $y$ acts on any atom. For the $\Rightarrow$
part, suppose $f:x\to y$ corresponds to a ZFU-function $f^{\prime}$ such that
$\mathbb{M}_{\mathfrak{a}}^{\dagger}(f^{\prime})$. That entails $f^{\prime}$
acts on ordered pairs $(u,v)$ where $x[u]$ and $y[v]$. If either $u$ or $v$ is
an atom, we get the same contradiction we got in the $\Leftarrow$ part.

###### Theorem 67

The Partition Principle holds in $\nu^{\mathfrak{a}}_{\dagger}$.

Proof

Let $f^{\prime}$ be a ZFU-function such that
$\mathbb{M}_{\mathfrak{a}}^{\dagger}(f^{\prime})$ and whose domain and range
are, respectively, $x$ and $y$ (Definition 40). Then, there is a unique
$f:x\to y$ in correspondence to $f^{\prime}$ (Theorems 62 and 63). Axiom F11
grants an injection $c:y\to x^{\prime}$ such that $x^{\prime}\subseteq x$. But
since $f:x\to y$ is in correspondence to $f^{\prime}$ where
$\mathbb{M}_{\mathfrak{a}}^{\dagger}(f^{\prime})$, that entails neither $x$
nor $y$ act on any atom (Theorem 66). Therefore, $c:y\to x^{\prime}$ is in
correspondence to a ZFU-function $c^{\prime}$ where
$\mathbb{M}_{\mathfrak{a}}^{\dagger}(c^{\prime})$ (recall $x^{\prime}\subseteq
x$). Consequently, for any ZFU-function $f^{\prime}$ in
$\nu^{\mathfrak{a}}_{\dagger}$ such that $f$ is correspondence to
$f^{\prime}$, Partition Principle holds for $f^{\prime}$ in
$\nu^{\mathfrak{a}}_{\dagger}$, in the sense that $c^{\prime}$ is a Menge in
$\nu^{\mathfrak{a}}_{\dagger}$. Observe as well that $c^{\prime}$ is injective
in the usual sense concerning functions as collections of ordered pairs
(labeled here as ZFU-functions).

###### Theorem 68

Axiom of Choice fails in $\nu^{\mathfrak{a}}_{\dagger}$.

Proof

Let $f:\mathfrak{a}\to r$ be a function where $r$ is an ordinal (Definition
15). Observe we have $\mathbb{M}_{\mathfrak{a}}^{\dagger}(\mathfrak{a})$ and
$\mathbb{M}_{\mathfrak{a}}^{\dagger}(r)$. According to Theorem 66, there is no
ZFU-function $f^{\prime}$ such that
$\mathbb{M}_{\mathfrak{a}}^{\dagger}(f^{\prime})$ and $f$ is in correspondence
to $f^{\prime}$. Therefore, even if there is an injection $f$ from
$\mathfrak{a}$ to $r$, there is no ZFU-function $f^{\prime}$ in
$\nu^{\mathfrak{a}}_{\dagger}$ which corresponds to such an injection.
Therefore, $\mathfrak{a}$ cannot be well ordered in
$\nu^{\mathfrak{a}}_{\dagger}$ by means of any ZFU-function $f^{\prime}$.

The trick in the last two theorems is the fact that PP is a conditional: if
there is a function from $x$ to $y$, then there is an injection from $y$ to
$x^{\prime}\subseteq x$. Nevertheless, certain ZFU-functions (those whose
domains or ranges act on atoms) do not exist in $\nu^{\mathfrak{a}}_{\dagger}$
(Theorem 66).

Obviously, theorems 67 and 68 do not grant we have succeeded into the
introduction of a model of ZFU where PP holds but AC fails. After all, we
still need to prove the remaining axioms of ZFU are, in some sense, true in
our Lévy universe. That is why we need the next Section. But before we go any
further, we need to state our model, based on our previous discussions.

###### Definition 42

$x\in_{\mathfrak{a}}y$ iff
$y[x]\wedge\mathbb{M}_{\mathfrak{a}}^{\dagger}(y)\wedge(\exists t(t\equiv
x\wedge(\mathfrak{a}[t]\vee\mathbb{M}_{\mathfrak{a}}^{\dagger}(t)))\Rightarrow
y[t])$. If $\neg(x\in_{\mathfrak{a}}y)$, we abbreviate that as
$x\not\in_{\mathfrak{a}}y$.

For example, formula $\alpha_{r}\in_{\mathfrak{a}}y$ is equivalent to
$\overline{\alpha_{r}}\in_{\mathfrak{a}}y$ despite the fact that
$\alpha_{r}\neq\overline{\alpha_{r}}$ for any finite ordinal $r$. Observe
Theorem 64 grants we do not need to worry about any indiscernible of $x$ when
$x\in_{\mathfrak{a}}y$ and $x$ is a Menge. In that case $x\in_{\mathfrak{a}}y$
is equivalent to $y[x]\wedge\mathbb{M}_{\mathfrak{a}}^{\dagger}(y)$. Thus,

###### Theorem 69

Let $z$ be a function such that $\mathbb{M}_{\mathfrak{a}}^{\dagger}(z)$, and
$x$ and $y$ be both atoms (or both Mengen) of $\nu^{\mathfrak{a}}_{\dagger}$.
If $x\equiv y$, then $x\in_{\mathfrak{a}}z\Leftrightarrow
y\in_{\mathfrak{a}}z$.

Proof

Straightforward from Definition 42.

If, e.g., $x$ is a Menge of $\nu^{\mathfrak{a}}_{\dagger}$, given by
$\alpha_{r}\stackrel{{\scriptstyle x}}{{{}_{\longmapsto}}}\alpha_{r}$ and
$\overline{\alpha_{r}}\stackrel{{\scriptstyle
x}}{{{}_{\longmapsto}}}\overline{\alpha_{r}}$, then the only restrictions of
$x$ who are Menge of $\nu^{\mathfrak{a}}_{\dagger}$ are $x$ itself and
$\varphi_{0}$. In other words, atoms in a Lévy universe always ‘come in
pairs’. That is feasible thanks to the fact that the Axiom of Extensionality
of ZFU cannot decide who is who between two indiscernible atoms. So, if we
need any atom to form a Menge, we always take its ‘twin’ with it. That is a
different approach if we we compare it with permutation models [15]. Finally,

###### Definition 43

Let
$u=\underline{\mathfrak{1}}\big{|}_{\mathbb{M}_{\mathfrak{a}}^{\dagger}\,(t)}$,
$F(t)$ be the formula $\exists a\exists b(a\in_{\mathfrak{a}}b)\Leftrightarrow
t=(a,b)$, and $\epsilon=\underline{\mathfrak{1}}\big{|}_{F(t)}$. Then,