[FOM] The use of replacement in model theory

[Harvey Friedman]

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