Sequent calculus, derivability, provability. Gödel’s completeness theorem.

*(English)*Zbl 1276.03045Summary: 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 \(4L\) 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. 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 [H.-D. Ebbinghaus et al., Mathematical logic. 2nd ed. New York, NY: Springer-Verlag (1994; Zbl 0795.03001)], 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 occurrence 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 [the author, “Yet another proof of Gödel’s completeness theorem for first-order classical logic”, Preprint (2009), arXiv:0910.2059].

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. 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 [H.-D. Ebbinghaus et al., Mathematical logic. 2nd ed. New York, NY: Springer-Verlag (1994; Zbl 0795.03001)], 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 occurrence 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 [the author, “Yet another proof of Gödel’s completeness theorem for first-order classical logic”, Preprint (2009), arXiv:0910.2059].

##### MSC:

03F40 | Gödel numberings and issues of incompleteness |

03B35 | Mechanization of proofs and logical operations |

03C07 | Basic properties of first-order languages and structures |

68T15 | Theorem proving (deduction, resolution, etc.) (MSC2010) |

##### Software:

Mizar
PDF
BibTeX
XML
Cite

\textit{M. Caminati}, Formaliz. Math. 19, No. 3, 205--222 (2011; Zbl 1276.03045)

Full Text:
DOI

**OpenURL**

##### References:

[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. · Zbl 1364.68157 |

[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. · Zbl 1276.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. · Zbl 1276.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. · Zbl 1276.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. · Zbl 1276.03033 |

[15] | M. B. Caminati. Yet another proof of Goedel’s completeness theorem for first-order classical logic. 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. |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.