Консервативное расширение

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

Более формально сформулированная теория $T_{2}$ является ( теоретико-доказательным ) консервативным расширением теории $T_{1}$ если каждая теорема $T_{1}$ представляет собой теорему $T_{2}$ и любая теорема $T_{2}$ на языке $T_{1}$ это уже теорема $T_{1}$ .

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

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

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

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

Примеры

${\mathsf {ACA}}_{0}$ , подсистема арифметики второго порядка, изучаемая в обратной математике , является консервативным расширением арифметики Пеано первого порядка .
Подсистемы арифметики второго порядка ${\mathsf {RCA}}_{0}^{*}$ и ${\mathsf {WKL}}_{0}^{*}$ являются $\Pi _{2}^{0}$ -консервативный ${\mathsf {EFA}}$ . ^[1]
Подсистема ${\mathsf {WKL}}_{0}$ это $\Pi _{1}^{1}$ -консервативное расширение ${\mathsf {RCA}}_{0}$ и $\Pi _{2}^{0}$ -консервативный ${\mathsf {PRA}}$ ( примитивная рекурсивная арифметика ). ^[1]
Теория множеств фон Неймана–Бернейса–Гёделя ( ${\mathsf {NBG}}$ ) является консервативным расширением теории множеств Цермело–Френкеля с аксиомой выбора ( ${\mathsf {ZFC}}$ ).
Внутренняя теория множеств представляет собой консервативное расширение теории множеств Цермело – Френкеля с аксиомой выбора ( ${\mathsf {ZFC}}$ ).
Расширения по определениям консервативны.
Расширения с помощью неограниченных предикатов или функциональных символов консервативны.
$I\Sigma _{1}$ (подсистема арифметики Пеано с индукцией только по $\Sigma _{1}^{0}$ -формулы ) — это $\Pi _{2}^{0}$ -консервативное расширение ${\mathsf {PRA}}$ . ^[2]
${\mathsf {ZFC}}$ это $\Sigma _{3}^{1}$ -консервативное расширение ${\mathsf {ZF}}$ по теореме Шенфилда об абсолютности .
${\mathsf {ZFC}}$ с гипотезой континуума является $\Pi _{1}^{2}$ -консервативное расширение ${\mathsf {ZFC}}$ . ^{[ нужна ссылка ]}

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

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

См. также

Ссылки

^ Перейти обратно: ^а ^б С.Г. Симпсон, Р.Л. Смит, « Факторизация полиномов и $\Sigma _{1}^{0}$ -индукция » (1986). Анналы чистой и прикладной логики, т. 31 (с.305)
^ Фернандо Феррейра, Простое доказательство теоремы Парсонса. Журнал формальной логики Нотр-Дама, том 46, № 1, 2005.
^ Ходжес, Уилфрид (1997). Более короткая модель теории . Кембридж: Издательство Кембриджского университета . п. 58 упражнение 8. ISBN 978-0-521-58713-6 .

Внешние ссылки

Важность консервативных расширений основ математики.

[Simpson86-1] Перейти обратно: ^а ^б С.Г. Симпсон, Р.Л. Смит, « Факторизация полиномов и $\Sigma _{1}^{0}$ -индукция » (1986). Анналы чистой и прикладной логики, т. 31 (с.305)

[2] Фернандо Феррейра, Простое доказательство теоремы Парсонса. Журнал формальной логики Нотр-Дама, том 46, № 1, 2005.

[3] Ходжес, Уилфрид (1997). Более короткая модель теории . Кембридж: Издательство Кембриджского университета . п. 58 упражнение 8. ISBN 978-0-521-58713-6 .

[1]

[2]

[3]