<abstract xmlns="http://www.w3.org/1999/xhtml"><p>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.</p></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.

Transition of Consistency and Satisfiability under Language Extensions

Mathematisches Institut, Rheinische Friedrich-Wilhelms-Universität Bonn, Endenicher Allee 60, D-53113 Bonn, Germany

Formalized Mathematics

{"article-title":"Transition of Consistency and Satisfiability under Language Extensions"}

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....

Transition of Consistency and Satisfiability under Language Extensions

Published Online: Feb 02, 2013

Page range: 193 - 197

DOI: https://doi.org/10.2478/v10037-012-0022-0

This content is open access.