 Kripke reconstructs a proof of the converse Barcan formula in quantified T and shows that the proof goes through only by allowing the necessitation of a sentence containing a free variable. But if free variables are instead to be considered as universally bound, this step is illicit. Necessitating directly an open formula, without first closing it, amounts to assuming what is to be proved. Kripke’s remarks constitute an objection not so much to the rule of Necessitation, but (following Quine) to the theoremhood of open formulas of first-order logic. Prior 1956 contains a proof of the Barcan formula in the alternative formulation