CODING INTO H(ω2), TOGETHER (OR NOT) WITH FORCING AXIOMS.

This paper is mainly a survey of recent results concerning the possibility of building forcing extensions in which there is a simple definition, over the structure 〈H(ω₂), ∈〉 and without parameters, of a prescribed member of H(ω₂) or of a well-order of H(ω₂). Some of these results are in conjunction with strong forcing axioms like PFA⁺⁺ or MM, some are not. I also observe (Corollary 4.4) that the existence of certain objects of size ℵ₁ follows outright from the existence of large cardinals. This observation is motivated by an (unsuccessful) attempt to extend a PFA⁺⁺ result to one mentioning MM⁺⁺.