  Languages with arbitrarily long conjunctions, disjunctions and (possibly) quantifications may also be introduced. For a fixed infinite cardinal λ, the language  L(∞,λ)  is defined by specifying its class of formulas, Form(∞,λ), to be the union, over all κ ≥ λ, of the sets Form(κ,λ). Thus  L(∞,λ)  allows arbitrarily long conjunctions and disjunctions, in the sense that if Φ is an arbitrary subset of Form(∞,λ), then both  ∧Φ  and  ∨Φ  are members of Form(∞,λ). But  L(∞,λ)  admits only quantifications of length &lt; λ: all its formulas have &lt; λ free variables. The language  L(∞,∞)  is defined in turn by specifying its class of formulas, Form(∞,∞), to be the union, over all infinite cardinals λ, of the classes Form(∞,λ). So  L(∞,∞)  allows arbitrarily long quantifications in addition to arbitrarily long conjunctions and disjunctions. Note that Form(∞,λ) and Form(∞,∞) are proper classes in the sense of Gödel-Bernays set theory. Satisfaction of formulas of  L(∞,λ)  and  L(∞,∞)  in a structure may be defined by an obvious extension of the corresponding notion for  L(κ,λ).