FOM: 5:Constructions

[Harvey Friedman]

This is the fifth in a series of positive self contained postings to fom
covering a wide range of topics in f.o.m. Previous ones are:

1:Foundational Completeness   11/3/97, 10:13AM, 10:26AM.
2:Axioms  11/6/97.
3:Simplicity  11/14/97 10:10AM.
4:Simplicity  11/14/97  4:25PM

>From the point of view of the usual set theoretic foundations of
mathematics, actual mathematical constructions consist in giving an
explicit definition of the entity constructed. However, this is not the
whole truth - there some ways of looking at this in which this is clearly
false. The most common situation is illustrated by, e.g., the
"construction" of the ordering of the rationals as "the countable dense
linear ordering without endpoints," which "defines" the ordering of the
rationals uniquely up to isomorphism.

A common criticism of set theoretic foundations is that this is normally
formalized in set theory in a rather awkward way, whereas mathematicians do
not find this construction stated this way as awkward at all. And this kind
of construction is used all the time - e.g., in giving constructions of the
standard number systems.

Now how is this normally formalized in set theory? One way is to pass to
class theory and take the class of all countable dense linear orderings
without endpoints. (CDLOWE). But this is not so good in that one has to
complicated matters by passing to class theory, with its restrictions and
additional problems. It's nicer to stick with set theory.

Of course, the normal way this is done is to pick some particular
construction of a CDLOWE and simply define the appropriate isomorphism
relation, and prove that any two are isomorphic. The awkward thing of
course here is the original choice of the particular CDLOWE. However, in
defense of this approach, note that after the original choice is made, and
after some early facts are established and constructions are made on it,
one never has to refer to the original construction again. So after this
initial development, the way the object is used is very similar to how it
would be used if one operated in the way mathematicians find more natural.
This is not too bad - actually it's quite good, but not perfect, and
mathematicians generally recognize that it's quite good and not perfect,
but totally manageable in light of the fact that one so quickly never again
has to refer to the original ad hoc construction.

It is also recognized that the cure can be worse than the disease.
Mathematicians agree to think and operate semi-formally, but still respect
the fact that the usual set theoretic foundation provides a welcomed kind
of ultimate security blanket so they don't have to worry. And they
recognize that set theory is the only adequate security blanket in town.

An alternative approach is to pick a nice set A which is large enough to
accomodate the CDLOWE, which in this case is simply any countably infinite
set. Then one can consider the set of all CDLOWE's whose domain is a subset
of A. Then prove that all of them are isomorphic, and whatever construction
is made for one, is automatically made for all. This too has some serious
drawbacks.

In this note, I want to indicate how one can directly incorporate such
constructions into the usual set theoretic framework with a minimal amount
of disruption and complication. And, as usual, I have some questions.

Consider the following rule: if one has proved that (therexists x)(A(x)),
where A has no side parameters, then one can introduce a new constant
symbol c and assert A(c).

How does this apply to the case of CDLOWE? Under any reasonable approach,
mathematicians are stuck proving the existence of a CDLOWE, with an ad hoc
construction. Then one can add a constant symbol for any particular one and
assert that it is one. In practice, one may introduce more than one
constant symbol at once, and the like - say introduce the notation (Q,<),
or whatever. But the main point is clear.

Now I come to the more meaty, sophisticated case of "the algebraic closure"
of a field. One proves that every field has an algebraic closure; i.e., a
field which includes the original field, which is algebraically closed, and
where every element is algebraic over the original field. One convenient
way to handle this in set theory is as follows. Firstly, the appropriate
uniquness theorems are proved separately in the ordinary way. Secondly, we
introduce a function symbol F together with the axiom that for every field
K, F(K) is an algebraic closure of K.

Thus we add the following rule to ZFC: if one can prove (forall
x1,...,xk)(therexists y)(A(x1,...,xk,y)), with no side paramters, then one
can introduce a k-ary funciton symbol F with the axiom (forall
x1,...,xk)(A(x1,...,xk,F(x1,...,xk)).

We want to draw a distinction between this more sophisticated case from the
earlier case for the following subtle reason. When we introduce a constant
symbol c, it is understood that c stands for a set (although we don't know
or care which particular set). And then any formula makes sense involving c
as an object in the role of a set. However, when we introduce a function
symbol F as above, any formula can use F. But F cannot be treated as an
object in set theory - it would be a proper class. This is an important
distinction.

Nevertheless, it is easy to see how the latter function symbol introduction
rule is more general than the former constant symbol introduction rule.
E.g., one can focus on the term F(emptyset), which behaves like a constant
symbol in that it is an object.

Here is a crucial point. We want the axiom schemes of ZFC to be expanded to
include all new formulas as one goes along and introduces new constant
symbols and functions in this way. In the case of constant symbols, one
doesn't get anything new. However, in the case of function symbols, one
does.

Now of course, using the function symbol introduction rule on top of ZFC,
one creates more and more function symbols, which in turn can be used in
the formulas A.

THEOREM 1. This expansion of ZFC is conservative over ZFC, in that every
sentence in the language of ZFC that is provable in the expansion of ZFC,
is already provable in the original ZFC.

Now suppose one is particularly interested in starting off with ZF, without
Choice. Notice that this expansion immediately implies Choice, so one does
not get conservativity. So how can we restrict the expansion so that it is
conservative over ZF? If we just do introduction of constant symbols, then
of course we do have conservativity over ZF. But we want to support, e.g.,
the introduction of a function symbol for algebraic closure.

Let us consider the following weakened rule. Suppose we have proved

***Let x1,...,xk,y be given. The z such that A(x1,...,xk,y,z) are
structures whose domain includes y, any two of which have an isomorphism
which is the identity on y, and there are such z.***

Then we can introduce a (k+1)-ary function symbol F with the axiom (forall
x1,...,xk,y)(A(x1,...,xk,y,F(x1,...,xk,y))).

THEOREM 2. This restricted expansion of ZF is conservative over ZF, in that
every sentence in the language of ZF that is provable in this restricted
expansion of ZF, is already provable in the original ZF.

Can we be more general? We are really using the important equivalence
relation on structures whose domain contains a set y: the existence of an
isomorphism which is the identity on y. This covers a lot of cases,
including algebraic and real closure. No doubt there are other
constructions that it does not cover. What is it about this equivalence
relation that allows for the conservative extension result (Theorem 2)?

Does Theorem 2 hold if we use ZF\F instead of ZF? (Here F stands for the
axiom of Foundation).

Here is yet another related situation. One would like to, say, construct
the family of all finite groups. Again, the problem in set theory is that
this forms a proper class. All the mathematicians care about is the family
of all finite groups, where isomorphic groups are identified. A common way
this is handled in set theory is to insist that the elements of a group be
natural numbers. This gets all finite groups as a set, but does not address
the idea that one has identified isomorphic finite groups.

In ZFC, one can handle this as follows. Suppose one has a defined
equivalence relation on the universe of sets. Suppose one can prove that
there exists a set A so large that every set is equivalent to an element of
A. Then one can prove that there is a set B such that every set is
equivalent to a unique element of B. And then one can introduce a constant
symbol - as discussed above - for such a set B.

Thus in this expansion of ZFC with constants, one can simply introduce a
constant c for a set of finite groups such that every finite group is
isomorphic to a unique one in c.

What if you want to handle this in ZF? It is well known that there are
equivalence relations for which this cannot be done; i.e., one cannot prove
the existence of a unique set of representatives. Consider, e.g., the
famous equivalence relation on reals of having rational difference.

However, for the equivalence relation of isomorphism, one can get a unique
set of representatives within ZF, provided there is some set of
representatives. A common situation where you have some set of
representatives is where all elements are of cardinality less than some
fixed cardinality.

Thus we can also, in the expansion of ZF with constants, simply introduce a
constant c for a set of finite (or countable, or any cardinality) groups
such that every finite (or coutable, or any cardinality) group is
isomorphic to a unique one in c.

Again, what is it about an equivalence relation that allows for ZF to prove
a unique set of representatives?

An aspect of this question is the special case where the equivalence
relation is a (light-faced) Borel equivalence relation on R. QUESTION: What
is the relationship between the existence of a Borel set of unique
representatives and there being a provable set of unique representatives in
ZF, and there being a definable set of representatives in ZFC?

NOTE: I was writing a posting about Undefinability/Nonstandard Models, and
came up with this posting as I was creating the setting. This posting was
obviously also influenced by the attacks on set theoretic f.o.m. earlier on
the fom. The lesson is this: if you listen carefully to people you strongly
disagree with (intellectual enemies), some interesting (new) ideas will
inevitably result. At the end, you may disagree with them even more
strongly, and they may disagree with you even more strongly. But so what?
And the process can be continued indefinitely. Also note the prolific
interaction of themes in f.o.m.