Semantic and formal inner-model theorem for L

Fix one axiom sigma. F1 supplies the six basic ZF axioms, while F2, F3, and F4 supply Separation, Power Set, and Replacement; each schema instance uses only its fixed formula and finitely many ZF instances. F6 supplies AC and F5 supplies V=L. Thus for this sigma there is a ZF derivation of ${\sigma }^L$. This assertion is indexed externally by standard axioms and is not an internal truth assertion about all formulas.

Suppose now that M is a transitive set model of ZF. External Separation on M, using satisfaction of the fixed predicate defining constructibility, forms $C=L^M$ as a set. By F5 it is the union of the actual $L_{\alpha }$ for ordinals alpha in M. Hence it is nonempty and transitive, all its ordinals belong to M, and every ordinal of M belongs to C (its successor stage is still indexed in M).

Evaluate each fixed derivation from step 1.1 in M. Its axioms hold there, and first-order inference preserves satisfaction; thus M satisfies the internally relativized sigma. Constructor comparison of that fixed formula, as in F7, identifies this with satisfaction in C: atoms are actual membership and each guarded quantifier ranges over exactly C. Therefore C satisfies each standard axiom of ZFC+V=L. Step 2.1 gives the same-ordinals conclusion. The result remains conditional on the supplied M, with no assertion that a model can be obtained from a consistency statement.