Sequent Calculus, Derivability, Provability. Gödel's Completeness Theorem
Fifth of a series of articles laying down the bases for classical first order model theory. This paper presents multiple themes: first it introduces sequents, rules and sets of rules for a first order language L as L-dependent types. Then defines derivability and provability according to a set of rules, and gives several technical lemmas binding all those concepts. Following that, it introduces a fixed set D of derivation rules, and proceeds to convert them to Mizar functorial cluster registrations...