%0 Journal Article
%T Sequent Calculus, Derivability, Provability. G del's Completeness Theorem
%A Marco B. Caminati
%J Formalized Mathematics
%@ 1898-9934
%D 2011
%I 
%R 10.2478/v10037-011-0029-y
%X 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 to give the user a slick interface to apply them. The remaining goals summon all the definitions and results introduced in this series of articles. First: D is shown to be correct and having the requisites to deliver a sensible definition of Henkin model (see [18]). Second: as a particular application of all the machinery built thus far, the satisfiability and G del completeness theorems are shown when restricting to countable languages. The techniques used to attain this are inspired from [18], then heavily modified with the twofold goal of embedding them into the more flexible framework of a variable ruleset here introduced, and of proving completeness of a set of rules more sparing than the one there used; in particular the simpler ruleset allowed to avoid the definition and tractation of free occurence of a literal, a fact which, along with shortening proofs, is remarkable in its own right. A preparatory account of some of the ideas used in the proofs given here can be found in [15].
%U http://versita.metapress.com/content/l1308k7164x57n65/?p=402fbc6153ad416ab80168a45b113833&pi=9