Transition of Consistency and Satisfiability under Language Extensions

Julian J. Schlöder; Peter Koepke

Formalized Mathematics (2012)

  • Volume: 20, Issue: 3, page 193-197
  • ISSN: 1426-2630

Abstract

top
This article is the first in a series of two Mizar articles constituting a formal proof of the Gödel Completeness theorem [17] for uncountably large languages. We follow the proof given in [18]. The present article contains the techniques required to expand formal languages. We prove that consistent or satisfiable theories retain these properties under changes to the language they are formulated in.

How to cite

top

Julian J. Schlöder, and Peter Koepke. "Transition of Consistency and Satisfiability under Language Extensions." Formalized Mathematics 20.3 (2012): 193-197. <http://eudml.org/doc/268111>.

@article{JulianJ2012,
abstract = {This article is the first in a series of two Mizar articles constituting a formal proof of the Gödel Completeness theorem [17] for uncountably large languages. We follow the proof given in [18]. The present article contains the techniques required to expand formal languages. We prove that consistent or satisfiable theories retain these properties under changes to the language they are formulated in.},
author = {Julian J. Schlöder, Peter Koepke},
journal = {Formalized Mathematics},
keywords = {Mizar; formal proof; Gödel completeness theorem},
language = {eng},
number = {3},
pages = {193-197},
title = {Transition of Consistency and Satisfiability under Language Extensions},
url = {http://eudml.org/doc/268111},
volume = {20},
year = {2012},
}

TY - JOUR
AU - Julian J. Schlöder
AU - Peter Koepke
TI - Transition of Consistency and Satisfiability under Language Extensions
JO - Formalized Mathematics
PY - 2012
VL - 20
IS - 3
SP - 193
EP - 197
AB - This article is the first in a series of two Mizar articles constituting a formal proof of the Gödel Completeness theorem [17] for uncountably large languages. We follow the proof given in [18]. The present article contains the techniques required to expand formal languages. We prove that consistent or satisfiable theories retain these properties under changes to the language they are formulated in.
LA - eng
KW - Mizar; formal proof; Gödel completeness theorem
UR - http://eudml.org/doc/268111
ER -

References

top
  1. [1] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382, 1990. 
  2. [2] Grzegorz Bancerek. K¨onig’s theorem. Formalized Mathematics, 1(3):589-593, 1990. 
  3. [3] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990. 
  4. [4] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107-114, 1990. 
  5. [5] Patrick Braselmann and Peter Koepke. Coincidence lemma and substitution lemma. Formalized Mathematics, 13(1):17-26, 2005. 
  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: Elementary properties. Formalized Mathematics, 13(1):5-15, 2005. 
  10. [10] 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. 
  11. [11] Czesław Bylinski. A classical first order language. Formalized Mathematics, 1(4):669-676, 1990. 
  12. [12] Czesław Bylinski. Functions and their basic properties. Formalized Mathematics, 1(1):55-65, 1990. 
  13. [13] Czesław Bylinski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990. 
  14. [14] Czesław Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990. 
  15. [15] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165-167, 1990. 
  16. [16] Agata Darmochwał. A first-order predicate calculus. Formalized Mathematics, 1(4):689-695, 1990. 
  17. [17] Kurt Gödel. Die Vollst¨andigkeit der Axiome des logischen Funktionenkalk¨uls. Monatshefte f¨ur Mathematik und Physik 37, 1930. 
  18. [18] W. Thomas H.-D. Ebbinghaus, J. Flum. Einf¨uhrung in die Mathematische Logik. Springer-Verlag, Berlin Heidelberg, 2007. 
  19. [19] Piotr Rudnicki and Andrzej Trybulec. A first order language. Formalized Mathematics, 1(2):303-311, 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. 
  24. [24] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181-186, 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.