В математической логике , консервативное расширение является супертеорией из теории , которая часто бывает удобно для доказательства теоремы , но не доказывает никаких новых теорем о языке исходной теории. Точно так же неконсервативное расширение - это неконсервативная супертеория, которая может доказать больше теорем, чем оригинал.
Формально говоря, теория является ( теоретическим доказательством ) консервативным расширением теории если каждая теорема это теорема , и любая теорема на языке это уже теорема .
В более общем смысле, если представляет собой набор формул на общем языке а также , тогда является -консервативный по если каждая формула из доказуемо в также доказуемо в .
Обратите внимание, что консервативное расширение непротиворечивой теории непротиворечиво. Если бы не было, то по принципу взрыва каждая формула на языке было бы теоремой , поэтому каждая формула на языке было бы теоремой , так не будет последовательным. Следовательно, консервативные расширения не несут риска внесения новых несоответствий. Это также можно рассматривать как методологию написания и структурирования больших теорий: начните с теории,, который известен (или предполагается), чтобы быть последовательным, и последовательно строить консервативные расширения , , ... этого.
В последнее время консервативные расширения использовались для определения понятия модуля для онтологий : если онтология формализована как логическая теория, субтеория является модулем, если вся онтология является консервативным расширением субтеории.
Расширение, которое не является консервативным, можно назвать правильным расширением .
Примеры
- ACA 0 (подсистема арифметики второго порядка ) является консервативным расширением арифметики Пеано первого порядка .
- Теория множеств фон Неймана – Бернейса – Гёделя является консервативным расширением теории множеств Цермело – Френкеля с аксиомой выбора (ZFC).
- Теория внутренних множеств является консервативным расширением теории множеств Цермело – Френкеля с аксиомой выбора (ZFC).
- Расширения по определениям консервативны.
- Расширения с помощью неограниченных предикатов или функциональных символов консервативны.
- IΣ 1 (подсистема арифметики Пеано с индукцией только для Σ 0 1 -формул ) является Π 0 2 -консервативным расширением примитивной рекурсивной арифметики (PRA). [1]
- ZFC является ∑ 1 3- консервативным расширением ZF по теореме Шенфилда об абсолютности .
- ZFC с гипотезой континуума является Π 2 1- консервативным расширением ZFC. [ необходима цитата ]
Теоретико-модельное консервативное расширение
С помощью теоретико-модельных средств получается более сильное понятие: расширение теории является консервативным с теоретической точки зрения, если и каждая модель можно расширить до модели . Каждое теоретико-модельное консервативное расширение также является (теоретико-доказательным) консервативным расширением в указанном выше смысле. [2] Теоретико-модельное понятие имеет то преимущество перед теоретическим доказательством, что оно не так сильно зависит от используемого языка; с другой стороны, обычно сложнее установить теоретическую консервативность модели.
Рекомендации
- ^ Фернандо Феррейра, Простое доказательство теоремы Парсонса. Журнал Нотр-Дам по формальной логике, том 46, № 1, 2005 г.
- ^ Ходжес, Уилфрид (1997). Более короткая модельная теория . Кембридж: Издательство Кембриджского университета . п. 58 упражнение 8. ISBN 978-0-521-58713-6.