FOM: sharp boundaries/tameness

[Kanovei]

>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