Coding by club-sequences

Given any subset A of ω1 there is a proper partial order which forces that the predicate x∈A and the predicate x∈ω1∖A can be expressed by -provably incompatible Σ3 formulas over the structure 〈Hω2,∈,NSω1〉. Also, if there is an inaccessible cardinal, then there is a proper partial order which forces the existence of a well-order of Hω2 definable over 〈Hω2,∈,NSω1〉 by a provably antisymmetric Σ3 formula with two free variables. The proofs of these results involve a technique for manipulating the guessing properties of club-sequences defined on stationary subsets of ω1 at will in such a way that the Σ3 theory of 〈Hω2,∈,NSω1〉 with countable ordinals as parameters is forced to code a prescribed subset of ω1. On the other hand, using theorems due to Woodin it can be shown that, in the presence of sufficiently strong large cardinals, the above results are close to optimal from the point of view of the Levy hierarchy.