Abstract
Let M be a transitive model of ZFC. We say that a transitive model of ZFC, N , is an outer model of M if M is a subset of N and the ordinals coincide.
The outer model theory of M is the collection of all formulas with parameters from M which hold in all outer models of M (which exist in a universe in which M is countable; this is independent of the choice of such a universe). Satisfaction defined with respect to outer models can be seen as a useful strengthening of first-order logic.
Starting from an inaccessible cardinal κ, we show that it is consistent to have a transitive model M of ZFC of size κ in which the outer model theory is lightface definable, and moreover M satisfies V = HOD. The proof combines the infinitary logic L_infinity, omega, Barwise's results on admissible sets, and a new forcing iteration of length strictly less than κ+ which manipulates the continuum function on certain regular cardinals below κ.
In the appendix, we review some unpublished results of Mack Stanley which are directly related to our topic.