[FOM] The use of replacement in model theory

Harvey Friedman friedman at math.ohio-state.edu
Sat Jan 30 13:33:29 EST 2010

On Jan 28, 2010, at 5:23 PM, John Baldwin wrote:

> Byunghan Kim proved that for a simple first order theory non-forking
> is
> equivalent to
> non-dividing. The notions of simple, non-forking, and non-dividing
> are all
> statements about countable sets of formulas.  Nevertheless, the
> argument
> for the result employs Morley's technique for omitting types; that
> is it
> uses the Erdos-Rado theorem on all cardinals less than $> \beth_{\omega_1}$.
>
> Thus, a priori, this is a use of the replacement axiom for a result
> whose
> statement does not require replacement.  (I use this more technical
> example rather than the original Hanf number computation, precisely
> for
> this reason).
>
> Does any one know whether this use is essential?
>
> An introductory account of this topic appears in the paper by Kim and
> Pillay: From stability to simplicity, Bulletin of Symbolic Logic,
> 4, (1998), 17-36.

The definition of forking starts on page 20 of [Kim,Pillay]. However,
the second sentence says "and we work in a saturated model C of T of
cardinality kappa for some large kappa. It is sometimes convenient to
assume that kappa is strongly inaccessible". So I read this as an
indication that the definition is not "about countable sets of
formulas".

Is there a theorem in countable mathematics in this area of model
theory whose only known proof uses more than ZC? If so, I would
appreciate a self contained indication in an FOM sposting of what the
statement is in purely countable terms.

In the case of Hnaf numbers, which is NOT such an example, readers may
wish to look at

H. Friedman, On Existence Proofs of Hanf Numbers, J. of Symbolic
Logic, Vol. 39, No. 2, (1974), pp. 318-324.

Harvey Friedman