Compactness Theorem for First-Order Logic

This is a translation of a HOL Light formalization covering foundational results in first-order model theory, including the compactness of first-order logic. The original work is described in the following paper: Formalizing Basic First Order Model Theory John Harrison Proceedings of the 11th International Conference on Theorem Proving in Higher Order Logics, TPHOLs'98, Springer LNCS 1497, pp. 153-170. The corresponding HOL Light theories can be found on GitHub.