Введение
В математической логике консервативное расширение — это супертеория теории, которая часто удобна для доказательства теорем, но не доказывает новых теорем о языке исходной теории. Аналогично, неконсервативное расширение — это супертеория, которая не является консервативной и может доказать больше теорем, чем исходная. Более формально, теория *T₂* является (в теоретико-доказательном смысле) консервативным расширением теории *T₁*, если каждая теорема *T₂* является теоремой *T₁*, и любая теорема *T₂* на языке *T₁* уже является теоремой *T₁*. Более общо, если *S* — множество формул на общем языке *T₁* и *T₂*, то *T₂* консервативно над *T₁*, если каждая формула из *S*, доказуемая в *T₂*, также доказуема в *T₁*. Следует отметить, что консервативное расширение непротиворечивой теории является непротиворечивым. Если бы это не было так, то по принципу взрыва, каждая формула на языке *T₁* была бы теоремой *T₂*, следовательно, каждая формула на языке *T₁* была бы теоремой *T₂*, а значит, *T₁* не была бы непротиворечивой. Таким образом, консервативные расширения не несут риска введения новых противоречий. Это также можно рассматривать как методологию написания и структурирования больших теорий: начать с теории *T₁*, которая известна (или предполагается) непротиворечивой, и последовательно строить консервативные расширения *T₂*, *T₃* и т.д. из нее. В последнее время консервативные расширения используются для определения понятия модуля для онтологий: если онтология формализована как логическая теория, то подтеория является модулем, если вся онтология является консервативным расширением подтеории. Расширение, которое не является консервативным, может быть названо собственным расширением.
More generally, if is a set of formulas in the common language of and , then is conservative over if every formula from provable in is also provable in
Note that a conservative extension of a consistent theory is consistent. If it were not, then by the principle of explosion, every formula in the language of would be a theorem of , so every formula in the language of would be a theorem of , so would not be consistent. Hence, conservative extensions do not bear the risk of introducing new inconsistencies. This can also be seen as a methodology for writing and structuring large theories: start with a theory, , that is known (or assumed) to be consistent, and successively build conservative extensions , , of it. Recently, conservative extensions have been used for defining a notion of module for ontologies: if an ontology is formalized as a logical theory, a subtheory is a module if the whole ontology is a conservative extension of the subtheory. An extension which is not conservative may be called a proper extension.
Примеры
, подсистема арифметики второго порядка, изучаемая в обратной математике, является консервативным расширением арифметики Пеано первого порядка. Подсистемы арифметики второго порядка и консервативны над . Подсистема является консервативным расширением , и консервативна над (примитивно рекурсивной арифметикой). является консервативным расширением по теореме абсолютности Шоенфилда. с гипотезой континуума является консервативным расширением .
Консервативное расширение теоретической модели
С помощью средств теории моделей получается более сильное понятие: расширение теории является модель-теоретически консервативным, если и каждая модель теории может быть расширена до модели . Любое модель-теоретически консервативное расширение также является (доказательно-) консервативным расширением в вышеуказанном смысле. Модель-теоретическое понятие имеет преимущество перед доказательно-теоретическим в том, что оно не так сильно зависит от используемого языка; с другой стороны, установить модель-теоретическую консервативность обычно сложнее.