  §§1 and 2. Infinitary propositional and predicate languages seem to have made their first explicit appearance in print with the papers of Scott and Tarski [1958] and Tarski [1958]. The completeness theorem for  L(ω1,ω), as well as for other infinitary languages, was proved by Karp [1964]. The Hanf number calculations for  L(ω1,ω) were first performed by Morley [1965]. The nondefinability of well-orderings in finite-quantifier languages was proved by Karp [1965] and Lopez-Escobar [1966]. The interpolation theorem for  L(ω1,ω) was proved by Lopez-Escobar [1965] and Scott's isomorphism theorem for  L(ω1,ω) by Scott [1965]. 