dmitgu (dmitgu) wrote,
dmitgu
dmitgu

Category:

... 8.1, Окончание. Первая теорема Гёделя о неполноте.

к Оглавлению


Хоть 1-я теорема Гёделя и требовала омега-непротиворечивости, но математическое сообщество признало, что мечты о полноте провалились. Программа Гильберта тогда показала свою эффективность и принесла важнейшие результаты.

К тому же, прикладных математиков не интересуют теории омега-противорчивые – там даже предикат доказуемости может неправильно работать. И теория Пеано является (как и прочие прикладные теории) омега-непротиворечивой. Интересные рассуждения (и отсылки к главам с доказательствами) о внешней непротиворечивости можно почитать у Д. Гильберта, П. Бернайса «Основания математики», Том 2, Глава 5 «Выход за рамки теории доказательств», Раздел 1 «Границы изобразимости и выводимости», Подраздел б) «Первая теорема Гёделя о неполноте» - в конце подраздела. А ранее середины подраздела сформулировано и понятие омега-непротиворечивости. Тема довольно принципиальная, кстати, хоть и подзабытая – думаю, временно.

Омега-непротиворечивость – это про то, что если некое утверждение недоказуемо в частном (при подстановке вместо x любого конкретного числа), то недоказуемо и в общем (в смысле «существования»). А внешняя непротиворечивость – это про то, что если доказуемо в частном, то потенциально доказуемо и в общем (для «любого»). И оба случая «особой» непротиворечивости включают в себя и «обычную» непротиворечивость.

Притом «потенциально доказуемо» означает, что расширив непротиворечивую теорию аксиомой-обобщением частных случаев, мы получим опять  непротиворечивую теорию.

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

Омега-непротиворечивость не очень интересна, так как чуть ниже будет приведена первая теорема Гёделя в форме Россера, где удаётся обойтись обычной непротиворечивостью, а вот для одного дополнительного доказательства после 2ой теоремы Гёделя нам потребуется внешняя непротиворечивость.

Поэтому дам пояснения:

Если почитать доказательство непротиворечивости теории Пеано в Э.Мендельсон «Введение в математическую логику» - то там сразу получается и доказательство внешней непротиворечивости. Дело в том, что теория-инструмент S_∞ включает в себя правило бесконечной индукции: Когда предикат A(n) истинный для каждого числа n, то выводится x A(x).

Для S_∞ выводятся все те замкнутые формулы , которые выводятся для теории S (теории Пеано). То есть – если бы в S выводилось существование чего-то, то – выводилось бы и в S_∞. Но существование x ~A(x) противоречиво в S_∞ для того A(n), который верен для каждого n: Так как в силу бесконечной индукции будет выведено «для любого» x A(x), что является отрицанием (противоречит) для x ~A(x). Поэтому, если теория S_∞ является просто непротиворечивой (а она является), то она является и внешне непротиворечивой. А раз в S_∞ не доказываются какие-то абсурдные утверждения с квантором существования, то тем более не доказаны они и в теории Пеано – а значит и там имеет место внешняя непротиворечивость.

Интересно, что квантор существования – это отрицание квантора «для любого» и напрямую из бесконечной индукции не выводится. Но дело в том, что вывод из S в «Введение в математическую логику» опирается только на правила вывода MP (из импликации и посылки выводится следствие) и Gen (из истинного A(x) выводится x A(x) ). А квантор существования определяется через квантор «для любого». Теория получается эквивалентной тому, что и в «Основаниях математики» – хотя в «Основаниях математики» есть свои правила вывода для кванторов «существует» и «для любого». В этом смысле подход Э.Мендельсона удобен для использования S_∞ – разбираться приходится только с одним квантором, а второй (квантор существования) не имеет самостоятельного значения.

И вот при правилах вывода MP и Gen выводы опираются лишь на то, что в состоянии сделать и S_∞. Поэтому ничего сверх того, что может делать S_∞, от неё не требуется для того, чтобы повторить доступное для вывода в S. Отсюда, кстати видно, что для внешней противоречивости потребовалось бы некая аксиома с квантором существования или нечто эквивалентное. А то, что имеется в Пеано, не содержит ничего подобного аксиоме о существовании небывалого.

Позже Б. Россер так построил формулировку 1-й теоремы Гёделя о неполноте, что она не требовала омега-непроиворечивости при доказательстве. Не углубляясь в формулы, 1-я теорема Гёделя в форме Россера такая:

«Если это утверждение доказано в данной теории, то в данной теории доказано его отрицание и длина доказательства отрицания не превышает доказательство данного утверждения».

Очевидно, что само утверждение Россера без противоречий нельзя доказать – противоречие (отрицание) будет найдено в заранее известном ограниченном наборе доказательств. А если и не будет найдено – то это тоже будет противоречием.

Отрицание Россера будет конъюнкцией 2х членов (отрицание импликации):

1. Доказанное утверждение Россера (опять оно!)

2. Отсутствие доказательства отрицания Россера в пределах известной длины.

Но само утверждение Россера (член 1) включает в себя требование наличия доказательства своего отрицания в пределах известной длины. А раз утверждение доказано (член 1), то и его требование истинно. И это истинное требование входит в противоречие с членом 2.

В строгом доказательстве нужна аккуратность, чтобы проделать всё это под кванторами, но кванторы охватывают ограниченный (а не бесконечный) круг объектов и доказательство всё равно получается небольшое. Подробности, например, в Э. Мендельсон, «Введение в математическую логику», Глава 3 «Формальная арифметика», раздел 5 «Теорема Гёделя для теории S». Или в указанном чуть выше подразделе «Оснований математики», но там «в нагрузку» решается много дополнительных вопросов.


Tags: NP≠P дискуссии, ЖЖвЖЖ математика
Subscribe

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 0 comments