Sequent Calculus, Derivability, Provability. Gödel's Completeness Theorem

Marco Caminati

Formalized Mathematics (2011)

  • Volume: 19, Issue: 3, page 205-222
  • ISSN: 1426-2630

Abstract

top
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].

How to cite

top

Marco Caminati. "Sequent Calculus, Derivability, Provability. Gödel's Completeness Theorem." Formalized Mathematics 19.3 (2011): 205-222. <http://eudml.org/doc/267726>.

@article{MarcoCaminati2011,
abstract = {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].},
author = {Marco Caminati},
journal = {Formalized Mathematics},
language = {eng},
number = {3},
pages = {205-222},
title = {Sequent Calculus, Derivability, Provability. Gödel's Completeness Theorem},
url = {http://eudml.org/doc/267726},
volume = {19},
year = {2011},
}

TY - JOUR
AU - Marco Caminati
TI - Sequent Calculus, Derivability, Provability. Gödel's Completeness Theorem
JO - Formalized Mathematics
PY - 2011
VL - 19
IS - 3
SP - 205
EP - 222
AB - 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].
LA - eng
UR - http://eudml.org/doc/267726
ER -

References

top
  1. Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382, 1990. 
  2. Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990. Zbl06213858
  3. Grzegorz Bancerek. König's theorem. Formalized Mathematics, 1(3):589-593, 1990. 
  4. Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107-114, 1990. 
  5. Grzegorz Bancerek and Andrzej Trybulec. Miscellaneous facts about functions. Formalized Mathematics, 5(4):485-492, 1996. 
  6. Czesław Byliński. Finite sequences and tuples of elements of a non-empty sets. Formalized Mathematics, 1(3):529-536, 1990. 
  7. Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55-65, 1990. 
  8. Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990. 
  9. Czesław Byliński. Partial functions. Formalized Mathematics, 1(2):357-367, 1990. 
  10. Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990. 
  11. Marco B. Caminati. Preliminaries to classical first order model theory. Formalized Mathematics, 19(3):155-167, 2011, doi: 10.2478/v10037-011-0025-2.[Crossref] Zbl1276.03030
  12. Marco B. Caminati. Definition of first order language with arbitrary alphabet. Syntax of terms, atomic formulas and their subterms. Formalized Mathematics, 19(3):169-178, 2011, doi: 10.2478/v10037-011-0026-1.[Crossref] Zbl1276.03031
  13. Marco B. Caminati. First order languages: Further syntax and semantics. Formalized Mathematics, 19(3):179-192, 2011, doi: 10.2478/v10037-011-0027-0.[Crossref] Zbl1276.03032
  14. Marco B. Caminati. Free interpretation, quotient interpretation and substitution of a letter with a term for first order languages. Formalized Mathematics, 19(3):193-203, 2011, doi: 10.2478/v10037-011-0028-z.[Crossref] Zbl1276.03033
  15. M. B. Caminati. Yet another proof of Goedel's completeness theorem for first-order classical logic. Arxiv preprint arXiv:0910.2059, 2009. 
  16. Patricia L. Carlson and Grzegorz Bancerek. Context-free grammar - part I. Formalized Mathematics, 2(5):683-687, 1991. 
  17. Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165-167, 1990. 
  18. H. D. Ebbinghaus, J. Flum, and W. Thomas. Mathematical logic. Springer, 1994. 
  19. Rafał Kwiatek and Grzegorz Zwara. The divisibility of integers and integer relative primes. Formalized Mathematics, 1(5):829-832, 1990. 
  20. Beata Padlewska. Families of sets. Formalized Mathematics, 1(1):147-152, 1990. 
  21. Marta Pruszyńska and Marek Dudzicz. On the isomorphism between finite chains. Formalized Mathematics, 9(2):429-430, 2001. 
  22. Konrad Raczkowski and Paweł Sadowski. Equivalence relations and classes of abstraction. Formalized Mathematics, 1(3):441-444, 1990. 
  23. Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1):115-122, 1990. 
  24. Andrzej Trybulec. Tuples, projections and Cartesian products. Formalized Mathematics, 1(1):97-105, 1990. 
  25. Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990. 
  26. Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73-83, 1990. 
  27. Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181-186, 1990. 
  28. Edmund Woronowicz and Anna Zalewska. Properties of binary relations. Formalized Mathematics, 1(1):85-89, 1990. 

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.