@LinearChristmas \Vdash usually means "forces" not "entails". "Entails" is \models. Look at exercise II.4.30 In the newer Kunen

@LinearChristmas Your concern about the reflection theorem running afoul of Godel makes sense, but I don't see how the expressibility of entailment could be the problem. Being able to express entailment is the only way that we could even make sense of the idea that a theory proving there is a model of itself contradicts the incompleteness theorem.

The answer is (a). The reflection theorem says (or implies) that for any fragment of ZFC, ZFC proves there is a model of that fragment. For each fragment, the promised proof is different, and uses the axioms of the fragment, assorted other axioms, and some instances of replacement that depend on the fragment.

Since the replacement axioms used involve the sentences of the fragment, there's no obvious reason why the axioms used the proof shouldn't always be strictly stronger than the fragment, and a big reason why they should (Godel).

(I meant finite fragment, not just fragment.)

@spaceisdarkgreen Notice that I put \vDash (not \Vdash), that should be the correct symbol? Or is there some small difference here? You're right that \models would be better semantically, for that I apologise. I used detexify which yielded \vDash, so looked no further.

@spaceisdarkgreen I have heard whispers... that for any proof that uses at least one instance of the replacement schema, there is an alternative proof which uses exactly one instance of replacement. But that is not enough either.

@spaceisdarkgreen About why "encoding entailment could be the problem". It would be the source of the problem if, for instance, we could also encode "is class model". Is that not correct? So I guess I just extended that intuition :)