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

• Autorzy: Marco Caminati
• Języki publikacji: EN

Abstrakty

EN

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

• Wydawca: De Gruyter Open
• Czasopismo: Formalized Mathematics
• Rocznik: 2011
• Tom: 19
• Numer: 3
• Strony: 205-222

Daty

wydano

2011-01-01

online

2012-04-26

Twórcy

autor

Marco Caminati

• Mathematics Department "G. Castelnuovo", Sapienza University of Rome, Piazzale Aldo Moro 5, 00185 Roma, Italy

Bibliografia

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

Identyfikatory

DOI

10.2478/v10037-011-0029-y