Консервативное расширение - Conservative extension

В математической логике , консервативное расширение является супертеорией из теории , которая часто бывает удобно для доказательства теоремы , но не доказывает никаких новых теорем о языке исходной теории. Точно так же неконсервативное расширение - это неконсервативная супертеория, которая может доказать больше теорем, чем оригинал.

Формально говоря, теория является ( теоретическим доказательством ) консервативным расширением теории, если каждая теорема о является теоремой о , а любая теорема о на языке о уже является теоремой о . ${\ displaystyle T_ {2}}$ ${\ displaystyle T_ {1}}$ ${\ displaystyle T_ {1}}$ ${\ displaystyle T_ {2}}$ ${\ displaystyle T_ {2}}$ ${\ displaystyle T_ {1}}$ ${\ displaystyle T_ {1}}$

В более общем смысле, if является набором формул на общем языке и , то является -консервативным по сравнению, если каждая формула из доказуемой в также доказуема в . ${\ displaystyle \ Gamma}$ ${\ displaystyle T_ {1}}$ ${\ displaystyle T_ {2}}$ ${\ displaystyle T_ {2}}$ ${\ displaystyle \ Gamma}$ ${\ displaystyle T_ {1}}$ ${\ displaystyle \ Gamma}$ ${\ displaystyle T_ {2}}$ ${\ displaystyle T_ {1}}$

Обратите внимание, что консервативное расширение непротиворечивой теории непротиворечиво. Если бы это было не так, то по принципу взрыва каждая формула на языке была бы теоремой о , поэтому каждая формула на языке была бы теоремой о , поэтому не была бы непротиворечивой. Следовательно, консервативные расширения не несут риска внесения новых несоответствий. Это также можно рассматривать в качестве методологии для написания и структурирования больших теорий: начать с теорией , которая , как известно (или предполагается) , чтобы быть последовательными, и последовательно строить консервативные расширения , ... от него. ${\ displaystyle T_ {2}}$ ${\ displaystyle T_ {2}}$ ${\ displaystyle T_ {1}}$ ${\ displaystyle T_ {1}}$ ${\ displaystyle T_ {1}}$ ${\ displaystyle T_ {0}}$ ${\ displaystyle T_ {1}}$ ${\ displaystyle T_ {2}}$

В последнее время консервативные расширения использовались для определения понятия модуля для онтологий : если онтология формализована как логическая теория, субтеория является модулем, если вся онтология является консервативным расширением субтеории.

Расширение, которое не является консервативным, можно назвать правильным расширением .

Примеры

ACA ₀ (подсистема арифметики второго порядка ) является консервативным расширением арифметики Пеано первого порядка .
Теория множеств фон Неймана – Бернейса – Гёделя является консервативным расширением теории множеств Цермело – Френкеля с аксиомой выбора (ZFC).
Теория внутренних множеств является консервативным расширением теории множеств Цермело – Френкеля с аксиомой выбора (ZFC).
Расширения по определению консервативны.
Расширения с помощью неограниченных предикатов или функциональных символов консервативны.
IΣ ₁ (подсистема арифметики Пеано с индукцией только для Σ ⁰₁ -формул ) является Π ⁰₂ -консервативным расширением примитивной рекурсивной арифметики (PRA).
ZFC является Σ ¹_3- консервативным расширением ZF по теореме Шенфилда об абсолютности .
ZFC с гипотезой континуума является Π ²_1- консервативным расширением ZFC.

Теоретико-модельное консервативное расширение

С помощью теоретико-модельных средств получается более сильное понятие: расширение теории является теоретически консервативным, если и каждая модель может быть расширена до модели . Каждое теоретико-модельное консервативное расширение также является (теоретико-доказательным) консервативным расширением в указанном выше смысле. Теоретико-модельное понятие имеет то преимущество перед теоретическим доказательством, что оно не так сильно зависит от используемого языка; с другой стороны, обычно сложнее установить теоретическую консервативность модели. ${\ displaystyle T_ {2}}$ ${\ displaystyle T_ {1}}$ ${\ displaystyle T_ {1} \ substeq T_ {2}}$ ${\ displaystyle T_ {1}}$ ${\ displaystyle T_ {2}}$