# 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

## Access Full Article

top## Abstract

top## How to cite

topJulian 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] Grzegorz Bancerek. Cardinal numbers. Formalized Mathematics, 1(2):377-382, 1990.
- [2] Grzegorz Bancerek. K¨onig’s theorem. Formalized Mathematics, 1(3):589-593, 1990.
- [3] Grzegorz Bancerek. The ordinal numbers. Formalized Mathematics, 1(1):91-96, 1990.
- [4] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Formalized Mathematics, 1(1):107-114, 1990.
- [5] Patrick Braselmann and Peter Koepke. Coincidence lemma and substitution lemma. Formalized Mathematics, 13(1):17-26, 2005.
- [6] Patrick Braselmann and Peter Koepke. Equivalences of inconsistency and Henkin models. Formalized Mathematics, 13(1):45-48, 2005.
- [7] Patrick Braselmann and Peter Koepke. G¨odel’s completeness theorem. Formalized Mathematics, 13(1):49-53, 2005.
- [8] Patrick Braselmann and Peter Koepke. A sequent calculus for first-order logic. FormalizedMathematics, 13(1):33-39, 2005.
- [9] Patrick Braselmann and Peter Koepke. Substitution in first-order formulas: Elementary properties. Formalized Mathematics, 13(1):5-15, 2005.
- [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] Czesław Bylinski. A classical first order language. Formalized Mathematics, 1(4):669-676, 1990.
- [12] Czesław Bylinski. Functions and their basic properties. Formalized Mathematics, 1(1):55-65, 1990.
- [13] Czesław Bylinski. Functions from a set to a set. Formalized Mathematics, 1(1):153-164, 1990.
- [14] Czesław Bylinski. Some basic properties of sets. Formalized Mathematics, 1(1):47-53, 1990.
- [15] Agata Darmochwał. Finite sets. Formalized Mathematics, 1(1):165-167, 1990.
- [16] Agata Darmochwał. A first-order predicate calculus. Formalized Mathematics, 1(4):689-695, 1990.
- [17] Kurt Gödel. Die Vollst¨andigkeit der Axiome des logischen Funktionenkalk¨uls. Monatshefte f¨ur Mathematik und Physik 37, 1930.
- [18] W. Thomas H.-D. Ebbinghaus, J. Flum. Einf¨uhrung in die Mathematische Logik. Springer-Verlag, Berlin Heidelberg, 2007.
- [19] Piotr Rudnicki and Andrzej Trybulec. A first order language. Formalized Mathematics, 1(2):303-311, 1990.
- [20] Zinaida Trybulec. Properties of subsets. Formalized Mathematics, 1(1):67-71, 1990.
- [21] Edmund Woronowicz. Interpretation and satisfiability in the first order logic. FormalizedMathematics, 1(4):739-743, 1990.
- [22] Edmund Woronowicz. Many argument relations. Formalized Mathematics, 1(4):733-737, 1990.
- [23] Edmund Woronowicz. Relations and their basic properties. Formalized Mathematics, 1(1):73-83, 1990.
- [24] Edmund Woronowicz. Relations defined on sets. Formalized Mathematics, 1(1):181-186, 1990.

## Citations in EuDML Documents

top## NotesEmbed ?

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