We study Σ1(ω1)-definable sets (i.e., sets that are equal to the collection of all sets satisfying a certain Σ1-formula with parameter ω1 ) in the presence of large cardinals. Our results show that the existence of a Woodin cardinal and a measurable cardinal above it imply that no well-ordering of the reals is Σ1(ω1)-definable, the set of all stationary subsets of ω1 is not Σ1(ω1)-definable and the complement of every Σ1(ω1)-definable Bernstein subset of ${}_{}^{{\omega _1}}\omega _1^{}$ is not Σ1(ω1)-definable. In contrast, we show that the existence of a Woodin cardinal is compatible with the existence of a Σ1(ω1)-definable well-ordering of H(ω2) and the existence of a Δ1(ω1)-definable Bernstein subset of ${}_{}^{{\omega _1}}\omega _1^{}$. We also show that, if there are infinitely many Woodin cardinals and a measurable cardinal above them, then there is no Σ1(ω1)-definable uniformization of the club filter on ω1. Moreover, we prove a perfect set theorem for Σ1(ω1)-definable subsets of ${}_{}^{{\omega _1}}\omega _1^{}$, assuming that there is a measurable cardinal and the nonstationary ideal on ω1 is saturated. The proofs of these results use iterated generic ultrapowers and Woodin’s ℙmax-forcing. Finally, we also prove variants of some of these results for Σ1(κ)-definable subsets of κκ, in the case where κ itself has certain large cardinal properties.

The main result of this paper is a combinatorial characterization of Magidor-generic sequences. Using this characterization, I show that the critical sequences of certain iterations are Magidor-generic over the target model. I then employ these results in order to analyze which other Magidor sequences exist in a Magidor extension. One result in this direction is that if we temporarily identify Magidor sequences with their ranges, then Magidor sequences are maximal, in the sense that they contain any other Magidor sequence that is present in their forcing extension, even if the other sequence is generic for a different Magidor forcing. A stronger result holds if both sequences come from the same forcing: I show that a Magidor sequence is almost unique in its forcing extension, in the sense that any other sequence generic for the same forcing which is present in the same forcing extension coincides with the original sequence at all but finitely many coordinates, and at all limit coordinates. Further, I ask the question: If d ε V[c], where c and d are Magidor-generic over V, then which Magidor forcing can d be generic for? It turns out that it must essentially be a collapsed version of the Magidor forcing for which c was generic. I treat several related questions as well. Finally, I introduce a special case of Magidor forcing which I call minimal Magidor forcing. This approach simplifies the forcing, and I prove that it doesn’t restrict the class of possible Magidor sequences. That is, if c is generic for a Magidor forcing over V, then it is generic for a minimal Magidor forcing over V.