Get 20M+ Full-Text Papers For Less Than $1.50/day. Start a 14-Day Trial for You or Your Team.

Learn More →

Permutative Renamings in the Extended Fraenkel-Mostowski Set Theory

Permutative Renamings in the Extended Fraenkel-Mostowski Set Theory In the new framework of the extended Fraenkel-Mostowski set theory, we define an extended interchange function as an action on a permutation group, and a new notion of permutative renaming by generalizing an existing notion of finitary permutative renaming. Some algebraic and combinatorial properties of permutative renamings expressed by using the Fraenkel-Mostowski axioms remain valid in the new framework even if we replace one axiom with a weaker axiom. Mathematics Subject Classification 2010: 03E25, 03E30, 03B70. Key words: finite support axiom, extendend Fraenkel-Mostowski framework, permutative renamings. 1. Introduction Renaming the variables of an expression in a way that preserves its meaning is called -renaming. Some of the subtleties related to -renaming can be described by using the abstraction operation of the -calculus, together with the operation of application. Application and abstraction work together according to the -rule (x.M ) N = M [x := N ]. Abstraction x. M [x] binds a free variable x in M . Substitution [x := N ] is only performed for free occurrences of x. In order to avoid ambiguities, it is assumed that the bound variables occurring in a certain expression are different from the free ones, and this can be obtained by renaming bound variables. The expressions differing only in the names used for bound variables are identified by -equivalence. A correct variable renaming is one that preserves the -equivalence class of the expression. The notion of choosing a fresh name often arises when manipulating syntactic expressions; therefore it is necessary to indicate some constraints whenever describing such a syntactic manipulation. Often it is just said that a name is fresh without specifying any restrictions. In such a case, we mean that the fresh name must be different from any name occurring anywhere else in the expression or program. Some programming systems have mechanisms for renaming, for binding a name with a value and for managing sets of such bindings. Modern programming languages are designed to manage bindings and fresh names by using the notions of scopes, workspaces, or environments. Since renaming, binding and fresh names appear in several approaches, it became evident that they deserve to be studied in their own terms. The nominal logic and semantics was presented by Gabbay and Pitts in [5, 7]; it uses the Fraenkel-Mostowski (FM) axioms of set theory. The FM set theory was originally developed to prove the independence of the Axiom of Choice (AC) from the other axioms of the Zermelo-Fraenkel (ZF) set theory. It was rediscovered and used by Gabbay and Pitts [5] to model the syntax of formal systems involving variable binding operations. An advantage of modeling syntax in a model of FM set theory is that datatypes of syntax modulo -equivalence can be modeled inductively. This is because nominal set theory delivers a model of variable symbols and -abstraction. The FM axioms are precisely the Zermelo-Fraenkel with atoms (ZFA) axioms over an infinite set of atoms [5], together with the special axiom of finite support which claims that for each element x in an arbitrary set we can find a finite set supporting x. In [1] we generalized the FM set theory by giving a new set of axioms which defines the Extended Fraenkel-Mostowski (EFM) set theory. The finite support axiom in the description of the FM set theory was replaced in [1] by a weaker axiom which requires only a certain structure of the set of atoms. Many algebraic properties of sets, which are valid in the FM framework, remain valid also in the EFM framework. In this paper we analyze how some classical results of nominal logic are changed (or not) when we work in the EFM framework instead of the FM framework, and how some results obtained in the EFM set theory can be translated to the FM set theory. We naturally extend some notions and results of nominal logic, and together with some mathematical properties obtained in [1] and some additional combinatorial results which are proved without using the axiom of choice, we are able now to give some new properties of the interchange function and permutative renamings. The structure of the paper is as follows. Section 2 presents formal definitions related to permutative renamings and extended interchange function. In Section 3 we present several group theory and combinatorial results applied in the nominal logic. These results allow us to solve some counting problems involving renamings. Some properties of permutative renamings which are valid in FM approach can be extended in EFM approach, even if in EFM we assume only a weaker axiom 11' instead of the finite support property in FM set theory. In Section 4, using group theory, we present some algebraic properties of the (domain of the) extended interchange function. Some connections between old and new results are presented in Section 5. Conclusions end the paper. 2. Renamings in the extended Fraenkel-Mostowski framework We remind several definitions and results from [1]. Let A be an infinite set of atoms (also called names). A is characterized by the axiom "y x x A" which means that only non-atoms can have / elements. Definition 2.1. i) A transposition is a function (a b) : A A with the property (a b)(a) = b, (a b)(b) = a and (a b)(n) = n for n = a, b. ii) A permutation of A is a bijection from A to A. iii) A substitution is a function {b|a} : A A with the property {b|a}(n) = n if n = a and {b|a}(a) = b. Let SA be the set of all permutations over A. SA is a group. Let SA be the group of finitary permutations (i.e the group of permutations which leave unchanged all but finitely many atoms). In fact SA is the set of all functions generated by composing finitely many transpositions. For S A, we denote by F ix(S) the set { | (a) = a for all a S}. Definition 2.2. · Let X be a set defined by the axioms of ZFA set theory. An interchange function over X is a function · : SA × X X defined inductively by · a = (a) for all atoms a A, and by · x = { · y | y x} otherwise. Moreover, it satisfies the following axiom: for each x X, there exists a finite nonempty set S A such that for each F ix(S) SA we have · x = x. · An FM set is a pair (X, ·), where X is a set defined in the ZFA set theory without axiom of choice, and · : SA × X X is an interchange function over X. We simply use X whenever no confusion arises. Definition 2.3. Let X be an FM set. We say that S A supports x whenever for each F ix(S) SA we have · x = x. The properties of the interchange function allow always to find a finite set supporting x; in fact this assertion is an axiom (axiom 11) in the description of the FM set theory. The new notion of "extended interchange function" was introduced in [1]. Definition 2.4. · Let X be a set defined by the axioms of ZFA set theory. An extended interchange function over X is a function · : SA × X X defined inductively by · a = (a) for all atoms a A, and by · x = { · y | y x} otherwise. Moreover, each subset of A is either finite or cofinite. · An EFM set is a pair (X, ·), where X is a set defined in the ZFA set theory without choice, and · : SA ×X X is an extended interchange function on X. We simply use X whenever no confusion arises. Remark 2.1. Since SA is a group, the interchange function and the extended interchange function · : SA × X X are actions of the group SA on the set X; we have Id · x = x and · · x = ( ) · x for all , SA and all x X. Example 2.1. 1. The set A of atoms is both an FM set and an EFM set (when each subset of A is either finite of cofinite) with interchange function, respectively extended interchange function given by · a = (a), SA , a A. 2. The set SA is both an FM set and an EFM set (when each subset of A is either finite of cofinite) with the interchange function, respectively extended interchange function given by · := -1 for all SA and SA . (SA , ·) is an FM set because for each SA we have that the finite set {a A | (a) = a} supports . 3. The set SA is an EFM set (when each subset of A is either finite of cofinite) with the extended interchange function given by · := -1 for all , SA . We present the axiomatic descriptions of both the Fraenkel-Mostowski [5] and Extended Fraenkel-Mostowski [1] set theories. The following axioms describes completely the Fraenkel-Mostowski set theory: 1. x.(y.y x) x A / (only non-atoms can have elements) 2. x, y.(x A and y A and z.(z x z y)) x = y / / (axiom of extensionality) 3. x, y.z.z = {x, y} 4. x.y.y = {z | z x} 5. x.y.y A and y = {z | w.(z w and w x)} / (axiom of pairing) (axiom of powerset) (axiom of union) 6. x.y.(y A and y = {f (z) | z x}), for each functional formula f (z) / (axiom of replacement) 7. x.y.(y A and y = {z | z x and p(z)}), for each formula p(z) / (axiom of separation) 8. (x.(y x.p(y)) p(x)) x.p(x) 9. x.( x and (y.y x y {y} x)) 10. A is not f inite 11. x.S A.S is f inite and S supports x (the finite support property) Therefore, we can see the FM set theory like the ZFA set theory over an infinite set A of atoms infinite and with an additional property of finite support. The following axioms describes completely the Extended Fraenkel-Mostowski set theory: 1. x.(y.y x) x A / (only non-atoms can have elements) (induction principle) (axiom of infinite) 2. x, y.(x A and y A and z.(z x z y)) x = y / / (axiom of extensionality) 3. x, y.z.z = {x, y} (axiom of pairing) 4. x.y.y = {z | z x} 5. x.y.y A and y = {z | w.(z w and w x)} / (axiom of powerset) (axiom of union) 6. x.y.(y A and y = {f (z) | z x}), for each functional formula f (z) / (axiom of replacement) 7. x.y.(y A and y = {z | z x and p(z)}), for each formula p(z) / (axiom of separation) 8. (x.(y x.p(y)) p(x)) x.p(x) 9. x.( x and (y.y x y {y} x)) 10. A is not f inite 11'. Each subset of A is either f inite or cof inite (axiom of the structure of A) Therefore, the Extended Fraenkel-Mostowski (EFM) set theory is similar to the ZFA set theory over an infinite set A of atoms infinite, having the additional property that each subset of A is either finite or cofinite. Remark 2.2. Axiom 11' of the EFM set theory is a direct consequence of axiom 11 of the FM set theory (see Example 2 from [1]). Thus, the EFM set theory is a natural extension of the FM set theory; an interchange function can be seen as an extended interchange function, and an FM set can be seen as an EFM set. Both in the FM framework and in the EFM framework, each subset of A is either finite or cofinite [1]. This structure of the atoms set A allows us to say that the axiom of choice fails both in the FM framework and in the EFM framework. More details are in [1]. We make the remark that, even the axiom of choice fails in the FM and EFM approach, a weaker form of the axiom of choice (where the choice is made from finite families) is valid. Remark 2.3. The axiom of choice says that, for each family F of nonempty disjoint sets, we can find a system of representatives, namely a set that contains exactly one element from each set in F. If F is a finite family of disjoint nonempty sets, this statement is a consequence of axioms (induction principle) (axiom of infinite) 1-9 (and does not involve the axiom of choice). Indeed, if F contains only one nonempty set U , then we can find an element x0 U (because U is nonempty). According to the axiom of pairing, we obtain the set {x0 } which is a set of representatives for F. According to the induction principle, we can obtain a set of representatives for each finite family F of disjoint nonempty sets. Now we generalize the notion of finitary permutative renaming. In this paper we deal with renamings induced by permutations, and not with renamings induced by substitutions and substitution actions (these renamings are presented in several papers of M.Gabbay and A.Pitts). In fact, a link between these viewpoints is given by the fact that for a -calculus expression t and two atoms a and b, we get {b|a}t = (b a) · t for b f n(t) (the / case {b|a}t for b f n(t) is explained in [4], and it is not considered here). Definition 2.5. Let x be an element of an EFM set X. A permutative renaming of x is an element of the form ·x, where SA and · : SA ×X X is an extended interchange function on X. The same definition can be used to characterize the permutative renamings of elements from an FM set. In the FM universe only finitely supported objects are allowed. According to Example 2.1 (3) we know that SA is an EFM set (when each subset of A is either finite or cofinite). For each SA we have that {a A | (a) = a} is the least set supporting in the sense of Definition 2.3. If we assume the supplementary axiom of finite support (axiom 11) we must have that {a A | (a) = a} is finite. Hence, in the FM framework, each permutation in SA have to be finitary which means that SA coincides with SA in FM. If x is an element of an FM set X, then a permutative renaming of x is an element of the form · x, where SA and · : SA × X X is an interchange function on X. Our intuition says that a permutative renaming of x in FM framework is of the form (a b) · x, where a, b A and (a b) · x is denoting the result of interchanging a and b in x. If a permutation is a composition of many transpositions, then · x is also a permutative renaming of x. For example, ((c d) (a b)) · x denotes the result of of interchanging c and d in (a b) · x, where (a b) · x is defined before. In the EFM framework we eliminate the finite support property (axiom 11), and hence we allow the presence of nonfinitary permutations. It is natural to define the permutative renamings of an element x as the elements of form · x, where SA , even if SA is different from SA in the EFM framework. By now on, the permutative renamings are simply called renamings. Remark 2.4. It is worth noting that M.Gabbay and A.Pitts work with permutations obtained by composing finitely many transpositions. In this section, since we eliminate the finite support property from the FM axioms, we work in the general case where SA is the set of all bijections from A to A, X is an EFM set and the extended interchange function is defined on SA not only on SA (like in [4, 5]). A permutative renaming in our approach is of the form · x, where SA . The particular class of finitary permutative renamings (namely the class of permutative renamings under the action ·|SA ) is well described in [4]. The notion of permutative renaming defined in [4] is a particular case of the notion of permutative renaming defined by Definition 2.5. 3. Combinatorial properties of permutative renamings We present several counting problems on renamings using the algebraic properties of EFM sets described in [1] and some combinatorial results which can be proved without using the axiom of choice. Let G be a subgroup of SA . Definition 3.1. 1. The representation of SA by permutations of the EFM set X is a group homomorphism : SA S(X) given by ()(x) = · x. 2. Let x and y be elements of an EFM set X. (a) x and y are called equivalent, and denote this by x y, whenever we can obtain one from another by a renaming. (b) x and y are called equivalent under permutations in G, and denote this by x G y, whenever we can obtain one from another by a renaming under a permutation in G (i.e. if there is G such that y = · x). 3. Let X be an EFM set. (a) REN (x) = { · x | SA } is the set of all renamings of x; we also say that REN (x) is a class of renamings in X. (b) RENG (x) = { · x | G} is the set of all renamings of x under the permutations in G; we also say that RENG (x) is a class of renamings in X under permutations in G. A renaming of an (arbitrary) atom under the permutations in G is called a G-renaming. 4. Let X be an EFM set. (a) IREN (x) = { SA | · x = x} is the set of permutations for which we obtain an invariant renaming of x (a renaming which keeps x unchanged). (b) IRENG (x) = { G | · x = x} is the set of permutations in G for which we obtain an invariant renaming of x. 5. Let X be an EFM set. (a) An element x X for which IREN (x) = SA is called invariant on all renamings. The set of elements in X which are invariants on all renamings is denoted by IRN (X). (b) An element x X for which IRENG (x) = G is called invariant on renamings under permutations in G. The set of elements in X which are invariants on renamings under permutations in G is denoted by IRNG (X). Let X be an EFM set, and G SA . From the general theory of group actions we have the following results which we present without proofs. Proposition 3.1. 1. G is an equivalence relation on X. 2. RENG (x) is the equivalence class of x modulo G which is the orbit of the element x under the action · : G × X X defined as the extended interchange function. 3. In terms of group theory, IREN (x) is the stabilizer of x under the extended interchange function, and IRENG (x) is the stabilizer of x under the action · : G × X X defined as the extended interchange function. A trivial consequence is that IRENG (x) G. Remark 3.1. If G is a finite subgroup of SA , we denote by IRENG (x) the left cosets modulo IRENG (x). A function : {IRENG (x) | G} - RENG (x) defined by (IRENG (x)) = · x is well defined, and it is a bijection. Thus, |RENG (x)| = [G : IRENG (x)]. Proposition 3.2. Let G be a finite subgroup of SA and X a finite EFM set. Let S be a system of representatives for classes of renamings in X under permutations in G, with at least two elements; such a system S exists because X is finite, and the axiom of choice is not requested (see Remark 2.3). Then, by using the classes equation in group theory, |X| = |IRNG (X)| + |RENG (x)| = |IRNG (X)| + [G : IRENG (x)] = |IRNG (X)| + |G| |IRENG (x)| Let IREN () be the set of invariants x X under , i.e., IREN () = {x X | · x = x}. If X is an FM set we say that S A supports x whenever for each F ix(S) SA we have · x = x. If X is a finite FM set, F ix(S) and S supports each x X, then IREN () = X. Let G SA be a finite group of permutations. Then we can find the number of orbits under the extended interchange function for finite EFM sets, even though we work in a set theory without the axiom of choice Proposition 3.3. Let X be a finite EFM set. If G SA is finite, the number k of classes of renamings in X under the permutations in G (i.e., the number k of orbits in X under the action · : G × X X) is k= 1 |G| |IREN ()| Proof. Let M = {(, x) G × X | · x = x}. We express |M | in two ways. We can build sets of representatives for finite families by using axioms 1-9 (see Remark 2.3). We have (, x) M iff IRENG (x), and so M is the disjoint union of the sets IRENG (x) × {x} (x X). Since X is finite, there is only a finite number of such sets. Using Lagrange Theorem for finite groups and Remark 3.1, (1) |M | = |IRENG (x)| = |G| = [G : IRENG (x)] |G| |RENG (x)| By Proposition 3.1, the classes of renamings in X are orbits in X under the action · : G × X X defined as an extended interchange function. If these orbits are X1 , X2 , ..., Xk , then they form a partition of X. According to (1), we have (2) |M | = i=1 i |G| = |RENG (x)| k i=1 i |G| = |Xi | |G| = k · |G| i=1 On the other hand, for a given G, (, x) M iff x IREN (). Thus, M is the disjoint union of the sets {} × IREN () ( G). Finally, (3) |M | = |IREN ()| From (2) and (3) it follows the identity: k= 1 |G| |IREN ()|. All these identities do not use the axiom of choice. Since G and X are finite, all the results used in our proofs are finite counting problems, and so they can be obtained from the axioms of the EFM set theory (see Remark 2.3). Remark 3.2. If X is a finite FM set, S supports each x X and G SA is finite, then the number k of classes of renamings in X under the permutations in G (i.e., the number k of orbits in X under the action · : G × X X) is k= 1 |G| |IREN ()| = 1 ( |G| |IREN ()| + G G |IREN ()|) F ix(S) 1 (|F ix(S)||X|+ |G| |IREN ()|)= |F ix(S)||X| + |G| |IREN ()| |G| Generally SA is not finite; however, locally, it has a finite behavior. By Theorem 3.2, the previous result remains true even if G is generated by a finite set of permutations of atoms. Therefore, in such a case, we can also obtain a formula which gives the number of classes of renamings in X under the permutations in G. The following results present some properties of permutative renamings in the EFM framework which follow from the mathematical properties of EFM sets described in [1]. By the following results we emphasize that, even we use only axiom 11' and the notion of extended interchange function to define the permutative renamings, these have similar properties with those of permutative renamings defined in [4] where the authors use axiom 11 (i.e. the finite support property) and the notion of interchange function. By Theorem 1 from [1] which states that SA is a torsion group we obtain: Theorem 3.1. Let x be an element of an arbitrary EFM set X, and an arbitrary permutation of atoms from A. We can obtain only a finite number of renamings of x generated by applying the extended interchange function to x and to each permutation obtained by composing and -1 multiple times (a permutation obtained by composing and -1 multiple times is of form k for an arbitrary k Z). By Theorem 2 from [1] we know that SA is locally finite. In the nominal framework we translate this as: Theorem 3.2. Let x be an element of an arbitrary EFM set X. If we have a finite number of permutations (in particular of transpositions), then we can obtain only a finite number of renamings of x generated by applying the extended interchange function to x and to each compositions of these permutations and their inverses. A composition of permutations k k k 1 , 2 , . . . , m and their inverses is of the form 1 1 2 2 ... r r , where r is a positive integer and k1 , k2 , . . . , kr are arbitrary from Z and i , i = 1, r are arbitrary from the set {1 , 2 , . . . , m }, not necessarily distinct. Corollary 3.1. Let X be a finite EFM set, and a group G = [{1 , 2 , ..., m }] generated by {1 , 2 , ..., m }, where 1 , 2 , ..., m SA . Then the number k of classes of renamings in X under the permutations in G is k= 1 |G| |IREN ()|. G def Proof. The result follows from Proposition 3.3. According to the proof of the previous theorem, it follows that G is finite, and so Proposition 3.3 could be applied. In this section we show that renamings defined in EFM approach have similar properties with the renamings defined in FM approach [4]. Therefore, we can work in a set theory where, instead of an axiom which forces each element to have finite support (i.e. axiom 11), we use an axiom on the structure of A (axiom 11'), and finally obtain similar properties of renamings. We do not say that our EFM set theory is better than the FM set theory (the finite support property have important benefits). We just emphasize that some weaker axioms can lead to similar properties of permutative renamings. 4. Algebraic properties of permutative renamings We present other algebraic properties of the domain SA of the extended interchange function which are also properties of permutative renamings because permutative renamings are defined involving the extended interchange function. We emphasize that the axiom of choice is not used in the proofs of these properties, and so the proofs remains true both in the FM framework and in the new EFM framework. First we present a collection of some known results from group theory providing certain characterizations of renamings and extended interchange function. We also give a characterization of the transitive subgroups of SA . Definition 4.1. A group G SA is called transitive if each atom can be obtain by other atom after a renaming under a permutation in G (i.e., the canonical action · : G × A A has only one orbit). Proposition 4.1. Let G SA . 1. If G is transitive, then the commutator subgroup D(G) is also transitive. 2. Suppose that H G with H transitive. Then D(G) H. 3. If G is transitive, then D(G) = D(D(G)). Some results of the group theory could be used in proving properties of the interchange function and permutative renamings: 1. Let G SA with G transitive. For each a A, the subgroup IREN (a) = { G | (a) = a} is not soluble [2]. 2. Let G SA with the property that G is transitive, and there is no B A such that either (B) = B or (B) B = for each G. If G contains a non-identity permutation of SA , then G must contain the group of even permutations in SA [3]. 3. Let G SA with G transitive, and B a finite subset of A. Then there is G such that (B) B = [6]. Remark 4.1. A transitive group G SA has the property that for any finite subset B of A there is a permutation G which moves B away from itself completely. The following result gives another characterization of the domain of the extended interchange function. This could be not particularly relevant for computer scientists, but it is interesting for mathematicians. Some techniques and results of this type can be found in [3]. We present here a specific result for the EFM set theory which contradicts the axiom of choice. Other results of this type (which characterize the domain of extended interchange function) could be proved by using the EFM axioms. We consider an additional condition on A only for the following result. We denote by F P A the partitions of A in which all the parts are finite. If (Ai )i F P A, then there exists a unique natural number |(Ai )i | such that all but finitely many parts of (Ai )i have the cardinal |(Ai )i |, and the cardinal |(Ai )i | is called the cardinal of the partition (Ai )i . We can prove this in a similar way to the Theorem 3.1 where all but finitely many cycles of a permutation have the same length. We assume that among the partitions in F P A we are able to choose a partition with a maximum cardinal (which can be as large as needed). We call this cardinal the "dimension of A", and the partition with maximum cardinal is called a "maximal partition". Over F P A we introduce the following order relation: (Ai )iI (Bj )jJ iff j J Ij I such that Bj = iIj Ai . Two partitions (Ai )iI and (Bj )jJ are equivalent (denoted by (Ai )iI (Bj )jJ ) if whenever there is B A, B inf inite and B = iI1 I Ai , then for C B we have (there exists i I such that C = Ai iff there is j J such that C = Bj ). Proposition 4.2. (F P A, ) is a complete lattice, and the equivalence relation over FPA defined before is a congruence. The next result shows that there is a one-to-one function between the subgroups lattice SA /SA and the lattice of equivalence classes of partitions of A, where SA is the subgroup of SA such that every permutation in SA keeps fixed the points of A, except a finite number of them (this number could be 0). Proposition 4.3. There exists a one-to-one function from the subgroups lattice SA /SA to the lattice of equivalence classes of partitions of A. Proof. Let H SA /SA , and 1 , 2 , ..., m SA be some left coset representatives for SA . Let (Ai )iI be a maximal partition of A. Then for each j {1, 2, ..., m} we have that j keeps fixed the equivalence class of (Ai )iI ; altering them on a finite subset, we can assume that all of them keeps (Ai )iI fixed. A result from the classical set theory says that if (Ai )iI F P A, then there is (Bj )jJ F P A such that (Ai )iI (Bj )jJ and (Bj )jJ is formed only by members with cardinal |(Bj )jJ | and members of cardinal 1. We can say that 1 , ..., m keep fixed all except finitely many elements of the maximal partition (Ai )iI . Let Aj be a part of this partition which is fixed by 1 , ..., m , and |Aj | = |(Ai )iI | = r. We use the notation Aj = {1, ..., r}. Now we consider a function f defined on SA having values in Sr with the property that for each SA , f () is the induced permutation in Sr for the representative of an equivalence class of modulo SA . It is not difficult to prove that f is a group homomorphism, and Ker(f ) = SA ; this homomorphism does not depend on the choice of representatives of the equivalence classes modulo SA . By renumbering the points of Aj , we can change the image with a conjugate in Sr . Since in every element in SA all except finitely many cycles have the same length, the image of the homomorphism defined before is represented by permutations in which all cycles have the same length. We can say that < 1 , ..., m > keep the partition (Ai )iI fixed, and < 1 , ..., m > acts semiregularly on all except finitely many parts of (Ai )iI . The group H1 generated by the representatives of left cosets in H has H-orbits of cardinal |H| in these parts of (Ai )iI , and so defines a partition whose cardinal is |H|. In the following we prove that function is one-to-one (injective). Let us assume that H and K provide equivalent partitions. We denote by [{H, K}] the subgroup generated by H and K; thus H [{H, K}]. Since H and[{H, K}] provide equivalent partitions, it follows that |H| = |[{H, K}]|, and so H = [{H, K}]. We also have K = [{H, K}], and so we conclude that H = K. The reader can note that an additional condition on A (namely the existence of the maximal partition) is used to prove this result. However, this condition does not restrict too much the generality because the maximum cardinal can be as large as we need. Even without this condition, P. Cameron and S. Tarzi proved in a similar way that there is a one-to-one function from the set of finitely generated subgroups of SA /SA to the set of equivalence classes of the partitions of A. 5. Connections between permutative renamings and finitary permutative renamings Fresh names and renamings are studied in some papers written by M. Gabbay and A. Pitts. In this paper we present a different perspective, extending the notion of permutative renamings to the EFM framework. Even the finite support axiom was relaxed in the new framework, we are able to present a connection between permutative renamings and finitary permutative renaimgs: Theorem 5.1. All the results presented in Sections 3 and 4 remain valid if we replace "EFM set" with "FM set", "extended interchange function" with "interchange function" and axiom 11' of the EFM set theory with "finite support property" (i.e. axiom 11) of the FM set theory . Proof. According to Example 2 in [1], we see that the finite support property implies that each subset of A is either finite or cofinite, and so all the results presented in Sections 3 and 4 for the EFM framework remains valid also for the FM framework. 6. Conclusions and related work Renaming, fresh names and binding appear in several new formalisms in computer science, and so they deserve to be studied by their own. Using group theory results, we present some properties of permutative renamings in the new Extended Fraenkel-Mostowski set theory which are also valid in the known Fraenkel-Mostowski set theory. The main benefit is that we can work with a weaker set of axioms (axioms 1-11') in the description of EFM set theory to obtain similar properties for permutative renamings as in the FM set theory (that assumed stronger axioms). Some important results are presented (e.g., Theorem 3.1, Theorem 3.2, Corollary 3.1); in their proofs, we use a weaker axiom 11' instead of the corresponding axiom 11 of FM set theory. Generalizing the notion of permutative renaming for the EFM framework (Definition 2.5), we prove that the permutative renamings have in the EFM framework similar properties as in the FM framework. A strong connection between the permutative renamings and the finitary permutative renamings is established in Theorem 5.1. An axiomatic description of the EFM set theory is presented in [1]. However, in this paper, we want to rewrite a part of nominal logic in EFM terms. A new notion of permutative renaming is given. Some properties of EFM sets obtained in [1] lead to similar properties of permutative renamings (Theorems 3.1 and 3.2). New algebraic and combinatorial properties of permutative renamings are proved according to the EFM axioms (Corollary 3.1 and Propositions 3.3 and 4.3). In a future work we will try to translate the nominal binding in the EFM framework. http://www.deepdyve.com/assets/images/DeepDyve-Logo-lg.png Annals of the Alexandru Ioan Cuza University - Mathematics de Gruyter

Permutative Renamings in the Extended Fraenkel-Mostowski Set Theory

Download PDF
17 pages

Loading next page...
 
/lp/de-gruyter/permutative-renamings-in-the-extended-fraenkel-mostowski-set-theory-1qkEPLhoTe
Publisher
de Gruyter
Copyright
Copyright © 2015 by the
ISSN
1221-8421
eISSN
1221-8421
DOI
10.2478/aicu-2014-0046
Publisher site
See Article on Publisher Site

Abstract

In the new framework of the extended Fraenkel-Mostowski set theory, we define an extended interchange function as an action on a permutation group, and a new notion of permutative renaming by generalizing an existing notion of finitary permutative renaming. Some algebraic and combinatorial properties of permutative renamings expressed by using the Fraenkel-Mostowski axioms remain valid in the new framework even if we replace one axiom with a weaker axiom. Mathematics Subject Classification 2010: 03E25, 03E30, 03B70. Key words: finite support axiom, extendend Fraenkel-Mostowski framework, permutative renamings. 1. Introduction Renaming the variables of an expression in a way that preserves its meaning is called -renaming. Some of the subtleties related to -renaming can be described by using the abstraction operation of the -calculus, together with the operation of application. Application and abstraction work together according to the -rule (x.M ) N = M [x := N ]. Abstraction x. M [x] binds a free variable x in M . Substitution [x := N ] is only performed for free occurrences of x. In order to avoid ambiguities, it is assumed that the bound variables occurring in a certain expression are different from the free ones, and this can be obtained by renaming bound variables. The expressions differing only in the names used for bound variables are identified by -equivalence. A correct variable renaming is one that preserves the -equivalence class of the expression. The notion of choosing a fresh name often arises when manipulating syntactic expressions; therefore it is necessary to indicate some constraints whenever describing such a syntactic manipulation. Often it is just said that a name is fresh without specifying any restrictions. In such a case, we mean that the fresh name must be different from any name occurring anywhere else in the expression or program. Some programming systems have mechanisms for renaming, for binding a name with a value and for managing sets of such bindings. Modern programming languages are designed to manage bindings and fresh names by using the notions of scopes, workspaces, or environments. Since renaming, binding and fresh names appear in several approaches, it became evident that they deserve to be studied in their own terms. The nominal logic and semantics was presented by Gabbay and Pitts in [5, 7]; it uses the Fraenkel-Mostowski (FM) axioms of set theory. The FM set theory was originally developed to prove the independence of the Axiom of Choice (AC) from the other axioms of the Zermelo-Fraenkel (ZF) set theory. It was rediscovered and used by Gabbay and Pitts [5] to model the syntax of formal systems involving variable binding operations. An advantage of modeling syntax in a model of FM set theory is that datatypes of syntax modulo -equivalence can be modeled inductively. This is because nominal set theory delivers a model of variable symbols and -abstraction. The FM axioms are precisely the Zermelo-Fraenkel with atoms (ZFA) axioms over an infinite set of atoms [5], together with the special axiom of finite support which claims that for each element x in an arbitrary set we can find a finite set supporting x. In [1] we generalized the FM set theory by giving a new set of axioms which defines the Extended Fraenkel-Mostowski (EFM) set theory. The finite support axiom in the description of the FM set theory was replaced in [1] by a weaker axiom which requires only a certain structure of the set of atoms. Many algebraic properties of sets, which are valid in the FM framework, remain valid also in the EFM framework. In this paper we analyze how some classical results of nominal logic are changed (or not) when we work in the EFM framework instead of the FM framework, and how some results obtained in the EFM set theory can be translated to the FM set theory. We naturally extend some notions and results of nominal logic, and together with some mathematical properties obtained in [1] and some additional combinatorial results which are proved without using the axiom of choice, we are able now to give some new properties of the interchange function and permutative renamings. The structure of the paper is as follows. Section 2 presents formal definitions related to permutative renamings and extended interchange function. In Section 3 we present several group theory and combinatorial results applied in the nominal logic. These results allow us to solve some counting problems involving renamings. Some properties of permutative renamings which are valid in FM approach can be extended in EFM approach, even if in EFM we assume only a weaker axiom 11' instead of the finite support property in FM set theory. In Section 4, using group theory, we present some algebraic properties of the (domain of the) extended interchange function. Some connections between old and new results are presented in Section 5. Conclusions end the paper. 2. Renamings in the extended Fraenkel-Mostowski framework We remind several definitions and results from [1]. Let A be an infinite set of atoms (also called names). A is characterized by the axiom "y x x A" which means that only non-atoms can have / elements. Definition 2.1. i) A transposition is a function (a b) : A A with the property (a b)(a) = b, (a b)(b) = a and (a b)(n) = n for n = a, b. ii) A permutation of A is a bijection from A to A. iii) A substitution is a function {b|a} : A A with the property {b|a}(n) = n if n = a and {b|a}(a) = b. Let SA be the set of all permutations over A. SA is a group. Let SA be the group of finitary permutations (i.e the group of permutations which leave unchanged all but finitely many atoms). In fact SA is the set of all functions generated by composing finitely many transpositions. For S A, we denote by F ix(S) the set { | (a) = a for all a S}. Definition 2.2. · Let X be a set defined by the axioms of ZFA set theory. An interchange function over X is a function · : SA × X X defined inductively by · a = (a) for all atoms a A, and by · x = { · y | y x} otherwise. Moreover, it satisfies the following axiom: for each x X, there exists a finite nonempty set S A such that for each F ix(S) SA we have · x = x. · An FM set is a pair (X, ·), where X is a set defined in the ZFA set theory without axiom of choice, and · : SA × X X is an interchange function over X. We simply use X whenever no confusion arises. Definition 2.3. Let X be an FM set. We say that S A supports x whenever for each F ix(S) SA we have · x = x. The properties of the interchange function allow always to find a finite set supporting x; in fact this assertion is an axiom (axiom 11) in the description of the FM set theory. The new notion of "extended interchange function" was introduced in [1]. Definition 2.4. · Let X be a set defined by the axioms of ZFA set theory. An extended interchange function over X is a function · : SA × X X defined inductively by · a = (a) for all atoms a A, and by · x = { · y | y x} otherwise. Moreover, each subset of A is either finite or cofinite. · An EFM set is a pair (X, ·), where X is a set defined in the ZFA set theory without choice, and · : SA ×X X is an extended interchange function on X. We simply use X whenever no confusion arises. Remark 2.1. Since SA is a group, the interchange function and the extended interchange function · : SA × X X are actions of the group SA on the set X; we have Id · x = x and · · x = ( ) · x for all , SA and all x X. Example 2.1. 1. The set A of atoms is both an FM set and an EFM set (when each subset of A is either finite of cofinite) with interchange function, respectively extended interchange function given by · a = (a), SA , a A. 2. The set SA is both an FM set and an EFM set (when each subset of A is either finite of cofinite) with the interchange function, respectively extended interchange function given by · := -1 for all SA and SA . (SA , ·) is an FM set because for each SA we have that the finite set {a A | (a) = a} supports . 3. The set SA is an EFM set (when each subset of A is either finite of cofinite) with the extended interchange function given by · := -1 for all , SA . We present the axiomatic descriptions of both the Fraenkel-Mostowski [5] and Extended Fraenkel-Mostowski [1] set theories. The following axioms describes completely the Fraenkel-Mostowski set theory: 1. x.(y.y x) x A / (only non-atoms can have elements) 2. x, y.(x A and y A and z.(z x z y)) x = y / / (axiom of extensionality) 3. x, y.z.z = {x, y} 4. x.y.y = {z | z x} 5. x.y.y A and y = {z | w.(z w and w x)} / (axiom of pairing) (axiom of powerset) (axiom of union) 6. x.y.(y A and y = {f (z) | z x}), for each functional formula f (z) / (axiom of replacement) 7. x.y.(y A and y = {z | z x and p(z)}), for each formula p(z) / (axiom of separation) 8. (x.(y x.p(y)) p(x)) x.p(x) 9. x.( x and (y.y x y {y} x)) 10. A is not f inite 11. x.S A.S is f inite and S supports x (the finite support property) Therefore, we can see the FM set theory like the ZFA set theory over an infinite set A of atoms infinite and with an additional property of finite support. The following axioms describes completely the Extended Fraenkel-Mostowski set theory: 1. x.(y.y x) x A / (only non-atoms can have elements) (induction principle) (axiom of infinite) 2. x, y.(x A and y A and z.(z x z y)) x = y / / (axiom of extensionality) 3. x, y.z.z = {x, y} (axiom of pairing) 4. x.y.y = {z | z x} 5. x.y.y A and y = {z | w.(z w and w x)} / (axiom of powerset) (axiom of union) 6. x.y.(y A and y = {f (z) | z x}), for each functional formula f (z) / (axiom of replacement) 7. x.y.(y A and y = {z | z x and p(z)}), for each formula p(z) / (axiom of separation) 8. (x.(y x.p(y)) p(x)) x.p(x) 9. x.( x and (y.y x y {y} x)) 10. A is not f inite 11'. Each subset of A is either f inite or cof inite (axiom of the structure of A) Therefore, the Extended Fraenkel-Mostowski (EFM) set theory is similar to the ZFA set theory over an infinite set A of atoms infinite, having the additional property that each subset of A is either finite or cofinite. Remark 2.2. Axiom 11' of the EFM set theory is a direct consequence of axiom 11 of the FM set theory (see Example 2 from [1]). Thus, the EFM set theory is a natural extension of the FM set theory; an interchange function can be seen as an extended interchange function, and an FM set can be seen as an EFM set. Both in the FM framework and in the EFM framework, each subset of A is either finite or cofinite [1]. This structure of the atoms set A allows us to say that the axiom of choice fails both in the FM framework and in the EFM framework. More details are in [1]. We make the remark that, even the axiom of choice fails in the FM and EFM approach, a weaker form of the axiom of choice (where the choice is made from finite families) is valid. Remark 2.3. The axiom of choice says that, for each family F of nonempty disjoint sets, we can find a system of representatives, namely a set that contains exactly one element from each set in F. If F is a finite family of disjoint nonempty sets, this statement is a consequence of axioms (induction principle) (axiom of infinite) 1-9 (and does not involve the axiom of choice). Indeed, if F contains only one nonempty set U , then we can find an element x0 U (because U is nonempty). According to the axiom of pairing, we obtain the set {x0 } which is a set of representatives for F. According to the induction principle, we can obtain a set of representatives for each finite family F of disjoint nonempty sets. Now we generalize the notion of finitary permutative renaming. In this paper we deal with renamings induced by permutations, and not with renamings induced by substitutions and substitution actions (these renamings are presented in several papers of M.Gabbay and A.Pitts). In fact, a link between these viewpoints is given by the fact that for a -calculus expression t and two atoms a and b, we get {b|a}t = (b a) · t for b f n(t) (the / case {b|a}t for b f n(t) is explained in [4], and it is not considered here). Definition 2.5. Let x be an element of an EFM set X. A permutative renaming of x is an element of the form ·x, where SA and · : SA ×X X is an extended interchange function on X. The same definition can be used to characterize the permutative renamings of elements from an FM set. In the FM universe only finitely supported objects are allowed. According to Example 2.1 (3) we know that SA is an EFM set (when each subset of A is either finite or cofinite). For each SA we have that {a A | (a) = a} is the least set supporting in the sense of Definition 2.3. If we assume the supplementary axiom of finite support (axiom 11) we must have that {a A | (a) = a} is finite. Hence, in the FM framework, each permutation in SA have to be finitary which means that SA coincides with SA in FM. If x is an element of an FM set X, then a permutative renaming of x is an element of the form · x, where SA and · : SA × X X is an interchange function on X. Our intuition says that a permutative renaming of x in FM framework is of the form (a b) · x, where a, b A and (a b) · x is denoting the result of interchanging a and b in x. If a permutation is a composition of many transpositions, then · x is also a permutative renaming of x. For example, ((c d) (a b)) · x denotes the result of of interchanging c and d in (a b) · x, where (a b) · x is defined before. In the EFM framework we eliminate the finite support property (axiom 11), and hence we allow the presence of nonfinitary permutations. It is natural to define the permutative renamings of an element x as the elements of form · x, where SA , even if SA is different from SA in the EFM framework. By now on, the permutative renamings are simply called renamings. Remark 2.4. It is worth noting that M.Gabbay and A.Pitts work with permutations obtained by composing finitely many transpositions. In this section, since we eliminate the finite support property from the FM axioms, we work in the general case where SA is the set of all bijections from A to A, X is an EFM set and the extended interchange function is defined on SA not only on SA (like in [4, 5]). A permutative renaming in our approach is of the form · x, where SA . The particular class of finitary permutative renamings (namely the class of permutative renamings under the action ·|SA ) is well described in [4]. The notion of permutative renaming defined in [4] is a particular case of the notion of permutative renaming defined by Definition 2.5. 3. Combinatorial properties of permutative renamings We present several counting problems on renamings using the algebraic properties of EFM sets described in [1] and some combinatorial results which can be proved without using the axiom of choice. Let G be a subgroup of SA . Definition 3.1. 1. The representation of SA by permutations of the EFM set X is a group homomorphism : SA S(X) given by ()(x) = · x. 2. Let x and y be elements of an EFM set X. (a) x and y are called equivalent, and denote this by x y, whenever we can obtain one from another by a renaming. (b) x and y are called equivalent under permutations in G, and denote this by x G y, whenever we can obtain one from another by a renaming under a permutation in G (i.e. if there is G such that y = · x). 3. Let X be an EFM set. (a) REN (x) = { · x | SA } is the set of all renamings of x; we also say that REN (x) is a class of renamings in X. (b) RENG (x) = { · x | G} is the set of all renamings of x under the permutations in G; we also say that RENG (x) is a class of renamings in X under permutations in G. A renaming of an (arbitrary) atom under the permutations in G is called a G-renaming. 4. Let X be an EFM set. (a) IREN (x) = { SA | · x = x} is the set of permutations for which we obtain an invariant renaming of x (a renaming which keeps x unchanged). (b) IRENG (x) = { G | · x = x} is the set of permutations in G for which we obtain an invariant renaming of x. 5. Let X be an EFM set. (a) An element x X for which IREN (x) = SA is called invariant on all renamings. The set of elements in X which are invariants on all renamings is denoted by IRN (X). (b) An element x X for which IRENG (x) = G is called invariant on renamings under permutations in G. The set of elements in X which are invariants on renamings under permutations in G is denoted by IRNG (X). Let X be an EFM set, and G SA . From the general theory of group actions we have the following results which we present without proofs. Proposition 3.1. 1. G is an equivalence relation on X. 2. RENG (x) is the equivalence class of x modulo G which is the orbit of the element x under the action · : G × X X defined as the extended interchange function. 3. In terms of group theory, IREN (x) is the stabilizer of x under the extended interchange function, and IRENG (x) is the stabilizer of x under the action · : G × X X defined as the extended interchange function. A trivial consequence is that IRENG (x) G. Remark 3.1. If G is a finite subgroup of SA , we denote by IRENG (x) the left cosets modulo IRENG (x). A function : {IRENG (x) | G} - RENG (x) defined by (IRENG (x)) = · x is well defined, and it is a bijection. Thus, |RENG (x)| = [G : IRENG (x)]. Proposition 3.2. Let G be a finite subgroup of SA and X a finite EFM set. Let S be a system of representatives for classes of renamings in X under permutations in G, with at least two elements; such a system S exists because X is finite, and the axiom of choice is not requested (see Remark 2.3). Then, by using the classes equation in group theory, |X| = |IRNG (X)| + |RENG (x)| = |IRNG (X)| + [G : IRENG (x)] = |IRNG (X)| + |G| |IRENG (x)| Let IREN () be the set of invariants x X under , i.e., IREN () = {x X | · x = x}. If X is an FM set we say that S A supports x whenever for each F ix(S) SA we have · x = x. If X is a finite FM set, F ix(S) and S supports each x X, then IREN () = X. Let G SA be a finite group of permutations. Then we can find the number of orbits under the extended interchange function for finite EFM sets, even though we work in a set theory without the axiom of choice Proposition 3.3. Let X be a finite EFM set. If G SA is finite, the number k of classes of renamings in X under the permutations in G (i.e., the number k of orbits in X under the action · : G × X X) is k= 1 |G| |IREN ()| Proof. Let M = {(, x) G × X | · x = x}. We express |M | in two ways. We can build sets of representatives for finite families by using axioms 1-9 (see Remark 2.3). We have (, x) M iff IRENG (x), and so M is the disjoint union of the sets IRENG (x) × {x} (x X). Since X is finite, there is only a finite number of such sets. Using Lagrange Theorem for finite groups and Remark 3.1, (1) |M | = |IRENG (x)| = |G| = [G : IRENG (x)] |G| |RENG (x)| By Proposition 3.1, the classes of renamings in X are orbits in X under the action · : G × X X defined as an extended interchange function. If these orbits are X1 , X2 , ..., Xk , then they form a partition of X. According to (1), we have (2) |M | = i=1 i |G| = |RENG (x)| k i=1 i |G| = |Xi | |G| = k · |G| i=1 On the other hand, for a given G, (, x) M iff x IREN (). Thus, M is the disjoint union of the sets {} × IREN () ( G). Finally, (3) |M | = |IREN ()| From (2) and (3) it follows the identity: k= 1 |G| |IREN ()|. All these identities do not use the axiom of choice. Since G and X are finite, all the results used in our proofs are finite counting problems, and so they can be obtained from the axioms of the EFM set theory (see Remark 2.3). Remark 3.2. If X is a finite FM set, S supports each x X and G SA is finite, then the number k of classes of renamings in X under the permutations in G (i.e., the number k of orbits in X under the action · : G × X X) is k= 1 |G| |IREN ()| = 1 ( |G| |IREN ()| + G G |IREN ()|) F ix(S) 1 (|F ix(S)||X|+ |G| |IREN ()|)= |F ix(S)||X| + |G| |IREN ()| |G| Generally SA is not finite; however, locally, it has a finite behavior. By Theorem 3.2, the previous result remains true even if G is generated by a finite set of permutations of atoms. Therefore, in such a case, we can also obtain a formula which gives the number of classes of renamings in X under the permutations in G. The following results present some properties of permutative renamings in the EFM framework which follow from the mathematical properties of EFM sets described in [1]. By the following results we emphasize that, even we use only axiom 11' and the notion of extended interchange function to define the permutative renamings, these have similar properties with those of permutative renamings defined in [4] where the authors use axiom 11 (i.e. the finite support property) and the notion of interchange function. By Theorem 1 from [1] which states that SA is a torsion group we obtain: Theorem 3.1. Let x be an element of an arbitrary EFM set X, and an arbitrary permutation of atoms from A. We can obtain only a finite number of renamings of x generated by applying the extended interchange function to x and to each permutation obtained by composing and -1 multiple times (a permutation obtained by composing and -1 multiple times is of form k for an arbitrary k Z). By Theorem 2 from [1] we know that SA is locally finite. In the nominal framework we translate this as: Theorem 3.2. Let x be an element of an arbitrary EFM set X. If we have a finite number of permutations (in particular of transpositions), then we can obtain only a finite number of renamings of x generated by applying the extended interchange function to x and to each compositions of these permutations and their inverses. A composition of permutations k k k 1 , 2 , . . . , m and their inverses is of the form 1 1 2 2 ... r r , where r is a positive integer and k1 , k2 , . . . , kr are arbitrary from Z and i , i = 1, r are arbitrary from the set {1 , 2 , . . . , m }, not necessarily distinct. Corollary 3.1. Let X be a finite EFM set, and a group G = [{1 , 2 , ..., m }] generated by {1 , 2 , ..., m }, where 1 , 2 , ..., m SA . Then the number k of classes of renamings in X under the permutations in G is k= 1 |G| |IREN ()|. G def Proof. The result follows from Proposition 3.3. According to the proof of the previous theorem, it follows that G is finite, and so Proposition 3.3 could be applied. In this section we show that renamings defined in EFM approach have similar properties with the renamings defined in FM approach [4]. Therefore, we can work in a set theory where, instead of an axiom which forces each element to have finite support (i.e. axiom 11), we use an axiom on the structure of A (axiom 11'), and finally obtain similar properties of renamings. We do not say that our EFM set theory is better than the FM set theory (the finite support property have important benefits). We just emphasize that some weaker axioms can lead to similar properties of permutative renamings. 4. Algebraic properties of permutative renamings We present other algebraic properties of the domain SA of the extended interchange function which are also properties of permutative renamings because permutative renamings are defined involving the extended interchange function. We emphasize that the axiom of choice is not used in the proofs of these properties, and so the proofs remains true both in the FM framework and in the new EFM framework. First we present a collection of some known results from group theory providing certain characterizations of renamings and extended interchange function. We also give a characterization of the transitive subgroups of SA . Definition 4.1. A group G SA is called transitive if each atom can be obtain by other atom after a renaming under a permutation in G (i.e., the canonical action · : G × A A has only one orbit). Proposition 4.1. Let G SA . 1. If G is transitive, then the commutator subgroup D(G) is also transitive. 2. Suppose that H G with H transitive. Then D(G) H. 3. If G is transitive, then D(G) = D(D(G)). Some results of the group theory could be used in proving properties of the interchange function and permutative renamings: 1. Let G SA with G transitive. For each a A, the subgroup IREN (a) = { G | (a) = a} is not soluble [2]. 2. Let G SA with the property that G is transitive, and there is no B A such that either (B) = B or (B) B = for each G. If G contains a non-identity permutation of SA , then G must contain the group of even permutations in SA [3]. 3. Let G SA with G transitive, and B a finite subset of A. Then there is G such that (B) B = [6]. Remark 4.1. A transitive group G SA has the property that for any finite subset B of A there is a permutation G which moves B away from itself completely. The following result gives another characterization of the domain of the extended interchange function. This could be not particularly relevant for computer scientists, but it is interesting for mathematicians. Some techniques and results of this type can be found in [3]. We present here a specific result for the EFM set theory which contradicts the axiom of choice. Other results of this type (which characterize the domain of extended interchange function) could be proved by using the EFM axioms. We consider an additional condition on A only for the following result. We denote by F P A the partitions of A in which all the parts are finite. If (Ai )i F P A, then there exists a unique natural number |(Ai )i | such that all but finitely many parts of (Ai )i have the cardinal |(Ai )i |, and the cardinal |(Ai )i | is called the cardinal of the partition (Ai )i . We can prove this in a similar way to the Theorem 3.1 where all but finitely many cycles of a permutation have the same length. We assume that among the partitions in F P A we are able to choose a partition with a maximum cardinal (which can be as large as needed). We call this cardinal the "dimension of A", and the partition with maximum cardinal is called a "maximal partition". Over F P A we introduce the following order relation: (Ai )iI (Bj )jJ iff j J Ij I such that Bj = iIj Ai . Two partitions (Ai )iI and (Bj )jJ are equivalent (denoted by (Ai )iI (Bj )jJ ) if whenever there is B A, B inf inite and B = iI1 I Ai , then for C B we have (there exists i I such that C = Ai iff there is j J such that C = Bj ). Proposition 4.2. (F P A, ) is a complete lattice, and the equivalence relation over FPA defined before is a congruence. The next result shows that there is a one-to-one function between the subgroups lattice SA /SA and the lattice of equivalence classes of partitions of A, where SA is the subgroup of SA such that every permutation in SA keeps fixed the points of A, except a finite number of them (this number could be 0). Proposition 4.3. There exists a one-to-one function from the subgroups lattice SA /SA to the lattice of equivalence classes of partitions of A. Proof. Let H SA /SA , and 1 , 2 , ..., m SA be some left coset representatives for SA . Let (Ai )iI be a maximal partition of A. Then for each j {1, 2, ..., m} we have that j keeps fixed the equivalence class of (Ai )iI ; altering them on a finite subset, we can assume that all of them keeps (Ai )iI fixed. A result from the classical set theory says that if (Ai )iI F P A, then there is (Bj )jJ F P A such that (Ai )iI (Bj )jJ and (Bj )jJ is formed only by members with cardinal |(Bj )jJ | and members of cardinal 1. We can say that 1 , ..., m keep fixed all except finitely many elements of the maximal partition (Ai )iI . Let Aj be a part of this partition which is fixed by 1 , ..., m , and |Aj | = |(Ai )iI | = r. We use the notation Aj = {1, ..., r}. Now we consider a function f defined on SA having values in Sr with the property that for each SA , f () is the induced permutation in Sr for the representative of an equivalence class of modulo SA . It is not difficult to prove that f is a group homomorphism, and Ker(f ) = SA ; this homomorphism does not depend on the choice of representatives of the equivalence classes modulo SA . By renumbering the points of Aj , we can change the image with a conjugate in Sr . Since in every element in SA all except finitely many cycles have the same length, the image of the homomorphism defined before is represented by permutations in which all cycles have the same length. We can say that < 1 , ..., m > keep the partition (Ai )iI fixed, and < 1 , ..., m > acts semiregularly on all except finitely many parts of (Ai )iI . The group H1 generated by the representatives of left cosets in H has H-orbits of cardinal |H| in these parts of (Ai )iI , and so defines a partition whose cardinal is |H|. In the following we prove that function is one-to-one (injective). Let us assume that H and K provide equivalent partitions. We denote by [{H, K}] the subgroup generated by H and K; thus H [{H, K}]. Since H and[{H, K}] provide equivalent partitions, it follows that |H| = |[{H, K}]|, and so H = [{H, K}]. We also have K = [{H, K}], and so we conclude that H = K. The reader can note that an additional condition on A (namely the existence of the maximal partition) is used to prove this result. However, this condition does not restrict too much the generality because the maximum cardinal can be as large as we need. Even without this condition, P. Cameron and S. Tarzi proved in a similar way that there is a one-to-one function from the set of finitely generated subgroups of SA /SA to the set of equivalence classes of the partitions of A. 5. Connections between permutative renamings and finitary permutative renamings Fresh names and renamings are studied in some papers written by M. Gabbay and A. Pitts. In this paper we present a different perspective, extending the notion of permutative renamings to the EFM framework. Even the finite support axiom was relaxed in the new framework, we are able to present a connection between permutative renamings and finitary permutative renaimgs: Theorem 5.1. All the results presented in Sections 3 and 4 remain valid if we replace "EFM set" with "FM set", "extended interchange function" with "interchange function" and axiom 11' of the EFM set theory with "finite support property" (i.e. axiom 11) of the FM set theory . Proof. According to Example 2 in [1], we see that the finite support property implies that each subset of A is either finite or cofinite, and so all the results presented in Sections 3 and 4 for the EFM framework remains valid also for the FM framework. 6. Conclusions and related work Renaming, fresh names and binding appear in several new formalisms in computer science, and so they deserve to be studied by their own. Using group theory results, we present some properties of permutative renamings in the new Extended Fraenkel-Mostowski set theory which are also valid in the known Fraenkel-Mostowski set theory. The main benefit is that we can work with a weaker set of axioms (axioms 1-11') in the description of EFM set theory to obtain similar properties for permutative renamings as in the FM set theory (that assumed stronger axioms). Some important results are presented (e.g., Theorem 3.1, Theorem 3.2, Corollary 3.1); in their proofs, we use a weaker axiom 11' instead of the corresponding axiom 11 of FM set theory. Generalizing the notion of permutative renaming for the EFM framework (Definition 2.5), we prove that the permutative renamings have in the EFM framework similar properties as in the FM framework. A strong connection between the permutative renamings and the finitary permutative renamings is established in Theorem 5.1. An axiomatic description of the EFM set theory is presented in [1]. However, in this paper, we want to rewrite a part of nominal logic in EFM terms. A new notion of permutative renaming is given. Some properties of EFM sets obtained in [1] lead to similar properties of permutative renamings (Theorems 3.1 and 3.2). New algebraic and combinatorial properties of permutative renamings are proved according to the EFM axioms (Corollary 3.1 and Propositions 3.3 and 4.3). In a future work we will try to translate the nominal binding in the EFM framework.

Journal

Annals of the Alexandru Ioan Cuza University - Mathematics – de Gruyter

Published: Jan 1, 2015

There are no references for this article.