Properties of the atoms in finitely supported structures

Abstract

The goal of this paper is to present a collection of properties of the set of atoms and the set of finite injective tuples of atoms, as well as of the (finite and cofinite) powersets of atoms in the framework of finitely supported structures. Some properties of atoms are obtained by translating classical Zermelo–Fraenkel results into the new framework, but several important properties are specific to finitely supported structures (i.e. they do not have related classical Zermelo–Fraenkel and related non-atomic correspondents).

1 Approaches related to finitely supported structures

The theory of finitely supported algebraic structures named finitely supported mathematics (abbreviated as FSM) represents an alternative framework for characterizing infinite structures, hierarchically defined by involving some basic elements named atoms and by emphasizing only a finite number of characteristics. More exactly, in FSM we associate to each object a finite family of basic elements which is called its “finite support” [1]. As an intuitive example, in a lambda-calculus interpretation, the finite support of a lambda term modulo $\alpha$-equivalence is represented by the set of all “free variables” of that term; these variables are those who are really important in order to characterize the term, while the other (bound) variables can be renamed (by choosing new names from an infinite family of names) without affecting the essential properties of the lambda-term. This means that we can obtain an infinite family of lambda-terms starting from an original one (by renaming each time its bound variables), but in order to characterize this infinite family of lambda-terms it is enough to analyze the finite set of free variables of the original term.

Regarding finitely supported structures, the following approaches are known:

• The permutation models of ZFA set theory were developed in 1930s by Fraenkel, Lindenbaum and Mostowski in order to prove the independence of the axiom of choice from the other axioms of Zermelo–Fraenkel set theory with atoms (ZFA), where atoms in ZFA are elements with no internal structure obtained by modifying ZF axiom of foundation. We mention Fraenkel basic and second models, and Mostowski ordered model [9]. The ZFA universe is described as the von-Neumann cumulative hierarchy $\nu (A)$ of sets involving atoms from the set of atoms A:

  • $\nu _{0}(A)=\emptyset$;

  • $\nu _{\alpha +1}(A)=A+\wp (\nu _{\alpha }(A))$ for every non-limit ordinal $\alpha$ (we require that an ordinal does not have atoms among its elements)

  • $\nu _{\lambda }(A)={\mathop {\cup }\nolimits _{\alpha < \lambda }}\nu _{\alpha }(A)$; ($\lambda$ a limit ordinal);

  • $\nu (A)= {\mathop {\cup }\nolimits _{\alpha \,\text {is an ordinal}}} \nu _{\alpha }(A)$,

  where $+$ is the disjoint union of sets, and $\wp (X)$ is the powerset of X.

• Fraenkel–Mostowski (FM) axiomatic set theory was defined in [5] to properly model the syntax of formal systems involving variable binding operations. It is inspired by Fraenkel basic model, i.e. model N1 in [8]. However, FM, ZFA and ZF set theories are independent axiomatic set theories. All of these theories are described by independent axioms, and all of them have distinct models. Axioms of FM set theory (see Definition 2.9 in [1]) are the ZFA axioms over an infinite set A of atoms with an additional axiom of finite support claiming that any element has to be finitely supported according to a hierarchically constructed group action of the group of all permutation of atoms defined as below. Formally, an element x in a ZFA set is finitely supported if there exists a finite family $S \subseteq A$ such that any permutation of atoms that fixes S pointwise also leaves x invariant under the canonical group action $\cdot$ recursively defined on the class $\nu (A)$ of all ZFA sets by $\pi \cdot a=\pi (a)$ if a is an atom and $\pi \cdot x=\{\pi \cdot y\,|\,y \in x\}$ if x is a ZFA set. Since they have no internal structure, atoms can be used to represent names in syntax. The finite support axiom is motivated by the fact that syntax can only involve finitely many names. Any atom outside the finite support of an element corresponds to the concept of ‘fresh name for bound variables’. Binding is modelled by a certain concept of FM abstraction generalizing the notion of $\alpha$-abstraction in the $\lambda$-calculus. A model of axiomatic FM set theory is represented by the von-Neumann cumulative hierarchy ${ FM}_{A}$ defined as follows:

  • ${ FM}_{0}(A)=\emptyset$;

  • ${ FM}_{\alpha +1}(A)=A+\wp _{fs}(FM_{\alpha }(A))$ for every non-limit ordinal $\alpha$;

  • ${ FM}_{\lambda }(A)={\mathop {\cup }\nolimits _{\alpha < \lambda }}FM_{\alpha }(A)$; (whenever $\lambda$ is a limit ordinal);

  • ${ FM}_{A}= {\mathop {\cup }\nolimits _{\alpha \, \text {is an ordinal}}} FM_{\alpha }(A)$,

  where $\wp _{fs}(X)$ represents the family of those subsets of X that are finitely supported as elements of $\wp (X)$ under the restriction of $\cdot$ on $\wp (X)$. Thus, an FM set (i.e. an element in the FM universe ${ FM}_{A}$) is an hereditary finitely supported ZFA set under the action $\cdot$. Furthermore, ${ FM}_{A}$ is a model of FM set theory, but it is not a model of ZFA; more details regarding the relative consistency of FM set theory with respect to ZFA set theory can be found in [5]. Thus, we have:

  

  • ZF is formed by the empty set $\emptyset$ and all non-atomic sets (hierarchically constructed over $\emptyset$) which are obviously empty supported;

  • FM is formed by all the atoms, all ZF sets and all hereditary finitely supported atomic sets under the action $\cdot$ (where an ‘atomic’ set is defined as a set containing atoms somewhere in its structure);

  • ZFA is formed by all ZF sets, all the atoms and all atomic sets (possibly non-finitely supported).

• Nominal sets were studied in [11] (and several earlier papers of A. Pitts) as an alternative approach to non-standard axiomatic FM set theory. They can be well defined both in ZF and in FM frameworks. In ZF, a nominal set is a classical ZF set equipped with an action of the group of permutations of a certain fixed countable set A (formed by elements whose internal structure is irrelevant) having the additional property that any element is finitely supported (in the sense of Definition 1). The definition of nominal sets also makes sense in the FM framework by replacing the fixed ZF set A with the set of atoms in ZFA (this is possible because the internal structure of the elements of A is ignored). In FM framework, a nominal set is a set constructed according to the FM axioms with the additional property of being empty supported (invariant under all permutations) with respect to the action $\cdot$ defined on the class ${ FM}_{A}$. This is because nominal sets need to be closed under the group actions with who they are equipped (meaning that the nominality requires empty-supportness at the following order stage in an hierarchical construction). Furthermore, we proved in [1] that those nominal sets defined in the FM universe are logical notions in Tarski’s sense. By allowing the atoms to have an internal structure, nominal sets and several extensions are used in various areas related to computer science [4, 11].

• Admissible sets introduced in [2] as being defined over an arbitrary collection of atoms are also related to finitely supported structures. The hereditary finite sets used to describe ‘Gandy machines’ [6] are particular examples of admissible sets. The FM sets represent a generalization of hereditary finite sets because any FM set is an hereditary finitely supported set.

2 Constructing the theory of finitely supported structures

In order to develop FSM, we use nominal sets (extending the requirement that the set of atoms is countable) which by now on will be called invariant sets motivated by Tarski’s approach regarding logicality (i.e. a logical notion is defined by Tarski as one that is invariant under the one-to-one transformations of the universe of discourse onto itself). There is no major technical difference regarding FSM and nominal (related to basic definitions); conceptually, the nominal approach is related to computer science applications, while our approach is on the foundations of mathematics and experimental sciences by studying the consistency and inconsistency of various results within the framework of atomic sets with finite support. In FSM we study the finitely supported subsets of invariant sets together with finitely supported relations (order relations, functions, algebraic laws etc); thus, FSM is a theory of atomic algebraic structures defined according to the finite support requirement which states that any logical construction should be finitely supported under a canonical permutation action defined under the rules in Proposition 2 (e.g. FSM analyzes finitely supported monoids, finitely supported groups, finitely supported partially ordered sets, finitely supported fuzzy sets etc). The definition of FSM is consistent with respect to ZF set theory by adjoining an infinite ZF set A (formed by basic elements, i.e. elements whose internal structure is ignored) and imposing the additional requirement of ‘being finitely supported’ for all constructions that involve elements of A. Alternatively, A can be replaced by the set of atoms in ZFA (this is because we did not require a certain internal structure for the elements of the fixed ZF set A) and FSM will correspond to FM axiomatic set theory (without any restriction regarding the countability of the set of atoms).

Intuitively, FSM contains both the family of ‘non-atomic’ (ordinary) ZF structures (which are hierarchically constructed over $\emptyset$, and so they are trivially invariant) and the family of ‘atomic’ structures (hierarchically constructed from $\emptyset$ and from the fixed ZF set A) which have to be finitely supported under the canonical permutation action that is hierarchically constructed (using Proposition 2) from the basic permutation action on A defined by $(\pi , a) \mapsto \pi (a)$. Our main question is if a classical ZF result can be adequately reformulated by replacing ‘non-atomic structure’ with ‘atomic finitely supported structure’ in order to remain valid in FSM. We can easily remark that not every ZF result can be directly reformulated in terms of atomic finitely supported objects. This is because, given an invariant set X, there could exist some subsets of X which fail to be finitely supported. A related example is represented by the simultaneously infinite and coinfinite subsets of A.

In order to reformulate a general ZF result into FSM, the proof of the related FSM result should not brake the principle that any structure has to be finitely supported, which means that the related proof should be internally consistent in FSM and not retrieved from ZF. Thus we always need to verify if the proof of such a result in FSM employs only finitely supported structures, even in the intermediate steps. Our proving techniques follow those in the permutation models of set theory, being adapted to group actions and invariant sets. We present below two general methods of proving that a certain structure is finitely supported.

The constructive method for supports means to provide a hierarchical step-by-step construction of the support of a certain structure by employing the supports of the sub-structures of a related structure.

The${{\varvec{S}}}$-finite support principle states that for any finite set $S \subseteq A$, anything that is definable (in higher-order logic) from S-supported structures using S-supported constructions is S-supported. This is a refinement of equivariance principle form [11] allowing to prove boundedness properties for supports [1]. However, the formal application of this method overlaps sometimes on the constructive method described above.

In this paper we present a large collection of properties of the set of atoms, of its (finite or cofinite) powerset and of its (finite) higher-order powerset in FSM. In Sect. 4 we proved that atomic sets have many specific FSM properties (that are not translated from ZF). We structured these specific properties into five subsections presenting the relationship between atomic and non-atomic sets, specific (Dedekind-)finiteness properties of atomic sets, specific (order) properties of cardinalities in FSM, surprising fixed point properties of self mappings on the (finite) powerset of atoms, and the inconsistency various choice principles for specific atomic sets. Other properties of the atoms are obtained by translating classical (non-atomic) ZF results into FSM, by replacing ‘non-atomic object’ with ‘atomic finitely supported object’ (Sect. 5). Furthermore, in Sect. 6 we proved that the powerset of atoms satisfies some choice principles such as Prime Ideal Theorem and Ultrafilter Theorem although these principles are generally not valid in FSM (as proved in [1]). Ramsey’s Theorem for the set of atoms and Kurepa’s Antichain Principle for powerset of atoms also hold, and admit constructive proofs.

3 Finitely supported sets: formal properties

Let A be a fixed infinite ZF set formed by elements whose internal structure is not taken into consideration, which will be named the set of atoms. Actually, atoms are entities that can be checked only for equality, being considered as basic entities for a higher-order construction. Furthermore, we will prove that there does not exist a finitely supported bijection between A and an ordinary (non-atomic) ZF set, and so we cannot associate to A a certain ZF cardinality (such as countable, uncountable, etc); thus, we just say that the atoms form an infinite set without any specifications regarding its cardinality.

A transposition in FSM is a function $(a\, b):A\rightarrow A$ defined by $(a\, b)(a)=b$, $(a\, b)(b)=a$, and $(a\, b)(n)=n$ for $n\ne a,b$. A (finite) permutation of A in FSM is a bijection of A generated by composing finitely many transpositions. We denote by $S_{A}$ the set of all finite permutations of A. Actually, the finite permutations of A are those bijections of A that leaves unchanged all but finitely many atoms of A. However, as proved in [1], any finitely supported bijection of A would be necessarily a finite permutation of A. Thus, the notions ‘permutation (bijection) of A’ and ‘finite permutation of A’ coincide in FSM.

Definition 1

Let X be a ZF set.

• 1. An $S_{A}$-action on X is a function $\cdot :S_{A}\times X\rightarrow X$ having the properties that $Id\cdot x=x$ and $\pi \cdot (\pi '\cdot x)=(\pi \circ \pi ')\cdot x$ for all $\pi ,\pi '\in S_{A}$ and $x\in X$, where Id is the identity mapping on A. An $S_{A}$-set is a pair $(X,\cdot )$ where X is a ZF set, and $\cdot :S_{A}\times X\rightarrow X$ is an $S_{A}$-action on X.

• 2. Let $(X,\cdot )$ be an $S_{A}$-set. We say that $S\subset A$supportsx whenever for each $\pi \in Fix(S)$ we have $\pi \cdot x=x$, where $Fix(S)=\{\pi \,|\,\pi (a)=a,\forall a\in S\}$. The least finite set supporting x (which exists according to Proposition 1) is called the support of x and is denoted by ${ supp}(x)$. An empty supported element is called equivariant; this means that $x \in X$ is equivariant if and only if $\pi \cdot x=x$, $\forall \pi \in S_{A}$.

• 3. Let $(X,\cdot )$ be an $S_{A}$-set. We say that X is an invariant set if for each $x\in X$ there exists a finite set $S_{x}\subset A$ which supports x.

Proposition 1

[1] Let X be an $S_{A}$-set and let $x\in X$. If there exists a finite set supporting x (particularly, if X is an invariant set), then there exists a least finite set supporting x which is constructed as the intersection of all finite sets supporting x.

Proposition 2

[1] Let $(X,\cdot )$ and $(Y,\diamond )$ be $S_{A}$-sets.

• 1. The set A is an invariant set with the $S_{A}$-action $\cdot$ defined by $\pi \cdot a:=\pi (a)$ for all $\pi \in S_{A}$ and $a\in A$. Furthermore, ${ supp}(a)=\{a\}$ for each $a\in A$.

• 2. If $x\in X$ is finitely supported, then $\pi \cdot x$ is finitely supported with ${ supp}(\pi \cdot x)=\pi ({ supp}(x))$ for any $\pi \in S_{A}$.

• 3. An ordinary ZF set X constructed without involving atoms is necessarily a trivial invariant set, i.e a set endowed with the $S_{A}$ action $(\pi , x) \mapsto x$.

• 4. The set $S_{A}$ is an invariant with the $S_{A}$-action $\cdot$ defined by $\pi \cdot \sigma :=\pi \circ \sigma \circ \pi ^{-1}$ for all $\pi ,\sigma \in S_{A}$, where $\circ$ represents the usual composition of functions. Furthermore, ${ supp}(\sigma )=\{a\in A\,|\,\sigma (a)\ne a\}$ for each $\sigma \in S_{A}$.

• 5. The Cartesian product $X\times Y$ is also an $S_{A}$-set with the $S_{A}$-action $\otimes$ defined by $\pi \otimes (x,y)=(\pi \cdot x,\pi \diamond y)$ for all $\pi \in S_{A}$ and all $x\in X$, $y\in Y$. If $(X,\cdot )$ and $(Y,\diamond )$ are invariant sets, then $(X\times Y,\otimes )$ is also an invariant set.

• 6. The powerset $\wp (X)=\{Z\,|\, Z\subseteq X\}$ is also an $S_{A}$-set with the $S_{A}$-action $\,\star \,$ defined by $\pi \,\star \, Z:=\{\pi \cdot z\,|\, z\in Z\}$ for all $\pi \in S_{A}$, and all $Z \subseteq X$. For each invariant set $(X,\cdot )$, we denote by $\wp _{fs}(X)$ the set formed from those subsets of X which are finitely supported according to the action $\,\star \,$ . $(\wp _{fs}(X),\,\star \,|_{\wp _{fs}(X)})$ is an invariant set, where $\,\star \,|_{\wp _{fs}(X)}$ represents the action $\,\star \,$ restricted to $\wp _{fs}(X)$.

• 7. The finite powerset of X$\wp _{{ fin}}(X)=\{Y \subseteq X\,|\, Y \text {finite}\}$ and the cofinite powerset of X$\wp _{{ cofin}}(X)=\{Y \subseteq X\,|\, X{\setminus } Y \text {finite}\}$ are $S_{A}$-sets with the $S_{A}$-action $\,\star \,$ defined as in item 6. If X is an invariant set, then both $\wp _{{ fin}}(X)$ and $\wp _{{ cofin}}(X)$ are invariant sets.

Definition 2

Let $(X,\cdot )$ be an invariant set. A subset Z of X is called finitely supported if and only if $Z\in \wp _{fs}(X)$ with the notations from Proposition 2. A subset Z of X is uniformly supported if all the elements of Z are supported by the same set S (meaning that Z itself is supported by S).

Since $S_{A}$ is a torsion group (i.e. $\forall \pi \in S_{A}, \exists n \in {\mathbb {N}}$ such that $\pi ^{n}=Id$), a subset Z of an invariant set $(X, \cdot )$ is finitely supported by a set $S \subseteq A$ if and only if $\pi \cdot z \in Z$ for all $z \in Z$ and all $\pi \in Fix(S)$. Not any subset of an invariant set is finitely supported.

Proposition 3

We have $\wp _{fs}(A)=\wp _{{ fin}}(A) \cup \wp _{{ cofin}}(A)$.

Proof

We know that, if $B \subset A$ and B is finite, then B is finitely supported by B with ${ supp}(B)=B$. If $C \subseteq A$ and C is cofinite, then C is finitely supported by $A {\setminus } C$ with ${ supp}(C)=A {\setminus } C$. However, if $D \subsetneq A$ is neither finite nor cofinite, then D is not finitely supported. Indeed, assume by contradiction that there exists a finite set of atoms S supporting D. Since S is finite and both D and its complementary $C_{D}$ are infinite, we can take $a \in D {\setminus } S$ and $b \in C_{D} {\setminus } S$. Then the transposition $(a\,b)$ fixes S pointwise, but $(a\,b) \,\star \, D \ne D$ because $(a\,b)(a)=b \notin D$; this contradicts the assertion that S supports D. Therefore, $\wp _{fs}(A)=\wp _{{ fin}}(A) \cup \wp _{{ cofin}}(A)$. $\square$

According to Proposition 3, for any fixed finite set $S \subseteq A$, there are only finitely many subsets of A supported by S, namely the subsets of S and the supersets of $A{\setminus } S$; therefore $\wp _{fs}(A)$ does not have an infinite uniformly supported subset. A related result is presented in Theorem 1(2).

Since functions are particular subsets of a Cartesian product of two sets, we have the following results.

Definition 3

Let X and Y be invariant sets.

• 1. A function $f{:}\,X\rightarrow Y$ is finitely supported if $f\in \wp _{fs}(X\times Y)$. The set of all finitely supported functions from X to Y is denoted by $Y^{X}_{fs}$.

• 2. Let Z be a finitely supported subset of X and T a finitely supported subset of Y. A function $f{:}\,Z\rightarrow T$ is finitely supported if $f\in \wp _{fs}(X\times Y)$. The set of all finitely supported functions from Z to T is denoted by $T^{Z}_{fs}$.

Proposition 4

[1] Let $(X,\cdot )$ and $(Y,\diamond )$ be two invariant sets.

• 1. $Y^{X}$ (i.e. the set of all functions from X to Y) is an $S_{A}$-set with the $S_{A}$-action ${\widetilde{\,\star \,}}:S_{A}\times Y^{X}\rightarrow Y^{X}$ defined by $(\pi {\widetilde{\,\star \,}}f)(x) = \pi \diamond (f(\pi ^{-1}\cdot x))$ for all $\pi \in S_{A}$, $f\in Y^{X}$ and $x\in X$. A function $f{:}\,X\rightarrow Y$ is finitely supported in the sense of Definition 3 if and only if it is finitely supported with respect the permutation action ${\widetilde{\,\star \,}}$.

• 2. Let Z be a finitely supported subset of X and T a finitely supported subset of Y. A function $f{:}\,Z\rightarrow T$ is supported by a finite set $S \subseteq A$ if and only if for all $x \in Z$ and all $\pi \in Fix(S)$ we have $\pi \cdot x \in Z$, $\pi \diamond f(x) \in T$ and $f(\pi \cdot x)=\pi \diamond f(x)$.

Two invariant sets X and Y are called equipollent if there exists a finitely supported bijection $f{:}\,X \rightarrow Y$. The cardinality of X is defined as the equivalence class of all invariant sets equipollent to X, and is denoted by |X|. On the family of cardinalities we can define the equivariant relation $\le$ by: $|X| \le |Y|$ if and only if there is a finitely supported injection $f{:}\,X \rightarrow Y$. It is not difficult to prove that $\le$ is an order relation. The reflexivity is obvious. The transitivity is also easy because whenever there exist a finitely supported injection $f{:}\, X \rightarrow Y$ and a finitely supported injection $g:Y \rightarrow Z$, there also exists an injection $g \circ f: X \rightarrow Z$ that is finitely supported by ${ supp}(f) \cup supp(g)$. The antisymmetry is a consequence of Lemma 3. Note that the relation $\le$ extended to FSM sets that are not necessarily invariant is also an equivariant order relation (the proof uses the similar arguments as above and the remark that whenever X, Y are FSM sets and $f{:}\,X \rightarrow Y$ is a finitely supported injection, we have that $\pi {\widetilde{\,\star \,}}f: \pi \,\star \, X \rightarrow \pi \,\star \, Y$ defined by $(\pi {\widetilde{\,\star \,}}f)(\pi \cdot x)=\pi \cdot f(x)$$\forall x \in X$ is a finitely supported injection which proves the equivariance of $\le$).

4 Specific properties of the atoms in FSM

The set of atoms, its powerset, the family of its (finite) subsets and the family of all finite injective tuples of atoms have some specific properties in FSM.

4.1 Connections with non-atomic sets

Theorem 1

Regarding functions between atomic and non-atomic sets we have:

• 1. If X is an infinite ordinary (non-atomic) ZF set, then for any finitely supported function $f : A \rightarrow X$ and any finitely supported function $g{:}\, X \rightarrow A$, Im(f) and Im(g) are finite. As a direct consequence, there are no finitely supported injective mappings and no finitely supported surjective mappings between A and X.

• 2. There are no finitely supported injective mappings $f{:}\,\wp _{fs}(A) \rightarrow X$ or $g:X \rightarrow \wp _{fs}(A)$ between $\wp _{fs}(A)$ and an infinite ordinary (non-atomic) ZF set X. As a direct consequence, when $X ={\mathbb {N}}$), $\wp _{fs}(A)$ has no finitely supported countably infinite subset.

• 3. There does not exist a finitely supported surjective mapping $f{:}\, X \rightarrow \wp _{fs}(A)$ from an infinite ordinary (non-atomic) ZF set X onto $\wp _{fs}(A)$, but there exists a finitely supported (equivariant) surjective mapping $f{:}\, \wp _{fs}(A) \rightarrow {\mathbb {N}}$ from $\wp _{fs}(A)$ onto the set of all natural numbers ${\mathbb {N}}$.

• 4. A function $f{:}\, A \rightarrow X$ between A and an ordinary (non-atomic) ZF set X is finitely supported if and only if there exists $x \in X$ such that $\{y \in A \;|\; f(y)\ne x\}$ is finite. In this case, ${ supp}(f)=\{y \in A \;|\; f(y)\ne x\}$.

Proof

• 1. Let us consider a finitely supported mapping $f{:}\,A \rightarrow X$. Let let us fix an element $b\in A$ with $b\notin supp(f)$. Such an atom b exists because A is infinite, while ${ supp}(f)$ is finite. Let c be an arbitrary element from $A{\setminus } supp(f)$. Since $b\notin supp(f)$, we have that $(b\, c)$ fixes every element from ${ supp}(f)$, i.e. $(b\, c)\in Fix({ supp}(f))$. However, ${ supp}(f)$ supports f, and so, by Proposition 4, we have $f((b\, c)(a))=(b\,c) \diamond f(a)=f(a)$ for all $a\in A$ (with $\diamond$ we denoted the necessarily trivial $S_{A}$-action on X). In particular, $f(c)=f((b\,c)(b))=f(b)$. Since c has been chosen arbitrarily from $A {\setminus } supp(f)$, it follows that $f(c)=f(b)$, for all $c \in A {\setminus } supp(f)$. If ${ supp}(f)=\{a_{1}, \ldots , a_{n}\}$, then $Im(f) = \{f(a_{1})\}\cup \cdots \cup \{f(a_{n})\} \cup \{f(b)\}$, and so Im(f) is finite (because it is a finite union of singletons).

  Let $g{:}\, X \rightarrow A$ be a finitely supported function. Assume by contradiction that Im(g) is infinite. Pick any atom $a \in Im(g) {\setminus } supp(g)$ (such an atom exists because ${ supp}(g)$ is finite). There exists an $x \in X$ such that $g(x) = a$. Now pick any atom $b \in Im(g) {\setminus } ({ supp}(g) \cup \{a\})$, The transposition $(a\,b)$ fixes ${ supp}(g)$ pointwise, and so $g(x)=g((a\,b) \diamond x)=(a\,b) \cdot g(x) =(a\, b)(a)= b$, contradicting the fact that g is a function. Thus Im(g) is finite.

• 2. Suppose by contradiction that there is a finitely supported injection $f{:}\,\wp _{fs}(A) \!\rightarrow \! X$. Since there also is an equivariant injection $a \mapsto \{a\}$ from A into $\wp _{fs}(A)$, this contradicts the statement in item 1 that there is no finitely supported injection from A to X.

  Furthermore, we prove by contradiction that there does not exist a finitely supported injective mapping $g:X\rightarrow \wp _{fs}(A)$. Suppose that there is a finitely supported injection $g:X\rightarrow \wp _{fs}(A)$. Then g(X) is an infinite family of subsets of A with the property that all the elements of g(X) are supported by the same finite set ${ supp}(g)$. This is because X is trivially invariant, and so $\pi \,\star \, g(x)=g(\pi \diamond x)=g(x)$ for all $x \in X$ and all $\pi \in Fix({ supp}(g))$. However, there are only finitely many subsets of A supported by ${ supp}(g)$, namely the subsets of ${ supp}(g)$ and the supersets of $A{\setminus } supp(g)$.

• 3. Suppose, by contradiction, that there exists a finitely supported surjective mapping $f{:}\, X \rightarrow \wp _{fs}(A)$. Obviously, one can define a finitely supported surjection $s:\wp _{fs}(A) \rightarrow A$ as below. Let us fix an atom $x \in A$. We define s by $s(X)=\left\{ \begin{array}{ll} a, &{} \text {if}\, X\text { is an one-element set } \{\text {a}\} ;\\ x, &{} \text {if}\, X\text { has more than one element}\, \end{array}\right.$. Clearly s is supported by ${ supp}(x)=\{x\}$. Then, $s \circ f$ is a finitely supported surjection from X onto A which contradicts item 1.

  We prove now that there exists a finitely supported surjective mapping $h:\wp _{fs}(A) \rightarrow {\mathbb {N}}$. Define $h(B)=|supp(B)|, \forall B \in \wp _{fs}(A)$. Let us consider the equivariant family $(X_{i})_{i \ge 1}$ where each $X_{i}$ is the set of all i-sized subsets of A. Since A is infinite, it follows that each $X_{i}, i \ge 1$ is non-empty. Furthermore, $h(\emptyset )=h(A)=0$ and for any fixed $n \in \mathbb {N^{*}}$ we have $h(\{a_{1}, \ldots , a_{n}\})=|supp(\{a_{1}, \ldots , a_{n}\})|=|\{a_{1}, \ldots , a_{n}\}|=n$, for all $\{a_{1}, \ldots , a_{n}\} \in X_{n}$. Thus, $Im(h)={\mathbb {N}}$, and so h is surjective. No choice principle is required because, for proving the surjectivity of h, we do not need to identify a set of representatives for the family $(X_{i})_{i \ge 1}$. We claim now that h is equivariant. According to Proposition 2(2) and because every permutation of atoms is bijective, we have $h(\pi \,\star \, B)=|supp(\pi \,\star \, B)|=|\pi ({ supp}(B))|=|supp(B)|=h(B)$ for all $\pi \in S_{A}$ and $B \in \wp _{fs}(A)$. From Proposition 4, h is equivariant.

• 4. Let $f{:}\,A\rightarrow X$ be a finitely supported function. According to item 1 and Proposition 3, we have $Im(f)= \{f(a_{1})\}\cup \cdots \cup \{f(a_{n})\} \cup \{f(b)\}$, where ${ supp}(f)=\{a_{1}, \ldots , a_{n}\}$ and b is an arbitrary element from $A {\setminus } supp(f)$. We take $x=f(b)$. Let us suppose now that $S=\{y\in A\,|\, f(y)\ne x\}$ supports f. Let $\pi \in Fix(S)$. According to Proposition 4, we have to prove that $f(\pi (a))=f(a)$ for all $a\in A$. Let $a\in A$ be an arbitrary element. If $f(a)\ne x$, we have $a\in S$, and $\pi (a)=a$ because $\pi$ fixes S pointwise. Therefore, $f(\pi (a))=f(a)$. Now let $a\in A$ with $f(a)=x$. Let us suppose, by contradiction, that $f(\pi (a))\ne x$. It follows that $\pi (a)\in S$ and $\pi (\pi (a))=\pi (a).$ Since $\pi$ is bijective, we get $\pi (a)=a$ and $f(\pi (a))=f(a)=x$ which contradicts our assumption that $f(\pi (a))\ne x$. Therefore, $f(\pi (a))=x=f(a)$. We proved that S supports f. It remains to prove that S is minimal between the finite sets supporting f. Let V be a finite set supporting f. We claim $S\subseteq V$. Let $b\in S$, i.e. $f(b)\ne x$. Suppose, by contradiction, that $b\notin V$. Let c be an arbitrary element from $A{\setminus } V$. Since $b,c\notin V$, we have $(b\, c)\in Fix(V)$. However, V supports f. This means $f((b\, c)(a))=f(a)$, $\forall a\in A$. In particular, $f(c)=f((b\, c)(b))=f(b)\ne x$. Therefore, $c\in S$, and so $(A{\setminus } V)\subseteq S$. Since $A{\setminus } V$ is infinite, we obtain that S is cofinite which contradicts the assumption that S is finite. Therefore, $b\in V$, and $S\subseteq V$. Thus, S is the least finite set supporting f, and so it is the support of f according to Proposition 1. $\square$

Remark 1

If X is an infinite ordinary ZF set and $f{:}\,A \rightarrow X$ is a finitely supported function, we proved that Im(f) is obviously finite. However, the converse of this assertion is not true. There may exist an ordinary ZF set X and a ZF function $f{:}\, A \rightarrow X$ such that Im(f) is finite, but f is not finitely supported. Indeed, let X be an ordinary ZF set X with at least two elements and let us fix two elements $u,v \in X$. Let P be a ZF subset of A which is simultaneously infinite and coinfinite. Such a subset of A may exist in ZF. We define $g:A \rightarrow X$ by $g(x)=\left\{ \begin{array}{ll} u &{} \text {for}\, x \in P\\ v &{} \text {for}\, x\in A {\setminus } P \end{array}\right.$. For any permutation $\pi$, we have that $g(\pi (x))=g(x)$ for all $x \in A$ if and only if we have $\pi (x) \in P$ whenever $x \in P$ (i.e. if and only if P is left invariant by $\pi$). Therefore, because P is not finitely supported, it follows that g is not finitely supported.

4.2 Finiteness properties

Lemma 1

Let $(X, \cdot )$ be an invariant set such that there exists a finitely supported injection of X into one of its finitely supported proper subsets. Then there exists a finitely supported injective mapping $f{:}\, {\mathbb {N}} \rightarrow X$.

Proof

Suppose that $g: X \rightarrow X$ is a finitely supported injection with the property that $Im(g) \subsetneq X$. This means that there exists $x_{0}\in X$ such that $x_{0}\notin Im(g)$. We can define a sequence of elements from X which has the first term $x_{0}$ and the general term $x_{n+1}=g(x_{n})$ for all $n \in {\mathbb {N}}$. Since $x_{0}\notin Im(g)$ it follows that $x_{0} \ne g(x_{0})$. Since g is injective and $x_{0} \notin Im(g)$, by induction we obtain that $g^{n}(x_{0}) \ne g^{m}(x_{0})$ for all $n,m \in {\mathbb {N}}$ with $n \ne m$. Moreover, $x_{n+1}$ is supported by ${ supp}(g)\cup supp(x_{n})$ for all $n \in {\mathbb {N}}$. Indeed, let $\pi \in Fix({ supp}(g)\cup supp(x_{n}))$. According to Proposition 4, $\pi \cdot x_{n+1}= \pi \cdot g(x_{n})=g(\pi \cdot x_{n})=g(x_{n})=x_{n+1}$, and so ${ supp}(x_{n+1}) \subseteq supp(g)\cup supp(x_{n})$ for all $n \in {\mathbb {N}}$. By finite recursion, we have ${ supp}(x_{n}) \subseteq supp(g)\cup supp(x_{0})$ for all $n\in {\mathbb {N}}$. Since all $x_{n}$ are supported by the same set of atoms, we have that the function $f{:}\,{\mathbb {N}} \rightarrow X$, defined by $f(n)=x_{n}$, is also finitely supported (by the set ${ supp}(g)\cup supp(x_{0})$ not depending on n). This follows from Proposition 4 because for any $\pi \in Fix({ supp}(g)\cup supp(x_{0}))$ we have $f(\pi \diamond n)=f(n)=x_{n}=\pi \cdot x_{n}=\pi \cdot f(n)$, $\forall n \in {\mathbb {N}}$, where by $\diamond$ we denoted the trivial $S_{A}$-action on ${\mathbb {N}}$. Obviously, f is also injective. $\square$

Theorem 2

Although A, $\wp _{fs}(A)$ and $S_{A}$ are infinite, we have the following specific FSM finiteness properties:

• 1. A finitely supported function $f{:}\,A \rightarrow A$ is surjective if and only if it is injective.

• 2. Any finitely supported injection $f{:}\,\wp _{fs}(A) \rightarrow \wp _{fs}(A)$ is also surjective.

• 3. Any finitely supported injection $f{:}\,\wp _{{ fin}}(\wp _{fs}(A)) \rightarrow \wp _{{ fin}}(\wp _{fs}(A))$ is also surjective.

• 4. For a finitely supported bijection $f{:}\,A \rightarrow A$, the set $\{a\in A\,|\,f(a)\ne a\}$ is finite and ${ supp}(f)=\{a\in A\,|\,f(a)\ne a\}$. This means any finitely supported bijection of A onto A should be a (finite) permutation of A. Consequently, the group of all finitely supported bijections of A onto A is locally finite (meaning that each of its finitely generated subgroups is finite).

• 5. Every finitely supported injection $f{:}\,S_{A} \rightarrow S_{A}$ is also surjective.

• 6. The set A of atoms has the property that for all increasing chain $X_{0}\subseteq X_{1}\subseteq \cdots \subseteq X_{n}\subseteq \cdots$ of finitely supported subsets such that $n\mapsto X_{n}$ is finitely supported, we have that $(X_{n})$ is eventually constant.

Proof

• 1. Suppose $f{:}\, A \rightarrow A$ is a finitely supported injection. Since A does not contain an infinite uniformly supported subset, from Lemma 1 we have that f is surjective. Conversely, let $f{:}\, A \rightarrow A$ be a finitely supported surjective function. Firstly, it is fairly easy to verify that $f[supp(f)] = supp(f)$. Indeed, let $c \in supp(f)$. Since f is onto (by hypothesis), there is an $x^{*} \in A$ such that $f(x^{*}) = c$. If $x^{*} \in supp(f)$, then we are done; so assume that $x^{*} \notin supp(f)$. But then it is fairly obvious that Im(f) is finite. Indeed, for any $y \in A{\setminus } ({ supp}(f) \cup \{x^{*}\})$, consider the transposition $\pi = (x^{*} \, y)$ and note that $\pi \in Fix({ supp}(f) \cup \{c\})$. Thus, $f(y)=f(\pi \cdot x^{*})=\pi \cdot f(x^{*})=\pi \cdot c=c$. This contradicts the hypothesis that $f{:}\, A \rightarrow A$ is onto, and so ${ supp}(f) \subseteq f[supp(f)]$. However, it is obvious that f(X) is supported by ${ supp}(f) \cup supp(X)$ whenever $X \in \wp _{fs}(A)$, and so f[supp(f)] is supported by ${ supp}(f) \cup supp({ supp}(f))=supp(f)$. According to Proposition 1, this means ${ supp}(f[supp(f)]) \subseteq supp(f)$. Since f[supp(f)] is a finite subset of A, we have $f[supp(f)]=supp(f[supp(f)]) \subseteq supp(f)$, from which we get ${ supp}(f) = f[supp(f)]$. It follows that the restriction $f|_{supp(f)} : supp(f) \rightarrow supp(f)$ is a bijection (recall that ${ supp}(f)$ is a finite set). Now we show that $f|_ {A {\setminus } supp(f)}$ is the identity mapping. Fix $a \in A {\setminus } supp(f)$ and by way of contradiction assume $f(a) \ne a$, say $f(a) = b$. Then arguing as above, it can be easily shown that $f[A {\setminus } ({ supp}(f) \cup \{b\})] = \{b\}$. Indeed, take any $c \in A {\setminus } ({ supp}(f) \cup \{a, b\})$ and consider the transposition $\pi = (a\, c) \in Fix({ supp}(f))$, then $f(c)=f((a\,c)\cdot a)=(a\,c) \cdot f(a)=(a\,c)\cdot b=b$. Thus Im(f) is finite, a contradiction. Hence $f|_{A {\setminus } supp(f)}$ is the identity mapping, and consequently in view of the first observation (that the restriction $f|_{supp(f)} : supp(f) \rightarrow supp(f)$ is bijective), f is one-to-one.

• 2. Let us consider a finitely supported injection $f{:}\,\wp _{fs}(A) \rightarrow \wp _{fs}(A)$. Since $\wp _{fs}(A)$ does not contained an infinite uniformly supported subset [see Theorem 1(2)], by Lemma 1f is surjective.

• 3. We denote $\wp _{fs}(A)=X$. Let us consider a finitely supported injection $f{:}\,\wp _{{ fin}}(X) \rightarrow \wp _{{ fin}}(X)$. If f is not surjective, then according to Lemma 1 there exist a countable infinite uniformly supported family ${\mathcal {F}}=(X_{i})_{i \in {\mathbb {N}}} \subseteq \wp _{{ fin}}(X)$. Thus, each element $X_{n}\in {\mathcal {F}}$ is supported by the same finite set ${ supp}({\mathcal {F}})$. Fix an arbitrary $j \in {\mathbb {N}}$. We claim that $X_{j}$ has the property that ${ supp}(x) \subseteq supp({\mathcal {F}})$ for all $x \in X_{j}$. Firstly we remind that $X_{j}$ is a finite subset of X. Thus, $X_{j}=\left\{ x_{1},\ldots , x_{n}\right\} \subseteq X$ for some $n \in {\mathbb {N}}$. Let $S=supp(x_{1})\cup \cdots \cup supp(x_{n})$. We prove that $S=supp(X_{j})$. Obviously, S supports $X_{j}$. Indeed, let us consider $\pi \in Fix(S)$. We have that $\pi \in Fix({ supp}(x_{i}))$ for each $i\in \{1,\ldots ,n\}$. Therefore, $\pi \cdot x_{i}=x_{i}$ for each $i\in \{1,\ldots , n\}$ because ${ supp}(x_{i})$ supports $x_{i}$ for each $i\in \{1,\ldots , n\}$, and so ${ supp}(X_{j}) \subseteq S$. It remains to prove that $S \subseteq supp(X_{j})$. Consider $a \in S$. This means there exists $k\in \{1,\ldots ,n\}$ such that $a \in supp(x_{k})$. Due to the infiniteness of A we can consider an atom b such that $b \notin supp(X_{j})$ and $b \notin supp(x_{i})$$\forall i\in \{1,\ldots ,n\}$. We prove by contradiction that $(b\; a) \cdot x_{k} \notin X_{j}$. Indeed, suppose that $(b\; a) \cdot x_{k} \in X_{j}$. In this case there is $y \in X_{j}$ with $(b\; a) \cdot x_{k}=y$. Since $a \in supp(x_{k})$, we have $b=(b\;a)(a) \in (b\; a)({ supp}(x_{k}))$. However, according to Proposition 2(2), we have ${ supp}(y)=(b\; a)({ supp}(x_{k}))$. We obtain that $b \in supp(y)$ for some $y \in X_{j}$, which is a contradiction with the choice of b. Therefore, $(b\; a) \,\star \, X_{j} \ne X_{j}$, where $\,\star \,$ is the standard $S_{A}$-action on $\wp (Y)$. Since $b \notin supp(X_{j})$, we prove by contradiction that $a \in supp(X_{j})$. Indeed, suppose that $a \notin supp(X_{j})$. It follows that the transposition $(b\; a)$ fixes each element from ${ supp}(X_{j})$, i.e. $(b\; a) \in Fix({ supp}(X_{j}))$. Since ${ supp}(X_{j})$ supports $X_{j}$, it follows that $(b\; a) \,\star \, X_{j}=X_{j}$, which is a contradiction. Thus, $a \in supp(X_{j})$, and so $S \subseteq supp(X_{j})$. Thus, $S=supp(X_{j})$. Now, since ${ supp}(X_{j}) \subseteq supp({\mathcal {F}})$, we have ${\mathop {\cup }\nolimits _{x \in X_{j}}}supp(x) \subseteq supp({\mathcal {F}})$, and so ${ supp}(x) \subseteq supp({\mathcal {F}})$ for all $x \in X_{j}$. Since j has been arbitrarily chosen, it follows that every element from every set of form $X_{i}$ is supported by $supp({\mathcal {F}})$, and so ${\mathop {\cup }\nolimits _{i}}X_{i}$ is an uniformly supported subset of X (all its elements being supported by $supp({\mathcal {F}})$). Furthermore, ${\mathop {\cup }\nolimits _{i \in {\mathbb {N}}}}X_{i}$ is infinite because the sequence $(X_{i})_{i \in {\mathbb {N}}}$ is infinite and injective. Otherwise, if ${\mathop {\cup }\nolimits _{i}}X_{i}$ was finite, the family $(X_{i})_{i \in {\mathbb {N}}}$ would be contained in the finite set $\wp ({\mathop {\cup }\nolimits _{i}}X_{i})$, and so it couldn’t be infinite and injective. We were able to construct an infinite uniformly supported subset of $X=\wp _{fs}(A)$, namely ${\mathop {\cup }\nolimits _{i}}X_{i}$, contradicting Theorem 1(2). Therefore, f is surjective.

• 4. This result is presented as Proposition 2.6 in [1].

• 5. If there was an element $\sigma _{0} \in S_{A}$ with $\sigma _{0} \notin Im(f)$, then according to Lemma 1 we could form an infinite sequence of distinct finite permutations of A uniformly supported by ${ supp}(f) \cup supp(\sigma _{0})$. By item 4, for each finitely supported bijection $\sigma :A \rightarrow A$ we have that the set of atoms changed by $\sigma$ is contained in ${ supp}(\sigma )$. For a finite set S of atoms there are at most |S|! bijections of A onto A supported by S. This assertion follows because whenever a bijection $\sigma :A \rightarrow A$ is finitely supported by S we have $\{a\in A\,|\,\sigma (a)\ne a\} \subseteq supp(\sigma ) \subseteq S$, and so the highest possible number of bijections of A onto A supported by S is the number of permutations of S. Thus, there could be at most $|supp(f) \cup supp(\sigma _{0})|!$ finite permutations of A supported by ${ supp}(f) \cup supp(\sigma _{0})$, and so there does not exist an infinite sequence of distinct bijections of A onto A uniformly supported by ${ supp}(f) \cup supp(\sigma _{0})$.

• 6. If there is an increasing chain $X_{0}\subseteq X_{1}\subseteq \cdots \subseteq A$ such that $n \mapsto X_{n}$ is finitely supported, then, according to Proposition 4 and because ${\mathbb {N}}$ is a trivial invariant set, each element $X_{i}$ of the chain must be supported by the same $S=supp(n \mapsto X_{n})$. However, by Theorem 1(2), $\wp _{fs}(A)$ does not contain an infinite uniformly supported subset. $\square$

4.3 Atomic cardinalities

Theorem 3

The set of atoms and its powerset have the following properties:

• 1. There does not exist a finitely supported surjection $f{:}\, \wp _{fs}(A) \rightarrow A \times A$.

• 2. There does not exist a finitely supported injection $f{:}\, A \times A \rightarrow \wp _{fs}(A)$.

• 3. There is no finitely supported surjection $f{:}\, \wp _{fs}(A) \rightarrow \wp _{fs}(A) \times \wp _{fs}(A)$.

• 4. There is no finitely supported injection $f{:}\, \wp _{fs}(A) \times \wp _{fs}(A) \rightarrow \wp _{fs}(A)$.

• 5. $|\wp _{fs}(A)|=2|\wp _{{ fin}}(A)|$.

• 6. $\wp _{{ fin}}(A)$ is infinite, but $|\wp _{{ fin}}(A)| \ne 2|\wp _{{ fin}}(A)|$.

• 7. $|A|<|\wp _{n}(A)|<|2^{A}_{fs}|$ for all $n \ge 2$, where $\wp _{n}(A)\overset{def}{=}\{X \subseteq A \,|\,|X|=n\}$.

• 8. $|A|<|\wp _{{ fin}}(A)|<|2^{A}_{fs}|$.

• 9. There is no finitely supported surjection $f{:}\, A \rightarrow A \times A$.

• 10. There is no finitely supported injection $f{:}\, A \times A \rightarrow A$.

• 11. There is a finitely supported surjection from the family of all finite one-to-one tuples of atoms onto the family of all finite one-to-one non-empty tuples of atoms, and a finitely supported surjection from the family of all finite one-to-one non-empty tuples of atoms onto the family of all finite one-to-one tuples of atoms, but there is no finitely supported bijection between these two families.

• 12. There is a finitely supported bijection between the powerset of the family of all finite one-to-one tuples of atoms and the powerset of the family of all finite one-to-one non-empty tuples of atoms, but there is no finitely supported bijection between the family of all finite one-to-one tuples of atoms and the family of all finite one-to-one non-empty tuples of atoms.

Proof

• 1. Suppose, by contradiction, that there is a finitely supported surjective mapping $f{:}\, \wp _{fs}(A) \rightarrow A \times A$. Let us consider two atoms $a,b\notin supp(f)$ with $a \ne b$. These atoms exist because A is infinite, while ${ supp}(f) \subseteq A$ is finite. It follows that the transposition $(a\, b)$ fixes each element from ${ supp}(f)$, i.e. $(a\, b) \in Fix({ supp}(f))$. Since f is surjective, it follows that there exists an element $X \in \wp _{fs}(A)$ such that $f(X)=(a,b)$. Since ${ supp}(f)$ supports f and $(a\, b) \in Fix({ supp}(f))$, from Proposition 4 we have $f((a\,b) \,\star \, X)=(a\,b) \otimes f(X)=(a\,b) \otimes (a,b)=((a\,b)(a), (a\,b)(b))=(b,a)$. Due to the functionality of f we should have $(a\,b) \,\star \, X \ne X$. Otherwise, we would obtain $(a,b)=(b,a)$.

  We claim that if both $a,b \in supp(X)$, then $(a\,b)\,\star \, X=X$. Indeed, suppose $a,b \in supp(X)$. Since X is a finitely supported subset of A, then X is either finite or cofinite (according to Proposition 3). If X is finite, then ${ supp}(X)=X$, and so $a,b \in X$. Moreover, $(a\, b)(a)=b$, $(a\, b)(b)=a$, and $(a\, b)(c)=c$ for all $c \in X$ with $c\ne a,b$. Therefore, $(a\,b) \,\star \, X=\{(a\,b)(x)\,|\,x \in X\}=\{(a\,b)(a)\} \cup \{(a\,b)(b)\} \cup \{(a\,b)(c)\,|\,c \in X {\setminus }\{a,b\}\}=\{b\} \cup \{a\} \cup (X {\setminus } \{a,b\})=X$. Informally, we remarked that, when $a,b \in X$, we have that the transposition $(a\,b)$ interchanges a with b in X and leaves the other atoms in X (different from a and b) unchanged. Essentially, X is left unchanged under $(a\,b)$ because the order of a and b in the set X is, obviously, non-important. Now, if X is cofinite, then ${ supp}(X)=A {\setminus } X$, and so $a,b \in A {\setminus } X$. Since $a,b \notin X$, we have $a,b \ne x$ for all $x \in X$, and so $(a\,b)(x)=x$ for all $x \in X$. Thus, in this case we also have $(a\,b) \,\star \, X=X$. Since when both $a,b \in supp(X)$ we have $(a\,b)\,\star \, X=X$, it follows that one of a or b does not belong to ${ supp}(X)$. Suppose $b \notin supp(X)$ (the other case is similar). Let us consider $c\ne a,b$, $c \notin supp(f)$, $c \notin supp(X)$. Then $(b\, c) \in Fix({ supp}(X))$, and, because ${ supp}(X)$ supports X, we have $(b\,c)\,\star \, X=X$. Furthermore, $(b\, c) \in Fix({ supp}(f))$, and by Proposition 4 we have $(a,b)=f(X)=f((b\,c) \,\star \, X)=(b\,c) \otimes f(X)=(b\,c) \otimes (a,b)=((b\,c)(a), (b\,c)(b))=(a,c)$ which is a contradiction because $b\ne c$.

• 2. Suppose, by contradiction, that there is a finitely supported injective mapping $f{:}\, A \times A \rightarrow \wp _{fs}(A)$. Let us fix two atoms x and y. We define the function $g: \wp _{fs}(A) \rightarrow A \times A$ by

  $$\begin{aligned} g(X)=\left\{ \begin{array}{ll} f^{-1}(X), &{} \quad \text {if}\, X\in \text {Im(f)} ;\\ (x,y), &{} \quad \text {if}\, X \notin \text {Im(f)}.\end{array}\right. \end{aligned}$$

  For any $(a,b) \in A \times A$ we have that the element f((a, b)) is a finitely supported subset of A (supported by ${ supp}(f) \cup supp(a) \cup supp(b)$), and $(a,b)=g(f((a,b)))$ Thus g is surjective. We claim that g is supported by ${ supp}(f) \cup supp(x) \cup supp(y)$. Indeed, let $\pi \in Fix({ supp}(f) \cup supp(x) \cup supp(y))$. Let $X \in \wp _{fs}(A)$. If $X \in Im(f)$, then $X=f(Y)$ for some $Y \in A \times A$. Since $\pi$ fixes ${ supp}(f)$ pointwise and ${ supp}(f)$ supports f, we have $\pi \,\star \, X = \pi \,\star \, f(Y)=f(\pi \otimes Y) \in Im(f)$. Thus, from Proposition 4 we get $g(\pi \,\star \, X)=f^{-1}(\pi \,\star \, X)=\{Y \in A \times A\;|\; f(Y)$=$\pi \,\star \, X\}=\{Y \in A \times A\;|\; \pi ^{-1} \,\star \, f(Y)$=$X\}=\{Y\in A \times A\;|\; f(\pi ^{-1} \otimes Y)$= $X\}\overset{\pi ^{-1} \otimes Y:= Z}{=}\{\pi \otimes Z \in A \times A\;|\; f(Z)$=$X\}=\pi \otimes \{ Z \in A \times A\;|\; f(Z)$=$X\}=\pi \otimes f^{-1}(X)=\pi \otimes g(X)$. Now, if $X \notin Im(f)$, we have that $\pi \,\star \, X \notin Im(f)$ (because we proved above that Im(f) is supported by ${ supp}(f)$). Thus $g(\pi \,\star \, X)=(x,y)$. Since $\pi$ fixes ${ supp}(x) \cup supp(y)$ pointwise, we get $\pi \otimes g(X)=\pi \otimes (x,y)=(\pi (x), \pi (y))=(x,y)=g(\pi \,\star \, X)$. Therefore, g is finitely supported according to Proposition 4. Since g is also surjective, this contradicts the fact that there does not exist a finitely supported surjective mapping from $(\wp _{fs}(A), \,\star \,)$ to $(A \times A, \otimes )$.

• 3. Suppose there is a finitely supported surjection $f{:}\, \wp _{fs}(A) \rightarrow \wp _{fs}(A) \times \wp _{fs}(A)$. Obviously, there exists a supported surjection $s:\wp _{fs}(A) \rightarrow A$ defined as in Theorem 1(3). Thus, we can define a surjection $g:\wp _{fs}(A) \times \wp _{fs}(A) \rightarrow A \times A$ by $g(X,Y)=(s(X),s(Y))$ for all $X,Y \in \wp _{fs}(A)$ which, according to Propositions 2 and 4 is supported by ${ supp}(s)$. Furthermore, the function $h=g \circ f: \wp _{fs}(A) \rightarrow A \times A$ is surjective and finitely supported by ${ supp}(s) \cup supp(f)$. This contradicts item 1.

• 4. If there exists a finitely supported injective mapping $f{:}\, \wp _{fs}(A) \times \wp _{fs}(A) \rightarrow \wp _{fs}(A)$, then we obtain that there exists a finitely supported injection $g{:}\, A \times A \rightarrow \wp _{fs}(A)$ which contradicts item 2.

• 5. Let us consider the function $f{:}\,\wp _{{ fin}}(A) \rightarrow \wp _{{ cofin}}(A)$ defined by $f(X)=A {\setminus } X$ for all $X \in \wp _{{ fin}}(A)$. Clearly, f is bijective. We claim that f is equivariant. Indeed, let $\pi \in S_{A}$. To prove that $f(\pi \,\star \, X)$=$\pi \,\star \, f(X)$ for all $X \in \wp _{{ fin}}(A)$, we have to prove that $A {\setminus } (\pi \,\star \, X)=\pi \,\star \, (A {\setminus } X)$ for all $X \in \wp _{{ fin}}(A)$. Let $y \in A {\setminus } (\pi \,\star \, X)$. We can express y as $y=\pi \cdot (\pi ^{-1} \cdot y)$. If $\pi ^{-1} \cdot y \in X$, then $y \in \pi \,\star \, X$, which is a contradiction. Thus, $\pi ^{-1} \cdot y \in (A {\setminus } X)$, and so $y \in \pi \,\star \, (A {\setminus } X)$. Conversely, if $y \in \pi \,\star \, (A {\setminus } X)$, then $y=\pi \cdot x$ with $x \in A {\setminus } X$. Suppose $y \in \pi \,\star \, X$. Then $y=\pi \cdot z$ with $z \in X$. Thus, $x=z$ which is a contradiction, and so $y \in A {\setminus } (\pi \,\star \, X)$. Since f is equivariant and bijective, it follows that $|\wp _{{ fin}}(A)|=|\wp _{{ cofin}}(A)|$. According to Proposition 3, $|\wp _{fs}(A)|=2|\wp _{{ fin}}(A)|$.

• 6. Obviously $\wp _{{ fin}}(A)$ is infinite, because there exist an equivariant injection $i: A \rightarrow \wp _{{ fin}}(A)$ defined by $i(a)=\{a\}$ for all $a \in A$. According to Theorem 2(2), there does not exist a finitely supported injective mapping from $\wp _{fs}(A)$ onto one of its finitely supported proper subsets. Thus, there could not exist a bijection $f{:}\, \wp _{fs}(A) \rightarrow \wp _{{ fin}}(A)$. Thus, $|\wp _{{ fin}}(A)| \ne |\wp _{fs}(A)|=2|\wp _{{ fin}}(A)|$.

• 7. Consider $a_{1},a_{2}, \ldots , a_{n-1}$$, a^{1}_{1}, \ldots , a^{n}_{1}, \ldots , a^{1}_{n-1}, \ldots , a^{n}_{n-1} \in A$ a family of pairwise different elements. Then $i: A \rightarrow \wp _{n}(A)$ defined by

  $$\begin{aligned} i(x)=\left\{ \begin{array}{ll} \{x,a_{1},a_{2}, \ldots , a_{n-1}\}, &{} \quad \text {if}\, {x \ne a_{1}, \ldots , a_{n-1} };\\ \{ a^{1}_{1}, \ldots , a^{n}_{1}\}, &{} \quad \text {if}\, {x=a_{1} };\\ \vdots \\ \{ a^{1}_{n-1}, \ldots , a^{n}_{n-1}\}, &{} \quad \text {if}\, {x=a_{n-1}} \, \end{array}\right. \end{aligned}$$

  This is obviously an injective mapping from $(A, \cdot )$ to $(\wp _{n}(A), \,\star \,)$. Furthermore, we can easy check that i is supported by the finite set of atoms {$a_{1},a_{2}, \ldots , a_{n-1},$$a^{1}_{1}, \ldots , a^{n}_{1}, \ldots , a^{1}_{n-1}, \ldots , a^{n}_{n-1}\}$, and so $|A| \le |\wp _{n}(A)|$ in FSM. We claim that there does not exist a finitely supported injection from $\wp _{n}(A)$ into A. Assume on the contrary that there exists an finitely supported injection $f{:}\,\wp _{n}(A) \rightarrow A$. According to the proof of Theorem 5(1), for any $Y \in \wp _{n}(A)$ which is disjoint from ${ supp}(f)$, we have $f(Y) \notin Y$. Since ${ supp}(f)$ is finite, there are infinitely many such Y with the property that $Y \cap supp(f)=\emptyset$. Thus, because it is injective, f takes infinitely many values on those Y. Since ${ supp}(f)$ is finite, there should exist at least one element in $\wp _{n}(A)$ denoted by Z such that $Z \cap supp(f)=\emptyset$ and $f(Z) \notin supp(f)$. Thus, $f(Z) = a$ for some $a \in A {\setminus } (Z \cup supp(f))$. Let $b \in A {\setminus } ({ supp}(f) \cup Z \cup \{a\})$ and also let $\pi = (a\, b)$. Then $\pi \in Fix({ supp}(f) \cup Z)$, and hence $f(Z) =f((a\,b) \,\star \, Z)=(a\,b)(f(Z))= b$, a contradiction. We obtained that $|A| \ne |\wp _{n}(A)|$ in FSM, and so $|A|<|\wp _{n}(A)|$. According to Theorem 6(3) (that will be independently proved below), we have that $|\wp _{fs}(A)|=|2^{A}_{fs}|$. Obviously, $|\wp _{n}(A)| \le |\wp _{fs}(A)|$. According to Theorem 2(2), there does not exist a finitely supported injective mapping from $\wp _{fs}(A)$ onto one of its finitely supported proper subsets. Because $\wp _{n}(A)$ is a particular subset of $\wp _{fs}(A)$, there could not exist a bijection $f{:}\, \wp _{fs}(A) \rightarrow \wp _{n}(A)$, and so $|\wp _{n}(A)| \ne |\wp _{fs}(A)|$. Thus, $|\wp _{n}(A)|<|\wp _{fs}(A)|=|2^{A}_{fs}|$.

• 8. According to item 7, we obviously have that $|A|< |\wp _{2}(A)| \le |\wp _{{ fin}}(A)| < |\wp _{fs}(A)|=|2^{A}_{fs}|$.

• 9. Since there is a finitely supported surjection from $\wp _{fs}(A)$ onto A [defined as in the proof of Theorem 1(3)], the result follows from item 1.

• 10. Since there is a finitely supported injection $a \mapsto \{a\}$ from A into $\wp _{fs}(A)$, the result follows from item 2.

• 11. For the invariant set $(A,\cdot )$, the family $T_{{ fin}}(A)=\{(x_{1}, \ldots , x_{m}) \subseteq (A \times \cdots \times A)\,|\,m \ge 0\}$ of all finite injective (one-to-one) tuples from A (including the empty tuple denoted by ${\bar{\emptyset }}$) is an $S_{A}$-set with the $S_{A}$-action $\,\star \,:S_{A}\times T_{{ fin}}(A) \rightarrow T_{{ fin}}(A)$ defined by $\pi \,\star \, {\bar{\emptyset }}={\bar{\emptyset }}$ for all $\pi \in S_{A}$ and $\pi \,\star \, (x_{1}, \ldots , x_{m})=(\pi \cdot x_{1}, \ldots , \pi \cdot x_{m})$ for all non-empty tuples $(x_{1}, \ldots , x_{m}) \in T_{{ fin}}(A)$ and all $\pi \in S_{A}$. This is a direct consequence of the fact that permutations of atoms are injective, and so finite injective tuples are transformed in finite injective tuples. Since A is an invariant set, we have that $T_{{ fin}}(A)$ is an invariant set with ${ supp}(a_{1}, \ldots , a_{m})=supp(a_{1}) \cup \ldots \cup supp(a_{m})=\{a_{1}, \ldots , a_{m}\}$, for any injective tuple of atoms $(a_{1}, \ldots , a_{m})$. Since ${ supp}({\bar{\emptyset }})=\emptyset$, it follows that $T_{{ fin}}(A){\setminus } {\bar{\emptyset }}$ is an equivariant subset of $T_{{ fin}}(A)$, and is itself an invariant set. Let us fix an atom $a \in A$. We define $f{:}\,T_{{ fin}}(A) \rightarrow T_{{ fin}}(A){\setminus } {\bar{\emptyset }}$ by $f(y)=\left\{ \begin{array}{ll} y, &{} \text {if}\, y\text { is an injective non-empty tuple};\\ (a), &{} \text {if}\, {y={\bar{\emptyset }}}\, \end{array}\right.$. Clearly, f is surjective. We claim that f is supported by ${ supp}(a)$. Let $\pi \in Fix({ supp}(a))$, i.e. $a=\pi (a)=\pi \,\star \,(a)$. If y is a non-empty tuple of atoms, we obviously have $f(\pi \,\star \, y)=\pi \,\star \, y=\pi \,\star \, f(y)$. If $y={\bar{\emptyset }}$, we have $\pi \,\star \, y={\bar{\emptyset }}$, and so $f(\pi \,\star \, y)=(a)=\pi (a)=\pi \,\star \, f(y)$. Thus, $f(\pi \,\star \, y)=\pi \,\star \, f(y)$ for all $y \in T_{{ fin}}(A)$. According to Proposition 4, we have that f is finitely supported.

  We define an equivariant surjective function $g:T_{{ fin}}(A){\setminus } {\bar{\emptyset }} \rightarrow T_{{ fin}}(A)$ by

  $$\begin{aligned} g(y)=\left\{ \begin{array}{ll} {\bar{\emptyset }}, &{} \quad \text {if}\, y\text { is a tuple with exactly one element};\\ y', &{} \quad \text {otherwise} ; \end{array}\right. \end{aligned}$$

  where $y'$ is a new tuple formed by deleting the first element in tuple y (the first position in a finite injective tuple exists without requiring any form of choice). Clearly, g is surjective. Indeed, ${\bar{\emptyset }}=g((a))$ for some one-element tuple (a); this is possible because A is non-empty, and so it has at least one atom. For a fixed finite injective non-empty m-tuple y, we have that y can be seen as being “contained” in an injective $(m+1)$-tuple z of form (b, y) (whose first element is a certain atom b, and the following elements are precisely the elements of y). The related atom b exists because y is finite, while A is infinite. We get $y=g (z)$. For proving the surjectivity of g we do not need to ‘choose’ precisely such an element b, being sufficient to prove that $g(b,y)=y$ for every $b \in A{\setminus }\{y\}$ and $A{\setminus }\{y\}$ is non-empty. We claim now that g is equivariant. Let (x) be a one-element tuple from A and $\pi$ an arbitrary permutation of atoms. We have that $\pi \,\star \, (x)=(\pi (x))$ is a one-element tuple from A, and so $g(\pi \,\star \, (x))={\bar{\emptyset }} = \pi \,\star \, {\bar{\emptyset }} = \pi \,\star \, g((x))$. Let $(x_{1}, \ldots , x_{m}) \in T_{{ fin}}(A), m \ge 2$ and $\pi \in S_{A}$. We have $g(\pi \,\star \, (x_{1}, \ldots , x_{m}))=g((\pi \cdot x_{1}, \ldots , \pi \cdot x_{m}))=g((\pi (x_{1}), \ldots , \pi (x_{m})))=(\pi (x_{2}), \ldots , \pi (x_{m}))=\pi \,\star \, (x_{2}, \ldots , x_{m})=\pi \,\star \, g(x_{1}, \ldots , x_{m})$. According to Proposition 4, we have that g is empty-supported (equivariant). Since $T_{{ fin}}(A)$ does not contain an infinite uniformly supported subset (the finite injective tuples of atoms supported by a finite set S are only those tuples formed by elements of S, being at most $1+A_{|S|}^{1}+A_{|S|}^{2}+\cdots +A_{|S|}^{|S|}$ such tuples, where $A_{n}^{k}=n(n-1)\ldots (n-k+1)$), according to Lemma 1, there could not exist a finitely supported injective $h: T_{{ fin}}(A) \rightarrow T_{{ fin}}(A){\setminus } {\bar{\emptyset }}$.

• 12. Firstly, we prove the following lemmas. $\square$

Lemma 2

Let X and Y be two invariant sets and $f{:}\,X \rightarrow Y$ a finitely supported function. Then the mappings $g:\wp _{fs}(Y) \rightarrow \wp _{fs}(X)$ defined by $g(V)=f^{-1}(V)$ for all $V \in \wp _{fs}(Y)$, and $h:\wp _{fs}(X) \rightarrow \wp _{fs}(Y)$ defined by $h(U)=f(U)$ for all $U \in \wp _{fs}(X)$ are well defined and finitely supported by ${ supp}(f)$. Furthermore, if f surjective, then g is injective and h is surjective, and if f injective, then g is surjective and h is injective.

Proof of Lemma 2

The proof of this lemma requires the involvement of the S-finite support principle. Let V be an arbitrary element from $\wp _{fs}(Y)$. We claim that $f^{-1}(V) \in \wp _{fs}(X)$. Indeed we prove that the set $f^{-1}(V)$ is supported by ${ supp}(f) \cup supp(V)$. Let $\pi \in Fix({ supp}(f) \cup supp(V))$, and $x \in f^{-1}(V)$. This means $f(x) \in V$. According to Proposition 4, and because $\pi$ fixes ${ supp}(f)$ pointwise and ${ supp}(f)$ supports f, we have $f(\pi \cdot x)= \pi \cdot f(x) \in \pi \,\star \, V = V$, and so $\pi \cdot x \in f^{-1}(V)$ (we denoted the actions on X and Y generically by $\cdot$, and the actions on their powersets by $\,\star \,$). Therefore, $f^{-1}(V)$ is finitely supported, and so the function g is well defined. We claim that g is supported by ${ supp}(f)$. Let $\pi \in Fix({ supp}(f))$ which means that $\pi ^{-1} \in Fix({ supp}(f))$, and so $f(\pi ^{-1} \cdot x)=\pi ^{-1} \cdot f(x)$ for all $x\in X$ according to Proposition 4. For any arbitrary $V \in \wp _{fs}(Y)$, we have that $z \in g(\pi \,\star \, V) = f^{-1}(\pi \,\star \, V) \Leftrightarrow f(z) \in \pi \,\star \, V \Leftrightarrow \pi ^{-1} \cdot f(z) \in V \Leftrightarrow f(\pi ^{-1} \cdot z) \in V \Leftrightarrow \pi ^{-1} \cdot z \in f^{-1}(V) \Leftrightarrow z \in \pi \,\star \, f^{-1}(V)=\pi \,\star \, g(V)$. If follows that $g(\pi \,\star \, V)=\pi \,\star \, g(V)$ for all $V \in \wp _{fs}(Y)$, and so g is finitely supported.

Using techniques presented above, we state that the set f(U) is supported by ${ supp}(f) \cup supp(U)$ for any $U \in \wp _{fs}(X)$. Let $\pi \in Fix({ supp}(f) \cup supp(U))$, and $x \in f(U)$. Then $x=f(y)$ for some $y \in U$. However, because $\pi \in Fix ({ supp}(U))$, it follows that $\pi \cdot y \in U$ and so, from Proposition 4 we get $\pi \cdot x= \pi \cdot f(y)= f(\pi \cdot y) \in f(U)$. Thus, h is well defined. For all $\pi \in Fix({ supp}(f))$ and $U \in \wp _{fs}(X)$, we have $f(\pi \,\star \, U)=\{f(\pi \cdot z)\;|\;z \in U\}=\{\pi \cdot f(z)\;|\;z \in U\}=\pi \,\star \, f(U)$, and so h is finitely supported by ${ supp}(f)$. The rest of the proof is a routine exercise. $\square$

Lemma 3

Let $(B, \cdot )$ and $(C, \diamond )$ be two invariant sets. If there exist a finitely supported injective mapping $f{:}\, B \rightarrow C$ and a finitely supported injective mapping $g: C \rightarrow B$, then there exists a finitely supported bijective mapping $h:B \rightarrow C$.

Proof of Lemma 3

Let us define $F:\wp _{fs}(B) \rightarrow \wp _{fs}(B)$ by $F(X)=B-g(C-f(X))$ for all finitely supported subsets X of B. F is correctly defined, i.e. $Im(F) \subseteq \wp _{fs}(B)$ because F(X) is supported by ${ supp}(g) \cup supp(f) \cup supp(X)$ for all $X \in \wp _{fs}(B)$. Furthermore, F is a finitely supported function, supported by ${ supp}(f) \cup supp(g)$ (by repeatedly applying Lemma 2). We can easily verify that for any $X,Y \in \wp _{fs}(B)$ with $X \subseteq Y$, we have $F(X) \subseteq F(Y)$. According to Theorem 6(4) there exists $T \in \wp _{fs}(B)$ supported by ${ supp}(F)$ such that $F(T)=T$. Thus, $T=B-g(C-f(T))$, or equivalently, $B-T=g(C-f(T))$. Since g is injective, we obtain that for each $x \in B-T$, $g^{-1}(x)$ is a set containing exactly one element.

We define $h:B \rightarrow C$ by $h(x)=\left\{ \begin{array}{ll} f(x), &{} \text {for}\, x \in T;\\ g^{-1}(x), &{} \text {for}\, x \in B-T.\end{array}\right.$

According to Proposition 4 we have that h is supported by the set ${ supp}(f) \cup supp(g) \cup supp(T)=supp(f) \cup supp(g)$. Indeed, let $\pi \in Fix({ supp}(f) \cup supp(g) \cup supp(T))$, and x an arbitrary element of B. If $x \in T$, because $\pi \in Fix({ supp}(T))$ and ${ supp}(T)$ supports T, we have $\pi \cdot x \in T$. Thus, from Proposition 4 we get $h(\pi \cdot x)=f(\pi \cdot x)=\pi \diamond f(x)=\pi \diamond h(x)$. If $x \in B-T$, we have $\pi \cdot x \in B-T$. Thus, because g is finitely supported, according to Proposition 4 we have $h(\pi \cdot x)=g^{-1}(\pi \cdot x)=\pi \diamond g^{-1}(x)=\pi \diamond h(x)$, by involving the first part of Lemma 2. Finally, one can easily remark that h is bijective.

We can now start the proof of item 12 of the theorem.

As in item 11, we consider the sets $B=T_{{ fin}}(A){\setminus } {\bar{\emptyset }}$ and $C=T_{{ fin}}(A)$. According to item 11 there exists a finitely supported surjective function $f{:}\,C \rightarrow B$ and a finitely supported (equivariant) surjection $g:B \rightarrow C$. Thus, according to Lemma 2, there exist a finitely supported injective function $f':\wp _{fs}(B) \rightarrow \wp _{fs}(C)$ and a finitely supported injective function $g':\wp _{fs}(C) \rightarrow \wp _{fs}(B)$. According to Lemma 3, there is a finitely supported bijection between $\wp _{fs}(B)$ and $\wp _{fs}(C)$. However, we proved in item 11 that there is no finitely supported bijection between $B=T_{{ fin}}(A){\setminus } {\bar{\emptyset }}$ and $C=T_{{ fin}}(A)$. $\square$

4.4 Fixed points of functions between atomic sets

Theorem 4

Finitely supported functions between atomic sets have the following specific FSM properties:

• 1. Weak Tarski fixed point theorem for self mappings on $\wp _{{ fin}}(A)$:

  Let $f{:}\,\wp _{{ fin}}(A)\rightarrow \wp _{{ fin}}(A)$ be a finitely supported order preserving function. Then there exists a least $X_{0}\in \wp _{{ fin}}(A)$ supported by ${ supp}(f)$ such that $f(X_{0})=X_{0}$.

• 2. Weak Tarski fixed point theorem for self mappings on $\wp _{{ fin}}(\wp _{fs}(A))$:

  Let $f{:}\,\wp _{{ fin}}(\wp _{fs}(A))\rightarrow \wp _{{ fin}}(\wp _{fs}(A))$ be a finitely supported order preserving function. Then there exists a least $X_{0}\in \wp _{{ fin}}(\wp _{fs}(A))$ supported by ${ supp}(f)$ such that $f(X_{0})=X_{0}$.

• 3. Bourbaki–Witt fixed point theorem for self mappings on $\wp _{{ fin}}(A)$:

  Let $f{:}\,\wp _{{ fin}}(A)\rightarrow \wp _{{ fin}}(A)$ be a finitely supported function with the property that $X \subseteq f(X)$ for all $X \in \wp _{{ fin}}(A)$. Then there is $X_{0}\in \wp _{{ fin}}(A)$ such that $f(X_{0})=X_{0}$.

• 4. Bourbaki–Witt fixed point theorem for self mappings on $\wp _{{ fin}}(\wp _{fs}(A))$:

  Let $f{:}\,\wp _{{ fin}}(\wp _{fs}(A))\rightarrow \wp _{{ fin}}(\wp _{fs}(A))$ be a finitely supported function with the property that $X \subseteq f(X)$ for all $X \in \wp _{{ fin}}(\wp _{fs}(A))$. Then there exists $X_{0}\in \wp _{{ fin}}(\wp _{fs}(A))$ such that $f(X_{0})=X_{0}$.

• 5. Iterative calculation of fixed points for self mappings on $\wp _{fs}(A)$:

  Let $f{:}\,\wp _{fs}(A) \rightarrow \wp _{fs}(A)$ be a finitely supported order preserving function. Then there is $n_{0} \in {\mathbb {N}}$ such that $\cap \{X \in \wp _{fs}(A)\,|\, f(X)\subseteq X\}=f^{n_{0}}(\emptyset )$ and $m_{0} \in {\mathbb {N}}$ such that $\cup \{X \in \wp _{fs}(A)\,|\, X \subseteq f(X)\}=f^{m_{0}}(A)$.

Proof

• 1 and 2. Let X be one of the sets A or $\wp _{fs}(A)$. We proved that X does not contain an infinite uniformly supported subset [see Theorem 1(2)]. We prove by contradiction that $\wp _{{ fin}}(X)$ does not contain an infinite uniformly supported subsets. If $X=A$, then, obviously $\wp _{{ fin}}(A)$ does not contain infinite uniformly supported subsets. If $X=\wp _{fs}(A)$, then suppose, by contradiction, that there is an infinite uniformly supported sequence ${\mathcal {F}}=(X_{n})_{n} \subseteq \wp _{{ fin}}(X)$. Therefore, there exists a finite set S of atoms such that ${ supp}(X_{n}) \subseteq S$ for all $n \in {\mathbb {N}}$. As in the proof of Theorem 2(3) we get ${\mathop {\cup }\nolimits _{x \in X_{n}}}supp(x) \subseteq S$ for all $n \in {\mathbb {N}}$. Thus ${ supp}(x) \subseteq S$ for all $x \in {\mathop {\cup }\nolimits _{i \in {\mathbb {N}}}}X_{i}$. Therefore, ${\mathop {\cup }\nolimits _{i \in {\mathbb {N}}}}X_{i}$ is an infinite uniformly supported subset of X, which is a contradiction. Hence every uniformly supported subset of $\wp _{{ fin}}(X)$ should be finite.

  Let $f{:}\,\wp _{{ fin}}(X)\rightarrow \wp _{{ fin}}(X)$ be a finitely supported order preserving function. Since $\emptyset \subseteq f(\emptyset )$ and f is order preserving, we can define the countable ascending sequence $\emptyset \subseteq f(\emptyset ) \subseteq f^{2}(\emptyset ) \subseteq \cdots \subseteq f^{n}(\emptyset ) \subseteq \cdots$. More exactly, we have that $(f^{n}(\emptyset ))_{n \in {\mathbb {N}}}$ is an ascending chain, where $f^{n}(\emptyset )=f(f^{n-1}(\emptyset ))$ and $f^{0}(\emptyset )=\emptyset$. We prove by induction that $(f^{n}(\emptyset ))_{n}$ is uniformly supported by ${ supp}(f)$, that is, ${ supp}(f^{n}(\emptyset ))\subseteq supp(f)$ for each $n \in {\mathbb {N}}$. We have ${ supp}(f^{0}(\emptyset ))=supp(\emptyset )=\emptyset \subseteq supp(f)$. Let us suppose that ${ supp}(f^{n}(\emptyset ))\subseteq supp(f)$ for some $n \in {\mathbb {N}}$. We have to prove that ${ supp}(f^{n+1}(\emptyset ))\subseteq supp(f)$. So, we have to prove that each permutation $\pi$ which fixes ${ supp}(f)$ pointwise also fixes $f^{n+1}(\emptyset )$. Let $\pi \in Fix({ supp}(f))$. From the inductive hypothesis, we have $\pi \in Fix({ supp}(f^{n}(\emptyset )))$, and so $\pi \,\star \, f^{n}(\emptyset )=f^{n}(\emptyset )$. According to Proposition 4, we have $\pi \,\star \, f^{n+1}(\emptyset )=\pi \,\star \, f(f^{n}(\emptyset ))=f(\pi \,\star \, f^{n}(\emptyset ))=f(f^{n}(\emptyset )) =f^{n+1}(\emptyset )$. Therefore, $(f^{n}(\emptyset ))_{n \in {\mathbb {N}}} \subseteq \wp _{{ fin}}(X)$ is uniformly supported by ${ supp}(f)$. Thus, $(f^{n}(\emptyset ))_{n \in {\mathbb {N}}}$ should be finite, and so there exists $n_{0} \in {\mathbb {N}}$ such that $f^{n}(\emptyset )=f^{n_{0}}(\emptyset )$ for all $n \ge n_{0}$. Thus, $f(f^{n_{0}}(\emptyset ))=f^{n_{0}+1}(\emptyset )=f^{n_{0}}(\emptyset )$, and so $f^{n_{0}}(\emptyset )$ is a fixed point of f, and, furthermore, it is supported by ${ supp}(f)$. If Y is another fixed point of f, then from $\emptyset \, \subseteq Y$, we get $f^{n}(\emptyset )\subseteq f^{n}(Y)$ for all $n \in {\mathbb {N}}$. Therefore, $f^{n_{0}}(\emptyset )\subseteq f^{n_{0}}(Y)=Y$, and so $f^{n_{0}}(\emptyset )$ is the least fixed point of f.

• 3 and 4. As in the proof of items 1 and 2, the fixed point of f is defined as the least upper bound of the uniformly supported, stationary ascending sequence $\emptyset \subseteq f(\emptyset ) \subseteq f^{2}(\emptyset ) \subseteq \cdots \subseteq f^{n}(\emptyset ) \subseteq \cdots$. However, since f is not necessarily order preserving, this fixed point of f is not necessarily a least one.

• 5. According to Theorem 6(4) we have that f has a least fixed point which is equal to $\cap \{X \in \wp _{fs}(A)\,|\, f(X)\subseteq X\}$. As in the proof of items 1 and 2, because $\emptyset \subseteq f(\emptyset )$ and f is order preserving, we can define the countable ascending sequence $\emptyset \subseteq f(\emptyset ) \subseteq f^{2}(\emptyset ) \subseteq \cdots \subseteq f^{n}(\emptyset ) \subseteq \cdots$ which is uniformly supported by ${ supp}(f)$. However, there could exist only finitely many subsets of A (i.e. only finitely many elements in $\wp _{fs}(A)$) supported by ${ supp}(f)$, namely the subsets of ${ supp}(f)$ and the supersets of $A{\setminus } supp(f)$. Thus, $(f^{n}(\emptyset ))_{n \in {\mathbb {N}}}$ should be finite, and so there exists $n_{0} \in {\mathbb {N}}$ such that $f^{n}(\emptyset )=f^{n_{0}}(\emptyset )$ for all $n \ge n_{0}$. Thus, $f(f^{n_{0}}(\emptyset )) = f^{n_{0}+1}(\emptyset ) = f^{n_{0}}(\emptyset )$, and so $f^{n_{0}}(\emptyset )$ is a fixed point of f, and furthermore, it is the least one (as in the proof of item 1). Since the least fixed point of f is unique, it follows that $\cap \{X \in \wp _{fs}(A)\,|\, f(X)\subseteq X\} = f^{n_{0}}(\emptyset )$. Dually, f has a greatest fixed point equal to $\cup \{X \in \wp _{fs}(A)\,|\, X \subseteq f(X)\}$. The descending chain $\cdots \subseteq f^{m}(A) \subseteq f^{m-1}(A) \subseteq \cdots \subseteq f(A) \subseteq A$ is uniformly supported by ${ supp}(f) \cup supp(A)=supp(f) \cup \emptyset =supp(f)$. Therefore, because $\wp _{fs}(A)$ cannot contain an infinite uniformly supported subset, the sequence $(f^{m}(A))_{m \in {\mathbb {N}}}$ is stationary, i.e. there exist an $m_{0} \in {\mathbb {N}}$ such that $f^{m}(A)=f^{m_{0}}(A)$ for all $m \ge m_{0}$. Thus, $f^{m_{0}}(A)$ is a fixed point of f, and furthermore, it is the greatest one because whenever Z is another fixed point of f, from $Z \subseteq A$, we get $Z=f^{m_{0}}(Z) \subseteq f^{m_{0}}(A)$. Since the greatest fixed point of f is unique we have $\cup \{X \in \wp _{fs}(A)\,|\, X \subseteq f(X)\}=f^{m_{0}}(A)$. $\square$

4.5 Inconsistency of some specific choice principles

At the end of the section devoted to specific properties of the atoms we presented some examples of atomic sets not satisfying certain choice principles.

Theorem 5

We provide constructions of certain atomic sets that do not satisfy specific forms of choice:

• 1. There does not exist a finitely supported choice function defined on $\wp _{n}(A)$ for any integer $n \ge 2$. Hence there does not exist a finitely supported choice function on $\wp _{{ fin}}(A)$ either.

• 2. There does not exist a finitely supported choice function defined on $\wp _{{ cofin}}(A)$.

• 3. There do not exist finitely supported total order relations (and so neither finitely supported well-order relations) defined on infinite finitely supported subsets of the sets A, $\wp _{{ fin}}(A)$, $\wp _{{ cofin}}(A)$, $\wp _{fs}(A)$, $A^{A}_{fs}$, or $\wp _{{ fin}}(\wp _{fs}(A))$.

• 4. Zorn’s lemma does not hold for $\wp _{{ fin}}(A)$: $(\wp _{{ fin}}(A), \,\star \,, \subseteq )$ is an invariant set having the property that any finitely supported totally ordered subset of $\wp _{{ fin}}(A)$ has an upper bound in $\wp _{{ fin}}(A)$, but $\wp _{{ fin}}(A)$ does not have a maximal element.

• 5. Zorn’s lemma does not hold for $\wp _{{ fin}}(\wp _{fs}(A))$: $(\wp _{{ fin}}(\wp _{fs}(A)), \,\star \,, \subseteq )$ is an invariant set having the property that any finitely supported totally ordered subset of $\wp _{{ fin}}(\wp _{fs}(A))$ has an upper bound in $\wp _{{ fin}}(\wp _{fs}(A))$, but $\wp _{{ fin}}(\wp _{fs}(A))$ does not have a maximal element.

Proof

• 1. Fix some $n \ge 2$, and consider a finitely supported function $f{:}\, \wp _{n}(A) \rightarrow A$ and an arbitrary set $Y:=\{a_{1}, \ldots , a_{n}\}$ from  $\wp _{n}(A)$ such that $a_{1}, \ldots , a_{n}$ do not belong to ${ supp}(f)$. Assume by contradiction that $f(Y) \in Y$. Let $\pi$ be a permutation of atoms which fixes ${ supp}(f)$ pointwise, and interchanges only all the elements of Y (e.g. $\pi$ is a cyclic permutation of Y). Since $\pi$ permutes all the elements of Y and $f(Y) \in Y$, we have $\pi \cdot f(Y)=\pi (f(Y)) \ne f(Y)$. However, $\pi \,\star \, Y =\{\pi (a_{1}), \ldots , \pi (a_{n})\}=\{a_{1}, \ldots , a_{n}\}=Y$. Since $\pi$ fixes ${ supp}(f)$ pointwise and ${ supp}(f)$ supports f, we have $\pi (f(Y))=\pi \cdot f(Y)= f(\pi \,\star \, Y)=f(Y)$, a contradiction. Thus $f(Y) \notin Y$, and so f cannot be a choice function on $\wp _{n}(A)$.

• 2. By contradiction, assume that f is a finitely supported choice function function on $\wp _{{ cofin}}(A)$. Since $A {\setminus } supp(f)$ is cofinite, we have $f(A {\setminus } supp(f)) \in A {\setminus } supp(f)$. Thus, $f(A {\setminus } supp(f))=b \notin supp(f)$. Let $c\ne b$ with $c \notin supp(f)$. Clearly $(b\,c)$ fixes ${ supp}(f)$ pointwise, and so $(b \,c) \,\star \, (A {\setminus } supp(f))=A {\setminus } ((b\,c) \,\star \, supp(f))=A {\setminus } supp(f)$. Furthermore, by Proposition 4, $(b\,c) \cdot f(A {\setminus } supp(f))=f((b\,c) \,\star \, (A {\setminus } supp(f)))=f(A {\setminus } supp(f))=b$. However, $(b\,c) \cdot f(A {\setminus } supp(f))=(b\, c)(b)=c$, i.e. a contradiction.

• 3. Let $(Y, \cdot )$ be one of the invariant sets A, $\wp _{{ fin}}(A)$, $\wp _{{ cofin}}(A)$, $\wp _{fs}(A)$, $A^{A}_{fs}$ or $\wp _{{ fin}}(\wp _{fs}(A))$, and X an infinite finitely supported subset of Y. Suppose there is a finitely supported total order relation $\le$ on X. Let $\pi \in Fix ({ supp}(\le ) \cup supp(X))$ and $x \in X$ an arbitrary element. Since X is supported by ${ supp}(X)$, $\pi$ fixes ${ supp}(X)$ pointwise (i.e $\pi \cdot x \in X$) and $\le$ is a total order on X, we have either $x<\pi \cdot x$ or $x=\pi \cdot x$ or $\pi \cdot x<x$. If $x<\pi \cdot x$, then we get $x<\pi \cdot x<\pi ^{2} \cdot x<\cdots < \pi ^{n} \cdot x$ for all $n \in {\mathbb {N}}$. However, since every permutation of atoms is expressed as a finite composition of transpositions, $\pi$ has a finite order in the group $S_{A}$ and so there is $m \in {\mathbb {N}}$ such that $\pi ^{m}=Id$. This means that $\pi ^{m} \cdot x=x$, and so we get $x<x$ which is a contradiction. Similarly, the assumption $\pi \cdot x<x$ leads to the relation $\pi ^{n} \cdot x<\cdots<\pi \cdot x<x$ for all $n \in {\mathbb {N}}$ which is also a contradiction (because $\pi$ has a finite order). Thus $\pi \cdot x=x$, and because x was arbitrary chosen from X, X should be uniformly supported by ${ supp}(\le ) \cup supp(X)$, which is a contradiction because Y cannot contain infinite uniformly supported subsets.

• 4 and 5. Let X be one of the sets A or $\wp _{fs}(A)$. Let ${\mathcal {F}}$ be finitely supported totally ordered subset of the invariant set $\wp _{{ fin}}(X)$ equipped with the equivariant order relation $\subseteq$. Since ${\mathcal {F}}$ is totally ordered with respect to the inclusion relation on $\wp _{{ fin}}(X)$, then there does not exist two different finite subsets of X of the same cardinality belonging to ${\mathcal {F}}$. Since ${\mathcal {F}}$ is finitely supported, then there exists a finite set $S \subseteq A$ such that $\pi \,\star \, Y \in {\mathcal {F}}$ for each $Y \in {\mathcal {F}}$ and each $\pi \in Fix(S)$. However, for each $Y \in {\mathcal {F}}$ and each $\pi \in Fix(S)$ we have that $|\pi \,\star \, Y|=|Y|$. Since there does not exist two distinct elements in ${\mathcal {F}}$ having the same cardinality, we conclude that $\pi \,\star \, Y=Y$ for all $Y \in {\mathcal {F}}$ and all $\pi \in Fix(S)$. Thus, ${\mathcal {F}}$ is uniformly supported by S. According to Theorem 1(2) and to the proof of Theorem 2(3), ${\mathcal {F}}$ must be finite, and so there exists the (finite) union of the members of ${\mathcal {F}}$ which is an element of $\wp _{{ fin}}(X)$ and an upper bound for ${\mathcal {F}}$. Suppose by contradiction that there exists a maximal element $X_{0}$ of $\wp _{{ fin}}(X)$. Then $X_{0}=\{x_{1}, \ldots x_{n}\}$, $x_{1}, \ldots , x_{n} \in X$ for some $n \in {\mathbb {N}}$. Since X is infinite, there exists $y \in X {\setminus } X_{0}$. However, $\{x_{1}, \ldots x_{n}\} \subsetneq \{x_{1}, \ldots x_{n}, y\}$ with $\{x_{1}, \ldots x_{n}, y\} \in \wp _{{ fin}}(X)$ which contradicts the maximality of $X_{0}$. $\square$

5 Atoms properties translated from ZF

Theorem 6

The following properties of the atoms are naturally translated from the ZF framework.

• 1. There exists a finitely supported (more exactly, an equivariant) injective mapping $g:\wp _{fs}(\wp _{fs}(A)) \rightarrow \wp _{fs}(\wp _{fs}(A))$ that is not surjective.

• 2. There exists a finitely supported (more exactly, an equivariant) injective mapping $g:\wp _{fs}(\wp _{{ fin}}(A)) \rightarrow \wp _{fs}(\wp _{{ fin}}(A))$ that is not surjective [analyze this in comparison with Theorem 2(3)].

• 3. There exists an equivariant bijective mapping from $\wp _{fs}(A)$ onto the family $2^{A}_{fs}$ (where $2=\{0,1\}$) of those finitely supported functions from A to the ordinary ZF set 2, i.e. $|\wp _{fs}(A)|=|2^{A}_{fs}|$ in FSM.

• 4. Tarski fixed point theorem: Let $(U, \cdot )$ be an invariant set (particularly, $U=A$, $U=\wp _{{ fin}}(A)$, or $U=\wp _{fs}(A)$). Any finitely supported order preserving function $f{:}\,\wp _{fs}(U) \rightarrow \wp _{fs}(U)$ has a least fixed point defined as $\cap \{X \in \wp _{fs}(U)\,|\, f(X)\subseteq X\}$ and a greatest fixed point defined as $\cup \{X \in \wp _{fs}(U)\,|\, X \subseteq f(X)\}$, which are both supported by ${ supp}(f)$.

Proof

• 1. Let $X_{i}$ be the set of all i-sized subsets of A, i.e. $X_{i}=\{Z \subseteq A\,|\,|Z|=i\}$. Obviously, we have that any i-sized subset of A is finitely supported. Since every permutation of atoms is bijective, the image of an i-sized subset of A under an arbitrary permutation is another i-sized subset of A. Thus, in FSM each $X_{i}$ is equivariant as a subset of $\wp _{fs}(A)$, and so each $X_{i}$ is an element from $\wp _{fs}(\wp _{fs}(A))$.

  We define $f{:}\, {\mathbb {N}} \rightarrow \wp _{fs}(\wp _{fs}(A))$ by $f(n)=X_{n}$. We claim that f is equivariant. Indeed, let $\pi \in S_{A}$. We have $\pi \,\star \, f(n)=\pi \,\star \, X_{n}=X_{n}=f(n)= f(\pi \diamond n)$ (where $\diamond$ is the trivial $S_{A}$-action on ${\mathbb {N}}$, and $\,\star \,$ represents the $S_{A}$-action on $\wp _{fs}(\wp _{fs}(A))$) for all $n \in {\mathbb {N}}$. According to Proposition 4, we have that f is equivariant. Furthermore, f is injective.

  Let us define $g:\wp _{fs}(\wp _{fs}(A)) \rightarrow \wp _{fs}(\wp _{fs}(A))$ by

  $$\begin{aligned} g(X)=\left\{ \begin{array}{ll} f(n+1), &{} \quad \text {if}\, {\exists n \in {\mathbb {N}}\text { with } X=f(n)};\\ X, &{} \quad \text {if}\, {X \notin Im(f)}.\end{array}\right. \end{aligned}$$

  We claim that g is equivariant. Indeed, let $\pi \in S_{A}$ and $X \in \wp _{fs}(\wp _{fs}(A))$. If there is some n such that $X=f(n)$, we have that $\pi \,\star \, X=\pi \,\star \, f(n)=f(n)$, and so $g(\pi \,\star \, X)=g(f(n))=f(n+1)=\pi \,\star \, f(n+1)=\pi \,\star \, g(X)$. If $X \notin Im(f)$, we prove by contradiction that $\pi \,\star \, X \notin Im(f)$. Indeed, suppose that $\pi \,\star \, X \in Im(f)$. Then there is $m \in {\mathbb {N}}$ such that $\pi \,\star \, X=f(m)$ or, equivalently, $X = \pi ^{-1} \,\star \, f(m)$. However, since f is equivariant, from Proposition 4 we have $\pi ^{-1} \,\star \, f(m)=f(\pi ^{-1} \diamond m)=f(m) \in Im(f)$ which contradicts the assumption that $X \notin Im(f)$. Thus, $\pi \,\star \, X \notin Im(f)$, and so $g(\pi \,\star \, X)=\pi \,\star \, X=\pi \,\star \, g(X)$. We obtained that $g(\pi \,\star \, X)=\pi \,\star \, X=\pi \,\star \, g(X)$ for all $X \in \wp _{fs}(\wp _{fs}(A))$ and all $\pi \in S_{A}$, and so g is equivariant. Since f is injective, it follows easily that g is injective. Furthermore, $Im(g)= \wp _{fs}(\wp _{fs}(A)) {\setminus } \{f(0)\}$ which is a proper subset of $\wp _{fs}(\wp _{fs}(A))$, finitely supported by ${ supp}(f(0))=\emptyset$.

• 2. The proof is actually the same as in item 1 because each $X_{i}$ in the proof of item 1 is an element from $\wp _{fs}(\wp _{{ fin}}(A))$.

• 3. We prove the result in the more general case emphasized in the following lemma, that makes it applicable also to other invariant sets. $\square$

Lemma 4

Let $(U, \cdot )$ be an invariant set. There exists an equivariant bijective mapping from $\wp _{fs}(U)$ onto the family $\{0,1\}^{U}_{fs}$ of those finitely supported functions from U to the ordinary ZF set $\{0,1\}$.

Proof of Lemma 4

Let $B \in \wp _{fs}(U)$, and $\varphi _{B}$ be the characteristic function on B, i.e. $\varphi _{B}(x)\overset{def}{=}\left\{ \begin{array}{ll} 1 &{} \text {for}\, x \in B\\ 0 &{} \text {for}\, x\in U {\setminus } B \end{array}\right.$. We claim that $X \mapsto \varphi _{X}$ is equivariant.

Firstly we prove that $\varphi _{B}$ is supported by ${ supp}(B)$. Let $\pi \in Fix({ supp}(B))$. Thus $\pi \,\star \, B=B$, and so $\pi \cdot x \in B$ if and only if $x \in B$. Thus, $\varphi _{B}(\pi \cdot x)=\varphi _{B}(x)$ for all $x \in U$, and from Proposition 4 we have that $\varphi _{B}$ is supported by ${ supp}(B)$.

According to Proposition 4, to prove that the function $g:=X \mapsto \varphi _{X}$ defined on $\wp _{fs}(U)$ (with the codomain contained in $\{0,1\}^{U}_{fs}$ according to the above paragraph) is equivariant, we have to prove that $\pi {\widetilde{\,\star \,}}g(X)=g(\pi \,\star \, X)$ for all $\pi \in S_{A}$ and $X \in \wp _{fs}(U)$ (where ${\widetilde{\,\star \,}}$ symbolizes the induced $S_{A}$-action on $\{0,1\}^{U}_{fs}$). This means that we need to verify the relation $\pi {\widetilde{\,\star \,}} \varphi _{X} = \varphi _{\pi \,\star \, X}$ for all $\pi \in S_{A}$ and $X \in \wp _{fs}(U)$. Let fix $\pi \in S_{A}$ and $X \in \wp _{fs}(U)$. We know that $x \in \pi \,\star \, X$ if and only if $\pi ^{-1} \cdot x \in X$ for all $x \in U$. Thus, $\varphi _{X}(\pi ^{-1} \cdot x )=\varphi _{\pi \,\star \, X}(x)$ for all $x \in U$, and so, by the definition of ${\widetilde{\,\star }}$ and because $(\{0,1\}, \diamond )$ is necessarily a trivial invariant set, we have $(\pi {\widetilde{\,\star \,}} \varphi _{X})(x)=\pi \diamond \varphi _{X}(\pi ^{-1} \cdot x ) = \varphi _{X}(\pi ^{-1} \cdot x )=\varphi _{\pi \,\star \, X}(x)$ for all $x\in U$. Hence $\pi {\widetilde{\,\star \,}} \varphi _{X} = \varphi _{\pi \,\star \, X}$, and because X has been arbitrarily chosen from $\wp _{fs}(U)$, we have that g is equivariant.

We proved that g is an equivariant function from $\wp _{fs}(U)$ to $\{0,1\}^{U}_{fs}$. Clearly, g is injective. Now we prove that g is surjective. Let us consider an arbitrary finitely supported function $f{:}\, U \rightarrow \{0,1\}$. Let $B_{f}\overset{def}{=}\{x \in U\;|\; f(x)=1\}$. We claim that $B_{f} \in \wp _{fs}(U)$. Let $\pi \in Fix({ supp}(f))$. According to Proposition 4, we have $f(\pi \cdot x)=f(x)$ for all $x \in U$. Thus, for each $x \in B_{f}$, we have $\pi \cdot x \in B_{f}$. Therefore, $\pi \,\star \, B_{f}=B_{f}$, and so $B_{f}$ is finitely supported by ${ supp}(f)$. A simple calculation show us that $g(B_{f})=f$, and so g is surjective.

• 4. Clearly, the inclusion relation $\subseteq$ is an equivariant order relation on the invariant set $(\wp _{fs}(U), \,\star \,)$ because, from the definition of $\,\star \,$, $X \subseteq Y$ leads to $\pi \,\star \, X=\{\pi \cdot x\,|\, x\in X\} \subseteq \{\pi \cdot y\,|\, y\in Y\}= \pi \,\star \, Y$ for all $\pi \in S_{A}$ and $X,Y \in \wp _{fs}(U)$. We prove that the set $S:=\{X\;|\; X \in \wp _{fs}(U), X \subseteq f(X)\}$ is a non-empty finitely supported subset of $(\wp _{fs}(U), \,\star \,)$. Obviously, $\emptyset \in S$. We claim that S is supported by ${ supp}(f)$. Let $\pi \in Fix({ supp}(f))$, and $X\in S$. Then $X \subseteq f(X)$. From the definition of $\,\star \,$ we have $\pi \,\star \, X \subseteq \pi \,\star \, f(X)$. According to Proposition 4, because ${ supp}(f)$ supports f, we have $\pi \,\star \, X \subseteq \pi \,\star \, f(X)=f(\pi \,\star \, X)$, and so $\pi \,\star \, X \in S$. It follows that S is finitely supported, and ${ supp}(S) \subseteq supp(f)$. We claim that $T:={\mathop {\cup }\nolimits _{X \in S}}X$ is finitely supported by ${ supp}(S)$. Indeed, let $\pi \in Fix({ supp}(S))$. Let $x\in {\mathop {\cup }\nolimits _{X \in S}}X$. There exists $Y\in S$ such that $x\in Y$. Since $\pi \in Fix({ supp}(S))$, we have $\pi \,\star \, Y\in S$, that is there exists $Z \in S$ such that $\pi \,\star \, Y=Z$. Therefore, $\pi \cdot x\in \pi \,\star \, Y=Z$, and so $\pi \cdot x\in {\mathop {\cup }\nolimits _{X \in S}}X$. We obtain $\pi \,\star \, {\mathop {\cup }\nolimits _{X \in S}}X={\mathop {\cup }\nolimits _{X\in S}}X$, and so T is finitely supported by ${ supp}(S) \subseteq supp(f)$.

We prove that $f(T)=T$. Considering an arbitrary $X \in S$, we have $X \subseteq f(X) \subseteq f(T)$. By taking the supremum (union) on S, this leads to $T \subseteq f(T)$. However, because $T \subseteq f(T)$ and f is order preserving, we also have $f(T) \subseteq f(f(T))$. Furthermore, f(T) is supported by ${ supp}(f) \cup supp(T)$, and so $f(T) \in S$. According to the definition of T, we get $f(T) \subseteq T$. Moreover, T is the greatest fixed point of f. Indeed, whenever $T'$ is an element in $\wp _{fs}(U)$ such that $f(T')=T'$, it follows that $T'\in S$, and so $T'\subseteq T$. In a similar way we prove that the set $S'=\{X \in \wp _{fs}(U)\,|\, f(X)\subseteq X\}$ is finitely supported by ${ supp}(f)$. Similarly (as in the paragraphs above), there exists ${\mathop {\cap }\nolimits _{X \in S'}}X' \in \wp _{fs}(U)$ (also supported by ${ supp}(f)$) which is the least fixed point of f. $\square$

6 Choice properties of the atoms

An invariant Boolean algebra is an invariant set $(L, \cdot )$ endowed with an equivariant lattice order $\sqsubseteq$ and with the additional condition that L is distributive and uniquely complemented. A finitely supported prime ideal of the Boolean algebra $(L, \sqcup , \sqcap )$ is a finitely supported subset I of L with the properties that I is a lower set (for every $x \in I$, $y \le x$ implies that $y \in I$), I is directed (for every $x,y \in I$ we have $x \sqcup y \in I$) and I is prime (for every $x,y \in L$ we have that $x \sqcap y \in I$ implies that $x \in I$ or $y \in I$). In Theorem 2.14 from [1] we proved that Boolean prime ideal theorem (claiming that every non-trivial invariant Boolean algebra has a finitely supported prime ideal) is false in FSM. However, we are able to prove that for $\wp _{fs}(A)$ the Boolean prime ideal theorem holds.

Antichains in a partially ordered set are subsets of pairwise incomparable elements. Maximal antichain principle claims that any partially ordered set has a maximal antichain. This statement is equivalent with the axiom of choice in ZF. Although $\wp _{fs}(A)$ has no choice function, we prove that it contains a maximal antichain.

Ramsey’s original theorem (ROT) in ZF states that if we consider an infinite set X and colour the elements of $\wp _{n}(X)$ in c different colours, then there exists some infinite subset M of X such that the all the subsets of M of size n are coloured by the same colour. In the ZF framework, ROT is not provable without assuming some form choice. In [3] it is proved that the axiom of countable choice (claiming the existence of a choice function on each countable family of non-empty sets) implies ROT. Furthermore, according to [10] ROT implies that every infinite family of nonempty finite sets has a partial choice function (i.e. it has an infinite subfamily with a choice function). There exist models of set theory in which ROT fails. In Proposition 8.8 of [7] it is proved that the set of atoms from Fraenkel’s second model of ZFA does not satisfy ROT, while from [3, 10] we know that ROT is false in the second Cohen model of ZF (model M7 in [8]) and in the basic Cohen model of ZF (model M1 in [8]). However ROT is true in the basic Fraenkel model according to [3]. A more recent development regarding ROT is in [12]. Although countable choice principle is inconsistent in FSM [1], we provide a constructive proof for a result stating that A satisfies ROT in FSM. Our proof of Theorem 7 follows Blass’s technique for proving the general validity of ROT in basic Fraenkel model (adapted to groups actions and invariant sets, and presented in a constructive manner for the invariant set A). Furthermore, we are able to prove easily that Infinite Pigeon-Hole Principle (the particular case of ROT for $n=1$) is valid for all invariant sets, but in this case we do not provide a constructive approach as in the case of ROT for A.

Theorem 7

For the set of atoms the following choice forms are valid:

• 1. $(\wp _{fs}(A), \,\star \,, \subseteq ,)$ is an invariant Boolean lattice and the subset $\wp _{{ fin}}(A)$ is a finitely supported prime and maximal ideal of $\wp _{fs}(A)$.

• 2. $(\wp _{fs}(A), \,\star \,, \subseteq )$ is an invariant Boolean lattice and $\wp _{{ cofin}}(A)$ is a finitely supported prime and maximal filter of $\wp _{fs}(A)$.

• 3. The invariant partially ordered set $(\wp _{fs}(A), \,\star \,, \subseteq )$ contains infinitely many maximal antichains (i.e. it contains infinitely many equivariant maximal subsets of pairwise incomparable elements).

• 4. Infinite Pigeon-Hole Principle holds for all invariant sets, and particularly for the invariant sets A, $\wp _{fs}(A)$, $\wp _{n}(A)$: Suppose that there exists an FSM colouring on the elements of an infinite invariant set $(X, \cdot )$ with finitely many colours belonging to a certain invariant set $(Y, \diamond )$. Then there exists a set $M \subseteq X$ infinite and finitely supported such that all elements of M are FSM coloured with the same colour.

• 5. Ramsey’s theorem for atoms holds in FSM, and furthermore, it admits a constructive proof: Let $n \ge 1$. If there exists an FSM colouring on the elements of $(\wp _{n}(A), \,\star \,)$ with finitely many colours belonging to a certain invariant set $(Y, \diamond )$ (i.e. a finitely supported function from $\wp _{n}(A)$ to a finite subset of Y), then we can construct$M \subseteq A$ infinite and finitely supported such that all n-sized subsets of M are FSM coloured with the same colour.

Proof

• 1. Clearly $\subseteq$ is an equivariant lattice order relation on $\wp _{fs}(A)$ by the definition of $\,\star \,$ in Proposition 2(6). The distributivity property over $(\wp _{fs}(A), \subseteq )$ follows directly. The greatest lower bound and the least upper bound in $\wp _{fs}(A)$ are $\emptyset$ and A, respectively. Let $X \in \wp _{fs}(A)$. Clearly, $A {\setminus } X$ is supported by ${ supp}(X)$, and so $A {\setminus } X \in \wp _{fs}(A)$. Thus, ($\wp _{fs}(A), \,\star \,, \subseteq )$ is an invariant Boolean lattice. We have that $\wp _{{ fin}}(A)$ is an equivariant subset of $\wp _{fs}(A)$. It is obviously a directed lower set. We prove now that $\wp _{{ fin}}(A)$ is prime. Let X and Y be two finitely supported subsets of A such that $X \cap Y \in \wp _{{ fin}}(A)$. Assume that neither X nor Y is finite. Then, because both X and Y are finitely supported subsets of A, and every finitely supported subset of A is either finite or cofinite, we have that both X and Y are cofinite, which means both $A{\setminus } X$ and $A {\setminus } Y$ are finite. By de Morgan laws, we have $A {\setminus } (X \cap Y)=(A{\setminus } X) \cup (A {\setminus } Y)$, and so $A {\setminus } (X \cap Y)$ is finite (as a union of two finite subsets of A), which means $X \cap Y$ is infinite, a contradiction. Thus, at least one of the subsets X and Y should be finite. Now, we prove that $\wp _{{ fin}}(A)$ is a maximal ideal in $\wp _{fs}(A)$. Let I be an ideal of $\wp _{fs}(A)$ with $\wp _{{ fin}}(A) \subsetneq I \subseteq \wp _{fs}(A)$. Then I contains a cofinite subset of A of form $A{\setminus } X$ with X finite. Since I is an ideal and $X \in I$, we have $A=X \cup (A {\setminus } X) \in I$. Since I is a lower set, we have that every $Y \in \wp _{fs}(A)$ (i.e. every $Y \subseteq _{fs} A$) is a member of I. Then $I=\wp _{fs}(A)$.

• 2. By duality with item 1.

• 3. For each $n \in {\mathbb {N}}$ we define $\wp _{n}(A)$. Since permutations of atoms are bijective functions, the effect of any permutation of atoms on an n-sized subset of A is another n-sized subset of A. Thus, each $\wp _{n}(A)$ is an equivariant subset of $\wp _{fs}(A)$. Obviously, for a fixed $n \in {\mathbb {N}}$, any two elements of $\wp _{n}(A)$ are incomparable via $\subseteq$ because they are different subsets of A having the same cardinality. Furthermore, if there was a finitely supported antichain U of $\wp _{fs}(A)$ with $\wp _{n}(A) \subsetneq U \subseteq \wp _{fs}(A)$, then U should contain at least a subset V of A having the size different from n (since $\wp _{n}(A)$ contains all the n-sized subsets of A). Such a subset V of A is comparable via the inclusion relation with at least one n-sized subset of A, and so U would not be an antichain of $\wp _{fs}(A)$. Thus, $\wp _{n}(A)$ is a maximal antichain of $\wp _{fs}(A)$ for each $n \in {\mathbb {N}}$.

• 4. We have that the set of colours $\{c_{1}, \ldots , c_{m}\}$ forms a subset of Y which is finitely supported by $S=supp(c_{1})\cup \cdots \cup supp(c_{m})$. By hypothesis, there exists an FSM colouring on X, which means there exists a finitely supported function $f{:}\, X \rightarrow \{c_{1}, \ldots , c_{m}\}$. We denote by $X_{i}=f^{-1}(c_{i})=\{x \in X\,|\,f(x)=c_{i}\}$ for all $i \in \{1, \ldots , n\}$. We claim that $X_{i}$ is supported by ${ supp}(f) \cup supp(c_{i})$ for any $i \in \{1, \ldots , n\}$. Fix some i, and let $\pi \in Fix({ supp}(f) \cup supp(c_{i}))$ and $y \in X_{i}=f^{-1}(c_{i})$. This means $f(y)=c_{i}$. Thus, because $\pi$ fixes ${ supp}(f)$ pointwise, we have $f(\pi \cdot y)= \pi \diamond f(y) =\pi \diamond c_{i}$. However, since $\pi$ fixes ${ supp}(c_{i})$ pointwise and ${ supp}(c_{i})$ supports $c_{i}$, we have $\pi \diamond c_{i}=c_{i}$, and so $\pi \cdot y \in f^{-1}(c_{i})$. Therefore, $X_{i}$ is finitely supported for all $i \in \{1, \ldots , n\}$. Since f is a function, it follows that $X={\mathop {\cup }\nolimits _{i}}X_{i}$. Since X is infinite, at least one $X_{i}$ should be infinite. Such an $X_{i}$ is the required subset M of X. Furthermore, the mapping $g=f|_{M}:M \rightarrow \{c_{i}\}$ is supported by ${ supp}(f) \cup supp(M)=supp(f) \cup supp(c_{i})$.

• 5. Suppose that the set of colours $\{c_{1}, \ldots , c_{m}\}$ belongs to the invariant set $(Y,\diamond )$, and so $\{c_{1}, \ldots , c_{m}\}$ is finitely supported by $S=supp(c_{1})\cup \cdots \cup supp(c_{m})$. By hypothesis, there exists an FSM colouring on $\wp _{n}(A)$, which means there exists a finitely supported function $f{:}\, \wp _{n}(A) \rightarrow \{c_{1}, \ldots , c_{m}\}$. Let us consider $M=A {\setminus } ({ supp}(f) \cup supp(c_{1}) \cup \cdots \cup supp(c_{m}))$. Since ${ supp}(f) \cup supp(c_{1}) \cup \cdots \cup supp(c_{m})$ is finite, it follows that M is cofinite, and so it is finitely supported with ${ supp}(M)=supp(f) \cup supp(c_{1}) \cup \cdots \cup supp(c_{m})$. Thus, M is an infinite finitely supported subset of A. Furthermore, $\wp _{n}(M)=\{X \subseteq M \,|\,|X|=n\}$ is a subset of $\wp _{n}(A)$ which is supported by ${ supp}(M)$; this follows because, whenever $\sigma \in Fix({ supp}(M))$ and $X \in \wp _{n}(M)$, we have $X \subseteq M$ and $|X|=n$, and so $\sigma \,\star \, X \subseteq \sigma \,\star \, M=M$ and $|\sigma \,\star \, X|=n$, from which $\sigma \,\star \, X \in \wp _{n}(M)$. Let us consider $X,Y \in \wp _{n}(M)$ with $X \ne Y$. Suppose that X and Y have $k<n$ identical elements. After o renumbering of the elements from X and Y (which is possible without requiring any form of choice because both X and Y are finite), we can suppose that the first k elements from X and Y coincide, while the other elements are all different. Thus, X is of from $\{x_{1}, \ldots , x_{k}, x_{k+1}, \ldots , x_{n}\}$ and Y is of form $\{x_{1}, \ldots , x_{k}, y_{k+1}, \ldots , y_{n}\}$ where $x_{i}\ne y_{j}$ for all $i \in \{1, \ldots , n \}$ and $j \in \{k+1, \ldots , n\}$. We define a function $\pi : A \rightarrow A$ by:

  $$\begin{aligned} \pi (x)=\left\{ \begin{array}{ll} x, &{} \quad \text {if}\, {x \in \{x_{1}, \ldots , x_{k}\}};\\ y_{l}, &{} \quad \text {if}\, {x=x_{l} \in \{x_{k+1}, \ldots , x_{n}\}};\\ x_{l}, &{} \quad \text {if}\, {x=y_{l} \in \{y_{k+1}, \ldots , y_{n}\}};\\ x, &{} \quad \text {if}\, {x \in A {\setminus } \{x_{1}, \ldots , x_{k}, x_{k+1}, \ldots x_{n}, y_{k+1}, \ldots , y_{n}\} }.\end{array}\right. \end{aligned}$$

  From the above definition we have that $\pi$ is a finite permutation of A, and $\pi \,\star \, X=\{\pi (x_{1}), \ldots , \pi (x_{k}), \pi (x_{k+1}), \ldots , \pi (x_{n})\}=\{x_{1}, \ldots , x_{k}, y_{k+1}, \ldots , y_{n}\}=Y$. Since $\pi$ changes only elements belonging to M, it follows that $\pi$ fixes ${ supp}(f) \cup supp(c_{1}) \cup \cdots \cup supp(c_{m})$ pointwise. Thus, since $\pi \in Fix({ supp}(f))$, by Proposition 4 we have $f(Y)=f(\pi \,\star \, X)=\pi \diamond f(X)$. However, since $\pi$ fixes ${ supp}(c_{1}) \cup \cdots \cup supp(c_{m})$ pointwise and $f(X) \in \{c_{1}, \ldots , c_{m}\}$, we have $\pi \diamond f(X)=f(X)$ and so $f(Y)=f(X)$. Since X and Y were arbitrarily chosen from the family of n-sized subsets of M, it follows that $f(\wp _{n}(M))$ is a single-element set. Furthermore, $g=f|_{\wp _{n}(M)}$ is a finitely supported function (supported by ${ supp}(f) \cup supp(M)=supp(f) \cup supp(c_{1}) \cup \cdots \cup supp(c_{m})$). $\square$

7 Conclusion and future work

Finitely Supported Mathematics studies finitely supported algebraic structures (i.e. finitely supported sets together with finitely supported internal laws), hierarchically defined starting from an infinite family of basic elements (i.e. atoms) by means of their finite supports. The S-finite support principle (Sect. 2) shows us how the property of being finitely supported is transferred to higher-order constructions starting from the basic elements. Thus, in order to provide finite support properties for higher-order finitely supported structures, it is important to find finite support properties of basic atomic sets (from which higher-order constructions are developed) such as the set of all atoms, its (finite or cofinite) powerset, its second order powerset, or the set of all (finite) injective tuples of atoms. In this paper we studied the properties of these basic atomic sets used to define FSM, proving the existence or the non-existence of finitely supported relations between them. Several properties of the atoms were obtained in Theorem 6 by translating non-atomic ZF results into FSM by using the methods described in Sect. 2. However, the most important properties of the atomic sets are those specific to FSM (i.e. they do not have a related non-atomic correspondent) which are presented in Theorem 1 (proving properties of finitely supported mappings between atomic and non-atomic sets), Theorem 2 (proving finiteness properties of infinite atomic sets), Theorem 3 (proving properties of the cardinalities of atomic sets), Theorem 4 (proving existence and calculability properties of fixed points for special finitely supported mappings on atomic sets) and Theorem 5 (emphasizing examples of atomic sets not satisfying certain choice principles). We also presented valid choice properties for the set of atoms and its powerset (Theorem 7). As a straightforward remark, the properties of atomic sets obtained in this paper are also valid in the FM axiomatic set theory (reformulated accordingly when the fixed ZF set A used for equipping classical sets with group actions is replaced by the set of atoms in ZFA) and in the categorical ZF framework of nominal sets which are invariant sets developed over countable families of atoms. Thus, the results presented in this paper provide new properties of the atoms in all these frameworks.

A future research direction will be to analyze the validity of the properties presented in this paper in the EFM set theory [1] defined by replacing the finite support axiom in FM set theory with a weaker axiom claiming that each subset of atoms should be either finite or cofinite. More exactly, in EFM set theory we require only the subsets of atoms to be finitely supported, while higher-order sets could be non-finitely supported. This research direction could also be a contribution to the theory of ZF amorphous sets.