FOM: sharp boundaries/tameness

[Harvey Friedman]

>  >Date: Wed, 13 Feb 2002 10:26:35 -0500
>>From: Harvey Friedman <friedman at math.ohio-state.edu>
>
>>
>there is no formula of set theory, phi(x), such that ZFC proves
>
>i) there exists a unique x such that phi(x);
>ii) x is such a proper elementary extension.
>>
>
>To this statement, can a reference be given?
>A standard Luxemburg construction of a nonmeasurable
>set does not really work in the Solovay model because
>elements of a definable "nonstandard universe" are not
>necessarily themselves definable.
>
>V.Kanovei


-- 
>I claim that from any proper elementary extension of the real field 
>together with a predicate for the integers, one can explicitly 
>obtain a nonprincipal ultrafilter on all subsets of omega.


I claim that from any proper elementary extension of the real field 
together with a predicate for the integers, one can explicitly define 
a finitely additive nonatomic probability measure on all subsets of 
omega.

It is well known that there is no formula of set theory, phi(x), such 
that ZFC proves

i) there exists a unique x such that phi(x);
ii) x is a finitely addivite nonatomic probability measure on all 
subsets of omega.

E.g., this follows from "there is no ordinally definable finitely 
additive nonatomic probability measure on all subsets of omega when 
you add a Cohen real".

*********************************************************

In connection with my question at the end of my posting of 10:26AM, 
2/13/02, there is the following well known fact:

Any 0-minimal expansion of the real field has an explicit proper 
elementary extension. Namely, the germs at infinity of the definable 
functions in one variable.

**********************************************************

I wrote R[x] for a proper elementary extension of the real field. 
This is not the appropriate notation. R[x] usually means the field or 
ordered field resulting from adjoining the "infinitely large" 
indeterminate x to R. To get a proper elementary extension, one has 
to then take the algebraic closure.