dmitgu (dmitgu) wrote,
dmitgu
dmitgu

Category:

8.1. Первая теорема Гёделя о неполноте

к Оглавлению

Смысл первой теоремы Гёделя следующий: «Это утверждение нельзя доказать в рамках данной теории». Утверждается, что внутри непротиворечивой теории доказать нельзя не только данное утверждение, но и его отрицание. Впрочем – насчёт «но» мы ещё разберём один нюанс.

Гёдель рассматривал предикат доказуемости. За основу он брал (обозначения тут не буквально как у Гёделя) предикат P_0(x, y), который имел простое доказательство, если некое утверждение с текстом в аргументе x доказано текстом из аргумента y. А если это не так, тогда имеется простое доказательство для отрицания данного выражения, то есть – доказано ~P_0(x, y).

Я изложу чуть иначе – P_0(x, y) будет алгоритмом, который возвращает 1, если y доказывает x, и возвращает 0 в противном случае. Смысл от этого не меняется, а наглядность увеличивается – и это ближе к нашей теме из теории алгоритмов. А главное – в следующем подразделе это сильно упростит нам доказательство 2-й т. Гёделя о неполноте.

Тогда выражение y (P_0(x, y) = 1) будет обозначать доказуемость утверждения x. Сокращенное обозначение такое: P(x). А у недоказуемости обозначение будет таким: ~P(x). И это уже – предикаты, а не алгоритмы.

И нам надо применить формулу ~P(x) к самой себе – как мы это рассматривали в Лемме о диагонализации (хоть она у нас об алгоритмах, но для предикатов доказывается то же самое практически, и изложено в учебниках):

~P(diag(«~P(diag(x))»)), это и есть формула из 1-й теорема Гёделя о неполноте. Из данной формулы мы выделим «это утверждение» G, текст которого получается так: diag(«~P(diag(x))»). Вот теперь утверждение ~PG») и обозначает, что «нельзя доказать» (~P(…)) «это» (G) утверждение. В соответствии с леммой о диагонализации получим (вместо равенства – будет эквивалентность для предикатов):

~PG») ó G

Если предположить, что утверждение G доказано, то в силу предыдущей эквивалентности доказано и ~PG»). И – доказано PG»). Последнее доказано потому, что у нас же есть текст для доказательства G – пусть k, значит P_0(«G», k) = 1 и по свойствам квантора существования будет y (P_0(«G», y) = 1). А последнее и есть PG»). А доказанные утверждения ~PG») и PG») образуют противоречие. Поэтому в непротиворечивой теории доказать G нельзя.

Доказывать вторую часть (про недоказуемость ~G) 1ой т. Гёделя теоремы – не обязательно, потому что для наших целей нужна 2-я т. Гёделя, а чтоб доказать 2-ю теорему – нам хватит и первой части 1ой теоремы. Однако ради целостности исторической картины хотя бы популярно разберём и вторую часть 1ой т. Гёделя о неполноте.

Допустим, у нас есть доказательство для ~G с текстом k. Тогда в непротиворечивой теории у нас нет доказательств для G, нет, соответственно, никаких таких q, что P_0(«G», q) = 1. И – вот здесь серьёзный нюанс! – нет доказательства для y (P_0(«G», y) = 1).

Вот переход от того, что в теории нет никаких значений q, при которых доказано выражение B(q) к тому, что тогда и выражение y B(y) не доказано – это свойство называется «омега-непротиворечивость». Оно кажется очевидным, но оно есть не у всех непротиворечивых теорий.

Если есть омега-непротиворечивость – то есть и просто непротиворечивость, потому что при омега-непротиворечивости что-то недоказуемо, а в противоречивой теории доказано всё. Но вот обратное – что непротиворечивая теория ещё и омега-непротиворечивая – не всегда верно.

Так вот, если омега-непротиворечивость есть, то нет доказательства для y (P_0(«G», y) = 1), то есть – нет доказательства для PG»). Но у нас же доказано ~G, у нас же есть эквивалентность ~PG») ó G, и, следовательно, PG») ó ~G. А из последней эквивалентности и ~G вытекает PG»). Но это входит в противоречие с тем, что у нас нет доказательства для PG»).

Первая теорема Гёделя доказана.

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