 Finite language support

A finite set of formulas mentions only finitely many nonlogical symbols. This observation lets compactness reduce arguments in a language indexed by a large set to a finite sublanguage.