Definable Models Without Choice

Jun 07 2018, 23:48

Suppose that a parameter formula defines an inner model. Does that inner model satisfy choice?

Well, obviously, if choice failed then the answer is no, just by taking \(x=x\). But what if we remove that option. Namely, if the inner model is not the entire universe, then choice holds.