|
|
Семинары отдела математической логики "Теория доказательств" и "Logic Online Seminar"
19 декабря 2016 г. 18:30–20:30, г. Москва, МИАН (ул. Губкина, 8), ауд. 313 + Zoom
|
|
|
|
|
|
О новом классе теорий, удовлетворяющих второй теореме Гёделя о неполноте
Ф. Н. Пахомов |
Количество просмотров: |
Эта страница: | 168 |
|
Аннотация:
Популярная нестрогая формулировка второй теоремы Гёделя о неполноте утверждает
Всякая достаточно выразительная теория не доказывает собственной непротиворечивости.
Стандартным способом уточнить формулировку "достаточно выразительная теория" являются требования о том, что теория интерпретирует некоторую арифметическую теорию, в которой можно развить теорию работы с формулами и доказательствами, как гёделевыми номерами. Нами будет рассмотрен другой подход к уточнению этой формулировки, фактически, позволяющий приблизиться к нестрогой формулировке
Всякая теория, которая может выразить утверждение о своей непротиворечивости не может его доказать.
Формальнее, нами рассматриваются классические первопорядковые теории, в которых есть некоторое кодирование формул языка самой теории и теория доказывает ряд свойств формул при этом кодирование. Для таких теорий нами устанавливается лемма о неподвижной точке. Далее, стандартным методом может быть установлено, что для любого предиката, удовлетворяющего условиям Гильберта-Бернайса-Лёба, в такого рода теориях не может доказать свою непротиворечивость относительно этого предиката.
Отметим, что само требование на кодирование формул не гарантирует, что теории интерпретируют даже такую слабую теорию, как арифметика Робинсона Q и, более того, такие теории даже могут быть разрешимы. В частности, примером разрешимой теории с таким свойством является теория канторовской функции пары (хотя обратим внимание, что для этой теории нет невырожденных предикатов, удовлетворяющих условиям Гильберта-Бернайса-Лёба).
|
|