Basic model theory of finitary and infinitary languages of first-order logic with dependent sorts (FOLDS)

The monograph [Mak95] introduced a multi-sorted first-order logic with dependent sorts (FOLDS) likely to serve as a 'perfectly invariant' foundational language for general category theory. In the same work, the model theory for FOLDS was developed to a large extent. We give here the exhaustive proofs for basic facts about the model theory of finitary and infinitary languages for FOLDS, most of which were sketched in [Mak95]