False statement: ZF proves L equals V

Let $P=2^{<\omega }$, ordered by extension, with stronger strings below weaker ones. Appending $0$ and appending $1$ gives two incompatible stronger conditions below every $p$, so $P$ is nonempty and atomless. If $M$ is a transitive ground model containing $P$ and $G$ is $M$-generic, F3 gives $G\mathrm{\notin }M$, while the generic-extension construction gives $G\in M[G]$.

If the ground and extension satisfy $K_L$, F4 gives them the same ordinals and F2 gives $L^{M[G]}=L^M\subseteq M$. Step 1.1 then gives $G\in M[G]\setminus L^{M[G]}$, and therefore $M[G]\models V\mathrm{\ne }L$.

Put $U=\mathrm{Z}\mathrm{F}\mathrm{C}+\mathrm{\neg }(V=L)$ and fix an external finite $\mathrm{\Delta }\subseteq U$. Let ${\mathrm{\Delta }}_0$ be its ZFC-labelled members. Enlarge ${\mathrm{\Delta }}_0$ by $K_L$ and by the finitely many target-side ZF instances used in the fixed proofs of generic-extension transitivity, membership of $G$ in the extension and ordinal preservation. For each sentence in this finite enlarged list, expand the corresponding forcing-theorem and extension-axiom proof for $P=2^{<\omega }$. Also retain on the source side $K_L$ and the finitely many instances used to construct $P$, enumerate the ground dense sets, prove the direct atomlessness argument of step 1.1 and carry out the rank proof behind F4. This is one finite formal forcing verification, obtained separately for this fixed $\mathrm{\Delta }$; it makes no uniform assertion over coded fragments.

Apply F5 to the verification in step 3.1. It gives a finite $\mathrm{\Gamma }\subseteq \mathrm{Z}\mathrm{F}\mathrm{C}$ and ZFC proofs of a countable transitive $\mathrm{\Gamma }$-model $M$ and of the corresponding extension $N=M[G]$ satisfying the enlarged target list. The retained source requirements make $M$ a $K_L$-model; the enlarged target list makes $N$ a $K_L$-model. The retained fixed proof blocks give $G\in N\setminus M$ and equality of their ordinals, so F2 gives $N\models \mathrm{\neg }(V=L)$. Consequently the same ZFC conversion proof ends with a set model of the original $\mathrm{\Delta }$, including its extra axiom when that axiom occurs.

Since step 4.1 supplies the two stipulated ZFC proofs for every external finite $\mathrm{\Delta }\subseteq U$, F6 yields externally $\mathrm{Con}(\mathrm{Z}\mathrm{F}\mathrm{C})\to \mathrm{Con}(\mathrm{Z}\mathrm{F}\mathrm{C}+\mathrm{\neg }(V=L))$. Together with F1, the stated $\mathrm{Con}(\mathrm{Z}\mathrm{F})$ hypothesis therefore gives $\mathrm{Con}(\mathrm{Z}\mathrm{F}\mathrm{C}+\mathrm{\neg }(V=L))$.

Suppose instead that ZF proved $V=L$. The same finite derivation is a ZFC derivation. Appending it to the distinguished axiom $\mathrm{\neg }(V=L)$ and then the fixed propositional contradiction block would be a $\mathrm{Z}\mathrm{F}\mathrm{C}+\mathrm{\neg }(V=L)$ refutation, contrary to step 5.1. Hence, assuming $\mathrm{Con}(\mathrm{Z}\mathrm{F})$, ZF does not prove $V=L$. The inner-model theorem proves a relativized assertion about the subclass $L$; it does not identify every ambient set with a constructible set.