  The language  L(ω1,ω) occupies a special place among infinitary languages because—like first-order languages—it admits an effective deductive apparatus. In fact, let us add to the usual first-order axioms and rules of inference the new axiom scheme