Solution (source code)

= Solution

\b[An <inner model> of <ZFC> is a transitive class containing every <ordinal> and satisfying all its axioms.] Write this class as $A$ with its inherited membership relation. Satisfaction is interpreted by restricting all quantifiers to $A$. In a first-order formulation this is a schema for a definable class, possibly with fixed parameters. The class may equal the whole universe. Transitivity means $x\in y\in A\Rightarrow x\in A$; containing all <ordinals> rules out treating an arbitrary <transitive set> model as an <inner model>.