@MISC{FOMODEL4.MIZ,
  AUTHOR = {Caminati, Marco B.},
  NOTE1 = {The author wrote this paper as part of his PhD thesis research},
  ACKNOWLEDGEMENT = {I would like to thank Marco Pedicini for his encouragement and support.},
  SECTION1 = {Constructions for countable languages: witness adjoining},
  SECTION2 = {Constructions for countable languages: consistently maximizing a set of formulas of a countable language (Lindenbaum's lemma)},
  DAY = {29},
  MONTH = {December},
  YEAR = {2010},
  ADDRESS1 = {Mathematics Department "G.Castelnuovo"\\Sapienza University of Rome\\Piazzale Aldo Moro 5, 00185 Roma, Italy},
  TITLE = {Sequent calculus, derivability, provability. Goedel's completeness theorem.},
  SUMMARY = {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 FO 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 \CITE{ebbinghaus1994mathematical})
- second, as a particular application of all the machinery built thus far, the satisfiability and Goedel completeness theorems are shown when restricting to countable languages.
The techniques used to attain this are inspired from \CITE{ebbinghaus1994mathematical}, 
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 \CITE{caminati2009yet}.
}}

@book{ebbinghaus1994mathematical,
  title={{Mathematical logic}},
  author={Ebbinghaus, H.D. and Flum, J. and Thomas, W.},
  year={1994},
  publisher={Springer}
}

@article{caminati2009yet,
  title={{Yet another proof of Goedel's completeness theorem for first-order classical logic}},
  author={Caminati, M.B.},
  journal={Arxiv preprint arXiv:0910.2059},
  year={2009}
}



