  (4.1) is proved by analyzing the set-theoretic definition of  H(ω1) and showing that it can be “internally” formulated in  L(ω1,ω1). (4.2) is established in much the same way as Tarski's theorem on the undefinability of truth for first- or second-order languages. (4.3) is obtained by formalizing the definition of the coding map σ  ↦  ⌈σ⌉ in  L(ω1,ω1). 