The Gödel Completeness Theorem for Uncountable Languages

Julian J. Schlöder; Peter Koepke

Formalized Mathematics (2012)

  • Volume: 20, Issue: 3, page 199-203
  • ISSN: 1426-2630

Abstract

top
This article is the second in a series of two Mizar articles constituting a formal proof of the Gödel Completeness theorem [15] for uncountably large languages. We follow the proof given in [16]. The present article contains the techniques required to expand a theory such that the expanded theory contains witnesses and is negation faithful. Then the completeness theorem follows immediately.

How to cite

top

Julian J. Schlöder, and Peter Koepke. "The Gödel Completeness Theorem for Uncountable Languages." Formalized Mathematics 20.3 (2012): 199-203. <http://eudml.org/doc/268200>.

@article{JulianJ2012,
abstract = {This article is the second in a series of two Mizar articles constituting a formal proof of the Gödel Completeness theorem [15] for uncountably large languages. We follow the proof given in [16]. The present article contains the techniques required to expand a theory such that the expanded theory contains witnesses and is negation faithful. Then the completeness theorem follows immediately.},
author = {Julian J. Schlöder, Peter Koepke},
journal = {Formalized Mathematics},
keywords = {Mizar; formal proof; Gödel completeness theorem},
language = {eng},
number = {3},
pages = {199-203},
title = {The Gödel Completeness Theorem for Uncountable Languages},
url = {http://eudml.org/doc/268200},
volume = {20},
year = {2012},
}

TY - JOUR
AU - Julian J. Schlöder
AU - Peter Koepke
TI - The Gödel Completeness Theorem for Uncountable Languages
JO - Formalized Mathematics
PY - 2012
VL - 20
IS - 3
SP - 199
EP - 203
AB - This article is the second in a series of two Mizar articles constituting a formal proof of the Gödel Completeness theorem [15] for uncountably large languages. We follow the proof given in [16]. The present article contains the techniques required to expand a theory such that the expanded theory contains witnesses and is negation faithful. Then the completeness theorem follows immediately.
LA - eng
KW - Mizar; formal proof; Gödel completeness theorem
UR - http://eudml.org/doc/268200
ER -

References

top
  1. [1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382, 1990. 
  2. [2] Grzegorz Bancerek. The fundamental properties of natural numbers. Formalized Mathematics, 1(1):41-46, 1990. Zbl06213858
  3. [3] Grzegorz Bancerek. König’s theorem. Formalized Mathematics, 1(3):589-593, 1990. 
  4. [4] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990. 
  5. [5] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107-114, 1990. 
  6. [6] Patrick Braselmann and Peter Koepke. Equivalences of inconsistency and Henkin models. Formalized Mathematics, 13(1):45-48, 2005. 
  7. [7] Patrick Braselmann and Peter Koepke. G¨odel’s completeness theorem. Formalized Mathematics, 13(1):49-53, 2005. 
  8. [8] Patrick Braselmann and Peter Koepke. A sequent calculus for first-order logic. FormalizedMathematics, 13(1):33-39, 2005. 
  9. [9] 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. 
  10. [10] Czesław Bylinski. A classical first order language. Formalized Mathematics, 1(4):669-676, 1990. 
  11. [11] Czesław Bylinski. Functions and their basic properties. Formalized Mathematics, 1(1):55-65, 1990. 
  12. [12] Czesław Bylinski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990. 
  13. [13] Czesław Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990. 
  14. [14] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165-167, 1990. 
  15. [15] Kurt G¨odel. Die Vollst¨andigkeit der Axiome des logischen Funktionenkalk¨uls. Monatshefte f¨ur Mathematik und Physik 37, 1930. 
  16. [16] W. Thomas H.-D. Ebbinghaus, J. Flum. Einf¨uhrung in die Mathematische Logik. Springer-Verlag, Berlin Heidelberg, 2007. 
  17. [17] Piotr Rudnicki and Andrzej Trybulec. A first order language. Formalized Mathematics, 1(2):303-311, 1990. 
  18. [18] Julian J. Schlöder and Peter Koepke. Transition of consistency and satisfiability under language extensions. Formalized Mathematics, 20(3):193-197, 2012, doi: 10.2478/v10037-012-0022-0.[Crossref] Zbl1288.03034
  19. [19] Andrzej Trybulec. Domains and their Cartesian products. Formalized Mathematics, 1(1):115-122, 1990. 
  20. [20] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990. 
  21. [21] Edmund Woronowicz. Interpretation and satisfiability in the first order logic. FormalizedMathematics, 1(4):739-743, 1990. 
  22. [22] Edmund Woronowicz. Many argument relations. Formalized Mathematics, 1(4):733-737, 1990. 
  23. [23] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73-83, 1990. 

NotesEmbed ?

top

You must be logged in to post comments.

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

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.