In mathematical logic, the conservativity theorem states the following: Suppose that a closed formula <math>\exists x_1\ldots\exists x_m\,\varphi(x_1,\ldots,x_m)</math> is a theorem of a first-order theory <math>T</math>. Let <math>T_1</math> be a theory obtained from <math>T</math> by extending its language with new constants <math>a_1,\ldots,a_m</math> and adding a new axiom <math>\varphi(a_1,\ldots,a_m)</math>.

PropertyValue
dbpprop:abstract
  • In mathematical logic, the conservativity theorem states the following: Suppose that a closed formula <math>\exists x_1\ldots\exists x_m\,\varphi(x_1,\ldots,x_m)</math> is a theorem of a first-order theory <math>T</math>. Let <math>T_1</math> be a theory obtained from <math>T</math> by extending its language with new constants <math>a_1,\ldots,a_m</math> and adding a new axiom <math>\varphi(a_1,\ldots,a_m)</math>. Then <math>T_1</math> is a conservative extension of <math>T</math>, which means that the theory <math>T_1</math> has the same set of theorems in the original language (i.e. , without constants <math>a_i\,\!</math>) as the theory <math>T</math>. In a more general setting, the conservativity theorem is formulated for extensions of a first-order theory by introducing a new functional symbol: Suppose that a closed formula <math>\forall \vec{y}\,\exists x\,\!\,\varphi(x,\vec{y})</math> is a theorem of a first-order theory <math>T</math>, where we denote <math>\vec{y}:=(y_1,\ldots,y_n)</math>. Let <math>T_1</math> be a theory obtained from <math>T</math> by extending its language with new functional symbol <math>f\,\!</math> (of arity <math>n</math>) and adding a new axiom <math>\forall \vec{y}\,\varphi(f,\vec{y})</math>. Then <math>T_1</math> is a conservative extension of <math>T</math>, i.e. the theories <math>T</math> and <math>T_1</math> prove the same theorems not involving the functional symbol <math>f\,\!</math>).
dbpprop:hasPhotoCollection
rdf:type
rdfs:comment
  • In mathematical logic, the conservativity theorem states the following: Suppose that a closed formula <math>\exists x_1\ldots\exists x_m\,\varphi(x_1,\ldots,x_m)</math> is a theorem of a first-order theory <math>T</math>. Let <math>T_1</math> be a theory obtained from <math>T</math> by extending its language with new constants <math>a_1,\ldots,a_m</math> and adding a new axiom <math>\varphi(a_1,\ldots,a_m)</math>.
rdfs:label
  • Conservativity theorem
owl:sameAs
skos:subject
foaf:page
is owl:sameAs of