Various forms of infinity for finitely supported structures

Abstract

The goal of this paper is to define and study the notion of infinity in the framework of finitely supported structures, presenting new properties of infinite cardinalities. Some of these properties are extended from the non-atomic Zermelo–Fraenkel set theory to the world of atomic objects with finite support, while other properties are specific to finitely supported structures. We compare alternative definitions for infinity in the world of finitely supported sets, and provide relevant examples of atomic sets which satisfy some forms of infinity, while do not satisfy others. Finally, we provide a characterization of finitely supported countable sets.

1 Introduction

The theory of finitely supported algebraic structures is essentially a reformulation of Zermelo–Fraenkel set theory obtained by requiring that every set theoretical construction to be finitely supported according to a certain action of a group of permutations of some basic elements named atoms. Its main purpose is to characterize infinite algebraic structures only by using their finite supports. This theory of finitely supported algebraic structures is known also under the name of ‘nominal sets’ when dealing with computer science applications. The theory of nominal sets is presented in a categorical manner as a Zermelo–Fraenkel (ZF) alternative to Fraenkel and Mostowski permutation models of Zermelo Fraenkel set theory with atoms [9]. A nominal set is defined as a usual ZF set endowed with a group action of the group of (finitary) permutations over a certain fixed countable ZF set A (also called the set of atoms by analogy with the Fraenkel and Mostowski framework) formed by elements whose internal structure is not taken into consideration (i.e. by elements that can be checked only for equality), satisfying a finite support requirement. This requirement states that for any element in a nominal set there should exist a finite set of atoms such that any permutation fixing pointwise this set of atoms also leaves the element invariant under the related group action. A finitely supported set is actually a finitely supported element in the powerset of a nominal set. Nominal sets represent a categorical mathematical theory of names studying scope, binding, freshness and renaming in formal languages based upon symmetry. Inductively defined finitely supported sets involving the name-abstraction together with Cartesian product and disjoint union can encode syntax modulo renaming of bound variables. In this way, the theory of algebraic data types can be extended to include signatures involving binding operators. In particular, there is an associated notion of structural recursion for defining syntax-manipulating functions and a notion of proof by structural induction. Various generalizations of nominal were used in order to study automata, languages or Turing machines that operate over infinite alphabets; for this a relaxed notion of finiteness, called ‘orbit finiteness’, was defined and means ‘having a finite number of orbits under a certain group action’ [4].

Finitely Supported Mathematics (shortly, FSM) is a general name for the theory of finitely supported algebraic structures (that are finitely supported sets together with finitely supported internal algebraic operations). It allows a discrete study of structures which are possibly infinite, but contain enough symmetries such that they can be concisely represented and manipulated. In order to develop FSM, the nominal sets are used without the requirement that the set A of atoms is countable. By now on, these sets will be called ‘invariant sets’, a name motivated by Tarski’s approach regarding logicality (i.e. a logical notion is defined by Tarski as one that is invariant under the permutations of the universe of discourse). The cardinality of the set of atoms cannot be internally compared with any other ZF cardinality, and so we just say that atoms form an infinite set without any specifications regarding its cardinality. In FSM, we actually study the finitely supported subsets of invariant sets together with finitely supported relations (order relations, functions, algebraic laws etc), and so FSM becomes a theory of atomic algebraic structures defined according to the finite support requirement. The requirement of being finitely supported under a canonical action of the group of permutation of atoms (constructed under the rules of Proposition 3) is actually an axiom adjoined to ZF, and so non-finitely supported structures are not allowed in FSM. Formally, FSM contains both the family of ‘non-atomic’ (i.e., ordinary) ZF structures which are proved to be trivial FSM structures (i.e., their elements are left unchanged under the effect of the canonical permutation action) and the family of ‘atomic’ structures (i.e., structures that are hierarchically defined by involving at least an element of A in a certain construction step). Our purpose is to analyze whether a classical ZF result (obtained in the framework of non-atomic structures) can be adequately reformulated by replacing ‘non-atomic ZF structure’ with ‘atomic and finitely supported structure’ in order to be valid also for atomic sets with finite supports.

The translation of the results from a non-atomic framework into an atomic framework (such as Zermelo Fraenkel set theory with atoms (ZFA)) is not an easy task. Results from ZF may lose their validity when reformulating them in ZFA. For example, it is known that multiple choice principle and Kurepa’s maximal antichain principle are both equivalent to the axiom of choice in ZF. However, multiple choice principle is valid in the Fraenkel Second Model, while the axiom of choice fails in this model [7]. Furthermore, Kurepa’s maximal antichain principle is valid in the Fraenkel Basic Model, while the axiom of choice fails in this model [7]. This means that the following two statements that are valid in ZF, namely ‘Kurepa’s principle implies axiom of choice’ and ‘Multiple choice principle implies axiom of choice’ fail in ZFA. Similarly, there are examples of ZF results that cannot be reformulated into FSM (there exist an analogy between ZFA and FSM, but we mention the construction of FSM makes sense over classical ZF without being necessary to modify the ZF axiom of extensionality); we particularly mention choice principles (that are proved to be independent from ZF axioms, but inconsistent in FSM) and Stone duality [1].

A proof of an FSM result should be internally consistent in FSM and not retrieved from ZF, that means it should involve only finitely supported constructions (even in the intermediate steps). The meta-theoretical techniques for the translation of a result from non-atomic structures to atomic structures are based on a refinement of the finite support principle from [9] called ‘S-finite supports principle’ claiming that for any finite set S of atoms, anything that is definable in higher-order logic from S-supported structures by using S-supported constructions is also S-supported [1]. The formal involvement of the S-finite support principle actually implies a hierarchical construction of the support of a structure by employing, step-by-step, the supports of the substructures of a related structure.

In this paper we introduce and study the notion of ‘cardinality’ for a finitely supported set, proving several properties related to this concept. Some properties are naturally extended from the non-atomic ZF framework into the world of atomic structures, while other properties of atomic cardinalities do not have a non-atomic correspondent. For example, we prove that Cantor-Schröder-Bernstein theorem for cardinalities is still valid in FSM. However, its ZF dual is no longer valid in FSM. Other order and arithmetic FSM properties of cardinalities are analyzed. We also introduce various definition for infinity and compare them, providing relevant examples of atomic sets verifying the conditions of each such definition. The classical notion of finite is related to the notion of ‘finite ordinal’ or natural number. In the presence of the axiom of choice, every set can be well-ordered, and the multiple definitions of ‘(in)finite’ are proved to be equivalent. In FSM the choice principles fail [1], there may exist FSM sets that are non well-orderable (particularly the set of atoms), and so it makes sense to study various non-equivalent definitions for (in)finite. The study of multiple definitions of (in)finite actually provides a way of classifying non well-orderable sets according to their cardinal-invariant properties. An important question is how ‘large’ an infinite set could be. For example, we prove that the set of atoms and its finite powerset are infinite, but they do not contain infinite finitely supported countable subsets, and for the finitely supported self-mappings defined on them, the injectivity is equivalent with the surjectivity. The union $A \cup {\mathbb {N}}$ between the set of atoms and the set of natural numbers contains an infinite, finitely supported, countable subset, but there is no finitely supported bijection between $A \cup {\mathbb {N}}$ and the disjoint union $(A \cup {\mathbb {N}})+(A \cup {\mathbb {N}})$. Furthermore, there is a finitely supported bijection between $A \times {\mathbb {N}}$ and the disjoint union $(A \times {\mathbb {N}})+(A \times {\mathbb {N}})$, but there is no finitely supported bijection between $A \times {\mathbb {N}}$ and the Cartesian product $(A \times {\mathbb {N}}) \times (A \times {\mathbb {N}})$.

The notion of Dedekind infinity was firstly discussed in [3] where the authors proved that some basic atomic sets (such as the set of atoms, its FSM powerset, the finite powerset of its FSM powerset, and the set of all permutation of atoms) are Dedekind finite. In this paper we prove that even larger atomic sets, such as the set of all finitely supported mappings from the set of atoms to an FSM set that does not contain an infinite uniformly supported subset is Dedekind finite. Moreover, new properties of Dedekind (in)finite sets are established, and the notion of Dedekind infinity is connected with other FSM concepts of infinity. Finally, we study the concept of countability in FSM.

2 Finitely supported sets

A finite set (without other specification) means a set for which there is a bijection with a finite ordinal, i.e. to a set that can be represented as $\{x_{1}, \ldots , x_{n}\}$ for some $n \in {\mathbb {N}}$. An infinite set (without other specification) means ‘a set which is not finite’, i.e. a set which is “FSM classical infinite" according to Definition 8. Adjoin to ZF a special infinite set A (called ‘the set of atoms’; despite classical set theory with atoms we do not need to modify the axiom of extensionality). Actually, atoms are entities whose internal structure is considered to be irrelevant which are considered as basic for a higher-order construction, i.e. their internal structure is not taken into consideration.

A transposition 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 (finitary) permutation of A in FSM is a one-to-one transformation of A onto itself (a bijection of A) generated by composing finitely many transpositions. We denote by $S_{A}$ the set of all finitary permutations of A. According to Proposition 2.6 from [1], a function $f:A \rightarrow A$ is a bijection on A in FSM if and only if it leaves unchanged all but finitely many elements of A. Thus, in FSM a function is a one-to-one transformation of A onto itself if and only if it is a (finitary) permutation of A. Thus, the notions ‘permutation (bijection) of A’ and ‘finitary permutation of A’ coincide in FSM, and when saying ‘permutation of A’ we actually refer to a ‘finitary permutation of A’.

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$ supports x 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$ for all $\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 )$ be an $S_{A}$-set, and $\pi \in S_{A}$. If $x\in X$ is finitely supported, then $\pi \cdot x$ is finitely supported and $supp(\pi \cdot x)=\pi (supp(x))$.

Example 1

• 1. The set A of atoms is an $S_{A}$-set with the $S_{A}$-action $\cdot :S_{A}\times A\rightarrow A$ defined by $\pi \cdot a:=\pi (a)$ for all $\pi \in S_{A}$ and $a\in A$. $(A,\cdot )$ is an invariant set because for each $a\in A$ we have that $\{a\}$ supports a. Furthermore, $supp(a)=\{a\}$ for each $a\in A$.

• 2. The set $S_{A}$ is an $S_{A}$-set with the $S_{A}$-action $\cdot :S_{A}\times S_{A}\rightarrow S_{A}$ defined by $\pi \cdot \sigma :=\pi \circ \sigma \circ \pi ^{-1}$ for all $\pi ,\sigma \in S_{A}$. $(S_{A},\cdot )$ is an invariant set because for each $\sigma \in S_{A}$ we have that the finite set $\{a\in A\,|\,\sigma (a)\ne a\}$ supports $\sigma$. Furthermore, $supp(\sigma )=\{a\in A\,|\,\sigma (a)\ne a\}$ for each $\sigma \in S_{A}$.

• 3. Any ordinary (non-atomic) ZF-set X (such as ${\mathbb {N}},{\mathbb {Z}},{\mathbb {Q}}$ or ${\mathbb {R}}$, for example) is an invariant set with the single possible $S_{A}$-action $\cdot :S_{A}\times X\rightarrow X$ defined by $\pi \cdot x:=x$ for all $\pi \in S_{A}$ and $x\in X$.

Proposition 3

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

• 1. The Cartesian product $X\times Y$ is also an $S_{A}$-set with the $S_{A}$-action $\otimes :S_{A}\times (X\times Y)\rightarrow (X\times Y)$ 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.

• 2. The powerset $\wp (X)=\{Z\,|\, Z\subseteq X\}$ is also an $S_{A}$-set with the $S_{A}$-action $\star : S_{A}\times \wp (X) \rightarrow \wp (X)$ 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)$.

• 3. 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 2. If X is an invariant set, then both $\wp _{fin}(X)$ and $\wp _{cofin}(X)$ are invariant sets.

• 4. The disjoint union of X and Y is defined by $X+Y=\{(0,x)\,|\, x\in X\}\cup \{(1,y)\,|\, y\in Y\}$. $X+Y$ is an $S_{A}$-set with the $S_{A}$-action $\star :S_{A}\times (X+Y)\rightarrow (X+Y)$ defined by $\pi \star z=(0,\pi \cdot x)$ if $z=(0,x)$ and $\pi \star z=(1,\pi \diamond y)$ if $z=(1,y)$. If $(X,\cdot )$ and $(Y,\diamond )$ are invariant sets, then $(X+Y,\star )$ is also an invariant set: each $z\in X+Y$ is either of the form (0, x) and supported by the finite set supporting x in X, or of the form (1, y) and supported by the finite set supporting y in Y.

Definition 2

• 1. Let $(X,\cdot )$ be an $S_{A}$-set. A subset Z of X is called finitely supported if and only if $Z\in \wp _{fs}(X)$ with the notations from Proposition 3. A subset Z of X is uniformly supported if all the elements of Z are supported by the same set S (and so Z is itself supported by S as an element of $\wp _{fs}(X)$). Generally, an FSM set is a finitely supported subset (possibly equivariant) of an invariant set.

• 2. Let $(X,\cdot )$ be a finitely supported subset of an $S_{A}$- set $(Y, \cdot )$. A subset Z of Y is called finitely supported subset of X (and we denote this by $Z \in \wp _{fs}(X)$) if and only if $Z\in \wp _{fs}(Y)$ and $Z \subseteq X$. Similarly, we say that a uniformly supported subset of Y contained in X is a uniformly supported subset of X.

From Definition 1, a subset Z of an invariant set $(X, \cdot )$ is finitely supported by a set $S \subseteq A$ if and only if $\pi \star Z \subseteq Z$ for all $\pi \in Fix(S)$. This is because any permutation of atoms should have finite order.

Proposition 4

• 1. Let X be a uniformly supported subset of an invariant set $(U, \cdot )$. Then X is finitely supported and $supp(X)=\cup \{supp(x)\,|\, x\in X\}$.

• 2. Let X be a finite subset of an invariant set $(U, \cdot )$. Then X is finitely supported and $supp(X)=\cup \{supp(x)\,|\, x\in X\}$.

Proof

• 1. Since X is uniformly supported, there exists a finite subset of atoms T such that T supports every $x \in X$, i.e. $supp(x) \subseteq T$ for all $x \in X$. Thus, $\cup \{supp(x)\,|\, x\in X\} \subseteq T$. Clearly, $supp(X) \subseteq \cup \{supp(x)\,|\, x\in X\}$. Conversely, let $a \in \cup \{supp(x)\,|\, x\in X\}$. Thus, there exists $x_{0} \in X$ such that $a \in supp(x_{0})$. Let b be an atom such that $b \notin supp(X)$ and $b \notin T$. Such an atom exists because A is infinite, while supp(X) and T are both finite. We prove by contradiction that $(b\; a) \cdot x_{0} \notin X$. Indeed, suppose that $(b\; a) \cdot x_{0}=y \in X$. According to Proposition 2, we have $supp(y)=(b\; a)(supp(x_{0}))$. Since $a \in supp(x_{0})$, we have $b =(b\;a)(a) \in (b\; a)(supp(x_{0}))=supp((b\; a) \cdot x_{0})=supp(y)$. Since $supp(y) \subseteq T$, we get $b \in T$, a contradiction. Therefore, $(b\; a) \star X \ne X$, where $\star$ is the standard $S_{A}$-action on $\wp (U)$ is defined in Proposition 3. Since $b \notin supp(X)$, we prove by contradiction that $a \in supp(X)$. Indeed, suppose that $a \notin supp(X)$. It follows that the transposition $(b\; a)$ fixes each element from supp(X), i.e. $(b\; a) \in Fix(supp(X))$. Since supp(X) supports X, by Definition 1, it follows that $(b\; a) \star X=X$, which is a contradiction. Thus, $a \in supp(X)$.

• 2. Any finite set $X=\left\{ x_{1},\ldots , x_{k}\right\}$ is uniformly supported by $S=supp(x_{1})\cup \ldots \cup supp(x_{k})$, and so the result follows from the above item.

$\square$

Corollary 1

Let X be a uniformly supported subset of an invariant set. Then X is uniformly supported by supp(X).

Proof

Since $supp(X)=\cup \{supp(x)\,|\, x\in X\}$, we have $supp(x) \subseteq supp(X)$ for all $x \in X$ which means supp(X) supports every $x \in X$. $\square$

Proposition 5

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

Proof

This result was proved as Proposition 3 in [3]. $\square$

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 6

[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 to 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)$. Particularly, a function $f:X\rightarrow Y$ is supported by a finite set $S \subseteq A$ if and only if for all $x \in X$ and all $\pi \in Fix(S)$ we have $f(\pi \cdot x)=\pi \diamond f(x)$.

3 Cardinalities and order properties

Definition 4

• An invariant partially ordered set (invariant poset) is an invariant set $(P,\cdot )$ together with an equivariant partial order relation $\sqsubseteq$ on P. An invariant poset is denoted by $(P,\sqsubseteq ,\cdot )$ or simply P.

• A finitely supported partially ordered set (finitely supported poset) is a finitely supported subset X of an invariant set $(P,\cdot )$ together with a partial order relation $\sqsubseteq$ on X that is finitely supported as a subset of $P\times P$.

The notion of cardinality cannot be developed in the world of atomic structures by involving the classical notion of ordinal. This is because ordinals are defined within non-atomic ZF, that is, they do not contain atoms. Despite of this, we are able to present a specific notion of cardinality in FSM.

Definition 5

Two FSM sets X and Y are called FSM equipollent if there exists a finitely supported bijection $f:X \rightarrow Y$.

Theorem 1

The equipollence relation is an equivariant equivalence relation on the family of all FSM sets.

Proof

• 1. The equipollence relation is equivariant. For any FSM sets X and Y, whenever there is a finitely supported bijection $f:X \rightarrow Y$, for any $\pi \in S_{A}$ we have that $\pi \star f:\pi \star X \rightarrow \pi \star Y$, defined by $(\pi \star f)(\pi \cdot x)=\pi \cdot f(x)$ for all $x \in X$, is bijective and finitely supported by $\pi (supp(f)) \cup \pi (supp(X)) \cup \pi (supp(Y))$. Indeed, according to Proposition 2 we have that $\pi (supp(X))$ supports $\pi \star X$ and $\pi (supp(Y))$ supports $\pi \star Y$. Let $\sigma \in Fix(\pi (supp(f)) \cup \pi (supp(X)) \cup \pi (supp(Y)))$. Thus, $\sigma (\pi (a))=\pi (a)$ for all $a\in supp(f)$. Therefore, $\pi ^{-1}(\sigma (\pi (a)))=\pi ^{-1}(\pi (a)) =a$ for all $a\in supp(f)$. So we get $\pi ^{-1}\circ \sigma \circ \pi \in Fix(supp(f))$. From Proposition 6, this means $(\pi ^{-1} \circ \sigma \circ \pi )\cdot x \in X$ and $f((\pi ^{-1} \circ \sigma \circ \pi )\cdot x)=(\pi ^{-1} \circ \sigma \circ \pi )\cdot f(x)$ for all $x \in X$. Fix an arbitrary $x\in X$. We have that $\sigma \cdot (\pi \cdot x) \in \pi \star X$, i.e. there exists $x' \in X$ such that $(\sigma \circ \pi ) \cdot x=\pi \cdot x'$, and so $x'=(\pi ^{-1} \circ \sigma \circ \pi )\cdot x$. According to Proposition 6, we have $(\pi \star f)(\sigma \cdot (\pi \cdot x))= (\pi \star f)(\pi \cdot x')=\pi \cdot f(x')=\pi \cdot f((\pi ^{-1} \circ \sigma \circ \pi )\cdot x)=\pi \cdot ((\pi ^{-1} \circ \sigma \circ \pi )\cdot f(x))=(\sigma \circ \pi )\cdot f(x)=\sigma \cdot (\pi \cdot f(x))=\sigma \cdot (\pi \star f)(\pi \cdot x)$. Now, from Proposition 6 we conclude that $\pi \star f$ is finitely supported. The bijectivity of $\pi \star f$ is obvious. Thus, $\pi \star X$ is equipollent with $\pi \star Y$ whenever X is equipollent with Y.

• 2. The equipollence relation is reflexive because for each FSM set X, the identity of X is a finitely supported (by supp(X)) bijection from X to X.

• 3. The equipollence relation is symmetric because for any FSM sets X and Y, whenever there exists a finitely supported bijection $f:X \rightarrow Y$, we have that $f^{-1}:Y \rightarrow X$ is bijective and supported by $supp(f) \cup supp(X) \cup supp(Y)$. Indeed, let $\pi \in Fix(supp(f) \cup supp(X) \cup supp(Y))$, and consider an arbitrary $y \in Y$. Since $\pi ^{-1} \in Fix(supp(f) \cup supp(X) \cup supp(Y))$, we have $f^{-1}(\pi \cdot y)=z \Leftrightarrow f(z)=\pi \cdot y \Leftrightarrow \pi ^{-1} \cdot f(z)=y \Leftrightarrow f(\pi ^{-1} \cdot z)=y \Leftrightarrow \pi ^{-1} \cdot z=f^{-1}(y) \Leftrightarrow z=\pi \cdot f^{-1}(y)$. Therefore, $f^{-1}(\pi \cdot y)=\pi \cdot f^{-1}(y)$ for all $y \in Y$, which, in the view of Proposition 6, means that $f^{-1}$ is finitely supported.

• 4. The equipollence relation is transitive because for any FSM sets X, Y and Z, whenever there are two finitely supported bijections $f:X \rightarrow Y$ and $g:Y \rightarrow Z$, there exists a bijection $g \circ f:X \rightarrow Z$ which is finitely supported by $supp(f) \cup supp(g)$. Indeed, let $\pi \in Fix(supp(f) \cup supp(g))$. According to Proposition 6, we get $\pi \cdot x \in X$, $\pi \cdot f(x) \in Y$, $\pi \cdot g(f(x)) \in Z$ and $(g \circ f)(\pi \cdot x)=g (f(\pi \cdot x))=g(\pi \cdot f(x))=\pi \cdot g(f(x))=\pi \cdot (g \circ f)(x)$ for all $x \in X$, and so the conclusion follows by involving again Proposition 6.

$\square$

We have to note that the equipollence relation is actually a relation of the family of all FSM sets which is actually a class. However, invariant classes can be defined as well in FSM, by updating Definition 1 accordingly.

Definition 6

The FSM cardinality of X is defined as the equivalence class of all FSM sets equipollent to X, and is denoted by |X|.

According to Definition 6 for two FSM sets X and Y we have $|X|=|Y|$ if and only if there exists a finitely supported bijection $f:X \rightarrow Y$. On the family of cardinalities we can define the relations:

• $\le$ by: $|X| \le |Y|$ if and only if there is a finitely supported injective (one-to-one) mapping $f:X \rightarrow Y$.

• $\le ^{*}$ by: $|X| \le ^{*} |Y|$ if and only if there is a finitely supported surjective (onto) mapping $f:Y \rightarrow X$.

Theorem 2

• 1. The relation $\le$ is equivariant, reflexive, anti-symmetric and transitive, but it is not total.

• 2. The relation $\le ^{*}$ is equivariant, reflexive and transitive, but it is not anti-symmetric, nor total.

Proof

Firstly, we prove that $\le$ and $\le ^{*}$ are well-defined, i.e. their definitions do not depend on the chosen representatives for cardinalities. Assume that there exist the FSM sets X, Y and $X',Y'$, such that $|X|=|X'|$ and $|Y|=|Y'|$ (i.e. there exist two finitely supported bijections $f:X\rightarrow X'$ and $g:Y\rightarrow Y'$).

If $|X| \le |Y|$, i.e. if there is a finitely supported injection $h:X\rightarrow Y$, then the function $g\circ h\circ f^{-1}:X'\rightarrow Y'$ is injective and finitely supported by $supp(f^{-1}) \cup supp(h) \cup supp(g)=supp(f) \cup supp(h) \cup supp(g)$. Thus, $|X'|\le |Y'|$.

If $|X|\le ^{\star }|Y|$, i.e. if there is a finitely supported surjection $h':Y\rightarrow X$, then the function $f\circ h'\circ g^{-1}:Y'\rightarrow X'$ is injective and finitely supported by $supp(f) \cup supp(h') \cup supp(g^{-1})=supp(f) \cup supp(h') \cup supp(g)$. Thus, $|X'|\le ^{\star } |Y'|$.

We start now to prove the mentioned properties for both relations: $\le$ and $\le ^{*}$.

• $\le$ and $\le ^{*}$ are equivariant because for any FSM sets X and Y, whenever there is a finitely supported injection/ surjection $f:X \rightarrow Y$, according to Proposition 2, we have that $\pi \star f:\pi \star X \rightarrow \pi \star Y$, defined by $(\pi \star f)(\pi \cdot x)=\pi \cdot f(x)$ for all $x \in X$, is a finitely supported (by $\pi (supp(f)) \cup \pi (supp(X)) \cup \pi (supp(Y))$) injective/surjective mapping, and so $\pi \star X$ is comparable with $\pi \star Y$ (under $\le$ or $\le ^{*}$, after case).

• $\le$ and $\le ^{*}$ are obviously reflexive because for each FSM set X, the identity of X is a finitely supported (by supp(X)) bijection from X to X.

• $\le$ and $\le ^{*}$ are transitive because for any FSM sets X, Y and Z, whenever there are two finitely supported injections/surjections $f:X \rightarrow Y$ and $g:Y \rightarrow Z$, there exists an injection/surjection $g \circ f:X \rightarrow Z$ which is finitely supported by $supp(f) \cup supp(g)$.

• The anti-symmetry of $\le$.

Lemma 1

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$. Furthermore, $supp(h) \subseteq supp(f) \cup supp(g)$.

Proof of Lemma 1

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.

Claim 1

F is correctly defined, i.e. $Im(F) \subseteq \wp _{fs}(B)$.

For every finitely supported subset X of B, we have that f(X) is supported by $supp(f) \cup supp(X)$. Indeed, let $\pi \in Fix(supp(f) \cup supp(X))$. Let y be an arbitrary element from f(X); then $y=f(x)$ for some $x \in X$. However, because $\pi \in Fix (supp(X))$, it follows that $\pi \cdot x \in X$ and so, because supp(f) supports f and $\pi$ fixes supp(f) pointwise, from Proposition 6 we get $\pi \diamond y= \pi \diamond f(x)= f(\pi \cdot x) \in f(X)$. Thus $\pi {\widetilde{\star }} f(X)=f(X)$, where ${\widetilde{\star }}$ is the $S_{A}$-action on $\wp _{fs}(C)$ defined as in Proposition 3. Similarly, g(Y) is finitely supported by $supp(g) \cup supp(Y)$ for all $Y \in \wp _{fs}(C)$. It is easy to remark that for every finitely supported subset X of B we have that $C-f(X)$ is also supported by $supp(f) \cup supp(X)$, $g(C-f(X))$ is supported by $supp(g) \cup supp(f) \cup supp(X)$, and $B-g(C-f(X))$ is supported by $supp(g) \cup supp(f) \cup supp(X)$. Thus, F is well-defined.

Claim 2

F is a finitely supported function.

We prove that F is finitely supported by $supp(f) \cup supp(g)$. Let us consider $\pi \in Fix(supp(f) \cup supp(g))$. Since $\pi \in Fix(supp(f))$ and supp(f) supports f, according to Proposition 6 we have that $f(\pi \cdot x)=\pi \diamond f(x)$ for all $x \in B$. Thus, for every finitely supported subset X of B we have $f(\pi \star X)=\{f(\pi \cdot x)\;|\;x \in X\}=\{\pi \diamond f(x)\;|\;x \in X\}=\pi {\widetilde{\star }} f(X)$, where $\star$ is the $S_{A}$-action on $\wp _{fs}(B)$ and ${\widetilde{\star }}$ is the $S_{A}$-action on $\wp _{fs}(C)$. Similarly, $g(\pi {\widetilde{\star }} Y)=\pi \star g(Y)$ for any finitely supported subset Y of C. Therefore, $F(\pi \star X)=B-g(C-f(\pi \star X))=B-g(C-\pi {\widetilde{\star }} f(X)) \overset{\pi {\widetilde{\star }}C=C}{=}B-g(\pi {\widetilde{\star }}(C-f(X)))=B-(\pi \star g(C-f(X))) \overset{\pi \star B=B}{=} \pi \star (B- g(C-f(X)))=\pi \star F(X)$. From Proposition 6 it follows that F is finitely supported. Moreover, because supp(F) is the least set of atoms supporting F, we have $supp(F) \subseteq supp(f) \cup supp(g)$.

Claim 3

For any $X,Y \in \wp _{fs}(B)$ with $X \subseteq Y$, we have $F(X) \subseteq F(Y)$. This remark follows by direct calculation.

Claim 4

The set $S:=\{X\;|\; X \in \wp _{fs}(B), X \subseteq F(X)\}$ is a non-empty finitely supported subset of $\wp _{fs}(B)$. 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$ (see Proposition 3) we have $\pi \star X \subseteq \pi \star F(X)$. According to Proposition 6, 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)$.

Claim 5

$T:=\cup _{{X \in S}} X$ is finitely supported by supp(S).

Let $\pi \in Fix(supp(S))$, and $t \in T$. Since $T=\cup _{{X \in S}} X$, we have that there exists $Z \in S$ such that $t \in Z$. Therefore, $\pi \cdot t \in \pi \star Z$. However, since $\pi$ fixes supp(S) pointwise and supp(S) supports S, we have that $\pi \star Z \in S$. Thus, there exists $Y \in S$ such that $\pi \star Z=Y$. Therefore $\pi \cdot t \in Y$, and so $\pi \cdot t \in \cup _{{X \in S}} X$. It follows that $\cup _{{X \in S}} X$ is finitely supported, and so $T=\cup _{{X \in S}} X \in \wp _{fs}(B)$. Furthermore, $supp(T) \subseteq supp(S)$.

Claim 6

We prove that $F(T)=T$.

Let $X \in S$ arbitrary. We have $X \subseteq F(X) \subseteq F(T)$. By taking the supremum on S, this leads to $T \subseteq F(T)$. However, because $T \subseteq F(T)$, from Claim 3 we also have $F(T) \subseteq F(F(T))$. Furthermore, F(T) is supported by $supp(F) \cup supp(T)$ (i.e. by $supp(f) \cup supp(g)$), and so $F(T) \in S$. According to the definition of T, we get $F(T) \subseteq T$.

We get $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. Let us define $h:B \rightarrow C$ by

$$\begin{aligned} 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. \end{aligned}$$

Claim 7

We claim that h is supported by the set $supp(f) \cup supp(g) \cup supp(T)$ (more exactly, by $supp(f) \cup supp(g)$, according to previous claims). 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 6 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$. Otherwise, we would obtain the contradiction $x=\pi ^{-1} \cdot (\pi \cdot x) \in T$ because $\pi ^{-1}$ also fixes supp(T) pointwise. Thus, because g is finitely supported, according to Proposition 6 we have $h(\pi \cdot x)=g^{-1}(\pi \cdot x)=\{y \in C\;|\; g(y)$=$\pi \cdot x\}=\{y \in C\;|\; \pi ^{-1} \cdot g(y)$=$x\}=\{y\in C\;|\; g(\pi ^{-1} \diamond y)$= $x\}\overset{\pi ^{-1} \diamond y:= z}{=}\{\pi \diamond z \in C\;|\; g(z)$=$x\}=\pi \diamond \{ z \in C\;|\; g(z)$=$x\}=\pi \diamond g^{-1}(x)=\pi \diamond h(x)$. We obtained $h(\pi \cdot x)=\pi \diamond h(x)$ for all $\pi \in Fix(supp(f) \cup supp(g) \cup supp(T))$ and all $x \in B$. According to Proposition 6, we get that h is finitely supported. Furthermore, we also have that $supp(h) \subseteq supp(f) \cup supp(g) \cup supp(T) \overset{Claim\; 5}{\subseteq } supp(f) \cup supp(g) \cup supp(S)$ $\overset{Claim \; 4}{\subseteq } supp(f) \cup supp(g) \cup supp(F) \overset{Claim \; 2}{\subseteq } supp(f)$ $\cup supp(g)$.

Claim 8

h is a bijective function.

First we prove that h is injective. Let us suppose that $h(x)=h(y)$. We claim that either $x,y \in T$ or $x,y \in B-T$. Indeed, let us suppose that $x\in T$ and $y \notin T$ (the case $x \notin T$, $y \in T$ is similar). We have $h(x)=f(x)$ and $h(y)=g^{-1}(y)$. If we denote $g^{-1}(y)=z$, we have $g(z)=y$. However, we supposed that $y \in B-T$, and so there exists $u \in C-f(T)$ such that $y=g(u)$. Since $y=g(z)$, from the injectivity of g we get $u=z$. This is a contradiction because $u \notin f(T)$, while $z=f(x) \in f(T)$. Since we proved that both x, y are contained either in T or in $B-T$, the injectivity of h follows from the injectivity of f or g, respectively.

Now we prove that h is surjective. Let $y \in C$ be arbitrarily chosen. If $y \in f(T)$, then there exists $z \in T$ such that $y=f(z)$, and so $y=h(z)$. If $y \in C-f(T)$, and because $g(C-f(T))=B-T$, there exists $x \in B-T$ such that $g(y)=x$. Thus, $y \in g^{-1}(x)$. Since g is injective, and so $g^{-1}(x)$ is a one-element set, we can say that $g^{-1}(x)=y$ with $x \in B-T$. Thus we have $y=h(x)$.

Lemma 2

Let $(B, \cdot )$ and $(C, \diamond )$ be two invariant sets (in particular, B and C could coincide), $B_{1}$ a finitely supported subset of B and $C_{1}$ a finitely supported subset of C. If there exist a finitely supported injective mapping $f: B_{1} \rightarrow C_{1}$ and a finitely supported injective mapping $g: C_{1} \rightarrow B_{1}$, then there exists a finitely supported bijective mapping $h:B_{1} \rightarrow C_{1}$. Furthermore, $supp(h) \subseteq supp(f) \cup supp(g) \cup supp(B_{1}) \cup supp(C_{1})$.

Proof of Lemma 2

We follow the proof of Lemma 1. We define $F:\wp _{fs'}(B_{1}) \rightarrow \wp _{fs'}(B_{1})$ by $F(X)=B_{1}-g(C_{1}-f(X))$ for all $X \in \wp _{fs'}(B_{1})$, where $\wp _{fs'}(B_{1})$ is a finitely supported subset of the invariant set $\wp _{fs}(B)$ (supported by $supp(B_{1})$) defined by $\wp _{fs'}(B_{1})=\{X \in \wp _{fs}(B)\;|\;X \subseteq B_{1}\}$. As in the previous lemma, but using Proposition 6, we get that F is well-defined, i.e. for every $X \in \wp _{fs'}(B_{1})$ we have that F(X) is supported by $supp(f) \cup supp(g) \cup supp(B_{1}) \cup supp(C_{1}) \cup supp(X)$ which means $F(X) \in \wp _{fs'}(B_{1})$. Moreover, F is itself finitely supported (in the sense of Definition 3) by $supp(f) \cup supp(g) \cup supp(B_{1}) \cup supp(C_{1})$. The set $S:=\{X\;|\; X \in \wp _{fs'}(B_{1}), \ X \subseteq F(X)\}$ is contained in $\wp _{fs'}(B_{1})$ and it is supported by supp(F) as a subset of $\wp _{fs}(B)$. The set $T:=\cup _{{X \in S}} X \in \wp _{fs'}(B_{1})$ is finitely supported by supp(S), and it is a fixed point of F.

As in the proof of Lemma 1, we define the bijection $h:B_{1} \rightarrow C_{1}$ by

$$\begin{aligned} h(x)=\left\{ \begin{array}{ll} f(x), &{} \text {for}\, x \in T;\\ g^{-1}(x), &{} \text {for}\, x \in B_{1}-T.\end{array}\right. \end{aligned}$$

According to Proposition 6, we obtain that h is finitely supported by $supp(f) \cup supp(g) \cup supp(B_{1}) \cup supp(C_{1}) \cup supp(T)$, and $supp(h) \subseteq supp(f) \cup supp(g) \cup supp(B_{1}) \cup supp(C_{1})$. Thus, h is the required finitely supported bijection between $B_{1}$ and $C_{1}$.

The anti-symmetry of $\le$ follows from Lemmas 1 and 2 because FSM sets are actually finitely supported subsets of invariant sets.

• $\le ^{*}$ is not anti-symmetric.

Lemma 3

There are two invariant sets B and C such that there exist both a finitely supported surjective mapping $f: C \rightarrow B$ and a finitely supported surjective mapping $g: B \rightarrow C$, but it does not exist a finitely supported bijective mapping $h:B \rightarrow C$.

Proof of Lemma 3

We consider C to be family $T_{fin}(A)=\{(x_{1}, \ldots , x_{m}) \subseteq (A \times \ldots \times A)\,|\,m \ge 0\}$ of all finite injective tuples from A (including the empty tuple denoted by ${\bar{\emptyset }}$) 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}$. We consider B to be $T^{*}_{fin}(A)=T_{fin}(A){\setminus } {\bar{\emptyset }}$ which is an equivariant subset of $T_{fin}(A)$, being itself an invariant set. The result follows from Theorem 3(11) of [3].

• $\le$ and $\le ^{\star }$ are not total. We have that whenever X is an infinite ordinary (non-atomic) ZF-set, 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. This result is presented as Theorem 1(1) and proved in [3]. As a direct consequence there are no finitely supported injective mappings and no finitely supported surjective mappings between A and X.

$\square$

Corollary 2

There exist two invariant sets B and C such that there is a finitely supported bijection between $\wp _{fs}(B)$ and $\wp _{fs}(C)$, but there is no finitely supported bijection between B and C.

Proof

Firstly we prove the following lemma.

Lemma 4

Let X and Y be two FSM sets and $f:X \rightarrow Y$ a finitely supported surjective function. Then the mapping $g:\wp _{fs}(Y) \rightarrow \wp _{fs}(X)$ defined by $g(V)=f^{-1}(V)$ for all $V \in \wp _{fs}(Y)$ is well-defined, injective and finitely supported by $supp(f) \cup supp(X) \cup supp(Y)$.

Proof of Lemma 4

We slightly generalize the proof of Lemma 2 from [3]. 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) \cup supp(X) \cup supp(Y)$. Let $\pi \in Fix(supp(f) \cup supp(V) \cup supp(X) \cup supp(Y))$, and $x \in f^{-1}(V)$, meaning $f(x) \in V$. According to Proposition 6, 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) \cup supp(X) \cup supp(Y)$. Let $\pi \in Fix(supp(f) \cup supp(X) \cup supp(Y))$. For any arbitrary $V \in \wp _{fs}(Y)$ we get $\pi \star V \in \wp _{fs}(Y)$ and $\pi \star g(V) \in \wp _{fs}(X)$, and by Proposition 6 we have that $\pi ^{-1} \in Fix(supp(f))$, and so $f(\pi ^{-1} \cdot x)=\pi ^{-1} \cdot f(x)$ for all $x\in X$. 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. Moreover, because f is surjective, a simple calculation shows us that g is injective. Indeed, let us suppose that $g(U)=g(V)$ for some $U,V \in \wp _{fs}(Y)$. We have $f^{-1}(U) = f^{-1}(V)$, and so $f(f^{-1}(U)) = f(f^{-1}(V))$. Since f is surjective, we get $U = f(f^{-1}(U))$=$f(f^{-1}(V)) = V$.

We start now the proof of the Corollary. As in Lemma 3, we consider the sets $B=T_{fin}(A){\setminus } {\bar{\emptyset }}$ and $C=T_{fin}(A)$. According to Lemma 3 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 4, 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 1, there is a finitely supported bijection between $\wp _{fs}(B)$ and $\wp _{fs}(C)$. However, we proved in Lemma 3 that there is no finitely supported bijection between $B=T_{fin}(A){\setminus } {\bar{\emptyset }}$ and $C=T_{fin}(A)$. $\square$

The following result communicated by Levy in 1965 for non-atomic ZF sets can be reformulated in the world of finitely supported atomic structures.

Corollary 3

Let X and Y be two invariant sets with the property that whenever $|2^{X}_{fs}|=|2^{Y}_{fs}|$ we have $|X|=|Y|$. If $|X|\le ^{\star }|Y|$ and $|Y|\le ^{\star }|X|$, then $|X|=|Y|$.

Proof

According to the hypothesis and to Lemma 4 there exist two finitely supported injective functions $f:\wp _{fs}(Y) \rightarrow \wp _{fs}(X)$ and $g:\wp _{fs}(X) \rightarrow \wp _{fs}(Y)$. According to Lemma 1, there is a bijective mapping $h:\wp _{fs}(X) \rightarrow \wp _{fs}(Y)$ . According to Theorem 3, we get $|2^{X}_{fs}|=|2^{Y}_{fs}|$, and so we get $|X|=|Y|$. $\square$

Proposition 7

(Cantor) Let X be a finitely supported subset of an invariant set $(Y, \cdot )$. Then $|X| \lneq |\wp _{fs}(X)|$ and $|X| \lneq ^{*} |\wp _{fs}(X)|$

Proof

First we prove that there is no finitely supported bijection between X and $\wp _{fs}(X)$, and so their cardinalities cannot be equal. Assume, by contradiction, that there is a finitely supported surjective mapping $f: X \rightarrow \wp _{fs}(X)$. Let us consider $Z=\{x \in X\,|\,x \notin f(x)\}$. We claim that $supp(X) \cup supp(f)$ supports Z. Let $\pi \in Fix(supp(X) \cup supp(f))$. Let $x \in Z$. Then $\pi \cdot x \in X$ and $\pi \cdot x \notin \pi \star f(x)=f(\pi \cdot x)$. Thus, $\pi \cdot x \in Z$, and so $Z \in \wp _{fs}(X)$. Therefore, since f is surjective there is $x_{0} \in X$ such that $f(x_{0})=Z$. However, from the definition of Z we have $x_{0} \in Z$ if and only if $x_{0}\notin f(x_{0})=Z$, which is a contradiction. Now, it is clear that the mapping $i: X \rightarrow \wp _{fs}(X)$ defined by $i(x)=\{x\}$ is injective and supported by supp(X). Thus, $|X| \lneq |\wp _{fs}(X)|$. Let us fix an atom $y \in X$. We define $s:\wp _{fs}(X) \rightarrow X$ by

$$\begin{aligned} s(U)=\left\{ \begin{array}{ll} u, &{} \text {if}\, U \text { is a one-element set \{u\} };\\ y, &{} \text {if}\, U \text { has more than one element}\, .\end{array}\right. \end{aligned}$$

Clearly, s is surjective. We claim that s is supported by $supp(y) \cup supp(X)$. Let $\pi \in Fix(supp(y) \cup supp(X))$. Thus, $y=\pi \cdot y$. If U is of form $U=\{u\}$, we obviously have $s(\pi \star U)=s(\{\pi \cdot u\})=\pi \cdot u=\pi \cdot s(U)$. If U has more than one element, then $\pi \star U$ has more than one element, and we have $s(\pi \star U)=y=\pi \cdot y=\pi \cdot s(U)$. Thus, $\pi \star U \in \wp _{fs}(X)$, $\pi \cdot s(U) \in X$, and $s(\pi \star U)=\pi \cdot s(U)$ for all $U \in \wp _{fs}(X)$ . According to Proposition 6, we have that s is finitely supported. Therefore, $|X| \lneq ^{*} |\wp _{fs}(X)|$. $\square$

Proposition 7 used a technique for constructing a surjection starting from an injection (defined in the opposite way); this technique can be generalized.

Proposition 8

Let X and Y be finitely supported subsets of invariant sets. If $|X| \le |Y|$, then $|X| \le ^{\star } |Y|$. The converse is not valid. However, if $|X| \le ^{\star } |Y|$, then $|X| \le |\wp _{fs}(Y)|$.

Proof

We generically denote the (possibly different) actions of the invariant sets containing X, Y by $\cdot$, and the actions of powersets by $\star$. Suppose there exists a finitely supported injective mapping $f: X \rightarrow Y$. We consider the case $Y \ne \emptyset$ (otherwise, the result follows trivially). Fix $x_{0} \in X$, and define the mapping $f':Y \rightarrow X$ by

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

Since f is injective, it follows that $f^{-1}(y)$ is a one-element set for each $y \in Im(f)$, and so $f'$ is a function. Clearly, $f'$ is surjective. We claim that $f'$ is supported by the set $supp(f) \cup supp(x_{0}) \cup supp(X) \cup supp(Y)$. Indeed, let us consider $\pi \in Fix(supp(f) \cup supp(x_{0}) \cup supp(X) \cup supp(Y))$. Whenever $y \in Im(f)$ we have $y=f(z)$ for some $z \in X$ and $\pi \cdot y=\pi \cdot f(z)=f(\pi \cdot z) \in Im(f)$, which means Im(f) is finitely supported by supp(f). Consider an arbitrary $y_{0} \in Im(f)$, and thus $\pi \cdot y_{0} \in Im(f)$. Then $f'(y_{0})= f^{-1}(y_{0})=z_{0}$ with $f(z_{0})=y_{0}$, and so $f(\pi \cdot z_{0})= \pi \cdot f(z_{0})=\pi \cdot y_{0}$, which means $f'(\pi \cdot y_{0})=f^{-1}(\pi \cdot y_{0})=\pi \cdot z_{0}=\pi \cdot f^{-1}(y_{0})=\pi \cdot f'(y_{0})$. Now, for $y \notin Im(f)$ we have $\pi \cdot y \notin Im(f)$, which means $f'(\pi \cdot y)=x_{0}=\pi \cdot x_{0}=\pi \cdot f(y)$ since $\pi$ fixes $x_{0}$ pointwise. Thus, $|X| \le ^{\star } |Y|$. Conversely, from the proof of Lemma 3 (which is related to the proof of Theorem 3(11) in [3]), we know that there is a finitely supported surjection $g:T_{fin}(A){\setminus } {\bar{\emptyset }} \rightarrow T_{fin}(A)$, but there does not exist a finitely supported injection $h: T_{fin}(A) \rightarrow T_{fin}(A){\setminus } {\bar{\emptyset }}$.

Assume now there is a finitely supported surjective mapping $f:Y \rightarrow X$. We proceed similarly as in the proof of Lemma 4. Fix $x \in X$. Then $f^{-1}(\{x\})$ is supported by $supp(f) \cup supp(x) \cup supp(X)$. Indeed, let $\pi \in Fix(supp(f) \cup supp(x) \cup supp(X))$, and $y \in f^{-1}(\{x\})$. This means $f(y)=x$. According to Proposition 6, we have $f(\pi \cdot y)= \pi \cdot f(y)= \pi \cdot x=x$, and so $\pi \cdot y \in f^{-1}(\{x\})$. Define $g:X \rightarrow \wp _{fs}(Y)$ by $g(x)=f^{-1}(\{x\})$. We claim that g is supported by $supp(f) \cup supp(X)$. Let $\pi \in Fix(supp(f) \cup supp(X))$. For any arbitrary $x \in X$, we have that $z \in g(\pi \cdot x) = f^{-1}(\{\pi \cdot x\}) \Leftrightarrow f(z)=\pi \cdot x \Leftrightarrow \pi ^{-1} \cdot f(z)=x \Leftrightarrow f(\pi ^{-1} \cdot z) =x \Leftrightarrow \pi ^{-1} \cdot z \in f^{-1}(\{x\}) \Leftrightarrow z \in \pi \star f^{-1}(\{x\})=\pi \star g(x)$. From Proposition 6 it follows that g is finitely supported. Since g is also injective, we get $|X| \le |\wp _{fs}(Y)|$. $\square$

As in the ZF case, we can define operations between FSM cardinalities.

Definition 7

Let X and Y be finitely supported subsets of invariant sets.

We define:

• 1. $|X|+|Y|=|X+Y|$, where $X+Y=\{(0,x)\,|\, x\in X\}\cup \{(1,y)\,|\, y\in Y\}$;

• 2. $|X|\cdot |Y|=|X \times Y|$, where $X \times Y=\{(x,y)\,|\,x \in X, y \in Y\}$;

• 3. $|Y|^{|X|}=|Y^{X}_{fs}|=|\{f:X \rightarrow Y\,|\,f\, \text {is finitely supported }\}|$.

We prove that the above definitions are correct (i.e. they do not depend on the chosen representatives for equivalence classes). Let us assume that there exist the finitely supported sets $X',Y'$ with $|X|=|X'|$ and $|Y|=|Y'|$. We generically denote the (possibly different) actions on the invariant sets containing $X,Y,X',Y'$ by $\cdot$, the actions on functions spaces by $\star$, the actions on Cartesian products by $\otimes$ and the actions on disjoint unions by $\diamond$.

• 1. There exist two finitely supported bijective mappings $f:X \rightarrow X'$ and $g:Y \rightarrow Y'$. Define $h:X+Y \rightarrow X'+Y'$ by $h((0,x))=(0,f(x))$ for all $x \in X$ and $h((1,y))=(1,g(y))$ for all $y \in Y$. Clearly, h is bijective. Let $\pi \in Fix(supp(f) \cup supp(g))$. According to Proposition 6 we have $h(\pi \diamond (0,x))=h((0, \pi \cdot x))=(0, f(\pi \cdot x))=(0, \pi \cdot f(x))=\pi \diamond (0,f(x))=\pi \diamond h((0,x))$ for all $x \in X$, and similarly, $h(\pi \diamond (1,y))=h((1, \pi \cdot y))=(1, g(\pi \cdot y))=(1, \pi \cdot g(y))=\pi \diamond h((1,y))$ for all $y \in Y$. According to Proposition 6, we get that h is supported by $supp(f) \cup supp(g)$, and so $|X+Y|=|X'+Y'|$.

• 2. There exist two finitely supported bijective mappings $f:X \rightarrow X'$ and $g:Y \rightarrow Y'$. Define $h:X \times Y \rightarrow X' \times Y'$ by $h(x,y)=(f(x),g(y))$ for all $x \in X$ and all $y \in Y$. Clearly, h is bijective. Let $\pi \in Fix(supp(f) \cup supp(g))$. According to Proposition 6, we have $h(\pi \otimes (x,y)) = h(\pi \cdot x, \pi \cdot y) =$ $(f(\pi \cdot x),g(\pi , \cdot y)) = (\pi \cdot f(x), \pi \cdot g(y)) = \pi \otimes (f(x),g(y))=\pi \otimes h(x,y)$ for all $x \in X$ and $y \in Y$. According to Proposition 6, we get that h is supported by $supp(f) \cup supp(g)$, and so $|X \times Y|=|X'\times Y'|$.

• 3. There exist two finitely supported bijective mappings $f:X \rightarrow X'$ and $g:Y \rightarrow Y'$. Define $\varphi : Y^{X}_{fs} \rightarrow Y'^{X'}_{fs}$ by $\varphi (h)=g \circ h \circ f^{-1}$ for any finitely supported mapping $h:X \rightarrow Y$. Clearly, $\varphi$ is bijective. Let $\pi \in Fix(supp(f) \cup supp(g))$ and h an arbitrary finitely supported mapping from X to Y. Fix an arbitrary $x' \in X'$. According to Proposition 6 and because $f^{-1}$ is also supported by supp(f), $\varphi (\pi \star h)(x') = (g \circ (\pi \star h) \circ f^{-1})(x') = g((\pi \star h)(f^{-1}(x'))) = g(\pi \cdot h(\pi ^{-1} \cdot f^{-1}(x'))) = g(\pi \cdot h(f^{-1}(\pi ^{-1} \cdot x'))) = \pi \cdot g(h(f^{-1}(\pi ^{-1} \cdot x')))= \pi \cdot \varphi (h) (\pi ^{-1} \cdot x')=(\pi \star \varphi (h))(x')$. Thus, $\varphi (\pi \star h) = \pi \star \varphi (h)$ for all $h \in Y^{X}_{fs}$, and so $\varphi$ is finitely supported according to Proposition 6, which means $|Y|^{|X|}=|Y'|^{|X'|}$.

Proposition 9

Let X, Y, Z be finitely supported subsets of invariant sets.

The following properties hold:

• 1. $|Z|^{|X| \cdot |Y|}=(|Z|^{|Y|})^{|X|}$;

• 2. $|Z|^{|X|+|Y|}=|Z|^{|X|} \cdot |Z|^{|Y|}$;

• 3. $(|X|\cdot |Y|)^{|Z|}=|X|^{|Z|}\cdot |Y|^{|Z|}$.

Proof

We generically denote the (possibly different) actions of the invariant sets containing X, Y, Z by $\cdot$, the actions on Cartesian products by $\otimes$, the actions of function spaces by $\star$, and the actions on disjoint unions by $\diamond$.

1. We prove that there is a bijection, finitely supported by $S=supp(X)\cup supp(Y) \cup supp(Z)$, between $Z^{X \times Y}_{fs}$ and $(Z^{Y}_{fs}) ^{X}_{fs}$. Let us define $\varphi : Z^{X \times Y}_{fs} \rightarrow (Z^{Y}_{fs}) ^{X}_{fs}$ in the following way. For each finitely supported mapping $f:X\times Y \rightarrow Z$ and each $x \in X$ we consider $\varphi (f):X \rightarrow Z^{Y}_{fs}$ to be the function defined by $(\varphi (f)(x))(y)=f(x,y)$ for all $y \in Y$. Let us prove that $\varphi$ is well-defined. For a fixed $x \in X$ we firstly prove that $\varphi (f)(x)$ is a finitely supported mapping from Y to Z. Indeed, according to Proposition 6 (since $\pi$ fixes supp(f) pointwise and supp(f) supports f), for $\pi \in Fix(supp(x) \cup supp(f) \cup S)$ we have $(\varphi (f)(x))(\pi \cdot y)=f(x, \pi \cdot y)=f(\pi \cdot x, \pi \cdot y)=f(\pi \otimes (x,y))=\pi \cdot f(x,y)=\pi \cdot (\varphi (f)(x))(y)$ for all $y \in Y$, and using again Proposition 6, we obtain that $\varphi (f)(x)$ is a finitely supported function. Now we prove that $\varphi (f):X \rightarrow Z^{Y}_{fs}$ is finitely supported by $supp(f) \cup S$. Let $\pi \in Fix(supp(f) \cup S)$. In the view of Proposition 6 we have to prove that $\varphi (f)(\pi \cdot x)=\pi \star \varphi (f)(x)$ for all $x \in X$. Fix $x \in X$ and consider an arbitrary $y \in Y$. We have $(\varphi (f)(\pi \cdot x))(y)=f(\pi \cdot x,y)$. According to Proposition 6, we also have $(\pi \star \varphi (f)(x))(y)=\pi \cdot (\varphi (f)(x))(\pi ^{1} \cdot y)=\pi \cdot f(x, \pi ^{-1}\cdot y)=f(\pi \otimes (x, \pi ^{-1} \cdot y))=f(\pi \cdot x,y)$. Thus, $\varphi (f):X \rightarrow Z^{Y}_{fs}$ is finitely supported. Now we claim that $\varphi$ is finitely supported by S. Let $\pi \in Fix(S)$. In the view of Proposition 6 we have to prove that $\varphi (\pi \star f)=\pi \star \varphi (f)$ for all $f:X\times Y \rightarrow Z$. Fix $f:X\times Y \rightarrow Z$. We have to prove that $\varphi (\pi \star f)(x)=(\pi \star \varphi (f))(x)$ for all $x \in X$. Fix some $x \in X$ and consider an arbitrary $y \in Y$. We have $(\varphi (\pi \star f)(x))(y)=(\pi \star f)(x,y)=\pi \cdot f(\pi ^{-1}\otimes (x,y))=\pi \cdot f(\pi ^{-1} \cdot x, \pi ^{-1} \cdot y)$. Furthermore, $((\pi \star \varphi (f))(x))(y)=(\pi \star \varphi (f)(\pi ^{-1}\cdot x))(y)=\pi \cdot (\varphi (f)(\pi ^{-1}\cdot x))(\pi ^{-1} \cdot y)=\pi \cdot f(\pi ^{-1} \cdot x, \pi ^{-1} \cdot y)$, and so our claim follows.

Similarly, define $\psi : (Z^{Y}_{fs}) ^{X}_{fs} \rightarrow Z^{X \times Y}_{fs}$ in the following way. For any finitely supported function $g:X \rightarrow Z^{Y}_{fs}$, define $\psi (g): X \times Y \rightarrow Z$ by $\psi (g)(x,y)=(g(x))(y)$ for all $x \in X$ and $y \in Y$. Firstly we prove that $\psi (g)$ is well-defined. Let $\pi \in Fix(supp(g))$. According to Proposition 6 we have $\psi (g)(\pi \otimes (x,y))=\psi (g)(\pi \cdot x, \pi \cdot y)=(g(\pi \cdot x))(\pi \cdot y)=(\pi \star g(x))(\pi \cdot y)=\pi \cdot (g(x))(\pi ^{-1} \cdot (\pi \cdot y))=\pi \cdot (g(x))(y)$ $=\pi \cdot \psi (x,y)$ for all $(x,y) \in X \times Y$. Thus, in the view of Proposition 6 we conclude that $\psi (g)$ is supported by supp(g). Now, let us prove that $\psi$ is finitely supported by S. We should prove that for $\pi \in Fix(S)$, $\psi (\pi \star g)=\pi \star \psi (g)$ for any finitely supported function $g:X\rightarrow Z^{Y}_{fs}$. Fix such a g and consider some arbitrary $x\in X$, $y \in Y$. We have $\psi (\pi \star g)(x,y)=((\pi \star g)(x))(y) =(\pi \star g(\pi ^{-1} \cdot x))(y)=\pi \cdot (g(\pi ^{-1} \cdot x))(\pi ^{-1} \cdot y)=\pi \cdot \psi (g)(\pi ^{-1} \cdot x, \pi ^{-1} \cdot y)= \pi \cdot \psi (g)(\pi ^{-1} \otimes (x, y))=(\pi \star \psi (g))(x,y)$.

It is routine to prove that $\psi \circ \varphi =1|_{Z^{X \times Y}_{fs}}$ and $\varphi \circ \psi =1|_{(Z^{Y}_{fs}) ^{X}_{fs}}$; thus, $\psi$ and $\varphi$ are bijective, the first being the inverse of the other.

2. We prove that there is a bijection, finitely supported by $S=supp(X)\cup supp(Y) \cup supp(Z)$, between $Z^{X + Y}_{fs}$ and $Z^{X}_{fs} \times Z^{Y}_{fs}$. We define $\varphi : Z^{X + Y}_{fs} \rightarrow Z^{X}_{fs} \times Z^{Y}_{fs}$ as follows. If $f:X+Y \rightarrow Z$ is a finitely supported mapping, then $\varphi (f)=(f_{1},f_{2})$ where $f_{1}:X \rightarrow Z$, $f_{1}(x)=f((0,x))$ for all $x \in X$, and $f_{2}:Y \rightarrow Z$, $f_{2}(y)=f((1,y))$ for all $y \in Y$. Clearly, $\varphi$ is well-defined since $f_{1}$ and $f_{2}$ are both supported by supp(f). Furthermore, $\varphi$ is bijective. It remains to prove that $\varphi$ is supported by S. Let $\pi \in Fix(S)$ and consider an arbitrary $f:X+Y \rightarrow Z$. We have $\varphi (\pi \star f)=(g_{1},g_{2})$ where $g_{1}(x)=(\pi \star f)((0,x))=\pi \cdot f(\pi ^{-1}\diamond (0,x))=\pi \cdot f((0,\pi ^{-1}\cdot x))=\pi \cdot f_{1}(\pi ^{-1} \cdot x)=(\pi \star f_{1})(x)$ for all $x \in X$, and similarly, $g_{2}(y)=(\pi \star f)((1,y))=\pi \cdot f(\pi ^{-1}\diamond (1,y))=\pi \cdot f((1,\pi ^{-1}\cdot y))=\pi \cdot f_{2}(\pi ^{-1} \cdot y)=(\pi \star f_{2})(y)$ for all $y \in Y$. Thus, $\varphi (\pi \star f)=(g_{1},g_{2})=(\pi \star f_{1}, \pi \star f_{2})=\pi \otimes (f_{1}, f_{2})=\pi \otimes \varphi (f)$. According to Proposition 6, we have that $\varphi$ is supported by S.

3. We prove that there is a bijection, finitely supported by $S=supp(X)\cup supp(Y) \cup supp(Z)$, between $(X \times Y)^{Z}_{fs}$ and $X^{Z}_{fs} \times Y^{Z}_{fs}$. We define $\varphi : X^{Z}_{fs} \times Y^{Z}_{fs} \rightarrow (X \times Y)^{Z}_{fs}$ by $\varphi (f_{1}, f_{2})(z)=(f_{1}(z),f_{2}(z))$ for all $f_{1} \in X^{Z}_{fs}$, all $f_{2} \in Y^{Z}_{fs}$ and all $z \in Z$. Fix some finitely supported mappings $f_{1}: Z \rightarrow X$ and $f_{2}: Z \rightarrow Y$. For $\pi \in Fix(supp(f_{1}) \cup supp(f_{2}))$, according to Proposition 6 we have $\varphi (f_{1}, f_{2})(\pi \cdot z)=(f_{1}(\pi \cdot z),f_{2}(\pi \cdot z))=(\pi \cdot f_{1}(z),\pi \cdot f_{2}(z))=\pi \otimes (f_{1}(z),f_{2}(z))=\pi \otimes \varphi (f_{1}, f_{2})(z)$ for all $z \in Z$. Thus, $\varphi (f_{1}, f_{2})$ is a finitely supported mapping, and so $\varphi$ is well-defined. Furthermore, $\varphi$ is bijective. Let us prove that $\varphi$ is finitely supported by S. Let $\pi \in Fix(S)$. Fix some arbitrary $f_{1} \in X^{Z}_{fs}$, $f_{2} \in Y^{Z}_{fs}$ and $z \in Z$. We have $\varphi (\pi \otimes (f_{1},f_{2}))(z)=\varphi (\pi \star f_{1}, \pi \star f_{2})(z)=((\pi \star f_{1})(z), (\pi \star f_{2})(z))=(\pi \cdot f_{1}(\pi ^{-1}\cdot z), \pi \cdot f_{2}(\pi ^{-1}\cdot z))=\pi \otimes (f_{1}(\pi ^{-1} \cdot z), f_{2}(\pi ^{-1}\cdot z))=\pi \otimes \varphi (f_{1},f_{2})(\pi ^{-1} \cdot z)=(\pi \star \varphi (f_{1},f_{2}))(z)$. According to Proposition 6, $\varphi$ is finitely supported. $\square$

Proposition 10

Let X, Y, Z be finitely supported subsets of invariant sets. The following properties hold:

• 1. If $|X| \le |Y|$, then $|X|+|Z| \le |Y|+|Z|$;

• 2. If $|X| \le |Y|$, then $|X| \cdot |Z| \le |Y| \cdot |Z|$;

• 3. If $|X| \le |Y|$, then $|X^{Z}_{fs}| \le |Y^{Z}_{fs}|$;

• 4. If $|X| \le |Y|$ and $Z\ne \emptyset$, then $|Z^{X}_{fs}| \le |Z^{Y}_{fs}|$;

• 5. $|X|+|Y| \le |X|\cdot |Y|$ whenever both X and Y have more than two elements.

Proof

We generically denote the (possibly different) actions of the invariant sets containing X, Y, Z by $\cdot$, the actions on function spaces by ${\widetilde{\star }}$, the actions on Cartesian products by $\otimes$ and the actions on disjoint unions by $\diamond$.

• 1. Suppose there exists a finitely supported injective mapping $f: X \rightarrow Y$. Define the injection $g: X+Z\rightarrow Y+Z$ by

  $$\begin{aligned} g(u)=\left\{ \begin{array}{ll} (0,f(x)), &{} \text {if}\, u=(0,x)\, \text {with}\, x \in X;\\ (1,z), &{} \text {if}\, u=(1,z)\, \text {with}\, z \in Z .\end{array}\right. \end{aligned}$$

  Since f is finitely supported we have that $f(\pi \cdot x)=\pi \cdot f(x)$ for all $x \in X$ and $\pi \in Fix(supp(f))$. Using Proposition 6, i.e verifying that $g(\pi \diamond u)=\pi \diamond g(u)$ for all $u \in X+Z$ and all $\pi \in Fix(supp(f) \cup supp(X) \cup supp(Y) \cup supp(Z))$, we have that g is also finitely supported.

• 2. Suppose there is a finitely supported injective mapping $f:X\rightarrow Y$. Define the injection $g: X\times Z\rightarrow Y \times Z$ by $g((x,z))=(f(x),z)$ for all $(x,z) \in X \times Z$. Clearly, g is injective. Since f is finitely supported we have that $f(\pi \cdot x)=\pi \cdot f(x)$ for all $x \in X$ and $\pi \in Fix(supp(f))$, and so $g(\pi \otimes (x,z))=g((\pi \cdot x, \pi \cdot z))=(f(\pi \cdot x),\pi \cdot z)=(\pi \cdot f(x),\pi \cdot z)=\pi \otimes g((x,z))$ for all $(x,z) \in X \times Z$ and $\pi \in Fix(supp(f) \cup supp(X) \cup supp(Y) \cup supp(Z))$, which means g is supported by $supp(f) \cup supp(X) \cup supp(Y) \cup supp(Z)$.

• 3. Suppose there exists a finitely supported injective mapping $f: X \rightarrow Y$. Define $g:X^{Z}_{fs} \rightarrow Y^{Z}_{fs}$ by $g(h)=f \circ h$. We have that g is injective and for any $\pi \in Fix(supp(f))$ we have $\pi {\widetilde{\star }} f=f$, and so $g(\pi {\widetilde{\star }} h)=f \circ (\pi {\widetilde{\star }} h)= (\pi {\widetilde{\star }} f) \circ (\pi {\widetilde{\star }} h)=\pi {\widetilde{\star }} (f \circ h)=\pi {\widetilde{\star }} g(h)$ for all $h \in X^{Z}_{fs}$. We used the relation $(\pi {\widetilde{\star }} f) \circ (\pi {\widetilde{\star }} h)=\pi {\widetilde{\star }} (f \circ h)$ for all $\pi \in S_{A}$. This can be proved as follows. Fix $x\in Z$, we have $(\pi {\widetilde{\star }}(f\circ h))(x)=\pi \cdot (f(h(\pi ^{-1}\cdot x)))$. Also, if we denote $(\pi {\widetilde{\star }} h)(x)=y$ we have $y=\pi \cdot (h(\pi ^{-1}\cdot x))$ and $((\pi {\widetilde{\star }} f)\circ (\pi {\widetilde{\star }} h))(x)=(\pi {\widetilde{\star }} f)(y)=\pi \cdot (f(\pi ^{-1}\cdot y))=\pi \cdot (f((\pi ^{-1}\circ \pi )\cdot h(\pi ^{-1}\cdot x)))=\pi \cdot (f(h(\pi ^{-1}\cdot x)))$. We finally obtain that g is supported by $supp(f) \cup supp(X) \cup supp(Y) \cup supp(Z)$.

• 4. Suppose there exists a finitely supported injective mapping $f: X \rightarrow Y$. According to Proposition 8, there is a finitely supported surjective mapping $f':Y \rightarrow X$. Define the injective mapping $g:Z^{X}_{fs} \rightarrow Z^{Y}_{fs}$ by $g(h)=h \circ f'$. As in item 3 one can prove that g is finitely supported by $supp(f') \cup supp(X) \cup supp(Y) \cup supp(Z)$.

• 5. Fix $x_{0}, x_{1} \in X$ with $x_{0} \ne x_{1}$ and $y_{0}, y_{1} \in Y$ with $y_{0}\ne y_{1}$. Define the injection $g: X+Y\rightarrow X \times Y$ by

  $$\begin{aligned} g(u)=\left\{ \begin{array}{ll} (x, y_{0}), &{} \text {if}\, u=(0,x)\, \text {with}\, x \in X, x \ne x_{0};\\ (x_{0},y), &{} \text {if}\, u=(1,y)\, \text {with}\, y \in Y;\\ (x_{1}, y_{1}), &{} \text {if}\, u=(0,x_{0}).\end{array}\right. \end{aligned}$$

  It follows easily that g is supported by $supp(x_{0}) \cup supp(y_{0}) \cup supp(x_{1}) \cup supp(y_{1}) \cup supp(X) \cup supp(Y)$, and g is injective. $\square$

Theorem 3

Let $(X, \cdot )$ be a finitely supported subset of an invariant set $(Z, \cdot )$. There exists a one-to-one mapping from $\wp _{fs}(X)$ onto $\{0,1\}^{X}_{fs}$ which is finitely supported by supp(X), where $\wp _{fs}(X)$ is considered the family of those finitely supported subsets of Z contained in X.

Proof

The theorem is proved in [2] as Theorem 4.7. $\square$

One can easy verify that the properties of $\le$ presented in Proposition 10 (1), (2) and (4) also hold for $\le ^{\star }$. We left the details to the reader.

Theorem 4

There exists an invariant set X having the following properties:

• 1. $|X \times X| \nleq ^{*} |\wp _{fs}(X)|$;

• 2. $|X \times X| \nleq |\wp _{fs}(X)|$;

• 3. $|X \times X| \nleq ^{*} |X|$;

• 4. $|X \times X| \nleq |X|$;

• 5. For each $n \in {\mathbb {N}}, n \ge 2$ we have $|X| \lneq |\wp _{n}(X)| \lneq |\wp _{fs}(X)|$, where $\wp _{n}(X)$ is the family of all n-sized subsets of X;

• 6. For each $n \in {\mathbb {N}}$ we have $|X| \lneq ^{*} |\wp _{n}(X)| \lneq ^{*} |\wp _{fs}(X)|$;

• 7. $|X| \lneq |\wp _{fin}(X)| \lneq |\wp _{fs}(X)|$;

• 8. $|X| \lneq ^{*} |\wp _{fin}(X)| \lneq ^{*} |\wp _{fs}(X)|$;

• 9. $|\wp _{fs}(X) \times \wp _{fs}(X)| \nleq ^{*} |\wp _{fs}(X)|$;

• 10. $|\wp _{fs}(X) \times \wp _{fs}(X)| \nleq |\wp _{fs}(X)|$;

• 11. $|X+X| \lneq ^{*} |X\times X|$;

• 12. $|X+X| \lneq |X\times X|$.

Proof

• 1. According to Theorem 3(1) in [3], there does not exist a finitely supported surjective mapping $f: \wp _{fs}(A) \rightarrow A \times A$. Thus, $|A \times A| \nleq ^{*} |\wp _{fs}(A)|$;

• 2. According to Theorem 3(2) in [3], there does not exist a finitely supported injective mapping $f: A \times A \rightarrow \wp _{fs}(A)$. Thus, $|A \times A| \nleq |\wp _{fs}(A)|$;

• 3. According to Theorem 3(9) in [3], there does not exist a finitely supported surjection $f: A \rightarrow A \times A$, and so $|A \times A| \nleq ^{*} |A|$;

• 4. According to Theorem 3(10) in [3], there does not exist a finitely supported injection $f: A \times A \rightarrow A$, which means $|A \times A| \nleq |A|$; Alternatively, one can prove that there does not exist a one-to-one mapping from $A \times A$ to A (and so neither a finitely supported one). Suppose, by contradiction, that there is a an injective mapping $i: A \times A \rightarrow A$. Let us fix two atoms x and y with $x\ne y$. The sets $\{i(a,x)\,|\,a \in A\}$ and $\{i(a,y)\,|\,a \in A\}$ are disjoint and infinite. Thus, $\{i(a,x)\,|\,a \in A\}$ is an infinite and coinfinite subset of A, which contradicts the fact that any subset of A is either finite or cofinite.

• 5. We proved in Theorem 3(7) of [3] that $|A| \lneq |\wp _{n}(A)| \lneq |\wp _{fs}(A)|$ for all $n \ge 2$.

• 6. Fix $n \in {\mathbb {N}}$. As in the above item there does not exist neither a finitely supported bijection between $\wp _{n}(A)$ and $\wp _{fs}(A)$, nor a finitely supported bijection between A and $\wp _{n}(A)$. However, there exists a finitely supported injection $i: A \rightarrow \wp _{n}(A)$. Fix an atom $a \in A$. The mapping $s: \wp _{n}(A) \rightarrow A$ defined by

  $$\begin{aligned} s(X)=\left\{ \begin{array}{ll} i^{-1}(X), &{} \text {if}\, {X\in Im(i) };\\ a, &{} \text {if}\, {X \notin Im(i)}\, \end{array}\right. \end{aligned}$$

  is supported by $supp(i) \cup \{a\}$ and is surjective. Now, fix n atoms $x_{1}, \ldots , x_{n}$. The mapping $g:\wp _{fs}(A) \rightarrow \wp _{n}(A)$ defined by

  $$\begin{aligned} g(X)=\left\{ \begin{array}{ll} X, &{} \text {if}\, {X\in \wp _{n}(A)};\\ \{x_{1}, \ldots x_{n}\}, &{} \text {if}\, {X \notin \wp _{n}(A)}\, \end{array}\right. \end{aligned}$$

  is supported by $\{x_{1}, \ldots x_{n}\}$ and is surjective.

• 7. According to Theorem 3(8) in [3] we have that $|A| \lneq |\wp _{fin}(A)| \lneq |\wp _{fs}(A)|$.

• 8. From the above item there does not exist neither a finitely supported bijection between $\wp _{fin}(A)$ and $\wp _{fs}(A)$, nor a finitely supported bijection between A and $\wp _{fin}(A)$. Fix an atom $a \in A$. The mapping $s: \wp _{fin}(A) \rightarrow A$ defined by

  $$\begin{aligned} s(X)=\left\{ \begin{array}{ll} x, &{} \text {if}\, X \text { is a one-element set } \{x\} ;\\ a, &{} \text {if}\, X \text { is not a one-element set}\, \end{array}\right. \end{aligned}$$

  is supported by $\{a\}$ and is surjective. Now, fix an atom b. The mapping $g:\wp _{fs}(A) \rightarrow \wp _{fin}(A)$ defined by

  $$\begin{aligned} g(X)=\left\{ \begin{array}{ll} X, &{} \text {if}\, {X\in \wp _{fin}(A) };\\ \{b\}, &{} \text {if}\, {X \notin \wp _{fin}(A)}\, \end{array}\right. \end{aligned}$$

  is supported by $\{b\}$ and is surjective.

• 9. According to Theorem 3(3) in [3], we get $|\wp _{fs}(A) \times \wp _{fs}(A)| \nleq ^{*} |\wp _{fs}(A)|$.

• 10. According to Theorem 3(4) in [3], we obtain $|\wp _{fs}(A) \times \wp _{fs}(A)| \nleq |\wp _{fs}(A)|$.

• 11. In the view of Proposition 10(5), there is a finitely supported injection from $A+A$ into $A \times A$, and a finitely supported surjection from $A \times A$ onto $A+A$ (Proposition 8). Thus, $|A+A|\le |A \times A|$ and $|A+A|\le ^{*}|A \times A|$. Fix three different atoms $a,b,c \in A$, and define the mapping $f:A+A \rightarrow \wp _{fs}(A)$ by

  $$\begin{aligned} f(u)=\left\{ \begin{array}{ll} \{x\}, &{} \text {if}\, u=(0,x)\, \text {with}\, x \in A;\\ \{a,y\}, &{} \text {if}\, u=(1,y)\, \text {with}\, y \in A, y \ne a;\\ \{b,c\}, &{} \text {if}\, u=(1,a).\end{array}\right. \end{aligned}$$

  One can directly prove that f is injective and supported by $\{a,b,c\}$. According to Proposition 8, we have $|A+A|\le ^{*}|\wp _{fs}(A)|$. If we had $|A \times A|=|A+A|$, we would obtain $|A\times A| \le ^{*} |\wp _{fs}(A)|$ which contradicts item 1.

• 12. According to the above item $|A+A|\le |\wp _{fs}(A)|$. If we had $|A \times A|=|A+A|$, we would obtain $|A\times A| \le |\wp _{fs}(A)|$ which contradicts item 2.

$\square$

Proposition 11

There exists an invariant set X having the properties:

• 1. $|X| \lneq |X|+|X|$;

• 2. $|X| \lneq ^{*} |X|+|X|$.

Proof

• 1. This item follows from Proposition 4.9 in [2].

  We can consider $X=\wp _{fin}(A)$ or $X=\wp _{cofin}(A)$.

• 2. It remains to prove that there is a finitely supported surjection from $\wp _{fs}(A)$ onto $\wp _{fin}(A)$. We either use Proposition 8 or we effectively construct the surjection as below. Fix $a \in A$. We define $g:\wp _{fs}(A) \rightarrow \wp _{fin}(A)$ by

  $$\begin{aligned}g(U)=\left\{ \begin{array}{ll} U, &{} \text {if}\, {U\in \wp _{fin}(A) };\\ \{a\}, &{} \text {if}\, {U \notin \wp _{fin}(A)}\, .\end{array}\right. \end{aligned}$$

  Clearly, g is supported by $\{a\}$ and is surjective.

  We can consider $X=\wp _{fin}(A)$ or $X=\wp _{cofin}(A)$. $\square$

4 Definitions of infinity for finitely supported structures

The notion of infinity appears at a variety of levels in computer science. Actually computers are able to work over discrete models, meaning that the ‘infinity’ can be at most approximated, but not effectively computed. The theory of finitely supported sets allows the computational study of structures which are very large, possibly infinite, but containing enough symmetries such that they can be concisely represented and manipulated. The equivalence of various definitions of infiniteness is provable in ZF under the consideration of the axiom of choice. Since in FSM the axiom of choice fails, our goal is to study various FSM forms of infinite and to provide several relations between them. We also present relevant examples of atomic sets that satisfy some forms of infinity, while do not satisfy other forms of infinity. In this way we prove the non-equivalence of various FSM definitions of infinity.

Definition 8

Let X be a finitely supported subset of an invariant set Y.

• 1. X is called FSM classical infinite if X does not correspond one-to-one and onto to a finite ordinal, i.e. if X cannot be represented as $\{x_{1}, \ldots , x_{n}\}$ for some $n \in {\mathbb {N}}$. We simply call an FSM classical infinite set as infinite, and an FSM non-classical infinite set as finite.

• 2. X is FSM covering infinite if there is a finitely supported directed family ${\mathcal {F}}$ of finitely supported subsets of Y with the property that X is contained in the union of the members of ${\mathcal {F}}$, but there does not exist $Z\in {\mathcal {F}}$ such that $X\subseteq Z$;

• 3. X is called FSM Tarski I infinite (TI i) if there exists a finitely supported one-to-one mapping of X onto $X \times X$, i.e. if $|X|=|X|^{2}$.

• 4. X is called FSM Tarski II infinite (TII i) if there exists a finitely supported family of finitely supported subsets of X, totally ordered by inclusion, having no maximal element.

• 5. X is called FSM Tarski III infinite (TIII i) if there exists a finitely supported one-to-one mapping of X onto $X+X$ (where $X+X$ is the disjoint union of X with X), i.e. if $|X|=2|X|$.

• 6. X is called FSM Mostowski infinite (M i) if there exists an infinite finitely supported totally ordered subset of X.

• 7. X is called FSM Dedekind infinite (D i) if there exists a finitely supported one-to-one mapping of X onto a finitely supported proper subset of X.

• 8. X is called FSM ascending infinite (Asc i) if there is a finitely supported increasing countable chain of finitely supported sets $X_{0}\subseteq X_{1}\subseteq \ldots \subseteq X_{n}\subseteq \ldots$ with $X\subseteq \cup X_{n}$, but there does not exist $n\in {\mathbb {N}}$ such that $X\subseteq X_{n}$;

Note that in the definition of FSM Tarski II infiniteness for a certain X, the existence of a finitely supported family of finitely supported subsets of X is required, while in the definition of FSM ascending infiniteness for X, the related family of finitely supported subsets of X has to be FSM countable (i.e. the mapping $n \mapsto X_{n}$ should be finitely supported, which means the family $(X_{n})_{n \in {\mathbb {N}}}$ is also uniformly supported). It is immediate that if X is FSM ascending infinite, then it is also FSM Tarski II infinite, while the reverse is not necessarily valid in the absence of axiom of choice over ZF sets (see Remark 3).

Theorem 5

Let X be a finitely supported subset of an invariant set Y.

• 1. X is FSM classical infinite if and only if X is FSM covering infinite.

• 2. X is FSM classical infinite if and only if there exists a non-empty finitely supported family of finitely supported subsets of X having no maximal element under inclusion.

Proof

1. Let us suppose that X is FSM classical infinite. Let ${\mathcal {F}}$ be the family of all FSM classical non-infinite (FSM classical finite) subsets of X ordered by inclusion. Since X is finitely supported, it follows that ${\mathcal {F}}$ is supported by supp(X). Moreover, since all the elements of ${\mathcal {F}}$ are finite sets, it follows that all the elements of ${\mathcal {F}}$ are finitely supported. Clearly, ${\mathcal {F}}$ is directed and X is the union of the members of ${\mathcal {F}}$. Suppose by contradiction, that X is not FSM covering infinite. Then there exists $Z\in {\mathcal {F}}$ such that $X\subseteq Z$. Thus, X should by FSM classical finite which is a contradiction with our original assumption.

Conversely, assume that X is FSM covering infinite. Suppose, by contradiction, that X is FSM classical finite, i.e. $X=\{x_{1}, \ldots , x_{n}\}$. Let ${\mathcal {F}}$ be an arbitrary directed family such that X is contained in the union of the members of ${\mathcal {F}}$ (at least one such a family exists, for example $\wp _{fs}(X)$). Then for each $i \in \{1, \ldots , n\}$ there exists $F_{i} \in {\mathcal {F}}$ such that $x_{i} \in F_{i}$. Since ${\mathcal {F}}$ is directed, there is $Z \in {\mathcal {F}}$ such that $F_{i} \subseteq Z$ for all $i \in \{1, \ldots , n\}$, and so $X \subseteq Z$ with $Z\in {\mathcal {F}}$, which is a contradiction.

2. Assume that X is FSM classical infinite. By contradiction, suppose that every non-empty finitely supported family of finitely supported subsets of X has a maximal element under inclusion. Particularly, $\wp _{fin}(X)$ is an equivariant family of finite (and so finitely supported) subsets of X, and so it should have a maximal element $Z \in \wp _{fin}(X)$. Assume $Z=\{z_{1},\ldots , z_{n}\}$. Since X is infinite, there is an element $z \in X$ different from all $z_{1}, \ldots , z_{n}$. However, in this case we have $\{z_{1},\ldots , z_{n},z\} \in \wp _{fin}(X)$ and $\{z_{1},\ldots , z_{n}\} \subsetneq \{z_{1},\ldots , z_{n}, z\}$ contradicting the maximality of Z.

Conversely, assume there exists a non-empty finitely supported family of finitely supported subsets of X having no a maximal element under inclusion. Suppose, by contradiction, that X is finite. Then X has only finitely many subsets, and all its subsets are finite. Let ${\mathcal {F}}$ be an arbitrary family of subsets of X. Then ${\mathcal {F}}$ is a finite family of finite sets, and so the elements of ${\mathcal {F}}$ of greatest cardinality are maximal elements of ${\mathcal {F}}$ with respect to inclusion, contradicting the assumption. $\square$

The notion of FSM Dedekind infiniteness was also introduced in Section 4.2 of [3] (or in [2], in a rather primary form). In this paper we extend the results obtained in [3] and in [2], providing new properties of FSM Dedekind infinite sets, and presenting much stronger examples of FSM sets that are not FSM Dedekind infinite, such as $T_{fin}(A)^{A}_{fs}$ and $\wp _{fs}(A)^{A}_{fs}$. The following theorem generalizes Theorem 2 from [3] that establishes Dedekind finiteness properties of basic atomic sets such as A, $\wp _{fs}(A)$, $\wp _{fin}(\wp _{fs}(A))$ and $S_{A}$.

Theorem 6

The following properties of FSM Dedekind infinite sets hold.

• 1. Let X be a finitely supported subset of an invariant set Y. Then X is FSM Dedekind infinite if and only if there is a finitely supported one-to-one mapping $f:{\mathbb {N}}\rightarrow X$. As a consequence, an FSM superset of an FSM Dedekind infinite set is FSM Dedekind infinite, and an FSM subset of an FSM set that is not Dedekind infinite is also not FSM Dedekind infinite.

• 2. Let X be an infinite finitely supported subset of an invariant set Y. Then the sets $\wp _{fs}(\wp _{fin}(X))$ and $\wp _{fs}(T_{fin}(X))$ are FSM Dedekind infinite.

• 3. Let X be an infinite finitely supported subset of an invariant set Y. Then the set $\wp _{fs}(\wp _{fs}(X))$ is FSM Dedekind infinite.

• 4. Let X be a finitely supported subset of an invariant set Y such that X does not contain an infinite uniformly supported subset Z. Then X is not FSM Dedekind infinite.

• 5. Let X be a finitely supported subset of an invariant set Y such that X does not contain an infinite uniformly supported subset. Then the set $\wp _{fin}(X)=\{Z\!\subseteq \! X\,|\, Z\, \text {finite}\}$ does not contain an infinite uniformly supported subset, and $\wp _{fin}(X)$ is not FSM Dedekind infinite.

• 6. Let X and Y be two finitely supported subsets of an invariant set Z. If neither X nor Y is FSM Dedekind infinite, then $X \times Y$ is not FSM Dedekind infinite.

• 7. Let X and Y be two finitely supported subsets of an invariant set Z. If neither X nor Y is FSM Dedekind infinite, then $X + Y$ is not FSM Dedekind infinite.

• 8. Let X be a finitely supported subset of an invariant set Y. Then $\wp _{fs}(X)$ is FSM Dedekind infinite if and only if X is FSM ascending infinite.

• 9. Let X be a finitely supported subset of an invariant set Y. If X is FSM Dedekind infinite, then X is FSM ascending infinite. The reverse implication is not valid.

Proof

• 1. We slightly generalize the proof of Lemma 1 from [3]. Let us suppose that $(X, \cdot )$ is FSM Dedekind infinite, and $g: X \rightarrow X$ is an injection supported by the finite set $S \subsetneq A$ with the property that $Im(g) \subsetneq X$. This means that there exists $supp(g) \subseteq S$ and there exists $x_{0}\in X$ such that $x_{0}\notin Im(g)$. We can form 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$. Furthermore, $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 6, $\pi \cdot x_{n+1}= \pi \cdot g(x_{n})=g(\pi \cdot x_{n})=g(x_{n})=x_{n+1}$. Since $supp(x_{n+1})$ is the least set supporting $x_{n+1}$, we obtain $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 $supp(g)\cup supp(x_{0})$, 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}) \cup supp(X)$ not depending on n). Indeed, for any $\pi \in Fix(supp(g)\cup supp(x_{0}) \cup supp(X))$ we have $f(\pi \diamond n)=f(n)=x_{n}=\pi \cdot x_{n}=\pi \cdot f(n)$ for all $n \in {\mathbb {N}}$, where by $\diamond$ we denoted the trivial $S_{A}$-action on ${\mathbb {N}}$. Furthermore, because $\pi$ fixes supp(X) pointwise we have $\pi \cdot f(n) \in X$ for all $n \in {\mathbb {N}}$. From Proposition 6 we have that f is finitely supported. Obviously, f is also injective.

  Conversely, suppose there exists a finitely supported injective mapping $f: {\mathbb {N}} \rightarrow X$. According to Proposition 6, it follows that for any $\pi \in Fix(supp(f))$ we have $\pi \cdot f(n)=f(\pi \diamond n)=f(n)$ and $\pi \cdot f(n) \in X$ for all $n \in {\mathbb {N}}$. We define $g:X \rightarrow X$ by

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

  We claim that g is supported by $supp(f) \cup supp(X)$. Indeed, let us consider $\pi \in Fix(supp(f) \cup supp(X))$ and $x \in X$. If there is some n such that $x=f(n)$, we have that $\pi \cdot x=\pi \cdot f(n)=f(n)$, and so $g(\pi \cdot x)=g(f(n))=f(n+1)=\pi \cdot f(n+1)=\pi \cdot g(x)$. If $x \notin Im(f)$, we prove by contradiction that $\pi \cdot x \notin Im(f)$. Indeed, suppose that $\pi \cdot x \in Im(f)$. Then there is $y \in {\mathbb {N}}$ such that $\pi \cdot x=f(y)$ or, equivalently, $x = \pi ^{-1} \cdot f(y)$. However, since $\pi \in Fix(supp(f))$, from Proposition 6 we have $\pi ^{-1} \cdot f(y)=f(\pi ^{-1} \diamond y)$, and so we get $x=f(\pi ^{-1} \diamond y)=f(y) \in Im(f)$ which contradicts the assumption that $x \notin Im(f)$. Thus, $\pi \cdot x \notin Im(f)$, and so $g(\pi \cdot x)=\pi \cdot x=\pi \cdot g(x)$. We obtained that $g(\pi \cdot x)=\pi \cdot x=\pi \cdot g(x)$ for all $x \in X$ and all $\pi \in Fix(supp(f) \cup supp(X))$. Moreover, $\pi \cdot g(x) \in \pi \star X=X$ (where by $\star$ we denoted the $S_{A}$-action on $\wp _{fs}(Y)$), and so g is finitely supported. Since f is injective, it follows immediately that g is injective. Furthermore, $Im(g)=X {\setminus } \{f(0)\}$ which is a proper subset of X, finitely supported by $supp(f(0)) \cup supp(X)=supp(f) \cup supp(X)$.

• 2. The family $\wp _{fin}(X)$ represents the family of those finite subsets of X (these subsets of X are finitely supported as subsets of the invariant set Y in the sense of Definition 2). Obviously, $\wp _{fin}(X)$ is a finitely supported subset of the invariant set $\wp _{fs}(Y)$, supported by supp(X). This is because whenever Z is an element of $\wp _{fin}(X)$ (i.e. whenever Z is a finite subset of X) and $\pi$ fixes supp(X) pointwise, we have that $\pi \star Z$ is also a finite subset of X. The family $\wp _{fs}(\wp _{fin}(X))$ represents the family of those subsets of $\wp _{fin}(X)$ which are finitely supported as subsets of the invariant set $\wp _{fs}(Y)$ in the sense of Definition 2. As above, according to Proposition 2, we have that $\wp _{fs}(\wp _{fin}(X))$ is a finitely supported subset of the invariant set $\wp _{fs}(\wp _{fs}(Y))$, supported by $supp(\wp _{fin}(X)) \subseteq supp(X)$.

  Let $X_{i}$ be the set of all i-sized subsets from X, i.e. $X_{i}=\{Z \subseteq X\,|\,|Z|=i\}$. Since X is infinite, it follows that each $X_{i}, i \ge 1$ is non-empty. Obviously, we have that any i-sized subset $\{x_{1}, \ldots , x_{i}\}$ of X is finitely supported (as a subset of Y) by $supp(x_{1}) \cup \ldots \cup supp(x_{i})$. Therefore, $X_{i} \subseteq \wp _{fin}(X)$ and $X_{i} \subseteq \wp _{fs}(Y)$ for all $i \in {\mathbb {N}}$. Since $\cdot$ is a group action, the image of an i-sized subset of X under an arbitrary permutation is an i-sized subset of Y. However, any permutation of atoms that fixes supp(X) pointwise also leaves X invariant, and so for any permutation $\pi \in Fix(supp(X))$ we have that $\pi \star Z$ is an i-sized subset of X whenever Z is an i-sized subset of X. Thus, each $X_{i}$ is a subset of $\wp _{fin}(X)$ finitely supported by supp(X), and so $X_{i} \in \wp _{fs}(\wp _{fin}(X))$. We define $f: {\mathbb {N}} \rightarrow \wp _{fs}(\wp _{fin}(X))$ by $f(n)=X_{n}$. We claim that supp(X) supports f. Indeed, let $\pi \in Fix(supp(X))$. Since supp(X) supports $X_{n}$ for all $n \in {\mathbb {N}}$, 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 $\pi \star f(n)=\pi \star X_{n}=X_{n} \in \wp _{fs}(\wp _{fin}(X))$ for all $n \in {\mathbb {N}}$. According to Proposition 6, we have that f is finitely supported. Furthermore, f is injective, and by item 1 we have that $\wp _{fs}(\wp _{fin}(X))$ is FSM Dedekind infinite. If we consider $Y_{i}$ the set of all i-sized injective tuples formed by elements of X, we have that each $Y_{i}$ is a subset of $T_{fin}(X)$ supported by supp(X), and the family $(Y_{i})_{i \in {\mathbb {N}}}$ is a countably infinite, uniformly supported, subset of $\wp _{fs}(T_{fin}(X))$. From item 1 we get that $\wp _{fs}(T_{fin}(X))$ is FSM Dedekind infinite.

• 3. The proof is the same as for the above item because every $X_{i} \in \wp _{fs}(\wp _{fs}(A))$.

• 4. If there does not exist a uniformly supported subset of X, then there does not exist a finitely supported injective mapping $f:{\mathbb {N}} \rightarrow X$, and so f cannot be FSM Dedekind infinite.

• 5. Suppose, by contradiction, that the set $\wp _{fin}(X)$ contains an infinite subset ${\mathcal {F}}$ such that all the elements of ${\mathcal {F}}$ are different and supported by the same finite set S. Therefore, we can express ${\mathcal {F}}$ as ${\mathcal {F}}=(X_{i})_{i \in I} \subseteq \wp _{fin}(X)$ with the properties that $X_{i} \ne X_{j}$ whenever $i \ne j$ and $supp(X_{i}) \subseteq S$ for all $i \in I$. Fix an arbitrary $j \in I$. However, from Proposition 4, because $supp(X_{j})=\underset{x \in X_{j}}{\cup }supp(x)$, then $X_{j}$ has the property that supp(x) $\subseteq S$ for all $x \in X_{j}$. Since j has been arbitrarily chosen from I, it follows that every element from every set of form $X_{i}$ is supported by S, and so $\underset{i}{\cup }X_{i}$ is an uniformly supported subset of X (all its elements being supported by S). Furthermore, $\underset{i \in I}{\cup }X_{i}$ is infinite because the family $(X_{i})_{i \in I}$ is infinite and $X_{i} \ne X_{j}$ whenever $i \ne j$. Otherwise, if $\underset{i}{\cup }X_{i}$ was finite, the family $(X_{i})_{i \in I}$ would be contained in the finite set $\wp (\underset{i}{\cup }X_{i})$, and so it couldn’t be infinite with the property that $X_{i} \ne X_{j}$ whenever $i \ne j$. We were able to construct an infinite uniformly supported subset of X, namely $\underset{i}{\cup }X_{i}$, and this contradicts the hypothesis that X does not contain an infinite uniformly supported subset.

  We proved that if X does not contain an infinite uniformly supported subset, then $\wp _{fin}(X)$ does not contain an infinite uniformly supported subset. Suppose, by contradiction, that $\wp _{fin}(X)$ is FSM Dedekind infinite. According to item 1, there exists a finitely supported injective mapping $f: {\mathbb {N}} \rightarrow \wp _{fin}(X)$. Thus, because ${\mathbb {N}}$ is a trivial invariant set, according to Proposition 6, there exists an infinite injective (countable) sequence $f({\mathbb {N}})=(X_{i})_{i \in {\mathbb {N}}} \subseteq \wp _{fin}(X)$ having the property $supp(X_{i}) \subseteq supp(f)$ for all $i \in {\mathbb {N}}$. We obtained that $\wp _{fin}(X)$ contains an infinite uniformly supported subset $(X_{i})_{i \in {\mathbb {N}}}$, which is a contradiction.

• 6. Suppose, by contradiction, that $X \times Y$ is FSM Dedekind infinite. According to item 1, there exists a finitely supported injective mapping $f: {\mathbb {N}} \rightarrow X \times Y$ Thus, according to Proposition 6, there exists an infinite injective sequence $f({\mathbb {N}})=((x_{i},y_{i}))_{i \in {\mathbb {N}}} \subseteq X \times Y$ with the property that $supp((x_{i}, y_{i})) \subseteq supp(f)$ for all $i \in {\mathbb {N}}$ (1). Fix some $j \in {\mathbb {N}}$. We claim that $supp((x_{j}, y_{j})) =supp(x_{j}) \cup supp(y_{j})$. Let $U=(x_{j}, y_{j})$, and $S=supp(x_{j})\cup supp(y_{j})$. Obviously, S supports U. Indeed, let us consider $\pi \in Fix(S)$. We have that $\pi \in Fix(supp(x_{j}))$ and also $\pi \in Fix(supp(y_{j}))$ Therefore, $\pi \cdot x_{j}=x_{j}$ and $\pi \cdot y_{j}=y_{j}$, and so $\pi \otimes (x_{j}, y_{j})=(\pi \cdot x_{j}, \pi \cdot y_{j})=(x_{j}, y_{j})$, where $\otimes$ represents the $S_{A}$ action on $X \times Y$ described in Proposition 3. Thus, $supp(U) \subseteq S$. It remains to prove that $S \subseteq supp(U)$. Fix $\pi \in Fix(supp(U))$. Since supp(U) supports U, we have $\pi \otimes (x_{j}, y_{j})=(x_{j}, y_{j})$, and so $(\pi \cdot x_{j}, \pi \cdot y_{j})=(x_{j}, y_{j})$, from which we get $\pi \cdot x_{j}=x_{j}$ and $\pi \cdot y_{j}= y_{j}$. Thus, $supp(x_{j}) \subseteq supp(U)$ and $supp(y_{j}) \subseteq supp(U)$. Hence $S=supp(x_{j})\cup supp(y_{j}) \subseteq supp(U)$. According to relation (1) we obtain, $supp(x_{i})\cup supp(y_{i}) \subseteq supp(f)$ for all $i \in {\mathbb {N}}$. Thus, $supp(x_{i}) \subseteq supp(f)$ for all $i \in {\mathbb {N}}$ and $supp(y_{i}) \subseteq supp(f)$ for all $i \in {\mathbb {N}}$ (2). Since the sequence $((x_{i},y_{i}))_{i \in {\mathbb {N}}}$ is infinite and injective, then at least one of the sequences $(x_{i})_{i \in {\mathbb {N}}}$ and $(y_{i})_{i \in {\mathbb {N}}}$ is infinite. Assume that $(x_{i})_{i \in {\mathbb {N}}}$ is infinite. Then there exists an infinite subset B of ${\mathbb {N}}$ such that $(x_{i})_{i \in B}$ is injective, and so there exists an injection $u: B \rightarrow X$ defined by $u(i)=x_{i}$ for all $i \in B$ which is supported by supp(f) (according to relation (2) and Proposition 6). However, since B is an infinite subset of ${\mathbb {N}}$, there exists a ZF bijection $h: {\mathbb {N}} \rightarrow B$. The construction of h requires only the fact that ${\mathbb {N}}$ is well-ordered which is obtained from the Peano construction of ${\mathbb {N}}$ and does not involve a form of the axiom of choice. Since both B and ${\mathbb {N}}$ are trivial invariant sets, it follows that h is equivariant. Thus, $u \circ h$ is an injection from ${\mathbb {N}}$ to X which is finitely supported by $supp(u) \subseteq supp(f)$. This contradicts the assumption that X is not FSM Dedekind infinite.

Remark 1

Similarly, using the relation $supp(x) \cup supp(y)=supp((x,y))$ for all $x \in X$ and $y \in Y$, it can be proved that $X \times Y$ does not contain an infinite uniformly supported subset if neither X nor Y contain an infinite uniformly supported subset.

• 7. Suppose, by contradiction, that $X + Y$ is FSM Dedekind infinite. According to item 1, there exists a finitely supported injective mapping $f: {\mathbb {N}} \rightarrow X + Y$. Thus, there exists an infinite injective sequence $(z_{i})_{i \in {\mathbb {N}}} \subseteq X+ Y$ such that $supp(z_{i}) \subseteq supp(f)$ for all $i \in {\mathbb {N}}$. According to the construction of the disjoint union of two $S_{A}$-sets (see Proposition 3), as in the proof of item 6, there should exist an infinite subsequence of $(z_{i})_{i}$ of form $((0, x_{j}))_{x_{j} \in X}$ which is uniformly supported by supp(f), or an infinite sequence of form $((1, y_{k}))_{y_{k} \in Y}$ which is uniformly supported by supp(f). Since 0 and 1 are constants, this means there should exist at least an infinite uniformly supported sequence of elements from X, or an infinite uniformly supported sequence of elements from Y. This contradicts the hypothesis neither X nor Y is FSM Dedekind infinite.

Remark 2

Similarly, it can be proved that $X + Y$ does not contain an infinite uniformly supported subset if neither X nor Y contain an infinite uniformly supported subset.

• 8. Let us suppose that $\wp _{fs}(X)$ is FSM Dedekind infinite. Assume that $(X_{n})_{n \in {\mathbb {N}}}$ is an infinite countable family of different subsets of X such that the mapping $n\mapsto X_{n}$ is finitely supported. Thus, each $X_{n}$ is supported by the same set $S=supp(n \mapsto X_{n})$. We define a countable family $(Y_{n})_{n \in {\mathbb {N}}}$ of subsets of X that are non-empty and pairwise disjoint. A ZF construction of such a family belongs to Kuratowski and can also be found in Lemma 4.11 from [6]. This approach works also in FSM in the view of the S-finite support principle because every $Y_{k}$ is defined only involving elements in the family $(X_{n})_{n \in {\mathbb {N}}}$, and so whenever $(X_{n})_{n \in {\mathbb {N}}}$ is uniformly supported (meaning that all $X_{n}$ are supported by the same set of atoms), we get that $(Y_{n})_{n \in {\mathbb {N}}}$ is uniformly supported. Formally the sequence $(Y_{n})_{n \in {\mathbb {N}}}$ is recursively constructed as below. For $n \in {\mathbb {N}}$, assume that $Y_{m}$ is defined for any $m<n$ such that the set $\{ X_{k} {\setminus } \underset{m<n}{\cup }Y_{m}\,|\,k \ge n\}$ is infinite. Define $n'=min\{k\,|\,k \ge n \,\text {and}\, X_{k} {\setminus } \underset{m<n}{\cup }Y_{m} \ne \emptyset \,\text {and}\, (X {\setminus } X_{k}) {\setminus } \underset{m<n}{\cup }Y_{m} \ne \emptyset \}$. Define

  $$\begin{aligned}Y_{n}=\left\{ \begin{array}{ll} X_{n'} {\setminus } \underset{m<n}{\cup }Y_{m}, &{} \text {if}\, \{X_{k}{\setminus } (X_{n'} \cup \underset{m<n}{\cup }Y_{m}) \,|\, k>n'\}\,\text {is infinite};\\ (X {\setminus } X_{n'}){\setminus } \underset{m<n}{\cup }Y_{m}, &{} \text {otherwise} .\end{array}\right. \end{aligned}$$

  Obviously, $Y_{1}$ is supported by $S \cup supp(X)$. By induction, assume that $Y_{m}$ is supported by $S \cup supp(X)$ for each $m<n$. Since $Y_{n}$ is defined as a set combination of $X_{i}$’s (which are all S-supported) and $Y_{m}$’s with $m<n$, we get that $Y_{n}$ is supported by $S \cup supp(X)$ according to the S-finite support principle. Therefore the family $(Y_{i})_{i \in {\mathbb {N}}}$ is uniformly supported by $S \cup supp(X)$. Let $U_{i}=Y_{0} \cup \ldots \cup Y_{i}$ for all $i \in {\mathbb {N}}$. Clearly, all $U_{i}$ are supported by $S \cup supp(X)$, and $U_{0} \subsetneq U_{1} \subsetneq U_{2} \subsetneq \ldots \subsetneq X$. Let $V_{n}=(X{\setminus }\underset{i\in {\mathbb {N}}}{\cup }U_{i})\cup U_{n}$. Clearly, $X=\underset{n\in {\mathbb {N}}}{\cup } V_{n}$. Moreover, $V_{n}$ is supported by $S \cup supp(X)$ for all $n \in {\mathbb {N}}$. Therefore, the mapping $n\mapsto V_{n}$ is finitely supported. Obviously, $V_{0} \subsetneq V_{1} \subsetneq V_{2} \subsetneq \ldots \subsetneq X$. However, there does not exist $n\in {\mathbb {N}}$ such that $X=V_{n}$, and so X is FSM ascending infinite.

  The converse holds since if X is FSM ascending infinite, there is a finitely supported increasing countable chain of finitely supported sets $X_{0}\subseteq X_{1}\subseteq \ldots \subseteq X_{n}\subseteq \ldots$ with $X\subseteq \cup X_{n}$, but there does not exist $n\in {\mathbb {N}}$ such that $X\subseteq X_{n}$. In this sequence there should exist infinitely many different elements of form $X_{i}$ (otherwise, their union is a term of the sequence), and the result follows from Proposition 21.

• 9. Suppose X is FSM Dedekind infinite. Therefore, $\wp _{fs}(X)$ is FSM Dedekind infinite. According to item 8, we have that X is FSM ascending infinite. The reverse implication is not valid because, as we prove in Proposition 16, $\wp _{fin}(A)$ is FSM ascending infinite while it is not FSM Dedekind infinite.

$\square$

Lemma 5

Let $S=\{s_{1},\ldots ,s_{n}\}$ be a finite subset of an invariant set $(U, \cdot )$ and X a finitely supported subset of an invariant set $(V, \diamond )$. Then if X does not contain an infinite uniformly supported subset, we have that $X^{S}_{fs}$ does not contain an infinite uniformly supported subset.

Proof

First we prove that there is an FSM injection g from $X^{S}_{fs}$ into $X^{|S|}$. For $f \in X^{S}_{fs}$ define $g(f)=(f(s_{1}),\ldots , f(s_{n}))$. Clearly, g is injective (and it is also surjective). Let $\pi \in Fix(supp(s_{1}) \cup \ldots \cup supp(s_{n}) \cup supp(X))$. Thus, $g(\pi {\widetilde{\star }} f)=(\pi \diamond f(\pi ^{-1} \cdot s_{1}),\ldots , \pi \diamond f(\pi ^{-1} \cdot s_{n}))=(\pi \diamond f( s_{1}),\ldots , \pi \diamond f(s_{n}))$ $=\pi \otimes g(f)$ for all $f \in X^{S}_{fs}$, where $\otimes$ is the $S_{A}$-action on $X^{|S|}$ defined as in Proposition 3. Hence g is finitely supported, and the conclusion follows from Theorem 6(1) and by repeatedly applying similar arguments as in Theorem 6(6) (if we slightly modify the proof of the theorem, using the fact that $supp(x) \cup supp(y)=supp((x,y))$ for all $x,y \in X$, we show that the |S|-time Cartesian product of X, i.e. $X^{|S|}$ does not contain an infinite uniformly supported subset; otherwise X should contain itself an infinite uniformly supported subset, which contradicts the hypothesis - see also Remark 1). $\square$

Lemma 6

Let $S=\{s_{1},\ldots ,s_{n}\}$ be a finite subset of an invariant set $(U, \cdot )$ and X a finitely supported subset of an invariant set $(V, \diamond )$. Then if X is not FSM Dedekind infinite, we have that $X^{S}_{fs}$ is not FSM Dedekind-infinite.

Proof

We proved that there is an FSM injection g from $X^{S}_{fs}$ into $X^{|S|}$. The conclusion follows from Theorem 6(1) and by repeatedly applying Theorem 6(6) (from which we know that the |S|-time Cartesian product of X, i.e. $X^{|S|}$, is not FSM Dedekind-infinite). $\square$

Theorem 7

Let X be a finitely supported subset of an invariant set $(Y, \cdot )$ such that X does not contain an infinite uniformly supported subset. The set $X^{A}_{fs}$ does not contain an infinite uniformly supported subset, and so it is not FSM Dedekind infinite.

Proof

Assume, by contradiction, that, for a certain finite set $S \subseteq A$, there exist infinitely many functions $f:A \rightarrow X$ that are supported by S. Each S-supported function $f:A \rightarrow X$ can be uniquely decomposed into two S-supported functions $f|_{S}$ and $f|_{A {\setminus } S}$ (this follows from Proposition 6 and because both S and $A {\setminus } S$ are supported by S). Since there exist only finitely many functions from S to X supported by S (see Lemma 5), there should exist an infinite family ${\mathcal {F}}$ of functions $g:(A{\setminus } S) \rightarrow X$ which are supported by S (the functions g are the restrictions of the functions f to $A {\setminus } S$). Let us fix an element $a\in A {\setminus } S$. Consider an arbitrary S-supported function $g:(A{\setminus } S) \rightarrow X$. For each $\pi \in Fix(S \cup \{a\})$, according to Proposition 6, we have $\pi \cdot g(a)=g(\pi (a))=g(a)$ which means that g(a) is supported by $S \cup \{a\}$. However, in X there are at most finitely many elements supported by $S \cup \{a\}$. Therefore, there is $n \in {\mathbb {N}}$ such that $h_{1}(a), \ldots , h_{n}(a)$ are distinct elements in X with $h_{1},\ldots , h_{n} \in {\mathcal {F}}$, and $h(a)\in \{h_{1}(a), \ldots , h_{n}(a)\}$ for all $h\in {\mathcal {F}}$. Fix some $h \in {\mathcal {F}}$ and an arbitrary $b \in A {\setminus } S$ (which means that the transposition $(a\,b)$ fixes S pointwise). We have that there is $i \in \{1,\ldots ,n\}$ such that $h(a)=h_{i}(a)$. Since $h,h_{i}$ are supported by S and $(a\,b) \in Fix(S)$, from Proposition 6 we have $h(b)=h((a\, b)(a))=(a\,b)\cdot h(a)=(a\,b) \cdot h_{i}(a)=h_{i}((a\,b)(a))=h_{i}(b)$, which finally leads to $h=h_{i}$ since b was arbitrarily chosen from their domain of definition. Thus, the family ${\mathcal {F}}=\{h_{1},\ldots , h_{n}\}$, which means ${\mathcal {F}}$ is finite, and so we get a contradiction. $\square$

Corollary 4

Let X be a finitely supported subset of an invariant set $(Y, \cdot )$ such that X does not contain an infinite uniformly supported subset. The set $X^{A^{n}}_{fs}$ does not contain an infinite uniformly supported subset, and so it is not FSM Dedekind infinite, whenever $n \in {\mathbb {N}}$.

Proof

We prove the result by induction on n. For $n=1$, the result follows from Theorem 7. Assume that $X^{A^{n-1}}_{fs}$ does not contain an infinite uniformly supported subset. According to Proposition 9, we have $|X^{A^{n}}_{fs}|=|X^{A^{n-1} \times A}_{fs}|=|X|^{|A^{n-1} \times A|}=|X|^{|A^{n-1}|\cdot |A|}=(|X|^{|A^{n-1}|})^{|A|}=|(X^{A^{n-1}}_{fs})^{A}_{fs}|$, which means that there is a finitely supported bijection between $X^{A^{n}}_{fs}$ and $(X^{A^{n-1}}_{fs})^{A}_{fs}$. However, by Theorem 7, $(X^{A^{n-1}}_{fs})^{A}_{fs}$ does not contain an infinite uniformly supported subset (since the set $Z=X^{A^{n-1}}_{fs}$ does not contain an infinite uniformly supported subset according to the inductive hypothesis). The result now follows. $\square$

Corollary 5

The set $\wp _{fs}(A^{n})$ (where $A^{n}$ is the n-times Cartesian product of A) does not contain an infinite uniformly supported subset, and so it is not FSM Dedekind infinite.

Proof

According to Theorem 3, we have $|\wp _{fs}(A^{n})|=|\{0,1\}^{A^{n}}_{fs}|$. The result follows from Corollary 4 since $\{0,1\}$ does not contain an infinite uniformly supported subset. $\square$

Corollary 6

Let X be a finitely supported subset of an invariant set $(Y, \cdot )$ such that $\wp _{fs}(X)$ does not contain an infinite uniformly supported subset. The set $(\wp _{fs}(A^{n}))^{X}_{fs}$ does not contain an infinite uniformly supported subset, and so it is not FSM Dedekind infinite.

Proof

According to Corollary 4, the set $(\wp _{fs}(X))^{A^{n}}_{fs}$ does not contain an infinite uniformly supported subset. However, according to Theorem 3 and Proposition 9, $|(\wp _{fs}(X))^{A^{n}}_{fs}|=|(\{0,1\}^{X}_{fs})^{A^{n}}_{fs}|=(|\{0,1\}|^{|X|})^{|A^{n}|}=|\{0,1\}|^{|X|\cdot |A^{n}|}=|\{0,1\}|^{|A^{n}|\cdot |X|}$ $=(|\{0,1\}|^{|A^{n}|})^{|X|}=|(\{0,1\}^{A^{n}}_{fs})^{X}_{fs}|=|(\wp _{fs}(A^{n}))^{X}_{fs}|$. Thus, there is a finitely supported bijection between $(\wp _{fs}(X))^{A^{n}}_{fs}$ and $(\wp _{fs}(A^{n}))^{X}_{fs}$, and the result follows. $\square$

The following corollary represents an extension of Theorem 2 in [3]: now we are able to prove that $T_{fin}(A)^{A}_{fs}$ and $\wp _{fs}(A)^{A}_{fs}$ are not FSM Dedekind infinite.

Corollary 7

The following sets and all of their FSM classical infinite subsets are FSM classical infinite, but they are not FSM Dedekind infinite.

• 1. The invariant set A of atoms.

• 2. The powerset $\wp _{fs}(A)$ of the set of atoms.

• 3. The set $T_{fin}(A)$ of all finite injective tuples of atoms.

• 4. The invariant set $A^{A}_{fs}$ of all finitely supported functions from A to A.

• 5. The invariant set of all finitely supported functions $f:A \rightarrow A^{n}$, $n\in {\mathbb {N}}$.

• 6. The invariant set of all finitely supported functions $f:A \rightarrow T_{fin}(A)$.

• 7. The invariant set of all finitely supported functions $f:A \rightarrow \wp _{fs}(A)$.

• 8. The sets $\wp _{fin}(A)$, $\wp _{cofin}(A)$, $\wp _{fin}(\wp _{fs}(A))$, $\wp _{fin}(\wp _{cofin}(A))$, $\wp _{fin}(\wp _{fin}(A))$, and $\wp _{fin}(A^{A}_{fs})$.

• 9. Any construction of finite powersets of the following forms $\wp _{fin}(\ldots \wp _{fin}(A))$, $\wp _{fin}(\ldots \wp _{fin}(P(A)))$, or $\wp _{fin}(\ldots \wp _{fin}(\wp _{fs}(A)))$.

• 10. Every finite Cartesian combination between the set A, $\wp _{fin}(A)$, $\wp _{cofin}(A)$, $\wp _{fs}(A)$ and $A^{A}_{fs}$.

• 11. The disjoint unions $A+A^{A}_{fs}$, $A+\wp _{fs}(A)$, $\wp _{fs}(A)+A^{A}_{fs}$ and $A+\wp _{fs}(A)+A^{A}_{fs}$ and all finite disjoint unions between A, $A^{A}_{fs}$ and $\wp _{fs}(A)$.

Proof

• 1. A does not contain an infinite uniformly supported subset, and so it is not FSM Dedekind infinite (according to Theorem 6(4)).

• 2. $\wp _{fs}(A)$ does not contain an infinite uniformly supported subset because for any finite set S of atoms there exist only finitely many elements of $\wp _{fs}(A)$ supported by S, namely the subsets of S and the supersets of $A{\setminus } S$. Thus, $\wp _{fs}(A)$ is not FSM Dedekind infinite (Theorem 6(4)).

• 3. $T_{fin}(A)$ does not contain an infinite uniformly supported subset because the finite injective tuples of atoms supported by a finite set S are only those injective tuples formed by elements of S, being at most $1+A_{|S|}^{1}+A_{|S|}^{2}+\ldots +A_{|S|}^{|S|}$ such tuples, where $A_{n}^{k}=n(n-1)\ldots (n-k+1)$.

  4–7. This items follow directly from Theorem 7.

• 8. The sets $\wp _{fin}(A)$, $\wp _{cofin}(A)$, $\wp _{fin}(\wp _{fs}(A))$, $\wp _{fin}(\wp _{cofin}(A))$, $\wp _{fin}(\wp _{fin}(A))$, and $\wp _{fin}(A^{A}_{fs})$ do not contain infinite uniformly supported subsets, and so they are not FSM Dedekind infinite (Theorem 6(5)).

• 9. Directly from Theorem 6(5).

• 10. According to Theorem 6(6).

• 11. According to Theorem 6(7). $\square$

Corollary 8

There exist two FSM sets that whose cardinalities incomparable via the relation $\le$ on cardinalities, and none of them is FSM Dedekind infinite.

Proof

According to Corollary 7, none of the sets $A \times A$ and $\wp _{fs}(A)$ is FSM Dedekind infinite. According to Theorem 4, there does not exist a finitely supported injective mapping $f: A \times A \rightarrow \wp _{fs}(A)$. According to Lemma 11.10 from [7] that is preserved in FSM (proof omitted) there does not exist a finitely supported injective mapping $f: \wp _{fs}(A) \rightarrow A \times A$. $\square$

Corollary 9

The following sets and all of their supersets, their powersets and the families of their finite subsets, are both FSM classical infinite and FSM Dedekind infinite.

• 1. The invariant sets $\wp _{fs}(\wp _{fs}(A))$, $\wp _{fs}(\wp _{fin}(A))$ and ${\mathbb {N}}$.

• 2. The set of all finitely supported mappings from X to Y, and the set of all finitely supported mappings from Y to X, where X is a finitely supported subset of an invariant set with at least two elements, and Y is an FSM Dedekind infinite set.

• 3. The set of all finitely supported functions $f:\wp _{fin}(Y) \rightarrow X$ and the set of all finitely supported functions $f:\wp _{fs}(Y) \rightarrow X$, where Y is an infinite finitely supported subset of an invariant set, and X is a finitely supported subset of an invariant set with at least two elements.

• 4. The set $T^{\delta }_{fin}(A)=\underset{n\in {\mathbb {N}}}{\cup }A^{n}$ of all finite tuples of atoms (not necessarily injective).

Proof

• 1. This follows from Theorems 6(3) and 6 (2).

• 2. Let $(y_{n})_{n \in {\mathbb {N}}}$ be an injective, uniformly supported, countable sequence in Y (it exists according to Theorem 6(1)). Thus, each $y_{n}$ is supported by the same set S of atoms. In $Y^{X}$ we consider the injective family $(f_{n})_{n \in {\mathbb {N}}}$ of functions from X to Y where for each $i \in {\mathbb {N}}$ we define $f_{i}(x)=y_{i}$ for all $x \in X$. According to Proposition 6, each $f_{i}$ is supported by S, and so is the infinite family $(f_{n})_{n \in {\mathbb {N}}}$, meaning that there is an S-supported injective mapping from ${\mathbb {N}}$ to $Y^{X}$. In this case it is necessary to require only that X is non-empty. Fix two different elements $x_{1}, x_{2} \in X$. Take ${\mathcal {F}}=(y_{n})_{n \in {\mathbb {N}}}$ an injective, uniformly supported (by T), countable sequence in Y. In $X^{Y}$ we consider the injective family $(g_{n})_{n \in {\mathbb {N}}}$ of functions from Y to X where for each $i \in {\mathbb {N}}$ we define

  $$\begin{aligned}g_{i}(y)=\left\{ \begin{array}{ll} x_{1} &{} \text {if}\, y=y_{i};\\ x_{2} &{} \text {if}\, y=y_{j} \; \text {with}\; j \ne i, \; \text {or}\; y\notin {\mathcal {F}}.\end{array} \right. \end{aligned}$$

  According to Proposition 6, each $g_{i}$ is supported by the finite set $supp(x_{1}) \cup supp(x_{2}) \cup T$, and so the infinite family $(g_{n})_{n \in {\mathbb {N}}}$ is uniformly supported, i.e. that there is an injective mapping from ${\mathbb {N}}$ to $X^{Y}$ supported by $supp(x_{1}) \cup supp(x_{2}) \cup T$.

• 3. From Theorem 3, there exists a one-to-one mapping from $\wp _{fs}(U)$ onto $\{0,1\}^{U}_{fs}$ for an arbitrary finitely supported subset of an invariant set U. Fix two distinct elements $x_{1},x_{2} \in X$. There exists a finitely supported (by $supp(x_{1}) \cup supp(x_{2})$) bijective mapping from $\{0,1\}^{U}_{fs}$ to $\{x_{1},x_{2}\}^{U}_{fs}$ which associates to each $f \in \{0,1\}^{U}_{fs}$ an element $g \in \{x_{1},x_{2}\}^{U}_{fs}$ defined by $g(x)=\left\{ \begin{array}{ll} x_{1} &{} \text {for}\, f(x)=0\\ x_{2} &{} \text {for}\, f(x)=1 \end{array}\right.$ for all $x \in U$ and supported by $supp(x_{1}) \cup supp(x_{2}) \cup supp(f)$. Obviously, there is a finitely supported injection between $\{x_{1},x_{2}\}^{U}_{fs}$ and $X^{U}_{fs}$. Thus, there is a finitely supported injection from $\wp _{fs}(U)$ into $X^{U}_{fs}$. If we take $U=\wp _{fin}(Y)$ or $U=\wp _{fs}(Y)$, the result follows from Theorem 6(1), Theorem 6(2) and Theorem 6(3).

• 4. Fix $a \in A$ and $i \in {\mathbb {N}}$. We consider the tuple $x_{i}=(a,\ldots ,a) \in A^{i}$. Clearly, $x_{i}$ is supported by $\{a\}$ for each $i \in {\mathbb {N}}$, and so $(x_{n})_{n \in {\mathbb {N}}}$ is a uniformly supported subset of $T^{\delta }_{fin}(A)$.

$\square$

By definition, if a set X is not FSM Dedekind infinite (which is equivalent with the non-existence of a finitely supported injection from ${\mathbb {N}}$ into X), then every finitely supported injection from X into X is also surjective. However, there may exist a finitely supported surjection from X onto X which is not injective. For example, let us consider $X=T_{fin}(A)$ which is not FSM Dedekind infinite. Similarly as in the proof of Theorem 3(11) from [3] we can define an equivariant surjective function $f:T_{fin}(A)\rightarrow T_{fin}(A)$ by

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

where $y'$ is a new tuple of atoms formed by deleting the first element in the tuple y. Clearly, g is not injective because every one-element tuple of atoms is mapped into the empty tuple. Despite of this, whenever $\wp _{fs}(X)$ is not FSM Dedekind infinite we are able to prove the equivalence between injectivity and surjectivity for finitely supported self-mappings of X. This follows from Proposition 12, and from the fact that whenever $\wp _{fs}(X)$ is not FSM Dedekind infinite we also have that X is not FSM Dedekind infinite, and so the finitely supported injective self-mappings of X should be surjective.

Proposition 12

Let X be a finitely supported subset of an invariant set. If $\wp _{fs}(X)$ is not FSM Dedekind infinite, then each finitely supported surjective mapping $f:X \rightarrow X$ should be injective. The converse does not hold.

Proof

Let $f: X \rightarrow X$ be a finitely supported surjection. Since f is surjective, we can define the function $g:\wp _{fs}(X) \rightarrow \wp _{fs}(X)$ by $g(Y) = f^{-1}(Y)$ for all $Y\in \wp _{fs}(X)$ which is finitely supported and injective according to Lemma 4. Since $\wp _{fs}(X)$ is not FSM Dedekind infinite, it follows that g is surjective. Now let us consider two elements $a,b \in X$ such that $f(a)=f(b)$. We prove by contradiction that $a=b$. Suppose that $a \ne b$, and consider Y=$\{a\}$ and Z=$\{b\}$. Obviously, $Y,Z \in \wp _{fs}(X)$. Since g is surjective, for Y and Z there exist $Y_{1}, Z_{1} \in \wp _{fs}(X)$ such that $f^{-1}(Y_{1})=g(Y_{1})=Y$ and $f^{-1}(Z_{1})=g(Z_{1})=Z$. We know that $f(Y) \cap f(Z)= \{f(a)\}$. Thus, $f(a) \in f(Y)=f(f^{-1}(Y_{1})) \subseteq Y_{1}$. Similarly, $f(a) =f(b) \in f(Z)=f(f^{-1}(Z_{1})) \subseteq Z_{1}$, and so $f(a) \in Y_{1} \cap Z_{1}$. Thus, $a \in f^{-1}(Y_{1} \cap Z_{1})=f^{-1}(Y_{1}) \cap f^{-1}(Z_{1})=Y \cap Z$. However, since we assumed that $a \ne b$, we have that $Y \cap Z = \emptyset$, which represents a contradiction. It follows that $a=b$, and so f is injective.

In order to prove the invalidity of the reverse implication, we prove that any finitely supported surjective mapping $f:\wp _{fin}(A) \rightarrow \wp _{fin}(A)$ is also injective, while $\wp _{fs}(\wp _{fin}(A))$ is FSM Dedekind infinite. Let consider a finitely supported surjection $f:\wp _{fin}(A)\rightarrow \wp _{fin}(A)$, and $X\in \wp _{fin}(A)$. Then $supp(X)=X$. By Proposition 6, for any $\pi \in Fix(supp(f) \cup supp(X))=Fix(supp(f) \cup X)$ we have $\pi \star f(X)=f(\pi \star X)=f(X)$ which means $supp(f) \cup X$ supports f(X), that is $f(X)=supp(f(X)) \subseteq supp(f) \cup X$ (1). If $X \subseteq supp(f)$, we get $f(X) \subseteq supp(f)$ (2).

For a fixed $m \ge 1$, let us fix m (arbitrarily chosen) atoms $b_{1}, \ldots , b_{m} \in A {\setminus } supp(f)$, and take $U=\{\{a_{1},\ldots , a_{n}, b_{1},\ldots , b_{m}\} \,|\, a_{1},\ldots , a_{n} \in supp(f) , n \ge 1\}$ $\cup$ $\{\{ b_{1},\ldots , b_{m}\}\}$. The set U is finite since supp(f) is finite and $b_{1}, \ldots , b_{m} \in A {\setminus } supp(f)$ are fixed. Let us consider $Y \in U$, that is, $Y {\setminus } supp(f)=\{b_{1},\ldots , b_{m}\}$. There exists $Z \in \wp _{fin}(A)$ such that $f(Z)=Y$. According to relations (1) and (2), Z should be of form $Z=\{c_{1},\ldots , c_{k}, b_{i_{1}},\ldots , b_{i_{l}}\}$ with $c_{1},\ldots , c_{k} \in supp(f)$ and $b_{i_{1}},\ldots , b_{i_{l}} \in A {\setminus } supp(f)$ or of form $Z=\{ b_{i_{1}},\ldots , b_{i_{l}}\}$ with $b_{i_{1}},\ldots , b_{i_{l}} \in A {\setminus } supp(f)$. Furthermore, by (1), in either case, $\{b_{1},\ldots , b_{m}\} \subseteq \{b_{i_{1}},\ldots , b_{i_{l}}\}$. We prove that $l=m$. Assume by contradiction that there exists $b_{i_{j}}$ with $j \in \{1,\ldots ,l\}$ such that $b_{i_{j}} \notin \{b_{1},\ldots , b_{m}\}$. Then $(b_{i_{j}}\; b_{1}) \star Z=Z$ since both $b_{i_{j}}, b_{1} \in Z$ and Z is a finite subset of atoms ($b_{i_{j}}$ and $b_{1}$ are interchanged in Z under the effect of the transposition $(b_{i_{j}}\; b_{1})$, but the whole Z is left invariant). Furthermore, since $b_{i_{j}}, b_{1} \notin supp(f)$ we have $(b_{i_{j}}\; b_{1}) \in Fix (supp(f))$, and by Proposition 6 we get $f(Z)=f((b_{i_{j}}\; b_{1}) \star Z)=(b_{i_{j}}\; b_{1}) \star f(Z)$ which is a contradiction because $b_{1} \in f(Z)$ while $b_{i_{j}} \notin f(Z)$. Thus, $\{b_{i_{1}},\ldots , b_{i_{l}}\} = \{b_{1},\ldots , b_{m}\}$, and so $Z \in U$. Thus, $U \subseteq f(U)$, which means $|U| \le |f(U)|$. However, since f is a function and U is finite, we get $|f(U)|\le |U|$. We obtain $|U|=|f(U)|$, and because U is finite with $U \subseteq f(U)$, we get $U=f(U)$, which means $f|_{U}:U \rightarrow U$ is surjective (3). Since U is finite, $f|_{U}$ should be injective, which means $f(U_{1}) \ne f(U_{2})$ whenever $U_{1}, U_{2} \in U$ with $U_{1}\ne U_{2}$ (4).

If $d_{1}, \ldots , d_{v} \in A {\setminus } supp(f)$ with$\{d_{1},\ldots , d_{v}\}\ne \{b_{1},\ldots , b_{m}\}$, $v \ge 1$, and we consider $V=\{\{a_{1},\ldots , a_{n}, d_{1},\ldots , d_{v}\} \,|\, a_{1},\ldots , a_{n} \in supp(f) , n \ge 1\} \cup \{\{ d_{1},\ldots , d_{v}\}\}$, then U and V are disjoint. Whenever $U_{1} \in U$ and $V_{1} \in V$ we have $f(U_{1}) \in U$ and $f(V_{1}) \in V$ (using the same arguments we involved to prove relation (3)), and so $f(U_{1})\ne f(V_{1})$ (5).

If $T=\{\{a_{1},\ldots , a_{n}\} \,|\, a_{1},\ldots , a_{n} \in supp(f)\}$ and $Y \in T$, then there is $T'\in \wp _{fin}(A)$ such that $Y=f(T')$. According to (3) we should have $T' \in T$ (otherwise, if $T'$ belongs to some V considered in the above paragraph, i.e. if $T'$ contains an element outside supp(f), we would get the contradiction $Y=f(T') \in V$, i.e. we would get that Y contains an element outside supp(f)), and so $T \subseteq f(T)$ from which $T=f(T)$ because T is finite (using similar arguments as those we involved to prove relation (3) from $U \subseteq f(U)$). Thus, $f|_{T}:T \rightarrow T$ is surjective. Since T is finite, $f|_{T}$ should also be injective which means $f(T_{1}) \ne f(T_{2})$ whenever $T_{1}, T_{2} \in T$ with $T_{1}\ne T_{2}$ (6). The case $supp(f)=\emptyset$ is included in the above analysis and leads to $f(\emptyset )=\emptyset$ and $f(X)=X$ for all $X \in \wp _{fin}(A)$.

We also have $f(T_{1}) \ne f(V_{1})$ whenever $T_{1} \in T$ and $V_{1} \in V$ since $f(T_{1}) \in T$, $f(V_{1}) \in V$ and T and V are disjoint (7). Since $b_{1}, \ldots , b_{m}$ and $d_{1}, \ldots , d_{v}$ were arbitrarily chosen from $A {\setminus } supp(f)$, the injectivity of f follows from (4), (5), (6) and (7) that describe all the possible cases for considering two different finite subsets of atoms for which we compare the values of f on them. $\square$

Proposition 13

• 1. Let X be a finitely supported subset of an invariant set. If $\wp _{fin}(X)$ is FSM Dedekind infinite, then X should be FSM non-uniformly amorphous, meaning that X should contain two disjoint, infinite, uniformly supported subsets.

• 2. Let X be a finitely supported subset of an invariant set. If $\wp _{fs}(X)$ is FSM Dedekind infinite, then X should be FSM non-amorphous (N-am), meaning that X should contain two disjoint, infinite, finitely supported subsets. The reverse implication is not valid.

Proof

• 1. Assume that $(X_{n})_{n \in {\mathbb {N}}}$ is a countable family of different finite subsets of X such that the mapping $n\mapsto X_{n}$ is finitely supported. Thus, each $X_{n}$ is supported by the same set $S=supp(n \mapsto X_{n})$. Since each $X_{n}$ is finite (and the support of a finite set coincides with the union of the supports of its elements), we have that $\underset{n \in {\mathbb {N}}}{\cup }X_{n}$ is uniformly supported by S. Furthermore, $\underset{n \in {\mathbb {N}}}{\cup }X_{n}$ is infinite since all $X_{i}$ are pairwise different. Moreover, the countable sequence $(Y_{n})_{n \in {\mathbb {N}}}$ defined by $Y_{n}=X_{n} {\setminus } \underset{m<n}{\cup }X_{m}$ is a uniformly supported (by S) sequence of pairwise disjoint uniformly supported sets with $\underset{n \in {\mathbb {N}}}{\cup }X_{n}=\underset{n \in {\mathbb {N}}}{\cup }Y_{n}$. Again since each $Y_{n}$ is finite (and the support of a finite set coincides with the union of the supports of its elements), any element belonging to a set from the sequence $(Y_{n})_{n \in {\mathbb {N}}}$ is S-supported. Since the union of all $Y_{n}$ is infinite, and each $Y_{n}$ is finite, there should exist infinitely many terms from the sequence $(Y_{n})_{n \in {\mathbb {N}}}$ that are non-empty. Assume that $(Y_{n})_{n \in M \subseteq {\mathbb {N}}}$ with M infinite is a subset of $(Y_{n})_{n \in {\mathbb {N}}}$ formed by non-empty terms. Let $U_{1}=\{\cup Y_{k}\,|\, k \in M, k \;\text {is odd}\}$ and $U_{2}=\{\cup Y_{k}\,|\, k \in M, k\; \text {is even}\}$. Then $U_{1}$ and $U_{2}$ are disjoint, uniformly S-supported and infinite subsets of X.

• 2. Assume that $\wp _{fs}(X)$ is FSM Dedekind infinite. As in the proof of Theorem 6(8), we can define a uniformly supported, countable family $(Y_{n})_{n \in {\mathbb {N}}}$ of subsets of X that are non-empty and pairwise disjoint. Let $V_{1}=\{\cup Y_{k}\,|\, k \;\text {is odd}\}$ and $V_{2}=\{\cup Y_{k}\,|\, k\; \text {is even}\}$. Then $V_{1}$ and $V_{2}$ are disjoint, infinite subsets of X. Since each $Y_{i}$ is supported by $S'=supp(n \mapsto Y_{n})$ we have $\pi \star Y_{i}=Y_{i}$ for all $i \in {\mathbb {N}}$ and $\pi \in Fix(S')$. Fix $\pi \in Fix(S')$ and $x \in V_{1}$. Thus, there is $l \in {\mathbb {N}}$ such that $x \in Y_{2l+1}$. We obtain $\pi \cdot x \in \pi \star Y_{2l+1}=Y_{2l+1}$, and so $\pi \cdot x \in V_{1}$. Thus, $V_{1}$ is supported by $S'$. Similarly, $V_{2}$ is supported by $S'$, and so X is FSM non-amorphous.

  Conversely, the set $A+A=\{0,1\}\times A$ (disjoint union of A and A) is obviously non-amorphous because $\{(0,a)\,|\,a \in A\}$ is equivariant, infinite and coinfinite. One can define the equivariant bijection $f: \wp _{fs}(A) \times \wp _{fs}(A) \rightarrow \wp _{fs}(\{0,1\}\times A)$ by $f(U,V)=\{(0,x)\,|\,x \in U\} \cup \{(1,y)\,|\,y \in V\}$ for all $U,V \in \wp _{fs}(A)$. Clearly, f is equivariant because for each $\pi \in S_{A}$ we have $f(\pi \star U,\pi \star V)=\pi \star f(U,V)$. However, $\wp _{fs}(A) \times \wp _{fs}(A)$ is not FSM Dedekind infinite according to Corollary 7(2) and Theorem 6(6). $\square$

It is also worth noting that non-uniformly amorphous FSM sets are non-amorphous FSM sets since uniformly supported sets are obviously finitely supported. The converse however is not valid since $\wp _{fin}(A)$ is non-amorphous, but it has no infinite uniformly supported subset (the only finite subsets of atoms supported by a finite set S of atoms being the subsets of S), and so it cannot be non-uniformly amorphous.

Corollary 10

Let X be a finitely supported amorphous subset of an invariant set (i.e. any finitely supported subset of X is either finite or cofinite). Then each finitely supported surjective mapping $f:X \rightarrow X$ should be injective.

Proof

Since any finitely supported subset of X is either finite or cofinite, then any uniformly supported subset of X is either finite or cofinite. From Proposition 13, $\wp _{fin}(X)$ is not FSM Dedekind infinite. For the rest of the proof we follow step-by-step the proof of Proposition 12 (and of Lemma 4). If X is finite, we are done, so assume X is infinite. If $Y \in \wp _{fin}(X)$, then $f^{-1}(Y) \in \wp _{fs}(X)$ (supported by $supp(f) \cup supp(X) \cup supp(Y)$). Since X is amorphous, it follows that $f^{-1}(Y)$ is either finite or cofinite. If $f^{-1}(Y)$ is cofinite, then its complementary $\{x \in X \;|\; f(x) \notin Y\}$ is finite. This means that all but finitely many elements in X would have their image under f belonging to the finite set Y. Therefore, Im(f) would be a finite subset of X, which contradicts the surjectivity of f. Thus, $f^{-1}(Y)$ is a finite subset of X. In this sense we can define the function $g:\wp _{fin}(X) \rightarrow \wp _{fin}(X)$ by $g(Y) = f^{-1}(Y)$ which is supported by $supp(f) \cup supp(X)$ and injective. Since $\wp _{fin}(X)$ is not FSM Dedekind infinite, it follows that g is surjective, and so f is injective exactly as in the last paragraph of the proof of Proposition 12. $\square$

Proposition 14

• 1. Let X be an FSM Dedekind infinite set. Then there is a finitely supported surjection $j:X\rightarrow {\mathbb {N}}$. The reverse implication is not valid.

• 2. If X is a finitely supported subset of an invariant set such that there exists a finitely supported surjection $j:X \rightarrow {\mathbb {N}}$, then $\wp _{fs}(X)$ is FSM Dedekind infinite. The reverse implication is also valid.

Proof

• 1. Let X be an FSM Dedekind infinite set. According to Theorem 6(1), there is a finitely supported injection $i:{\mathbb {N}} \rightarrow X$. Let us fix $n_{0} \in {\mathbb {N}}$. We define the function $j: X \rightarrow {\mathbb {N}}$ by

  $$\begin{aligned} j(x)=\left\{ \begin{array}{ll} i^{-1}(x), &{} \text {if}\, {x\in Im(i) };\\ n_{0}, &{} \text {if}\, {x\notin Im(i)}\, .\end{array}\right. \end{aligned}$$

  Since Im(i) is supported by supp(i) and $n_{0}$ is empty supported, by verifying the condition in Proposition 6 we have that j is supported by $supp(i) \cup supp(X)$. Indeed, when $\pi \in Fix(supp(i) \cup supp(X))$, then $x \in Im(i) \Leftrightarrow \pi \cdot x \in Im(i)$, and $n=i^{-1}(\pi \cdot x) \Leftrightarrow i(n)=\pi \cdot x \Leftrightarrow \pi ^{-1} \cdot i(n)=x \Leftrightarrow i(\pi ^{-1} \diamond n)=x \Leftrightarrow i(n)=x \Leftrightarrow n=i^{-1}(x)$, where $\diamond$ is the trivial action on ${\mathbb {N}}$; similarly $y \notin Im(i) \Leftrightarrow \pi \cdot y \notin Im(i)$ and $j(\pi \cdot y)=n_{0}=\pi \diamond n_{0}=\pi \diamond j(y)$. Clearly, j is surjective. However, the reverse implication is not valid because the mapping $f:\wp _{fin}(A) \rightarrow {\mathbb {N}}$ defined by $f(X)=|X|$ for all $X \in \wp _{fin}(A)$ is equivariant and surjective, but $\wp _{fin}(A)$ is not FSM Dedekind infinite.

• 2. Suppose now there exists a finitely supported surjection $j:X \rightarrow {\mathbb {N}}$. Clearly, for any $n \in {\mathbb {N}}$, the set $j^{-1}(\{n\})$ is non-empty and supported by supp(j). Define $f: {\mathbb {N}} \rightarrow \wp _{fs}(X)$ by $f(n)=j^{-1}(\{n\})$. For $\pi \in Fix(supp(j))$ and an arbitrary $n \in {\mathbb {N}}$ we have $j(x)=n \Leftrightarrow j(\pi ^{-1} \cdot x)=n$, and so $x \in j^{-1}(\{n\}) \Leftrightarrow \pi ^{-1} \cdot x \in j^{-1}(\{n\})$, which means $f(n) = \pi \star f(n)$ for all $n \in {\mathbb {N}}$, and so f is supported by supp(j). Since f is also injective, by Theorem 6(1) we have that $\wp _{fs}(X)$ is FSM Dedekind infinite.

  Conversely, assume that $\wp _{fs}(X)$ is FSM Dedekind infinite. As in the proof of Theorem 6(8), we can define a uniformly supported, countable family $(Y_{n})_{n \in {\mathbb {N}}}$ of subsets of X that are non-empty and pairwise disjoint. The mapping f can be defined by $f(x)=\left\{ \begin{array}{ll} n, &{} \text {if}\ \exists n. x\in Y_{n};\\ 0, &{} \text {otherwise} \end{array}\right.$, and obviously, f is supported by $supp(n \mapsto Y_{n})$. $\square$

Proposition 15

Let X be an infinite finitely supported subset of an invariant set. Then there exists a finitely supported surjection $f:\wp _{fs}(X) \rightarrow {\mathbb {N}}$.

Proof

Let $X_{i}$ be the set of all i-sized subsets from X, $X_{i}=\{Z \subseteq X\,|\,|Z|=i\}$. The family $(X_{i})_{i \in {\mathbb {N}}}$ is uniformly supported by supp(X) and all $X_{i}$ are non-empty and pairwise disjoint. We define f by $f(Y)=\left\{ \begin{array}{ll} n, &{} \text {if}\, Y\in X_{n};\\ 0, &{} \text {if}\; Y\; \text {is infinite} .\end{array}\right.$

According to Proposition 6, f is supported by supp(X) (since any $X_{n}$ is supported by supp(X)) and it is surjective. We actually proved the existence of a finitely supported surjection from $\wp _{fin}(X)$ onto ${\mathbb {N}}$. $\square$

The sets A and $\wp _{fin}(A)$ are both FSM classical infinite and none of them is FSM Dedekind infinite. We prove below that A is not FSM ascending infinite, while $\wp _{fin}(A)$ is FSM ascending infinite.

Proposition 16

• 1. The set A is not FSM ascending infinite.

• 2. Let X be a finitely supported subset of an invariant set U. If X is FSM classical infinite, then the set $\wp _{fin}(X)$ is FSM ascending infinite.

Proof

• 1. In order to prove that A is not FSM ascending infinite, we prove firstly that each finitely supported increasing countable chain of finitely supported subsets of A must be stationary. Indeed, if there exists an increasing countable chain $X_{0}\subseteq X_{1}\subseteq \ldots \subseteq A$ such that $n \mapsto X_{n}$ is finitely supported, then, according to Proposition 6 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, there are only finitely many such subsets of A namely the subsets of S and the supersets of $A{\setminus } S$. Therefore the chain is finite, and because it is ascending, there exists $n_{0}\in {\mathbb {N}}$ such that $X_{n}=X_{n_{0}}$ for all $n\ge n_{0}$. Now, let $Y_{0}\subseteq Y_{1}\subseteq \ldots \subseteq Y_{n}\subseteq \ldots$ be a finitely supported countable chain with $A\subseteq \underset{n \in {\mathbb {N}}}{\cup } Y_{n}$. Then $A \cap Y_{0}\subseteq A \cap Y_{1}\subseteq \ldots \subseteq A \cap Y_{n}\subseteq \ldots \subseteq A$ is a finitely supported countable chain of subsets of A (supported by $supp(n \mapsto Y_{n})$) which should be stationary (finite). Furthermore, since $\underset{i \in {\mathbb {N}}}{\cup }(A\cap Y_{i})=A \cap (\underset{i \in {\mathbb {N}}}{\cup } Y_{i})=A$, there is some $k_{0}$ such that $A \cap Y_{k_{0}}=A$, and so $A \subseteq Y_{k_{0}}$. Thus, A is not FSM ascending infinite.

• 2. We know that $\wp _{fin}(X)$ is a subset of the invariant set $\wp _{fin}(U)$ supported by supp(X). Let us consider $X_{n}\!=\!\{Z\!\in \!\wp _{fin}(X)\,|\,|Z|\!\le \! n\}$. Clearly, $X_{0}\subseteq X_{1}\subseteq \ldots \subseteq X_{n}\subseteq \ldots$. Furthermore, because permutations of atoms are bijective, we have that for an arbitrary $k \in {\mathbb {N}}$, $|\pi \star Y| =|Y|$ for all $\pi \in S_{A}$ and all $Y \in X_{k}$, and so $\pi \star Y \in X_{k}$ for all $\pi \in Fix(supp(X))$ and all $Y \in X_{k}$. Thus, each $X_{k}$ is a subset of $\wp _{fin}(X)$ finitely supported by supp(X), and so $(X_{n})_{n \in {\mathbb {N}}}$ is finitely (uniformly) supported by supp(X). Obviously, $\wp _{fin}(X)=\underset{n \in {\mathbb {N}}}{\cup } X_{n}$. However, there exists no $n\in {\mathbb {N}}$ such that $\wp _{fin}(X)=X_{n}$. Thus, $(\wp _{fin}(X), \star )$ is FSM ascending infinite.

$\square$

Theorem 8

Let X be a finitely supported subset of an invariant set $(Z, \cdot )$.

• 1. If X is FSM Dedekind infinite, then X is FSM Mostowski infinite.

• 2. If X is FSM Mostowski infinite, then X is FSM Tarski II infinite. The reverse implication is not valid.

Proof

• 1. Suppose X is FSM Dedekind infinite. According to Theorem 6(1) there exists an uniformly supported infinite injective sequence $T=(x_{n})_{n \in {\mathbb {N}}}$ of elements from X. Thus, each element of T is supported by supp(T) and there is a bijective correspondence between ${\mathbb {N}}$ and T defined as $n \mapsto x_{n}$ which is supported by supp(T). If we define the relation $\sqsubset$ on T by: $x_{i} \sqsubset x_{j}$ if and only if $i<j$, we have that $\sqsubset$ is a (strict) total order relation supported by supp(T). Thus T is an infinite finitely supported (strictly) totally ordered subset of X, and so X is FSM Mostowski infinite since any strict total order can be extended to a total order.

• 2. Suppose that X is not FSM Tarski II infinite. Then every non-empty finitely supported family of finitely supported subsets of X which is totally ordered by inclusion has a maximal element under inclusion. Let $(U, <)$ be a finitely supported strictly totally ordered subset of X (any total order relation induces a strict total order relation). We prove that U is finite, and so X is not FSM Mostowski infinite. In this sense it is sufficient to prove that < and > are well-orderings. Since both of them are (strict) total orderings, we need to prove that any finitely supported subset of U has a least and a greatest element wrt <, i.e. a minimal and a maximal element (because < is total). Let Y be a finitely supported subset of U. The set $\downarrow z=\{y \in Y\,|\,y<z\}$ is supported by $supp(z) \cup supp(Y) \cup supp(<)$ for all $z \in Y$. The family $T=\{\downarrow z\,|\,z \in Y\}$ is itself finitely supported by $supp(Y) \cup supp(<)$ because for all $\pi \in Fix(supp(Y) \cup supp(<))$ we have $\pi \cdot \downarrow z=\downarrow \pi \cdot z$. Since < is transitive, we have that T is (strictly) totally ordered by inclusion, and so it has a maximal element, which means Y has a maximal element. Similarly, the set $\uparrow z=\{y \in Y\,|\,z<y\}$ is supported by $supp(z) \cup supp(Y) \cup supp(<)$ for all $z \in Y$ and the family $T'=\{\uparrow z\,|\,z \in Y\}$ is itself finitely supported by $supp(Y) \cup supp(<)$ because for all $\pi \in Fix(supp(Y) \cup supp(<))$ we have $\pi \cdot \uparrow z=\uparrow \pi \cdot z$. The family $T'$ is (strictly) totally ordered by inclusion, and so it has a maximal element, from which Y has a minimal element. We used the obvious properties $z<t$ if and only if $\downarrow z \subset \downarrow t$, and $z<t$ if and only if $\uparrow t \subset \uparrow z$.

  Conversely, according to Proposition 16, $\wp _{fin}(A)$ is FSM ascending infinite, and so it is FSM Tarski II infinite. However $\wp _{fin}(A)$ is not FSM Mostowski infinite according to Corollary 12

$\square$

Proposition 17

Let X be a finitely supported subset of an invariant set $(Z, \cdot )$. If X is FSM Mostowski infinite, then X is non-amorphous meaning that X can be expressed as a disjoint union of two infinite finitely supported subsets. The reverse implication is not valid.

Proof

Suppose that there is an infinite finitely supported totally ordered subset $(Y, \le )$ of X. Assume, by contradiction, that Y is amorphous, meaning that any finitely supported subset of Y is either finite or cofinite. As in the proof of Theorem 8 (without making the requirement that $\le$ is strict, which anyway would not essentially change the proof), for $z \in Y$ we define the finitely supported subsets $\downarrow z=\{y \in Y\,|\,y \le z\}$ and $\uparrow z=\{y \in Y\,|\,z \le y\}$ for all $z \in Y$. We have that the mapping $z \mapsto \downarrow z$ from Y to $T=\{\downarrow z\,|\,z \in Y\}$ is itself finitely supported by $supp(Y) \cup supp(\le )$. Furthermore it is bijective, and so T is amorphous. Thus, any subset Z of T is either finite or cofinite, and obviously any subset Z of T is finitely supported. Similarly, the mapping $z \mapsto \uparrow z$ from Y to $T'=\{\uparrow z\,|\,z \in Y\}$ is finitely supported and bijective, which means that any subset of $T'$ is either finite or cofinite, and clearly any subset of $T'$ is finitely supported.

We distinguish the following two cases:

1. There are only finitely many elements $x_{1}, \ldots , x_{n}\in Y$ such that $\downarrow x_{1}, \ldots , \downarrow ~x_{n}$ are finite. Thus, for $y \in U= Y {\setminus } \{x_{1}, \ldots , x_{n}\}$ we have $\downarrow y$ infinite. Since $\downarrow ~y$ is a subset of Y, it should be cofinite, and so $\uparrow y$ is finite (because $\le$ is a total order relation). Let $M=\{\uparrow y\,|\,y \in U\}$. As in Theorem 8, we have that M is totally ordered with respect to sets inclusion. Furthermore, for an arbitrary $y \in U$ we cannot have $y \le x_{k}$ for some $k\in \{1,\ldots ,n\}$ because $\downarrow ~y$ is infinite, while $\downarrow x_{k}$ is finite, and so $\uparrow y$ is a subset of U. Thus, M is an infinite, finitely supported (by $supp(U) \cup supp(\le )$), totally ordered family formed by finite subsets of U. Since M is finitely supported, for each $y \in U$ and each $\pi \in Fix(supp(M))$ we have $\pi \cdot \uparrow y \in M$. Since $\uparrow y$ is finite, we have that $\pi \cdot \uparrow y$ is finite having the same number of elements as $\uparrow y$. Since $\pi \cdot \uparrow y$ and $\uparrow y$ are comparable via inclusion, they should be equal. Thus, M is uniformly supported. Since $\le$ is a total order, for $\pi \in Fix(supp(\uparrow y))$ we have $\uparrow \pi \cdot y=\pi \cdot \uparrow y=\uparrow y$, and so $\pi \cdot y=y$, from which $supp(y) \subseteq supp(\uparrow y)$. Therefore, U is uniformly supported. Since any element of U has only a finite number of successors (leading to the conclusion that $\ge$ is an well-ordering on U uniformly supported by supp(U)) and U is uniformly supported, we can define an order monomorphism between ${\mathbb {N}}$ and U which is supported by supp(U). For example, choose $u_{0}\ne u_{1}\in U$, then let $u_{2}$ be the greatest element (w.r.t. $\le$) in $U{\setminus } \{u_{0}, u_{1}\}$, $u_{3}$ be the greatest element in $U{\setminus } \{u_{0}, u_{1}, u_{2}\}$ (no choice principle is used since $\ge$ is an well-ordering, and so such a greatest element is precisely defined), and so on, and find an infinite, uniformly supported countable sequence $u_{0}, u_{1}, u_{2},\ldots$. Since ${\mathbb {N}}$ is non-amorphous (being expressed as the union between the even elements and the odd elements), we conclude that U is non-(uniformly) amorphous containing two infinite uniformly supported disjoint subsets.

2. We have cofinitely many elements z such that $\downarrow z$ is finite. Thus, there are only finitely many elements $y_{1}, \ldots , y_{m} \in Y$ such that $\downarrow y_{1}, \ldots , \downarrow y_{m}$ are infinite. Since every infinite subset of Y is cofinite, only $\uparrow y_{1}, \ldots , \uparrow y_{m}$ are finite. Let $z \in Y {\setminus } \{y_{1}, \ldots , y_{m}\}$ which means $\uparrow z$ infinite. Since $\uparrow z$ is a subset of Y it should be cofinite, and so $\downarrow z$ is finite. As in the above item, the set $M'=\{\downarrow z\,|\,z \in Y {\setminus } \{y_{1}, \ldots , y_{m}\} \}$ is an infinite, finitely supported, totally ordered (by inclusion) family of finite sets, and so it has to be uniformly supported, from which $Y {\setminus } \{y_{1}, \ldots , y_{m}\}$ is uniformly supported, and so $\le$ is an FSM well-ordering on $Y {\setminus } \{y_{1}, \ldots , y_{m}\}$. Therefore, $Y {\setminus } \{y_{1}, \ldots , y_{m}\}$ has an infinite, uniformly supported, countable subset, and so $Y {\setminus } \{y_{1}, \ldots , y_{m}\}$ is non-(uniformly) amorphous containing two infinite uniformly supported disjoint subsets. Thus, Y is non-amorphous, and so X is non-amorphous.

Conversely, the set $A+A$ (disjoint union of A and A) is obviously non-amorphous because $\{(0,a)\,|\,a \in A\}$ is equivariant, infinite and coinfinite. However, if we assume there exists a finitely supported total order relation on an infinite subset of $A+A$, then there should exist an infinite, finitely supported, total order on at least one of the sets $\{(0,a)\,|\,a \in A\}$ or $\{(1,a)\,|\,a \in A\}$, which leads to an infinite finitely supported total order relation on A. However A is not FSM Mostowski infinite by Corollary 12. $\square$

Theorem 9

Let X be a finitely supported subset of an invariant set $(Z, \cdot )$. If X contains no infinite uniformly supported subset, then X is not FSM Mostowski infinite.

Proof

Assume, by contradiction, that X is FSM Mostowski infinite, meaning that X contains an infinite, finitely supported, totally ordered subset $(Y, \le )$. We claim that Y is uniformly supported by $supp(\le ) \cup supp(Y)$. Let $\pi \in Fix (supp(\le ) \cup supp(Y))$ and let $y \in Y$ an arbitrary element. Since $\pi$ fixes supp(Y) pointwise and supp(Y) supports Y, we obtain that $\pi \cdot y \in Y$, and so we should have either $y<\pi \cdot y$, or $y=\pi \cdot y$, or $\pi \cdot y<y$. If $y<\pi \cdot y$, then, because $\pi$ fixes $supp(\le )$ pointwise and because the mapping $z\mapsto \pi \cdot z$ is bijective from Y to $\pi \star Y$, we get $y<\pi \cdot y<\pi ^{2} \cdot y<\ldots < \pi ^{n} \cdot y$ for all $n \in {\mathbb {N}}$. However, since any permutation of atoms interchanges only finitely many atoms, it has a finite order in the group $S_{A}$, and so there is $m \in {\mathbb {N}}$ such that $\pi ^{m}=Id$. This means $\pi ^{m} \cdot y=y$, and so we get $y<y$ which is a contradiction. Similarly, the assumption $\pi \cdot y<y$, leads to the relation $\pi ^{n} \cdot y<\ldots<\pi \cdot y<y$ for all $n \in {\mathbb {N}}$ which is also a contradiction since $\pi$ has finite order. Therefore, $\pi \cdot y=y$; because y was arbitrary chosen form Y, Y should be a uniformly supported infinite subset of X. $\square$

Looking to the proof of Proposition 17, the following result follows directly.

Corollary 11

Let X be a finitely supported subset of an invariant set $(Z, \cdot )$. If X is FSM Mostowski infinite, then X is non-uniformly amorphous meaning that X has two disjoint, infinite, uniformly supported subsets.

Remark 3

In a permutation model of set theory with atoms, a set can be well-ordered if and only if there exists a one-to-one mapping of the related set into the kernel of the model. Furthermore, in a permutation model defined by using supports, a set U is well-orderable in the model if and only if there exists a set supporting every element in U. Also it is noted that the axiom of choice is valid in the kernel of the model [7]. Therefore, totally ordered, finitely supported sets in Basic Fraenkel Model (that are proved to be uniformly supported similarly as in Theorem 9, and so they are well-orderable according to the above statements) can be embedded into the kernel of the model, and they should contain countable (uniformly supported) subsets; this provides an equivalence between Dedekind infinity and Mostowski infinity in the related permutation model. Although FSM (or the theory of nominal sets) is somehow related to (has connections with) permutation models of set theory with atoms, it is independently developed over ZF without being necessary to relax the ZF axiom of extensionality. FSM sets are ZF sets together with group actions satisfying a certain finite support requirement, and such a theory makes sense over ZF without being necessary to impose the validity of the axiom of choice on (non-atomic) ZF sets. Thus, FSM is described as the entire ZF together with atomic sets/structures with finite supports, where the set of atoms is a fixed ZF set (formed by elements whose internal structure is ignored). There could exist infinite ZF sets that do not contain infinite countable subsets, and there could also exist infinite uniformly supported FSM sets (particularly such ZF sets) that do not contain infinite countable, uniformly supported subsets.

Corollary 12

• 1. The sets A, $A+A$ and $A \times A$ are FSM classical infinite, but they are not FSM Mostowski infinite, nor FSM Tarski II infinite.

• 2. None of the sets $\wp _{fin}(A)$, $\wp _{cofin}(A)$, $\wp _{fs}(A)$ and $\wp _{fin}(\wp _{fs}(A))$ is Mostowski infinite in FSM.

• 3. None of the sets $A^{A^{n}}_{fs}$, $T_{fin}(A)^{A^{n}}_{fs}$ and $\wp _{fs}(A)^{A^{n}}_{fs}$ is FSM Mostowski infinite.

Proof

In the view of Theorem 9, it is sufficient to prove that none of the sets A, $\wp _{fin}(A)$, $\wp _{cofin}(A)$, $\wp _{fs}(A)$, $A+A$, $A \times A$, $A^{A^{n}}_{fs}$,$T_{fin}(A)^{A^{n}}_{fs}$ and $\wp _{fs}(A)^{A^{n}}_{fs}$ contain infinite uniformly supported subsets. For A, $\wp _{fin}(A)$, $\wp _{cofin}(A)$ and $\wp _{fs}(A)$ this is obvious since for any finite set S of atoms there are at most finitely many subsets of A supported by S, namely the subsets of S and the supersets of $A {\setminus } S$. Moreover, $\wp _{fin}(\wp _{fs}(A))$ does not contain an infinite uniformly supported subset according to Theorem 6(5), since $\wp _{fs}(A)$ does not contain an infinite uniformly supported subset.

From Theorem 7 and Corollary 4, the invariant sets $A^{A^{n}}_{fs}$, $T_{fin}(A)^{A^{n}}_{fs}$ and $\wp _{fs}(A)^{A^{n}}_{fs}$ do not contain infinite uniformly supported subsets.

We also have that A is not FSM Tarski II infinite because $\wp _{fs}(A)$ contains no infinite uniformly supported subsets, and so every totally ordered subset (particularly via inclusion) of $\wp _{fs}(A)$ should be finite meaning that it should have a maximal element. Furthermore, we have that there is an equivariant bijection between $\wp _{fs}(A+A)$ and $\wp _{fs}(A)\times \wp _{fs}(A)$. Since $\wp _{fs}(A)$ does not contain an infinite uniformly supported subset, we have that $\wp _{fs}(A) \times \wp _{fs}(A)$ does not contain an infinite uniformly supported subset (the proof is quasi-identical to the one of Theorem 6(6) without taking count on the countability of the related infinite uniformly supported family). Therefore, any infinite totally ordered (via inclusion) uniformly supported family of $\wp _{fs}(A+A)$ should be finite containing a maximal element. There is an equivariant bijection between $\wp _{fs}(A)^{A}_{fs}$ and $\wp _{fs}(A \times A)$. Therefore any uniformly supported totally ordered subset of $\wp _{fs}(A \times A)$ should be finite containing a maximal element. $\square$

Corollary 13

Let X be a finitely supported subset of an invariant set Y such that X does not contain an infinite uniformly supported subset. Then the set $\wp _{fin}(X)$ is not FSM Mostowski infinite.

Proof

According to Theorem 6(5), $\wp _{fin}(X)$ does not contain an infinite uniformly supported subset. Thus, by Theorem 9, $\wp _{fin}(X)$ is not FSM Mostowski infinite. $\square$

Theorem 10

Let X be a finitely supported subset of an invariant set $(Y, \cdot )$.

• 1. If X is FSM Tarski I infinite, then X is FSM Tarski III infinite. The converse does not hold. However if X is FSM Tarski III infinite, then $\wp _{fs}(X)$ is FSM Tarski I infinite.

• 2. If X is FSM Tarski III infinite, then X is FSM Dedekind infinite. The converse does not hold. However if X is FSM Dedekind infinite, then $\wp _{fs}(X)$ is FSM Tarski III infinite.

Proof

1. We consider the case when X has at least two elements (otherwise the theorem is trivial). Let X be FSM Tarski I infinite. Then $|X \times X|= |X|$. Fix two elements $x_{1}, x_{2} \in X$ with $x_{1}\ne x_{2}$. We can define an injection $f:X \times \{0,1\} \rightarrow X \times X$ by $f(u)=\left\{ \begin{array}{ll} (x,x_{1}) &{} \text {for}\, u=(x,0)\\ (x,x_{2}) &{} \text {for}\, u=(x,1) \end{array}\right.$. Clearly, by checking the condition in Proposition 6 and using Proposition 3, we have that f is supported by $supp(X) \cup supp(x_{1}) \cup supp(x_{2})$ (since $\{0,1\}$ is necessarily a trivial invariant set), and so $|X\times \{0,1\}|\le |X \times X|$. Thus, $|X\times \{0,1\}| \le |X|$. Obviously, there is an injection $i: X \rightarrow X\times \{0,1\}$ defined by $i(x)=(x,0)$ for all $x \in X$ which is supported by supp(X). According to Lemma 2, we obtain $2|X|=|X \times \{0,1\}|=|X|$.

Let us consider $X={\mathbb {N}} \times A$. We make the remark that $|{\mathbb {N}}\times {\mathbb {N}}|=|{\mathbb {N}}|$ by considering the equivariant injection $h:{\mathbb {N}} \times {\mathbb {N}} \rightarrow {\mathbb {N}}$ defined by $h(m,n)=2^{m}3^{n}$ and using Lemma 2. Similarly, $|\{0,1\}\times {\mathbb {N}}|=|{\mathbb {N}}|$ by considering the equivariant injection $h':{\mathbb {N}} \times \{0,1\}\rightarrow {\mathbb {N}}$ defined by $h'(n,0)$=$2^{n}$, $h'(n,1)$=$3^{n}$ and using Lemma 2. We have $2|X|=2|{\mathbb {N}}||A|=|{\mathbb {N}}||A|=|X|$. However, we prove that $|X \times X|\ne |X|$. Assume the contrary, and so $|{\mathbb {N}} \times (A \times A)| = |{\mathbb {N}} \times A \times {\mathbb {N}} \times A| = |{\mathbb {N}} \times A|$. Thus, there is a finitely supported injection $g: A \times A \rightarrow {\mathbb {N}} \times A$, and by Proposition 8 there is a finitely supported surjection $f:{\mathbb {N}} \times A \rightarrow A \times A$. Let us consider three different atoms $a,b,c \notin supp(f)$. There exists $(i,x) \in {\mathbb {N}} \times A$ such that $f(i,x)=(a,b)$. Since $(a\,b) \in Fix(supp(f))$ and ${\mathbb {N}}$ is trivial invariant set, we have $f(i,(a\,b)(x))=(a\,b)f(i,x)=(a\,b)(a,b)=((a\,b)(a),(a\,b)(b))=(b,a)$. We should have $x=a$ or $x=b$, otherwise f is not a function. Assume without losing the generality that $x=a$, which means $f(i,a)=(a,b)$. Therefore $f(i,b)=f(i,(a\,b)(a))=(a\,b)f(i,a)=(a\,b)(a,b)=(b,a)$. Similarly, since $(a\,c),(b\,c) \in Fix(supp(f))$, we have $f(i,c)=f(i,(a\,c)(a))=(a\,c)f(i,a)=(a\,c)(a,b)=(c,b)$ and $f(i,b)=f(i,(b\,c)(c))=(b\,c)f(i,c)=(b\,c)(c,b)=(b,c)$. But $f(i,b)=(b,a)$ contradicting the functionality of f. Therefore, X is FSM Tarski III infinite, but it is not FSM Tarski I infinite.

Now, suppose that X is FSM Tarski III infinite, which means $|\{0,1\}\times X|=|X|$. We define $\psi :\wp _{fs}(X) \times \wp _{fs}(X) \rightarrow \wp _{fs}(\{0,1\}\times X)$ by $f(U,V)=\{(0,x)\,|\,x \in U\} \cup \{(1,y)\,|\,y \in V\}$ for all $U,V \in \wp _{fs}(X)$. Clearly, $\psi$ is well-defined and bijective, and for each $\pi \in Fix(supp(X))$ we have $\psi (\pi \star U,\pi \star V)=\pi \star \psi (U,V)$ which means $\psi$ is finitely supported. Therefore, $|\wp _{fs}(X) \times \wp _{fs}(X)|=|\wp _{fs}(\{0,1\}\times X)|=|\wp _{fs}(X)|$. The last equality follows by applying twice Lemma 4 (using the fact that there is a finitely supported surjection from X onto $X\times \{0,1\}$ and a finitely supported surjection from $X\times \{0,1\}$ onto X, we obtain there is a finitely supported injection from $\wp _{fs}(X\times \{0,1\})$ into $\wp _{fs}(X)$, and a finitely supported injection from $\wp _{fs}(X)$ into $\wp _{fs}(X\times \{0,1\})$) and Lemma 2.

2. Suppose X is FSM Tarski III infinite. Let us consider an element $y_{1}$ belonging to an invariant set (with action denoted also by $\cdot$) and $y_{1}\notin X$ (such an element can be, for example, a non-empty element in $\wp _{fs}(X) {\setminus } X$). Fix $y_{2} \in X$. We can define a mapping $f:X \cup \{y_{1}\} \rightarrow X \times \{0,1\}$ by $f(x)=\left\{ \begin{array}{ll} (x,0) &{} \text {for}\, x \in X\\ (y_{2}, 1) &{} \text {for}\, x=y_{1} \end{array}\right.$. Clearly, f is injective and it is supported by $S=supp(X) \cup supp(y_{1}) \cup supp(y_{2})$ because for all $\pi$ fixing S pointwise we have $f(\pi \cdot x)=\pi \cdot f(x)$ for all $x \in X \cup \{y_{1}\}$. Therefore, $|X \cup \{y_{1}\}| \le |X \times \{0,1\}|=|X|$, and so there is a finitely supported injection $g:X \cup \{y_{1}\} \rightarrow X$. The mapping $h:X \rightarrow X$ defined by $h(x)=g(x)$ is injective, supported by $supp(g) \cup supp(X)$, and $g(y_{1}) \in X {\setminus } h(X)$, which means h is not surjective. It follows that X is FSM Dedekind infinite.

Let us consider $X=A \cup {\mathbb {N}}$. Since A and ${\mathbb {N}}$ are disjoint, we have that X is an invariant set (similarly as in Proposition 3). Clearly, X is FSM Dedekind infinite. Assume, by contradiction, that $|X|=2|X|$, that is $|A \cup {\mathbb {N}}|=|A+A+{\mathbb {N}}|=|(\{0,1\}\times A) \cup {\mathbb {N}}|$. Thus, there is a finitely supported injection $f:(\{0,1\}\times A) \cup {\mathbb {N}}\rightarrow A \cup {\mathbb {N}}$, and so there exists a finitely supported injection $f:(\{0,1\}\times A) \rightarrow A \cup {\mathbb {N}}$. We prove that whenever $\varphi :A \rightarrow A \cup {\mathbb {N}}$ is finitely supported and injective, for $a \notin supp(\varphi )$ we have $\varphi (a) \in A$. Assume, by contradiction, that there is $a \notin supp(\varphi )$ such that $\varphi (a)\in {\mathbb {N}}$. Since $supp(\varphi )$ is finite, there exists $b \notin supp(\varphi )$, $b \ne a$. Thus, $(a\,b) \in Fix(supp(\varphi ))$, and so $\varphi (b)=\varphi ((a\,b)(a))=(a\,b)\diamond \varphi (a)=\varphi (a)$ since $({\mathbb {N}}, \diamond )$ is a trivial invariant set. This contradicts the injectivity of $\varphi$. We can consider the mappings $\varphi _{1},\varphi _{2}: A \rightarrow A \cup {\mathbb {N}}$ defined by $\varphi _{1}(a)=f(0,a)$ for all $a \in A$ and $\varphi _{2}(a)=f(1,a)$ for all $a \in A$, that are injective and supported by supp(f). Therefore, $f(\{0\} \times A)=\varphi _{1}(A)$ contains at most finitely many element from ${\mathbb {N}}$, and $f(\{1\} \times A)=\varphi _{2}(A)$ also contains at most finitely many element from ${\mathbb {N}}$. Thus, f is an injection from $(\{0,1\}\times A)$ to $A \cup Z$ where Z is a finite subset of ${\mathbb {N}}$. It follows that $f(\{0\} \times A)$ contains an infinite subset of atoms U, and $f(\{1\} \times A)$ contains an infinite subset of atoms V. Since f is injective, it follows that U and V are infinite disjoint subsets of A, which contradicts Proposition 5 stating that A is amorphous.

Now, if X is FSM Dedekind infinite, we have that there is a finitely supported injection h from X onto a finitely supported proper subset Z of X. Consider an element $y_{1}$ belonging to an invariant set with $y_{1}\notin X$. We can define an injection $h': X \cup \{y_{1}\} \rightarrow X$ by taking $h'(x)=h(x)$ for all $x \in X$ and $h'(y_{1})=b$ with $b \in X {\setminus } Z$. Clearly, $h'$ is supported by $supp(h) \cup supp(y_{1}) \cup supp(b)$. Since there also exists an supp(X)-supported injection from X to $X \cup \{y_{1}\}$, according to Lemma 2, one can define a finitely supported bijection $\psi$ from X to $X \cup \{y_{1}\}$. According to Lemma 4 the mapping $g:\wp _{fs}(X \cup \{y_{1}\}) \rightarrow \wp _{fs}(X)$ defined by $g(V)=f^{-1}(V)$ for all $V \in \wp _{fs}(X \cup \{y_{1}\})$ is finitely supported and injective. Therefore, $2^{|X|}\ge 2^{|X|+1} =2\cdot 2^{|X|}$ which in the view of Lemma 2 (since we also have $2^{|X|}\le 2\cdot 2^{|X|}$) leads to the conclusion that $\wp _{fs}(X)$ is FSM Tarski III infinite. $\square$

Corollary 14

• 1. The set ${\mathbb {N}} \times A$ is FSM Tarski III infinite, but it is not FSM Tarski I infinite.

• 2. The set $A \cup {\mathbb {N}}$ is FSM Dedekind infinite, but it is not FSM Tarski III infinite.

Corollary 15

The following sets are FSM classical infinite, but they are not FSM Tarski I infinite, nor FSM Tarski III finite.

• 1. The invariant set A.

• 2. The invariant set $\wp _{fs}(A)$.

• 3. The invariant sets $\wp _{fin}(A)$ and $\wp _{cofin}(A)$.

• 4. The set $\wp _{fin}(X)$ where X is a finitely supported subset of an invariant set containing no infinite uniformly supported subset.

Proof

The result follows directly because, according to Theorem 6 and Corollary 7, the related sets are not FSM Dedekind infinite. $\square$

Corollary 16

Let X be an infinite finitely supported subset of an invariant set. Then $\wp _{fs}(\wp _{fs}(\wp _{fs}(X)))$ is FSM Tarski III infinite, and consequently, $\wp _{fs}(\wp _{fs}(\wp _{fs}(\wp _{fs}(X))))$ is FSM Tarski I infinite.

Proof

Since $\wp _{fs}(\wp _{fs}(X))$ is FSM Dedekind infinite, as in the proof of Theorem 10(2) one can prove $|\wp _{fs}(\wp _{fs}(X))|+1=|\wp _{fs}(\wp _{fs}(X))|$. The result now follows directly using arithmetic properties of FSM cardinalities proved above. $\square$

In a future work we intend to prove an even stronger result claiming that $\wp _{fs}(\wp _{fs}(X))$ is FSM Tarski III infinite, and consequently, $\wp _{fs}(\wp _{fs}(\wp _{fs}(X)))$ is FSM Tarski I infinite, whenever X is an infinite finitely supported subset of an invariant set.

Corollary 17

The sets $A^{{\mathbb {N}}}_{fs}$ and ${\mathbb {N}}^{A}_{fs}$ are FSM Tarski I infinite, and so they are also Tarski III infinite.

Proof

There is an equivariant bijection $\psi$ between $(A^{{\mathbb {N}}})^{2}_{fs}$ and $A^{{\mathbb {N}} \times \{0,1\}}_{fs}$ that associates to each Cartesian pair (f, g) of mappings from ${\mathbb {N}}$ to A a mapping $h:{\mathbb {N}} \times \{0,1\} \rightarrow A$ defined as follows:

$$\begin{aligned} h(u)=\left\{ \begin{array}{ll} f(n) &{} \text {if}\, u=(n,0) ;\\ g(n) &{} \text {if}\, u=(n,1) . \end{array}\right. \end{aligned}$$

The equivariance of $\psi$ follows from Proposition 6; when $\pi \in S_{A}$, we have $\psi (\pi {\widetilde{\star }} f,$ $\pi \widetilde{\star } g)=h'$, where $h'(n,0)=(\pi {\widetilde{\star }} f)(n)=\pi (f(n))$ and $h'(n,1)=(\pi {\widetilde{\star }} g)(n)=\pi (g(n))$. Thus, $h'(u)=\pi (h(u))$ for all $u \in {\mathbb {N}} \times \{0,1\}$ which means $h'=\pi \widetilde{\star } h=\pi {\widetilde{\star }} \psi (f,g)$.

There also exists an equivariant bijection $\varphi$ between $({\mathbb {N}}^{A})^{2}_{fs}$ and $({\mathbb {N}} \times {\mathbb {N}})^{A}_{fs}$ that associates to each Cartesian pair (f, g) of mappings from A to ${\mathbb {N}}$ a mapping $h: A \rightarrow {\mathbb {N}} \times {\mathbb {N}}$ defined by $h(a)=(f(a),g(a))$ for all $a \in A$. The equivariance of $\varphi$ follows from Proposition 6; if $\pi \in S_{A}$ we have $\varphi (\pi {\widetilde{\star }} f, \pi {\widetilde{\star }} g)=h'$, where $h'(a)=((\pi {\widetilde{\star }} f)(a), (\pi {\widetilde{\star }} g)(a))=(f(\pi ^{-1}(a)), g(\pi ^{-1}(a)))=h(\pi ^{-1}(a))=(\pi {\widetilde{\star }}h)(a)$ for all $a \in A$, and so $h'=\pi {\widetilde{\star }} h=\pi {\widetilde{\star }} \varphi (f,g)$. Therefore, $|(A^{{\mathbb {N}}})^{2}_{fs}|=|A^{{\mathbb {N}} \times \{0,1\}}_{fs}| = |A^{{\mathbb {N}}}_{fs}|$. Thus, $|({\mathbb {N}}^{A})^{2}_{fs}|= |({\mathbb {N}} \times {\mathbb {N}})^{A}_{fs}|=|{\mathbb {N}}^{A}_{fs}|$ according to Proposition 10(3) and Lemma 2 (we used $|{\mathbb {N}} \times {\mathbb {N}}|=|{\mathbb {N}}|$). $\square$

Theorem 11

Let X be a finitely supported subset of an invariant set $(Y, \cdot )$. If $\wp _{fs}(X)$ is FSM Tarski I infinite, then $\wp _{fs}(X)$ is FSM Tarski III infinite. The converse does not hold.

Proof

The direct implication is a consequence of Theorem 10(1). Thus, we focus on the proof of the invalidity of the reverse implication. Firstly, we make the remark that whenever U, V are finitely supported subsets of an invariant set with $U \cap V=\emptyset$, we have that there is a finitely supported (by $supp(U) \cup supp(V)$) bijection from $\wp _{fs}(U\cup V)$ into $\wp _{fs}(U) \times \wp _{fs}(V)$ that maps each $X \in \wp _{fs}(U\cup V)$ into the pair $(X \cap U, X \cap V)$. Similarly, whenever B, C are invariant sets there is an equivariant bijection from $\wp _{fs}(B) \times \wp _{fs}(C)$ into $\wp _{fs}(B+C)$ mapping each pair $(B_{1},C_{1}) \in \wp _{fs}(B) \times \wp _{fs}(C)$ into the set $\{(0,b)\,|\,b \in B_{1}\} \cup \{(1,c)\,|\,c \in C_{1}\}$. This follows directly by verifying the conditions of Proposition 6.

Let us consider the set $A \cup {\mathbb {N}}$ which is FSM Dedekind infinite. According to Theorem 10(2), we have that $\wp _{fs}(A \cup {\mathbb {N}})$ is FSM Tarski III infinite. We prove that it is not FSM Tarski I infinite. Assume, by contradiction that $|\wp _{fs}(A \cup {\mathbb {N}}) \times \wp _{fs}(A \cup {\mathbb {N}})|=|\wp _{fs}(A \cup {\mathbb {N}})|$ which means $|\wp _{fs}(A + {\mathbb {N}}+A + {\mathbb {N}})|=|\wp _{fs}(A \cup {\mathbb {N}})|$, and so $|\wp _{fs}(A +A + {\mathbb {N}})|=|\wp _{fs}(A \cup {\mathbb {N}})|$. Thus, according to Proposition 10(4), there is a finitely supported injection from $\wp _{fs}(A + A)$ to $\wp _{fs}(A \cup {\mathbb {N}})$, which means there is a finitely supported injection from $\wp _{fs}(A) \times \wp _{fs}(A)$ to $\wp _{fs}(A) \times \wp _{fs}({\mathbb {N}})$, and so there is a finitely supported injection from $A \times A$ to $\wp _{fs}(A) \times \wp _{fs}({\mathbb {N}})$. According to Proposition 8, there should exist a finitely supported surjection $f: \wp _{fs}(A) \times \wp _{fs}({\mathbb {N}}) \rightarrow A \times A$. Let us consider two atoms $a,b\notin supp(f)$ with $a \ne b$. It follows that $(a\, b) \in Fix(supp(f))$. Since f is surjective, there exists $(X,M) \in \wp _{fs}(A) \times \wp _{fs}({\mathbb {N}})$ such that $f(X,M)=(a,b)$. According to Proposition 6 and because ${\mathbb {N}}$ is a trivial invariant set meaning that $(a\,b) \star M = M$, we have $f((a\,b) \star X,M)=f((a\,b) \otimes (X,M))=(a\,b) \otimes f(X,M)=(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,M) \ne (X,M)$, which means $(a\,b) \star X \ne X$.

We prove that if both $a,b \in supp(X)$, then $(a\,b)\star X=X$. Indeed, suppose $a,b \in supp(X)$. Since $X \in \wp _{fs}(A)$, from Proposition 5 we have that X is either finite or cofinite. If X is finite, then $supp(X)=X$, and so $a,b \in X$. 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$. 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$, which means $(a\,b)(x)=x$ for all $x \in X$, and again $(a\,b)\star X=X$.

Thus, one of a or b does not belong to supp(X). Assume $b \notin supp(X)$. Let us consider $c\ne a,b$, $c \notin supp(f)$, $c \notin supp(X)$. Then $(b\, c) \in Fix(supp(X))$, and so $(b\,c)\star X=X$. Moreover, $(b\, c) \in Fix(supp(f))$, and by Proposition 6 we have $(a,b)=f(X,M)=f((b\,c) \star X,M)=f((b\,c)\otimes (X,M))=(b\,c) \otimes f(X,M)=(b\,c) \otimes (a,b)=(a,c)$ which is a contradiction because $b\ne c$. $\square$

Proposition 18

Let X be a finitely supported subset of an invariant set $(Y, \cdot )$. If X is FSM Tarski III infinite, then there exists a finitely supported bijection $g:{\mathbb {N}} \times X \rightarrow X$. The reverse implication is also valid.

Proof

By hypothesis, there is a finitely supported bijection $\varphi :\{0,1\} \times X \rightarrow X$. Let us consider the mappings $f_{1},f_{2}: X \rightarrow X$ defined by $f_{1}(x)=\varphi (0,x)$ for all $x \in X$ and $f_{2}(x)=\varphi (1,x)$ for all $x \in X$, that are injective and supported by $supp(\varphi )$ according to Proposition 6. Since $\varphi$ is injective we also have $Im(f_{1}) \cap Im(f_{2})=\emptyset$, and because $\varphi$ is surjective we get $Im(f_{1}) \cup Im(f_{2})=X$. We prove by induction that the n-times auto-composition of $f_{2}$, denoted by $f_{2}^{n}$, is supported by $supp(f_{2})$ for all $n\in {\mathbb {N}}$. For $n=1$ this is obvious. So assume that $f_{2}^{n-1}$ is supported by $supp(f_{2})$. By Proposition 6 we must have $f_{2}^{n-1}(\sigma \cdot x)=\sigma \cdot f_{2}^{n-1}(x)$ for all $\sigma \in Fix(supp(f_{2}))$ and $x \in X$. Let us fix $\pi \in Fix(supp(f_{2}))$. According to Proposition 6, we have $f_{2}^{n}(\pi \cdot x)=f_{2}(f_{2}^{n-1}(\pi \cdot x))=f_{2}(\pi \cdot f_{2}^{n-1}(x))=\pi \cdot f_{2}(f_{2}^{n-1}(x))=\pi \cdot f_{2}^{n}(x)$ for all $x \in X$, and so $f_{2}^{n}$ is finitely supported from Proposition 6. Define $f:{\mathbb {N}} \times X \rightarrow X$ by $f((n,x))=f_{2}^{n}(f_{1}(x))$. Let $\pi \in Fix(supp(f_{1}) \cup supp(f_{2}))$. According to Proposition 6 and since $({\mathbb {N}}, \diamond )$ is a trivial invariant set, we get $f(\pi \otimes (n,x))=f((n, \pi \cdot x))=f_{2}^{n}(f_{1}(\pi \cdot x))=f_{2}^{n}(\pi \cdot f_{1}(x))=\pi \cdot f_{2}^{n}(f_{1}(x))=\pi \cdot f((n,x))$ for all $(n,x) \in {\mathbb {N}} \times X$, which means that f is supported by $supp(f_{1}) \cup supp(f_{2})$. We prove the injectivity of f. Assume $f((n,x))=f((m,y))$ which means $f_{2}^{n}(f_{1}(x))=f_{2}^{m}(f_{1}(y))$. If $n>m$ this leads to $f_{2}^{n-m}(f_{1}(x))=f_{1}(y)$ (since $f_{2}$ is injective) which is in contradiction with the relation $Im(f_{1}) \cap Im(f_{2})=\emptyset$. Similarly, we cannot have $n<m$. Thus, $n=m$ which leads to $f_{1}(x)=f_{1}(y)$, and so $x=y$ due to the injectivity of $f_{1}$. Therefore, f is injective. Since we obviously have a finitely supported injection from X into ${\mathbb {N}} \times X$ (e.g $x \mapsto (0,x)$ which is supported by supp(X)), in the view of Lemma 2 we can find a finitely supported bijection between X and ${\mathbb {N}} \times X$.

The reverse implication is almost trivial. There is a finitely supported injection from $\{0,1\} \times X$ into ${\mathbb {N}} \times X$. If there is a finitely supported injection from ${\mathbb {N}} \times X$ into X, then there is a finitely supported injection from $\{0,1\} \times X$ into X. The desired result follows from Lemma 2. $\square$

5 Countability in FSM

Definition 9

Let Y be a finitely supported subset of an invariant set X. Then Y is countable in FSM (or FSM countable) if there exists a finitely supported onto mapping $f: {\mathbb {N}} \rightarrow Y$.

Proposition 19

Let Y be a finitely supported countable subset of an invariant set $(X, \cdot )$. Then Y is uniformly supported.

Proof

There exists a finitely supported onto mapping $f: {\mathbb {N}} \rightarrow Y$. Thus, for each arbitrary $y\in Y$, there exists $n \in {\mathbb {N}}$ such that $f(n)=y$. According to Proposition 6, for each $\pi \in Fix(supp(f))$ we have $\pi \cdot y=\pi \cdot f(n)=f(\pi \diamond n)=f(n)=y$, where $\diamond$ is the necessarily trivial action on ${\mathbb {N}}$. Thus, Y is uniformly supported by supp(f). $\square$

Proposition 20

Let Y be a finitely supported subset of an invariant set X. Then Y is countable in FSM if and only if there exists a finitely supported one-to-one mapping $g: Y \rightarrow {\mathbb {N}}$.

Proof

Suppose that Y is countable in FSM. Then there exists a finitely supported onto mapping $f: {\mathbb {N}} \rightarrow Y$. We define $g: Y \rightarrow {\mathbb {N}}$ by $g(y)=min[f^{-1}(\{y\})]$, for all $y \in Y$. According to Proposition 6, g is supported by $supp(f) \cup supp(Y)$. Obviously, g is one-to-one. Conversely, if there exists a finitely supported one-to-one mapping $g: Y \rightarrow {\mathbb {N}}$, then g(Y) is supported is equivariant as a subset of the trivial invariant set ${\mathbb {N}}$. Thus, there exists a finitely supported bijection $g: Y \rightarrow g(Y)$, where $g(Y) \subseteq {\mathbb {N}}$. We define $f: {\mathbb {N}} \rightarrow Y$ by

$$\begin{aligned} f(n)=\left\{ \begin{array}{ll} g^{-1}(n) &{} \text {if}\, n \in g(Y) \\ t &{} \text {if}\, n \in {\mathbb {N}} {\setminus } g(Y) \end{array}\right. , \end{aligned}$$

where t is a fixed element of Y. According to Proposition 6, we have that f is supported by $supp(g) \cup supp(Y) \cup supp(t)$. Moreover, f is onto. $\square$

Proposition 21

Let Y be an infinite, finitely supported, countable subset of an invariant set X. Then there exists a finitely supported bijective mapping $g: Y \rightarrow {\mathbb {N}}$.

Proof

First we prove that for any infinite subset B of ${\mathbb {N}}$, there is an injection from ${\mathbb {N}}$ into B. Fix such a B. It follows that B is well-ordered. Define $f:{\mathbb {N}} \rightarrow B$ by: $f(1)=min(B)$, $f(2)=min(B {\setminus } f(1))$, and recursively $f(m)= min(B {\setminus } \{f(1),f(2),...,f(m-1)\})$ for all $m \in {\mathbb {N}}$ (since B is infinite). Since ${\mathbb {N}}$ is well-ordered, choice is not involved. Obviously since both B and ${\mathbb {N}}$ are trivial invariant sets, we have that f is equivariant. Since B is a subset of ${\mathbb {N}}$ we also have an equivariant injective mapping $h:B \rightarrow {\mathbb {N}}$. According to Lemma 1, there is an equivariant bijection between B and ${\mathbb {N}}$ (we can even prove that f is bijective).

Since Y is countable, there exists a finitely supported one-to-one mapping $u: Y \rightarrow {\mathbb {N}}$. Thus, the mapping $u: Y \rightarrow u(Y)$ is finitely supported and bijective. Since $u(Y) \subseteq N$, we have that there is an equivariant bijection v between u(Y) and ${\mathbb {N}}$, and so there exists a finitely supported bijective mapping $g: Y \rightarrow {\mathbb {N}}$ defined by $g=v \circ u$.

$\square$

From [1] we know that the (in)consistency of the choice principle $\mathbf{CC}(fin)$ in FSM is an open problem, meaning that we do not know whether this principle is consistent or not with respect to the FSM axioms. A relationship between countable union principles and countable choice principles is presented in ZF in [6]. Below we prove that such a relationship is preserved in FSM.

Definition 10

• 1. The Countable Choice Principle for finite sets in FSM CC(fin) has the form “Given any invariant set X, and any countable family ${\mathcal {F}}=(X_{n})_{n}$ of finite subsets of X such that the mapping $n\mapsto X_{n}$ is finitely supported, there exists a finitely supported choice function on ${\mathcal {F}}$."

• 2. The Countable Union Theorem for finite sets in FSM, CUT(fin), has the form “Given any invariant set X and any countable family ${\mathcal {F}}=(X_{n})_{n}$ of finite subsets of X such that the mapping $n\mapsto X_{n}$ is finitely supported, then there exists a finitely supported onto mapping $f: {\mathbb {N}} \rightarrow \underset{n}{\cup }X_{n}$".

• 3. The Countable Union Theorem for k-element sets in FSM, CUT(k), has the form “Given any invariant set X and any countable family ${\mathcal {F}}=(X_{n})_{n}$ of k-element subsets of X such that the mapping $n\mapsto X_{n}$ is finitely supported, then there exists a finitely supported onto mapping $f: {\mathbb {N}} \rightarrow \underset{n}{\cup }X_{n}$".

• 4. The Countable Choice Principle for sets of k-element sets in FSM, CC(k) has the form “Given any invariant set X, and any countable family ${\mathcal {F}}=(X_{n})_{n}$ of k-element subsets of X in FSM such that the mapping $n\mapsto X_{n}$ is finitely supported, there exists a finitely supported choice function on ${\mathcal {F}}$".

Proposition 22

In FSM, the following equivalences hold.

• 1. CUT(fin) $\Leftrightarrow$ CC(fin);

• 2. CUT(2) $\Leftrightarrow$ CC(2);

• 3. CUT(n) $\Leftrightarrow$ CC(i) for all $i \le n$.

Proof

1. Let us assume that CUT(fin) is valid in FSM. We consider the finitely supported countable family ${\mathcal {F}}=(X_{n})_{n}$ in FSM, where each $X_{n}$ is a non-empty finite subset of an invariant set X in FSM. From CUT(fin), there is a finitely supported onto mapping $f: {\mathbb {N}} \rightarrow \underset{n}{\cup }X_{n}$. Since f is onto and each $X_{n}$ is non-empty, we have that $f^{-1}(X_{n})$ is a non-empty subset of ${\mathbb {N}}$ for each $n\in {\mathbb {N}}$. Consider the function $g: {\mathcal {F}} \rightarrow \cup {\mathcal {F}}$, defined by $g(X_{n})=f(min[f^{-1}(X_{n})])$. We claim that $supp(f) \cup supp(n \mapsto X_{n})$ supports g. Let $\pi \in Fix(supp(f) \cup supp(n \mapsto X_{n}))$. According to Proposition 6, because ${\mathbb {N}}$ is a trivial invariant set and each element $X_{n}$ is supported by $supp(n \mapsto X_{n})$, we have $\pi \cdot g(X_{n})=\pi \cdot f(min[f^{-1}(X_{n})])= f(\pi \diamond min[f^{-1}(X_{n})])=f(min[f^{-1}(X_{n})])=g(X_{n})=g(\pi \star X_{n})$, where by $\star$ we denoted the $S_{A}$-action on ${\mathcal {F}}$, by $\cdot$ we denoted the $S_{A}$-action on $\cup {\mathcal {F}}$ and by $\diamond$ we denoted the trivial action on ${\mathbb {N}}$. Therefore, g is finitely supported. Moreover, $g(X_{n}) \in X_{n}$, and so g is a choice function on ${\mathcal {F}}$.

Conversely, let ${\mathcal {F}}=(X_{n})_{n}$ be a countable family of finite subsets of X such that the mapping $n\mapsto X_{n}$ is finitely supported. Thus, each $X_{n}$ is supported by the same set $S=supp(n \mapsto X_{n})$. Since each $X_{n}$ is finite (and the support of a finite set coincides with the union of the supports of its elements) we have that $Y=\underset{n \in {\mathbb {N}}}{\cup }X_{n}$ is uniformly supported by S. Moreover, the countable sequence $(Y_{n})_{n \in {\mathbb {N}}}$ defined by $Y_{n}=X_{n} {\setminus } \underset{m<n}{\cup }X_{m}$ is a uniformly supported (by S) sequence of pairwise disjoint uniformly supported sets with $Y=\underset{n \in {\mathbb {N}}}{\cup }Y_{n}$. Consider the infinite family $M \subseteq {\mathbb {N}}$ such that all the terms of $(Y_{n})_{n \in M}$ are non-empty.

For each $n \in M$, the set $T_{n}$ of total orders on $Y_{n}$ is finite, non-empty, and uniformly supported by S. Thus, by applying CC(fin) to $(T_{n})_{n \in M}$, there is a choice function f on $(T_{n})_{n \in M}$ which is also supported by S. Furthermore, $f(T_{n})$ is supported by $supp(f) \cup supp(T_{n})=S$ for all $n \in M$. One can define a uniformly supported (by S) total order relation on Y (which is also a well-order relation on Y) as follows $x \le y$ if and only if $\left\{ \begin{array}{ll} x \in Y_{n} \; \text {and}\; y \in Y_{m} \;\text {with}\; n<m \\ \text {or}\\ x,y \in Y_{n}\; \text {and}\; xf(T_{n})y . \end{array}\right.$

Clearly, if Y is infinite, then there is an S-supported order isomorphism between $(Y, \le )$ and M with the natural order, which means, according to Proposition 21, that Y is countable.

2. As in the above item $\mathbf{CUT}(2) \Rightarrow \mathbf{CC}(2)$.

For proving $\mathbf{CC}(2) \Rightarrow \mathbf{CUT}(2)$, let ${\mathcal {F}}=(X_{n})_{n}$ be a countable family of 2-element subsets of X such that the mapping $n\mapsto X_{n}$ is finitely supported. According to CC(2) we have that there exists a finitely supported choice function g on $(X_{n})_{n}$. Let $x_{n}=g(X_{n}) \in X_{n}$. As in the above item, we have that $supp(n \mapsto X_{n})$ supports $x_{n}$ for all $n \in {\mathbb {N}}$. For each n, let $y_{n}$ be the unique element of $X_{n}{\setminus } \{x_{n}\}$. Since for any n both $x_{n}$ and $X_{n}$ are supported by the same set $supp(n \mapsto X_{n})$, it follows that $y_{n}$ is also supported by $supp(n \mapsto X_{n})$ for all $n \in {\mathbb {N}}$.

Define $f: {\mathbb {N}} \rightarrow \underset{n}{\cup }X_{n}$ by $f(n)=\left\{ \begin{array}{ll} x_{\frac{n}{2}} &{} \text {if}\, n \;\text {is even}\\ y_{\frac{n-1}{2}} &{} \text {if}\, n \;\text{ is } \text{ odd } \end{array}\right.$. We can equivalently describe f as being defined by $f(2k)=x_{k}$ and $f(2k+1)=y_{k}$. Clearly, f is onto. Furthermore, because all $x_{n}$ and all $y_{n}$ are uniformly supported by $supp(n \mapsto X_{n})$, we have that $f(n)=\pi \cdot f(n)$, for all $\pi \in Fix(supp(n \mapsto X_{n}))$ and all $n \in {\mathbb {N}}$. According to Proposition 6, we obtain that f is also supported by $supp(n \mapsto X_{n})$, and so $\underset{n}{\cup }X_{n}$ is FSM countable.

Fig. 1

Relationships between various forms of infinity in FSM

3. Similar to the proof of item 1. $\square$

We can note that under $\mathbf{CC}(fin)$ a finitely supported subset X of an invariant set is FSM Dedekind infinite if and only if $\wp _{fin}(X)$ is FSM Dedekind infinite.

Proposition 23

Let Y be a finitely supported countable subset of an invariant set X. Then the set $\underset{n \in {\mathbb {N}}}{\cup }Y^{n}$ is countable, where $Y^{n}$ is the n-time Cartesian product of Y.

Proof

Since Y is countable, we can order it as a sequence $Y=\{x_{1}, \ldots , x_{n}, \ldots \}$. The other sets of form $Y^{k}$ are uniquely represented with respect to the previous enumeration of the elements of Y. Since Y is finitely supported and countable, all the elements of Y are supported by the same set S of atoms. Thus, in the view of Proposition 3, all the elements of $Y^{k}$ are supported by S for each $k \in {\mathbb {N}}$. Fix $n \in {\mathbb {N}}$. On $Y^{n}$ define the S-supported strict well-order relation $\sqsubset$ by $(x_{i_{1}}, x_{i_{2}}, \ldots , x_{i_{n}}) \sqsubset (x_{j_{1}}, x_{j_{2}}, \ldots , x_{j_{n}})$

if and only if $\left\{ \begin{array}{ll} i_{1}< j_{1} \ \text { or}\\ i_{1}=j_{1}\; \text {and}\; i_{2}<j_{2} \ \text { or}\\ \ldots \ \text { or}\\ i_{1}=j_{1}, \ldots , i_{n-1}=j_{n-1}\; \text {and}\; i_{n}<j_{n} . \end{array}\right.$

Now, we define an S-supported strict well-order relation $\prec$ on $\underset{n \in {\mathbb {N}}}{\cup }Y^{n}$ by

$u \prec v$ if and only if $\left\{ \begin{array}{ll} u \in Y^{n} \; \text {and}\; v \in Y^{m} \;\text {with}\; n<m \\ \text {or}\\ u,v \in Y_{n}\; \text {and}\; u \sqsubset v . \end{array}\right.$ Thus, there is an S-supported order isomorphism between $(\underset{n \in {\mathbb {N}}}{\cup }Y^{n},\prec )$ and $({\mathbb {N}},<)$. $\square$

6 Conclusion

In this paper we study infinite cardinalities of finitely supported structures. For two finitely supported sets X and Y we say that they have the same cardinality, i.e. $|X|=|Y|$, if and only if there exists a finitely supported bijection $f:X \rightarrow Y$. This equivalence relation is well-defined in FSM according to Theorem 1. We are able to prove that the relation $\le$ on FSM cardinalities (where the cardinalities are ordered via finitely supported injective mappings) is well-defined, equivariant, reflexive, anti-symmetric and transitive, but it is not total, while the relation $\le ^{*}$ on FSM cardinalities (where the cardinalities are ordered via finitely supported surjective mappings) is well-defined, equivariant, reflexive and transitive, but it is not anti-symmetric, nor total. Operations on cardinalities such as sum, product and exponential can be well-defined in FSM and their properties are studied in Proposition 9 and Proposition 10. Several other properties of cardinalities are also mentioned in Sect. 3.

In Fig. 1 we summarize the relationship results between the FSM definitions of infinity proved in this paper. The ‘ultra thick arrows’ symbolize strict implications (of from p implies q, but q does not imply p), while ‘thin dashed arrows’ symbolize implications for which is not proved yet if they are strict or not (the validity of the reverse implications follows when assuming choice principles over non-atomic ZF sets; see Remark 3). ‘Thick arrows’ match equivalences.

We study various forms of infinity (of Tarski type, Dedekind type, Mostowski type, ...), and provide several relationship results between them. The idea of presenting various approaches regarding ‘infinity’ belongs to Tarski who formulates in 1924 several definitions of infinite. The independence of these definitions was later proved in set theory with atoms by Levy [8]. Such independence results can be transferred into classical ZF set theory by employing Jech-Sochor’s embedding theorem stating that permutation models of set theory with atoms can be embedded into symmetric models of ZF, and so a statement which holds in a given permutation model of set theory with atoms and whose validity depend only on a certain fragment of that model, also holds in some well-founded model of ZF. In this paper we emphasized the connections and differences between various definitions of infinity internally in FSM. By presenting examples of atomic sets that satisfy a certain form of infinity, while they do not satisfy other forms of infinity, we were able to conclude that the FSM definitions of infinity are pairwise non-equivalent.

We particularly focused on the notion of FSM Dedekind infinity, and we proved a full characterization of FSM Dedekind (in)finite sets. The notion of Dedekind infinity is related to the notion of uniform support. Uniformly supported sets are of interest because they involve boundedness properties of supports, meaning that the support of each element in a uniformly supported set is contained in the same finite set of atoms; in this way, all the individuals in an infinite uniformly supported family can be characterized by involving only the same finitely many characteristics. Those sets that do not contain infinite uniformly supported subsets are also of interest since they are FSM Dedekind finite, and for them several properties such as fixed point properties, stability properties, calculability properties, or approximation properties could be proved; this will be the topic of a future work.

We proved (see Theorem 7 and Corollary 4) that the set of all finitely supported functions from $A^{n}$ (with n an arbitrary positive integer) to an FSM set that does not contain an infinite uniformly supported subset also does not contain an infinite uniformly supported subset, and so it is Dedekind finite, although this set seems to be ‘very large’ since it is constructed as a function space on two infinite sets. Particularly, $A^{A^{n}}_{fs}$, $\wp _{fs}(A)^{A^{n}}_{fs}$, $T_{fin}(A)^{A^{n}}_{fs}$ are FSM Dedekind finite. Such properties extend related properties presented by the authors in [2] or [3]. The notion of ‘countability’ is described in Sect. 5, where we present connections between countable choice principles and countable union theorems within finitely supported sets.

In the following table we present the forms of infinity satisfied by the classical infinite atomic sets in Finitely Supported Mathematics, such as the set of atoms, its (finite) powerset, the set of all finite injective tuples of atoms, the set of all finitely supported functions from the set of atoms to its powerset, the powerset of the n-times Cartesian product of the set of atoms, the union and the Cartesian product between the set of atoms and a non-atomic set, the powerset of the union between the set of atoms and a non-atomic set, the set of all finitely supported functions between the set of atoms and a non-atomic set, the second-order powerset of atoms, etc.

Set	TI i	TIII i	D i	M i	Asc i	TII i	N-am
A	No	No	No	No	No	No	No
$A+A$	No	No	No	No	No	No	Yes
$A \times A$	No	No	No	No	No	No	Yes
$\wp _{fin}(A)$	No	No	No	No	Yes	Yes	Yes
$T_{fin}(A)$	No	No	No	No	Yes	Yes	Yes
$\wp _{fs}(A)$	No	No	No	No	Yes	Yes	Yes
$\wp _{fin}(\wp _{fs}(A))$	No	No	No	No	Yes	Yes	Yes
$A^{A^{n}}_{fs}$	No	No	No	No	Yes	Yes	Yes
$T_{fin}(A)^{A^{n}}_{fs}$	No	No	No	No	Yes	Yes	Yes
$\wp _{fs}(A)^{A^{n}}_{fs}$	No	No	No	No	Yes	Yes	Yes
$\wp _{fs}(A^{n})$	No	No	No	No	Yes	Yes	Yes
$A \cup {\mathbb {N}}$	No	No	Yes	Yes	Yes	Yes	Yes
$A \times {\mathbb {N}}$	No	Yes	Yes	Yes	Yes	Yes	Yes
$\wp _{fs}(A \cup {\mathbb {N}})$	No	Yes	Yes	Yes	Yes	Yes	Yes
$\wp _{fs}(\wp _{fs}(A))$	?	Yes	Yes	Yes	Yes	Yes	Yes
$A^{{\mathbb {N}}}_{fs}$	Yes	Yes	Yes	Yes	Yes	Yes	Yes
${\mathbb {N}}^{A}_{fs}$	Yes	Yes	Yes	Yes	Yes	Yes	Yes