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

Formalized Mathematics (2011)

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

## Access Full Article

top## Abstract

top## How to cite

topMarco 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- Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382, 1990.
- Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990. Zbl06213858
- Grzegorz Bancerek. König's theorem. Formalized Mathematics, 1(3):589-593, 1990.
- Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107-114, 1990.
- Grzegorz Bancerek and Andrzej Trybulec. Miscellaneous facts about functions. Formalized Mathematics, 5(4):485-492, 1996.
- Czesław Byliński. Finite sequences and tuples of elements of a non-empty sets. Formalized Mathematics, 1(3):529-536, 1990.
- Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55-65, 1990.
- Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990.
- Czesław Byliński. Partial functions. Formalized Mathematics, 1(2):357-367, 1990.
- Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990.
- 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
- 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
- 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
- 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
- M. B. Caminati. Yet another proof of Goedel's completeness theorem for first-order classical logic. Arxiv preprint arXiv:0910.2059, 2009.
- Patricia L. Carlson and Grzegorz Bancerek. Context-free grammar - part I. Formalized Mathematics, 2(5):683-687, 1991.
- Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165-167, 1990.
- H. D. Ebbinghaus, J. Flum, and W. Thomas. Mathematical logic. Springer, 1994.
- Rafał Kwiatek and Grzegorz Zwara. The divisibility of integers and integer relative primes. Formalized Mathematics, 1(5):829-832, 1990.
- Beata Padlewska. Families of sets. Formalized Mathematics, 1(1):147-152, 1990.
- Marta Pruszyńska and Marek Dudzicz. On the isomorphism between finite chains. Formalized Mathematics, 9(2):429-430, 2001.
- Konrad Raczkowski and Paweł Sadowski. Equivalence relations and classes of abstraction. Formalized Mathematics, 1(3):441-444, 1990.
- Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1):115-122, 1990.
- Andrzej Trybulec. Tuples, projections and Cartesian products. Formalized Mathematics, 1(1):97-105, 1990.
- Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990.
- Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73-83, 1990.
- Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181-186, 1990.
- Edmund Woronowicz and Anna Zalewska. Properties of binary relations. Formalized Mathematics, 1(1):85-89, 1990.

## Citations in EuDML Documents

top## NotesEmbed ?

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