lo.logic - Algebraic structures at hypernatural parameters

You can build your group directly as an ultraproduct without fussing about the particular language. Namely, let U be any nonprincipal ultrafilter on ω, and let S be the ultraproduct Π_n S_n/U. That is, one defines f ≡ g in the product Π S_n if and only if { n | f(n) = g(n) } ∈ U. This is an equivalence relation, and the ultraproduct is the collection of equivalence classes [f], where the algebraic structure is well-defined coordinate-wise. Los's theorem then states that S will satisfy a statement about [f] in the language of groups if and only if the set of n for which f(n) has the property in S_n has the property is in U. For example, S will have elements of infinite order, since we can let f(n) select an element of S_n of order n, and then observe that for any fixed k, the set of n for which f(n) has order at least k is co-finite and hence in U. As Gerald observed, S is not itself a full symmetric group, since one will never be able to define the standard/nonstandard cut.

But let me describe a more general way to accomplish what you want, for all kinds of structures simultaneously. There is little reason when taking ultraproducts to restrict to any particular structure. Rather, one should simply consider the ultrapower of the entire set-theoretic universe V. This results in a new set-theoretic universe W = V^ω/U that satisfies all the truths about any [f] that are true of f(n) in V on a set in U. In particular, S is the just [〈 S_n | n ∈ ω 〉] in the universe W. (What this shows is that ultraproducts of any set structures are elements of the ultrapower of the universe, and in this sense, ultraproducts are a special case of ultrapowers, although one usually hears the converse.) With this construction, we are not limited to the language of group theory when discussing properties of your group S, and we can freely refer to properties involving subgroups, group extensions and whatever else is expressible in set theory. If almost every S_n (that is, on a set in U) has some property expressible in set theory, then S will have this property in W. Thus, the group S is a "finite" permutation group inside W on the nonstandard natural number N represented by the identity function id(n) = n. That is, W thinks that S is just S_N, where N = [id]. So any property that you can prove about all S_n, will be true of S in W. Some but not all of these properties are absolute between W and V, and it is often interesting to compare the differences.

What this shows is that there IS a sense in which your group S is a full group of permutations on a set, because it is the group of all permutations on N inside W. That is, it is a full symmetric group inside the alternative set-theoretic universe W, rather than in the original universe V. In particular, Gerald's counterexample permutation does not exist in W, since W also cannot define the standard/nonstandard cut.