W BIAŁYMSTOKU
Proszę używać tego identyfikatora do cytowań lub wstaw link do tej pozycji:
http://hdl.handle.net/11320/21383Pełny rekord metadanych
| Pole DC | Wartość | Język |
|---|---|---|
| dc.contributor.author | Braselmann, Patrick | - |
| dc.contributor.author | Koepke, Peter | - |
| dc.date.accessioned | 2026-10-30T09:52:16Z | - |
| dc.date.available | 2026-10-30T09:52:16Z | - |
| dc.date.issued | 2005 | - |
| dc.identifier.citation | Formalized Mathematics, Volume 13, Issue 1, Pages 49-53 | pl |
| dc.identifier.issn | 1426-2630 | - |
| dc.identifier.uri | http://hdl.handle.net/11320/21383 | - |
| dc.description.abstract | This articleis part of a series of Mizar articles which constitute a formal proof (of a basic version) of Kurt Gödel’s famous completeness theorem (K. Gödel, “Die Vollständigkeit der Axiome des logischen Funktionenkalkuls”, Monatshefte für Mathematik und Physik 37 (1930), 349–360). The completeness theorem provides the theoretical basis for a uniform formalization of mathematics as in the Mizar project. We formalize first-order logic up to the completeness theorem as in H. D. Ebbinghaus, J. Flum, and W. Thomas, Mathematical Logic, 1984, Springer Verlag New York Inc. The present article contains the proof of a simplified completeness theorem for a countable relational language without equality. | pl |
| dc.language.iso | en | pl |
| dc.publisher | University of Białystok | pl |
| dc.rights | Attribution-ShareAlike 4.0 International | - |
| dc.rights.uri | https://creativecommons.org/licenses/by-sa/4.0/ | - |
| dc.title | Gödel’s Completeness Theorem | pl |
| dc.type | Article | pl |
| dc.rights.holder | © 2005 University of Białystok | pl |
| dc.rights.holder | This work is licensed under the Creative Commons License. | pl |
| dc.description.Affiliation | Patrick Braselmann - University of Bonn | pl |
| dc.description.Affiliation | Peter Koepke - University of Bonn | pl |
| dc.description.references | Grzegorz Bancerek. Connectives and subformulae of the first order language. Formalized Mathematics, 1(3):451–458, 1990. | pl |
| dc.description.references | Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41–46, 1990. | pl |
| dc.description.references | Grzegorz Bancerek. Countable sets and Hessenberg’s theorem. Formalized Mathematics, 2(1):65–69, 1991. | pl |
| dc.description.references | Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107–114, 1990. | pl |
| dc.description.references | Patrick Braselmann and Peter Koepke. Coincidence lemma and substitution lemma. Formalized Mathematics, 13(1):17–26, 2005. | pl |
| dc.description.references | Patrick Braselmann and Peter Koepke. Equivalences of inconsistency and Henkin models. Formalized Mathematics, 13(1):45–48, 2005. | pl |
| dc.description.references | Patrick Braselmann and Peter Koepke. Equivalences of inconsistency and Henkin models. Formalized Mathematics, 13(1):45–48, 2005. | pl |
| dc.description.references | Patrick Braselmann and Peter Koepke. Substitution in first-order formulas: Elementary properties. Formalized Mathematics, 13(1):5–15, 2005. | pl |
| dc.description.references | Patrick Braselmann and Peter Koepke. Substitution in first-order formulas. Part II. The construction of first-order formulas. Formalized Mathematics, 13(1):27–32, 2005. | pl |
| dc.description.references | Czesław Byliński. A classical first order language. Formalized Mathematics, 1(4):669–676, 1990. | pl |
| dc.description.references | Czesław Byliński. Functions and their basic properties. Formalized Mathematics, 1(1):55-65, 1990. | pl |
| dc.description.references | Czesław Byliński. Functions from a set to a set. Formalized Mathematics, 1(1):153–164, 1990. | pl |
| dc.description.references | Czesław Byliński. Some basic properties of sets. Formalized Mathematics, 1(1):47–53, 1990. | pl |
| dc.description.references | Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165–167, 1990. | pl |
| dc.description.references | Agata Darmochwał and Andrzej Trybulec. Similarity of formulae. Formalized Mathematics, 2(5):635–642, 1991. | pl |
| dc.description.references | Piotr Rudnicki and Andrzej Trybulec. A first order language. Formalized Mathematics, 1(2):303–311, 1990. | pl |
| dc.description.references | Andrzej Trybulec. Subsets of complex numbers. To appear in Formalized Mathematics. | pl |
| dc.description.references | Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1):115–122, 1990. | pl |
| dc.description.references | Andrzej Trybulec. Tarski Grothendieck set theory. Formalized Mathematics, 1(1):9–11, 1990. | pl |
| dc.description.references | Andrzej Trybulec. Tuples, projections and Cartesian products. Formalized Mathematics, 1(1):97–105, 1990. | pl |
| dc.description.references | Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67–71, 1990. | pl |
| dc.description.references | Edmund Woronowicz. Interpretation and satisfiability in the first order logic. Formalized Mathematics, 1(4):739–743, 1990. | pl |
| dc.description.references | Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73–83, 1990. | pl |
| dc.description.references | Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181–186, 1990. | pl |
| dc.identifier.eissn | 1898-9934 | - |
| dc.description.volume | 13 | pl |
| dc.description.issue | 1 | pl |
| dc.description.firstpage | 49 | pl |
| dc.description.lastpage | 53 | pl |
| dc.identifier.citation2 | Formalized Mathematics | pl |
| Występuje w kolekcji(ach): | Formalized Mathematics, 2005, Volume 13, Issue 1 | |
Pliki w tej pozycji:
| Plik | Opis | Rozmiar | Format | |
|---|---|---|---|---|
| Godel’s_Completeness_Theorem.pdf | 92,33 kB | Adobe PDF | Otwórz |
Pozycja ta dostępna jest na podstawie licencji Licencja Creative Commons CCL
