Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
Tytuł: Sequent Calculus, Derivability, Provability. Gödel's Completeness Theorem
Autorzy: Caminati, Marco
Data wydania: 2011
Data dodania: 6-gru-2015
Wydawca: De Gruyter Open
Źródło: Formalized Mathematics, Volume 19, Issue 3, 2011, Pages 205-222
Abstrakt: 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].
Afiliacja: Mathematics Department "G. Castelnuovo", Sapienza University of Rome, Piazzale Aldo Moro 5, 00185 Roma, Italy
DOI: 10.2478/v10037-011-0029-y
ISSN: 1426-2630
Typ Dokumentu: Article
Występuje w kolekcji(ach):Formalized Mathematics, 2011, Volume 19, Issue 3

Pliki w tej pozycji:
Plik Opis RozmiarFormat 
v10037-011-0029-y.pdf311,65 kBAdobe PDFOtwórz
Pokaż pełny widok rekordu Zobacz statystyki

Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL Creative Commons