...and Slepnev posted a proof (on the list) that in my formulation, X can be successfully deceived. It's not so much a Henkin sentence, just a program that enumerates all proofs, looking for a particular spurious counterfactual, and doesn't give up until it finds it. If the spurious counterfactual is provable, the program will find it, and so the agent will be tricked by it, and then the spurious counterfactual will be true. We have an implication from provability of the spurious argument to its truth, so by Loeb's theorem it's true, and X is misled. So you were right!