PL EN


Preferencje help
Widoczny [Schowaj] Abstrakt
Liczba wyników
2012 | 20 | 3 | 193-197
Tytuł artykułu

Transition of Consistency and Satisfiability under Language Extensions

Treść / Zawartość
Warianty tytułu
Języki publikacji
EN
Abstrakty
EN
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.
Słowa kluczowe
Wydawca
Rocznik
Tom
20
Numer
3
Strony
193-197
Opis fizyczny
Daty
wydano
2012-12-01
online
2013-02-02
Twórcy
  • Mathematisches Institut, Rheinische Friedrich-Wilhelms-Universität Bonn, Endenicher Allee 60, D-53113 Bonn, Germany
autor
  • Mathematisches Institut, Rheinische Friedrich-Wilhelms-Universität Bonn, Endenicher Allee 60, D-53113 Bonn, Germany
Bibliografia
  • [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.
Typ dokumentu
Bibliografia
Identyfikatory
Identyfikator YADDA
bwmeta1.element.doi-10_2478_v10037-012-0022-0
JavaScript jest wyłączony w Twojej przeglądarce internetowej. Włącz go, a następnie odśwież stronę, aby móc w pełni z niej korzystać.