# Is there a general result that theorems about finite structures proved in ZFC can be proved in ZF?

The title question is too vague so let me be specific.

Much of modern finite semigroup theory uses profinite semigroups and properties of profinite semigroups that depend on the existence of prime ideals in Boolean algebras, which is a choice principle weaker than AC. Often results are proved first via profinite methods and then explicit proofs using finite means are found later.

To narrow my question down, let me consider the following situation. Let V be what is sometimes called a variety of finite semigroups, that is, a class of finite semigroups closed under finite products, subsemigroups and homomorphic images. A pro-V semigroup is an inverse limit of semigroups in V. It is known, using Tychnoff's theorem for products of finite spaces, that every continuous finite quotient of a pro-V semigroup belongs to V. So if you want to show a variety W of finite semigroups is contained in a variety V it suffices to show each element of W is a continuous quotient of a free pro-V semigroup. Sometimes one has good information on the structure of free pro-V semigroups and can exploit this.

For example, Almeida proved that the smallest variety of finite semigroups containing all finite commutative semigroups and all finite groups is the variety of finite semigroups with central idempotents using the approach sketched above. Later Auinger gave a proof using only finite semigroups.

Question. Is there some general result in logic or set theory that would imply that the existence of a proof in ZF+Boolean prime ideal theoerem that a variety W of finite semigroups is contained in a variety V of finite semigroups implies the existence of a proof in ZF that W is contained in V?

Many results of this sort in finite semigroup theory were motivated by questions in automata theory and in principle one would like to avoid choice in this context.

Caveat: I know very little set theory or model theory so please take that into account in answer.

-

As long as your varieties have reasonable definitions, the axiom of choice will be eliminable from proofs like these. The point is that any finite semigroup has an isomorphic copy whose underlying set consists of natural numbers, and that copy will be in Gödel's constructible universe $L$, where the axiom of choice holds. So if there were a semigroup in $W$ that isn't in $V$, then the same would be true in $L$.

Now about that proviso "reasonable definitions": You can sneak a lot of set theory into the definition of a variety. Consider the variety that consists of all groups if the continuum hypothesis holds and consists of all commutative semigroups if the continuum hypothesis fails. With such "cheating" you can surely arrange for $W$ to be included in $V$ iff the axiom of choice holds. My argument in the preceding paragraph tacitly assumed that the definitions of the varieties were absolute, in the sense that the constructible universe $L$ and the whole universe agree as to whether any particular finite semigroup is in the variety. By working harder, one can get by with weaker absoluteness requirements, but one can't get rid of them completely.

-
Most varieties I care about are generated by applying nice operations to already understood varieties. I think your unreasonable definitions are not a problem because it is somehow hidden in the meta theory. There is the variety of finite groups and the variety of finite commutative semigroups. The undecidable issue is which one we are talking about if we define V that way. Thanks for your nice answer. – Benjamin Steinberg Apr 6 '12 at 14:29
Would an inverse limit of finite semigroups indexed by a countable set still live in Godel's constructible universe? – Benjamin Steinberg Apr 6 '12 at 14:36
@Benjamin: Not as such, unless all reals are constructible. However, since it is $\Pi^0_1$-definable, I guess you can get around it with tools like Shoenfield absoluteness theorem. – Emil Jeřábek Apr 6 '12 at 16:01
Thanks Emil. One of these days I will know logic well enough to recognize where a particular construction lives. Until then let us be thankful for MO:) – Benjamin Steinberg Apr 7 '12 at 2:14

There is a standard method to handle this kind of situation which uses the absoluteness of certain statements over models of set theory.

The basic idea is this. If you're investigating the properties of a certain "well-behaved" set $A$, then instead of working in the full set-theoretic universe $V$, you can work in the smallest universe $L[A]$ that contains $A$ and all the ordinal numbers. By classical results of Gödel and others, this smaller universe $L[A]$ satisfies some very strong forms of choice and many other nice properties. You can then freely use these facts to show that "$A$ has property $X$" holds in $L[A]$. As is this doesn't really mean much, but if "property $X$" is upward absolute, then you can conclude that "$A$ has property $X$" holds in the full set-theoretic universe $V$.

There are several tricks to analyze when a property is absolute or not. Many of them are syntactic in nature, for example Shoenfield's absoluteness theorem states that $\Sigma^1_3$ properties are always upward absolute. Assuming the existence of some large cardinals, a whole lot of statements can be shown to be absolute.

For the situation you describe, I believe everything is absolute for even simpler reasons. The constructible universe $L$ already contains isomorphic copies of all finite objects in the real universe $V$. Since the definition of a variety is finitary, varieties of finite semigroups are essentially the same in $L$ as they are in $V$. Therefore, inclusions of varieties of finite semigroups are absolute between $L$ and $V$. So you can freely use the axiom of choice in $L$ and the conclusions drawn automatically transfer from $L$ to $V$.

-
I looked once at Shoenfield's absoluteness theorem on Wiki but my logical incompetence made it unclear if it helps with my question. Nonetheless your answer does seem to help. – Benjamin Steinberg Apr 6 '12 at 14:25
I'll ask you the same question I asked Andreas. Do inverse limits of finite semigroups indexed by countable sets stay in the constructible universe? – Benjamin Steinberg Apr 6 '12 at 15:08
$L$ is a model of ZFC so all the usual constructions work in there as usual. The inverse limits may not be the same in $V$ and in $L$ - $V$ may be able to see more points than $L$ does. However, this doesn't matter since $L$ believes that what it sees is the inverse limit and all facts about inverse limits hold true in $L$. The only thing you can't do is transfer the inverse limit itself from $L$ to $V$, so if your final conclusion doesn't mention the inverse limit itself then you're safe even if you use the inverse limit profusely in getting to that conclusion in $L$. – François G. Dorais Apr 6 '12 at 15:45
I would like to accept both answers but since Andreas was first I have to take his. But your comments were very helpful. – Benjamin Steinberg Apr 6 '12 at 19:55