Remarks on an infinitary language with constructive formulas

Abstract
It is well known that L, the first-order predicate calculus, is unsuitable for characterizing certain mathematical structures. Since some of those structures are quite often considered by mathematicians, extensions of L have been considered which (partially) solve the above problem. Roughly speaking, the extensions of L fall into two main categories: (I) extensions obtained by allowing higher order variables, and (II) extensions obtained by allowing infinitely long formulas.