Чому нас вчить теорема Геделя. Теорема Геделя про неповноту формальної арифметики

Однією з найвідоміших теорем математичної логіки пощастило і не пощастило одночасно. У цьому вона схожа на спеціальну теорію відносності Ейнштейна. З одного боку, майже всі про них щось чули. З іншого - у народній інтерпретації теорія Ейнштейна, як відомо, «каже, що все у світі щодо». А теорема Геделя про неповноту (далі просто ТГН), приблизно так само вільного фолк-формулювання, «Доводить, що є речі, незбагненні для людського розуму». І ось одні намагаються пристосувати її як аргумент проти матеріалізму, а інші, навпаки, доводять за її допомогою, що бога немає. Забавно не тільки те, що обидві сторони не можуть виявитися правими одночасно, але й те, що ні ті, ні інші не спроможні розібратися, що ж, власне, ця теорема стверджує.

Отже, що? Нижче я спробую "на пальцях" розповісти про це. Виклад мій буде, зрозуміло несуворим та інтуїтивним, але я попрошу математиків не судити мене суворо. Можливо, що для нематематиків (до яких, взагалі-то, належу і я), у розказаному нижче буде щось нове та корисне.

Математична логіка – наука справді досить складна, а головне – не дуже звична. Вона вимагає акуратних і строгих маневрів, у яких важливо не переплутати реально доведене про те, що «і так зрозуміло». Тим не менш, я сподіваюся, що для розуміння наступного нижче «малюнок доказу ТГН» читачеві знадобиться лише знання шкільної математики/інформатики, навички логічного мислення та 15-20 хвилин часу.

Дещо спрощуючи, ТГН стверджує, що у досить складних мовах існують недоказні висловлювання. Але цієї фрази майже кожне слово потребує пояснення.

Почнемо із того, що спробуємо розібратися, що таке доказ. Візьмемо якесь шкільне завдання з арифметики. Наприклад, нехай потрібно довести вірність наступної нехитрої формули: «» (нагадаю, що символ читається «для будь-якого» і називається «квантор загальності»). Довести її можна, тотожно перетворюючи, скажімо, так:

Перехід від однієї формули до іншої відбувається за деякими відомими правилами. Перехід від 4-ї формули до 5-ї відбувся, скажімо, тому, що всяке число дорівнює самому собі - така аксіома арифметики. А вся процедура доведення, таким чином, переводить формулу в булеве значення ІСТИНА. Результатом могла бути і брехня - якби ми спростовували якусь формулу. У такому разі ми б довели її заперечення. Можна собі уявити програму (і такі програми дійсно написані), які доводили б подібні (і складніші) висловлювання без участі людини.

Викладемо те саме трохи формальніше. Нехай у нас є безліч, що складається з рядків символів якогось алфавіту, і існують правила, за якими з цих рядків можна виділити підмножину так званих висловлювань- тобто граматично осмислених фраз, кожна з яких є істинною або помилковою. Можна сміливо сказати, що є функція , зіставляюча висловлюванням з одне із двох значень: ІСТИНА чи БРЕХНЯ (тобто що їх у булево безліч із двох елементів).

Назвемо таку пару - безліч висловлювань і функція з - «мовою висловлювань». Зауважимо, що у повсякденному сенсі поняття мови дещо ширше. Наприклад, фраза російської мови "А ну йди сюди!"не істинна і хибна, тобто висловлюванням, з погляду математичної логіки, немає.

Для подальшого нам знадобиться поняття алгоритму. Наводити тут формальне визначення я не буду - це завело б нас досить далеко в бік. Обмежуся неформальним: «алгоритм»- ця послідовність однозначних інструкцій («програма»), яка за кінцеву кількість кроківпереводить вихідні дані на результат. Виділене курсивом важливо - якщо на якихось початкових даних програма зациклюється, то алгоритму вона не описує. Для простоти та у застосуванні до нашого випадку читач може вважати, що алгоритм - це програма, написана будь-якою відомою йому мовою програмування, яка для будь-яких вхідних даних із заданого класу гарантовано завершує свою роботу з видачею булевого результату.

Запитаємо себе: чи для будь-якої функції існує «доказовий алгоритм» (або, коротше, «дедуктика»), еквівалентний цій функції, тобто перекладає кожне висловлювання саме в те булеве значення, що і вона? Лаконічніше те саме питання можна сформулювати так: чи будь-яка функція над безліччю висловлювань обчислювана? Як ви вже здогадуєтеся, із справедливості ТГН випливає, що ні, не всяка – існують незліченні функції такого типу. Інакше кажучи, не всяке правильне висловлювання можна довести.

Цілком можливо, що це твердження викличе у вас внутрішній протест. Пов'язано це з кількома обставинами. По-перше, коли нас вчать шкільній математиці, то іноді виникає помилкове враження майже повної тотожності фраз «теорема вірна» та «можна довести чи перевірити теорему». Але якщо вдуматися, це зовсім не очевидно. Деякі теореми доводяться досить просто (наприклад, перебором небагатьох варіантів), а деякі - дуже складно. Згадаймо, наприклад, знамениту Велику теорему Ферма:

доказ якої знайшли лише через три з половиною століття після першого формулювання (і воно далеко не просто). Слід розрізняти істинність висловлювання та її доказовість. Нізвідки годі було, що немає істинних, але недоказуваних (і які перевіряються повною мірою) висловлювань.

Другий інтуїтивний аргумент проти ТГН тонший. Припустимо, у нас є якесь недоказове (в рамках цієї дедуктики) висловлювання. Що заважає нам прийняти його як нову аксіому? Тим самим ми трохи ускладнимо нашу систему доказів, але це не страшно. Цей аргумент був би цілком вірний, якби недоказних висловлювань було кінцеве число. Насправді ж може статися таке - після постулювання нової аксіоми ви натрапите на нове недоказне висловлювання. Прийміть його ще як аксіоми - натрапите на третє. І так до безкінечності. Говорять, що дедуктика залишиться неповний. Ми можемо також вжити силових заходів, щоб алгоритм, що доводить, закінчувався через кінцеве число кроків з якимось результатом для будь-якого висловлювання мови. Але при цьому він почне брехати – приводити до істини для невірних висловлювань, або до брехні – для вірних. У таких випадках кажуть, що дедуктика суперечлива. Таким чином, ще одне формулювання ТГН звучить так: «Існують мови висловлювань, для яких неможлива повна несуперечлива дедуктика» - звідси назва теореми.

Іноді називають «теоремою Ґеделя» твердження про те, що будь-яка теорія містить проблеми, які не можуть бути вирішені в рамках самої теорії та потребують її узагальнення. В якомусь сенсі це вірно, хоча таке формулювання швидше затьмарює питання, ніж прояснює його.

Зауважу також, що якби йшлося про звичні функції, що відображають безліч речових чисел у нього ж, то «незлічуваність» функції нікого б не здивувала (тільки не треба плутати «обчислювані функції» та «числи, що обчислюються» - це різні речі). Будь-якому школяру відомо, що, скажімо, у разі функції вам має сильно пощастити з аргументом, щоб процес обчислення точного десяткового уявлення значення цієї функції скінчився за кінцеве число кроків. А швидше за все ви обчислюватимете її за допомогою нескінченного ряду, і це обчислення ніколи не приведе до точного результату, хоча може підійти до нього як завгодно близько - просто тому, що значення синуса більшості аргументів ірраціонально. ТГН просто говорить нам про те, що навіть серед функцій, аргументами якої є рядки, а значеннями - нуль або одиниця, незліченні функції, хоч і зовсім інакше влаштовані, теж бувають.

Для подальшого опишемо «мову формальної арифметики». Розглянемо клас рядків тексту кінцевої довжини, що складаються з арабських цифр, змінних (літер латинського алфавіту), що приймають натуральні значення, прогалин, знаків арифметичних дій, рівності та нерівності, кванторів («існує») і («для будь-якого») і, можливо , якихось символів (точна їх кількість і склад для нас неважливі). Зрозуміло, що не всі такі рядки осмислені (наприклад, «-» - це безглуздя). Підмножина осмислених виразів із цього класу (тобто рядків, які є істинними чи хибними з погляду звичайної арифметики) і буде нашим безліччю висловлювань.

Приклади висловлювань формальної арифметики:

і т.д. Тепер назвемо «формулою з вільним параметром» (ФСП) рядок, який стає висловлюванням, якщо як цей параметр підставити до неї натуральне число. Приклади ФСП (з параметром):

і т.д. Інакше кажучи, ФСП еквівалентні функцій натурального аргументу з булевими значенням.

Позначимо безліч всіх ФСП буквою. Зрозуміло, що його можна впорядкувати (наприклад, спочатку випишемо впорядковані за алфавітом однолітерні формули, за ними - дволітерні і т.д.; за яким саме алфавітом відбуватиметься впорядкування, нам непринципово). Таким чином, будь-яка ФСП відповідає її номеру в упорядкованому списку, і ми позначатимемо її .

Перейдемо тепер до нарису доказу ТГН у такому формулюванні:

• Для мови висловлювань формальної арифметики немає повної несуперечливої ​​дедуктики.

Доводитимемо від протилежного.

Отже, скажімо, що така дедуктика існує. Опишемо наступний допоміжний алгоритм, що ставить у відповідність натуральному числу булеве значення наступним чином:

Простіше кажучи, алгоритм призводить до значення ІСТИНА тоді й лише тоді, коли результат підстановки у ФСП її власного номера у списку дає хибне висловлювання.

Тут ми підходимо до єдиного місця, де я попрошу читача повірити мені на слово.

Очевидно, що, при зробленому вище припущенні, будь-який ФСП можна зіставити алгоритм, що містить на вході натуральне число, а на виході - значення значення. Менш очевидним є зворотне твердження:

Доказ цієї леми зажадав би, як мінімум, формального, а чи не інтуїтивного, визначення поняття алгоритму. Однак, якщо трохи подумати, вона досить правдоподібна. Справді, алгоритми записуються алгоритмічними мовами, серед яких є такі екзотичні, як, наприклад, Brainfuck, що складається з восьми односимвольних слів, на якому, проте, можна реалізувати будь-який алгоритм. Дивно було б, якби описана нами багатша мова формул формальної арифметики виявилася б біднішою - хоча, без сумніву, для звичайного програмування вона не дуже підходить.

Пройшовши це слизьке місце, ми швидко дістаємось до кінця.

Отже, вище описали алгоритм . Відповідно до леми, в яку я попросив вас повірити, існує еквівалентна йому ФСП. Вона має якийсь номер у списку – скажімо, . Запитаємо себе, чому одно? Нехай це ІСТИНА. Тоді, по побудові алгоритму (а отже, і еквівалентної йому функції), це означає, що результат підстановки числа в функцію - брехня. Аналогічно перевіряється і зворотне: з БРЕХНЯ випливає ІСТИНА. Ми дійшли протиріччя, отже, вихідне припущення неправильно. Отже, для формальної арифметики немає повної несуперечливої ​​дедуктики. Що й потрібно було довести.

Тут доречно згадати Епіменіда (див. портрет у заголовку), який, як відомо, заявив, що всі критяни - брехуни, сам будучи критянином. У більш лаконічному формулюванні його висловлювання (відоме як «парадокс брехуна») можна сформулювати так: «Я брешу». Саме такий вислів, який сам проголошує свою хибність, ми й використали для доказу.

Насамкінець я хочу зауважити, що нічого особливого дивного ТГН не стверджує. Зрештою, всі давно звикли, що не всі числа представимі у вигляді відношення двох цілих (пам'ятаєте, це твердження має дуже витончений доказ, якому більше двох тисяч років?). І корінням поліномів з раціональними коефіцієнтами є також не всі числа. А тепер з'ясувалося, що не всі функції натурального аргументу обчислювані.

Наведений малюнок докази ставився до формальної арифметики, але неважко зрозуміти, що ТГН застосовна і до інших мов висловлювань. Зрозуміло, не всі мови такі. Наприклад, визначимо мову так:

• "Будь-яка фраза китайської мови є вірним висловлюванням, якщо вона міститься в цитатнику товариша Мао Дзе Дуна, і невірна, якщо не міститься".

Тоді відповідний повний і несуперечливий алгоритм, що доводить (його можна назвати «догматичною дедуктикою») виглядає приблизно так:

• «Гаркуй цитатник товариша Мао Дзе Дуна, поки не знайдеш шуканий вислів. Якщо воно знайдено, то воно вірне, а якщо цитатник закінчився, а висловлювання не знайдено, воно неправильне».

Тут нас рятує те, що будь-який цитатник, вочевидь, є кінцевим, тому процес «доведення» неминуче закінчиться. Таким чином, до мови догматичних висловлювань ТГН не застосовується. Але ж ми говорили про складні мови, правда?

Будь-яка система математичних аксіом починаючи з певного рівня складності або внутрішньо суперечлива, або неповна.

У 1900 році в Парижі пройшла Всесвітня конференція математиків, на якій Давид Гільберт (David Hilbert, 1862-1943) виклав у вигляді тез сформульовані ним 23 найважливіші, на його думку, завдання, які потрібно було вирішити вченим-теоретикам Х століття. Під другим номером у його списку значилося одне з тих простих завдань, відповідь на які здається очевидним, поки не копнеш трішки глибше. Говорячи сучасною мовою, це було питання: чи математика є самодостатньою? Друге завдання Гільберта полягала в необхідності суворо довести, що система аксіом— базових тверджень, що приймаються в математиці за основу без доказів, — досконала та повна, тобто дозволяє математично описати все, що існує. Треба було довести, що можна задати таку систему аксіом, що вони будуть, по-перше, взаємно несуперечливими, а по-друге, з них можна вивести висновок щодо істинності чи хибності будь-якого твердження.

Візьмемо приклад із шкільної геометрії. У стандартній Євклідової планіметрії(Геометрії на площині) можна беззастережно довести, що твердження «сума кутів трикутника дорівнює 180 °» істинно, а твердження «сума кутів трикутника дорівнює 137 °» хибно. Якщо говорити по суті, то в Евклідовій геометрії будь-яке твердження або хибно, або істинно, і третього не дано. І на початку ХХ століття математики наївно вважали, що така ж ситуація має спостерігатися у будь-якій логічно несуперечливій системі.

І тут 1931 року якийсь віденський очкарик — математик Курт Гедель — узяв і опублікував коротку статтю, яка просто перекинула весь світ так званої «математичної логіки». Після довгих та складних математико-теоретичних преамбул він встановив буквально таке. Візьмемо будь-яке твердження типу: «Припущення №247 у цій системі аксіом логічно недоведено» і назвемо його «затвердженням A». Так ось, Гедель просто довів таку дивовижну властивість будь-якийсистеми аксіом:

"Якщо можна довести твердження A, то можна довести і твердження не-A".

Іншими словами, якщо можна довести справедливість затвердження «припущення 247 не можна довести і справедливість затвердження «припущення 247 доведено». Тобто, повертаючись до формулювання другого завдання Гільберта, якщо система аксіом повна (тобто будь-яке твердження у ній може бути доведено), вона суперечлива.

Єдиним виходом із такої ситуації залишається прийняття неповної системи аксіом. Тобто доводиться миритися з тим, що в контексті будь-якої логічної системи у нас залишаться твердження «типу А», які є свідомо істинними чи хибними, — і ми можемо судити про їхню істинність лише позарамок прийнятої нами аксіоматики. Якщо ж таких тверджень немає, значить наша аксіоматика суперечлива, і в її рамках неминуче будуть присутні формулювання, які можна одночасно і довести, і спростувати.

Отже, формулювання першою,або слабкою теореми Геделя про неповноту: «Будь-яка формальна система аксіом містить невирішені припущення». Але на цьому Гедель не зупинився, сформулювавши та довівши другу,або сильну теорему Геделя про неповноту: «Логічна повнота (або неповнота) будь-якої системи аксіом не може бути доведена у рамках цієї системи. Для її доказу чи спростування потрібні додаткові аксіоми (посилення системи)».

Спокійніше було б думати, що теореми Геделя мають абстрактний характер і стосуються не нас, а лише областей піднесеної математичної логіки, проте фактично виявилося, що вони пов'язані з пристроєм людського мозку. Англійський математик і фізик Роджер Пенроуз (Roger Penrose, р. 1931) показав, що теореми Ґеделя можна використовуватиме докази наявності важливих відмінностей між людським мозком і комп'ютером. Сенс його міркування простий. Комп'ютер діє строго логічно і не здатний визначити, істинно чи хибно твердження А, якщо воно виходить за рамки аксіоматики, а такі твердження, згідно з теоремою Геделя, неминуче є. Людина ж, зіткнувшись із таким логічно недоведеним і незаперечним твердженням А, завжди здатна визначити його істинність чи хибність — виходячи з повсякденного досвіду. Принаймні у цьому людський мозок перевершує комп'ютер, скований чистими логічними схемами. Людський мозок здатний зрозуміти всю глибину істини, яка полягає в теоремах Геделя, а комп'ютерний — ніколи. Отже, людський мозок є будь-що, але не просто комп'ютер. Він здатний приймати рішення, і тест Тьюринга пройде успішно

Цікаво, чи здогадувався Гільберт, як далеко заведуть нас його запитання?

Kurt Godel, 1906-78

Австрійський, згодом американський математик. Народився в Брюнн (Brünn, нині Брно, Чехія). Закінчив Віденський університет, де й залишився викладачем кафедри математики (з 1930 року – професором). У 1931 році опублікував теорему, яка згодом отримала його ім'я. Будучи людиною суто аполітичною, вкрай тяжко пережив убивство свого друга та співробітника по кафедрі студентом-нацистом і впав у глибоку депресію, рецидиви якої переслідували його до кінця життя. У 1930-ті роки емігрував було до США, але повернувся до рідної Австрії та одружився. У 1940 році, в розпал війни, вимушено біг до Америки транзитом через СРСР та Японію. Деякий час пропрацював у Прінстонському інституті перспективних досліджень. На жаль, психіка вченого не витримала, і він помер у психіатричній клініці від голоду, відмовляючись їсти, оскільки був переконаний, що його мають намір отруїти.

Теорема Геделя про неповноту

Успенський В.А.

Мабуть, теорема Геделя про неповноту є справді унікальною. Унікальна в тому, що на неї посилаються, коли хочуть довести "все на світі" - від наявності богів до відсутності розуму. Мене завжди цікавило більш "первинне питання" - а хто з тих, хто посилається на теорему про неповноту, зміг би не тільки сформулювати її, а й довести? Я публікую цю статтю з тієї причини, що в ній викладено цілком доступне формулювання теореми Геделя. Рекомендую попередньо ознайомитись зі статтею Тулліо Редже Курт Гедель та його знаменита теорема

Висновок про неможливість універсального критерію істини є безпосереднім наслідком результату, отриманого Тарським шляхом з'єднання теореми Геделя про нерозв'язність з його власною теорією істини, згідно з яким універсального критерію істини не може бути навіть щодо вузької області теорії чисел, а значить, і для будь-якої науки, що використовує арифметику. Природно, що це результат застосовний a fortiori до поняття істини у будь-якій нематематичної області знання, у якій широко використовується арифметика.

Карл Поппер

Успенський Володимир Андрійович народився 27 листопада 1930 р. в Москві. Закінчив механіко-математичний факультет МДУ (1952). Доктор фізико-математичних наук (1964). Професор, завідувач кафедри математичної логіки і теорії алгоритмів механіко-математичного факультету (1966). Читає курси лекцій "Вступ до математичної логіки", "Обчислювані функції", "Теорема Геделя про повноту". Підготував 25 кандидатів та 2 докторів наук

1. Постановка задачі

Теорема про неповноту, точне формулювання якої ми дамо наприкінці цього розділу, а можливо пізніше (у разі виникнення до цього інтересу у читача) і доказ, стверджує приблизно таке: за певних умов у будь-якій мові існують справжні, але недоказні твердження.

Коли ми в такий спосіб формулюємо теорему, майже кожне слово потребує певних пояснень. Тому ми почнемо з того, що пояснимо значення слів, які ми використовуємо в цьому формулюванні.

1.1. Мова

Ми не даватимемо найбільш загального з можливих визначень мови, вважаючи за краще обмежитися тими мовними концепціями, які нам знадобляться згодом. Є два таких поняття: "алфавіт мови" та "безліч справжніх тверджень мови".

1.1.1. Алфавіт

Під алфавітом ми розуміємо кінцевий набір елементарних знаків (тобто речей, які неможливо розбити на складові). Ці символи називаються буквами алфавіту. Під словом алфавіту ми розуміємо кінцеву послідовність букв. Наприклад, прості слова в англійській мові (включаючи власні імена) є словами 54-хлітерного алфавіту (26 маленьких літер, 26 великих, тире і апостроф). Інший приклад - натуральні числа в десятковому записі є словами 10-тибуквенного алфавіту, чиї літери - знаки: 0, 1, 2, 3, 4, 5, 6, 7, 8, 9. Для позначення алфавітів ми використовуватимемо прості великі літери. Якщо L – алфавіт, то L? буде позначати безліч всіх слів алфавіту L, - слів, утворених із його літер. Ми припустимо, що будь-яка мова має свій алфавіт, тому всі вирази цієї мови (тобто - імена різних об'єктів, твердження щодо цих об'єктів тощо) є словами цього алфавіту. Наприклад, будь-яка пропозиція англійської мови, так само як і будь-який текст, написаний англійською, може розглядатися як слово розширеного алфавіту з 54-х букв, що включає також знаки пунктуації, міжмовну прогалину, знак червоного рядка і, можливо, деякі інші корисні знаки. Припускаючи, що висловлювання мови є словами деякого алфавіту, ми, таким чином, виключаємо з розгляду "багатошарові" вирази типу ???f(x)dx. Однак, це обмеження не надто суттєве, оскільки будь-яке подібне вираження, при використанні відповідних конвенцій, може бути "розтягнуте" у лінійну форму. Будь-яка множина М, що міститься в L? називається ніби множиною алфавіту L. Якщо ми просто говоримо, що М - ніби множина, то ми маємо на увазі, що воно є словом деякого алфавіту. Тепер сформульоване вище припущення про мову може бути перефразовано наступним чином: у будь-якій мові будь-яка множина виразів є ніби множиною.

1.1.2. Безліч справжніх тверджень

Ми припустимо, що нам задано підмножину Т множини L? (де L алфавіт деякої мови, що розглядається нами), яке називається безліччю "істинних тверджень" (або просто "істин"). Переходячи безпосередньо до підмножини Т, ми опускаємо наступні проміжні кроки міркування: по-перше, які саме слова алфавіту L є коректно освіченими виразами мови, тобто мають певне значення в нашій інтерпретації цієї мови (наприклад, 2+3, х+3, х=у, х=3, 2=3, 2=2 є коректно освіченими виразами, тоді як вирази типу +=х такими є); по-друге, які вирази є формулами, тобто. можуть залежати від параметра (наприклад, х=3, х=у, 2=3, 2=2); по-третє, які з формул є закритими формулами, тобто. твердженнями, які не залежать параметрів (наприклад, 2=3, 2=2); і, нарешті, які саме закриті формули є істинними твердженнями (наприклад, 2=2).

1.1.3. Фундаментальна пара мови

1.2. "Недоказні"

"Недоказувані" означає не мають доказів.

1.3. Доведення

Незважаючи на те, що термін "доказ" є, можливо, одним з найважливіших в математиці (Бурбаки починають свою книгу "Підстави математики" словами: "З часу давніх греків сказати "математика" означало те ж, що сказати "доказ""), він немає своєї точної дефініції. У цілому нині, поняття докази з його смисловими відгалуженнями належить, скоріш, до галузі психології, ніж до математики. Але як би там не було, доказ - це просто аргумент, який ми знаходимо цілком переконливим для того, щоб переконати всіх інших.

Будучи записано, доказ стає словом у певному алфавіті Р, як і будь-який англійський текст є словом алфавіту L, приклад якого було наведено вище. Безліч всіх доказів утворюють підмножину (і досить велике підмножина) множини Р?. Ми не намагатимемося дати точне визначення цієї одночасно "наївної" та "абсолютної" концепції доказу, або - що рівносильно - дати визначення відповідному підмножині Р?. Натомість ми розглянемо формальний аналог цього смутного поняття, для позначення якого надалі ми все ж таки користуватимемося терміном "доказ". Цей аналог має дві дуже важливі особливості, які відрізняють його від інтуїтивного поняття (хоча інтуїтивна ідея доказу все ж таки відображає певною мірою ці особливості). Насамперед ми припустимо, що є різні концепції докази, тобто - допустимі різні підмножини доказів у Р?, і навіть більше того: ми, насправді, припускатимемо, що сам алфавіт доказів Р може змінюватися. Далі ми вимагаємо, щоб для кожної такої концепції доказу існував ефективний метод, тобто алгоритм, який би з необхідністю визначав, чи є дане слово алфавіту Р доказом чи ні. Ми також припустимо, що існує алгоритм, за допомогою якого завжди можна визначити, яке саме твердження доводить цей доказ. (У багатьох ситуаціях твердженням, що доводиться, просто є останнє твердження в послідовності кроків, що утворюють доказ.)

Таким чином, наше остаточне формулювання визначення виглядає так:

(1) Ми маємо алфавіт L (алфавіт мови) і алфавіт Р (алфавіт доказу).

(2) Нам дано безліч Р, що є підмножиною Р?, Чиї елементи називаються "доказами". Надалі ми будемо припускати, що також у нас є алгоритм, який дозволяє нам визначити, чи є довільне слово алфавіту Р елементом множини Р, тобто доказом, чи ні.

(3) Також ми маємо функцію? (Для знаходження того, що саме було доведено), чия область визначення? задовольняє умові Р?Р?, і чия область значень знаходиться в Р?. Ми припускаємо, що у нас є алгоритм, який обчислює цю функцію (точне значення слів "алгоритм обчислює функцію" таке: значення функції виходять за допомогою цього алгоритму – набору спеціальних правил перетворення). Ми говоритимемо, що елемент р? Р є доказ слова? (р) алфавіту L.

Трійка<Р, Р, ?>, що задовольняє умов (1)-(3) називається дедуктивною системою над алфавітом L.

Для читача, знайомого зі звичайним способом визначення "доказу" у термінах "аксіома" та "правило виведення", ми зараз пояснимо, як цей метод може розглядатися як спеціальний випадок визначення, даного в параграфі 1.3.2. Тобто - доказ зазвичай визначається як послідовність таких виразів мови, кожне з яких є або аксіомою, або раніше отриманим з існуючих тверджень за допомогою одного з правил виведення. Якщо ми додамо нове слово * до алфавіту нашої мови, ми зможемо записати такий доказ у вигляді слова складеного за допомогою отриманого в результаті такої модифікації алфавіту: послідовність виразів стає словом C1*C2*...*Cn. У такому разі, функція, що визначає, що саме було доведено, своїм значенням має частину цього слова, що стоїть одразу за останньою у послідовності буквою *. Алгоритм, існування якого потрібно у частині 1.3.2. визначення, може легко бути сконструйований, як тільки ми точно визначимо якесь із прийнятих значень слів "аксіома" та "правила виведення".

1.4.Спроби точного формулювання теореми про неповноту

1.4.1. Перша спроба

"За певних умов для фундаментальної пари мови алфавіту L та дедуктивної системи<Р, Р, ?>над L - завжди існує слово в Т, що не має доказів". Цей варіант все ще виглядає невиразним. Зокрема, ми могли б запросто придумати скільки завгодно дедуктивних систем, що мають дуже трохи слів, що доводяться. Наприклад, у порожній дедуктивній системі (де Р = ?) зовсім немає слів, які мали б докази.

1.4.2. Друга спроба

Є інший, природніший підхід. Припустимо, нам задана мова – у тому сенсі, що нам задана фундаментальна пара цієї мови. Тепер ми будемо шукати таку дедуктивну систему над L (інтуїтивно, ми шукаємо техніку доказу), за допомогою якої ми могли б довести якнайбільше слів з Т, у межі всі слова з Т. Теорема Геделя описує ситуацію, в якій така дедуктивна система ( за допомогою якої кожне слово в Т було б доведено) не існує. Таким чином, нам хотілося б сформулювати наступне твердження:

"За певних умов щодо фундаментальної пари не існує такої дедуктивної системи, в якій кожне слово з Т мало б доказ".

Однак таке твердження, очевидно, хибне, оскільки необхідно лише взяти таку дедуктивну систему, в якій Р = L, Р = Р? і?(р) = р всім р з Р?; тоді кожне слово з L? є тривіально доведеним. Отже, нам потрібно прийняти певне обмеження на те, якими системами дедуктивних ми користуємося.

1.5. Несуперечливість

Було б цілком природно вимагати, що тільки "справжні твердження", тобто тільки слова з Т, можуть бути підтверджені. Ми говоритимемо, що дедуктивна система<Р, Р, ?>є несуперечливою щодо фундаментальної пари, якщо? (Р)? У всіх наступних міркуваннях нас цікавитимуть лише такі несуперечливі дедуктивні системи. Якщо ж нам задана мова, то було б надзвичайно спокусливо знайти таку несуперечливу дедуктивну систему, в якій кожне твердження було б доказом. Цікавий варіант теореми Геделя в точності стверджує, що за певних умов щодо фундаментальної пари, неможливо знайти таку дедуктивну систему.

1.6. Повнота

Йдеться про те, що дедуктивна система<Р,Р,?>повна щодо фундаментальної пари, за умови якщо? (Р)? Тоді наше формулювання теореми про неповноту набуває наступного вигляду:

За певних умов щодо фундаментальної пари не існує такої дедуктивної системи<Р,Р,?>над L, яка була б одночасно повна і несуперечлива щодо.

Список літератури

Для підготовки даної роботи було використані матеріали із російського сайту internet

1. Формальні аксіоматичні теорії та натуральні числа

2. Формальна арифметика та її властивості

3. Теорема Геделя про неповноту

4. Гедель та його роль у математичній логіці XX ст

Ця теорема, яка вже неодноразово зустрічалася нам, стверджує, що будь-яка несуперечлива формальна аксіоматична теорія, що формалізує арифметику натуральних чисел, не є (абсолютно) повною. У цьому параграфі дається доказ цієї теореми, що спирається на ідеї та методи теорій алгоритмів. Тим самим буде ще раз продемонстровано на найвищому рівні найтісніший зв'язок математичної логіки та теорії алгоритмів - двох математичних дисциплін, що утворюють фундамент усієї сучасної математики. Наш виклад ґрунтуватиметься на доказі, розробленому М.Арбібом.

Після доказу теореми 35.7 про те, що існує перерахована, але нерозв'язна безліч натуральних чисел, було заявлено, що вона фактично включає в себе в неявному вигляді теорему Геделя про неповноту формальної арифметики. Ціль цього параграфа полягає в тому, щоб обґрунтувати цю заяву. Таким чином, у рамках загальної теорії алгоритмів, крім тих теорем, які були доведені у двох попередніх параграфах, буде продемонстровано просування теорії алгоритмів у напрямі вирішення суто логічних проблем. Для цього спочатку належить ув'язати термінологію логічної проблеми про неповноту формальної арифметики з методологічною термінологією загальної теорії алгоритмів, методами якої цю проблему буде вирішено. При цьому твердження теореми 35.7 про існування перерахованої, але нерозв'язної множини натуральних чисел буде основною передумовою для доказу теореми Геделя, яку ми доведемо в наступному формулюванні: "Кожна адекватна со-несуперечлива формальна арифметика неповна". Далі, ми пояснимо, що розумітимемо під формальною арифметикою, а також визначимо та роз'яснимо ті поняття, які беруть участь у наведеному формулюванні теореми Ґеделя. Почнемо з формальних аксіоматичних теорій.

Формальні аксіоматичні теорії та натуральні числа

Раніше було визначено поняття формальної аксіоматичної теорії. Щоб задати таку теорію T потрібно задати алфавіт (лічильна безліч символів); у багатьох слів, складених з літер даного алфавіту, виділити підмножина, елементи якого будуть називатися формулами (або правильно побудованими виразами) даної теорії; у множині формул виділити ті, які будуть називатися аксіомами теорії; нарешті, має бути задане кінцеве число відносин між формулами, які називають правилами виведення. При цьому повинні існувати ефективні процедури (алгоритми) для визначення того, чи є дані слова (вирази) формулами (тобто правильно побудованими виразами), чи є дані формули аксіомами і, нарешті, виходить одна дана формула з ряду інших Даних формул за допомогою цього правила виведення. Це означає, що безліч всіх формул можна розв'язати і безліч всіх аксіом можна. Отже, кожну з цих множин перелічимо.

Поняття висновку та теореми у формальній аксіоматичній теорії дано у визначенні 28.2.

Усі теореми, що наводяться у цій лекції, відповідно до нашої термінології є фактично метатеоремами, тобто. теоремами про властивості (формальних) аксіоматичних теорій. Але оскільки тут жодної конкретної аксіоматичної теорії ми розглядаємо, жодних теорем такий теорії не доводимо, тобто. ніяких теорем, крім метатеорем, тут не буде, то ми метатеореми називатимемо просто теоремами.

Теорема 37.1. Безліч всіх теорем формальної аксіоматичної теорії Т перелічимо.

Доведення.Ми вже зазначили, що безліч аксіом формальної теорії перерахуємо, тобто ми можемо їх ефективно перенумерувати A_1,A_2,A_3,\ldots. Оскільки всі формули складаються з кінцевого числа букв (символів), всі висновки містять кінцеве число формул і кожен висновок використовує лише кінцеве число аксіом, то ясно, що для кожного натурального п існує лише кінцеве число висновків, що мають не більше ніж формул (кроків) і тих, що використовують тільки аксіоми \(A_1,A_2,\ldots,A_n\). Отже, рухаючись від n=1 до n=2,~ n=3 тощо, можна ефективно перенумерувати всі теореми цієї теорії. Це означає, що безліч теорем перелічимо.

Тепер від довільних формальних теорій переходитимемо до таких, які так чи інакше мають справу з натуральними числами. Якщо ми хочемо в нашій теорії говорити про підмножину Q множини натуральних чисел, то ми повинні мати ефективний спосіб виписування для кожного натурального формули W_n , що означає, що n \ in Q . Більш того, якщо ми зможемо довести, що формула W_n є теоремою теорії T тоді і тільки тоді, коли n\in Q , то будемо говорити, що теорія T напівповна для Q (або що T є напівповний опис Q ). Точніше, цю ухвалу сформулюємо так.

Визначення 37.2.Теорія T називається напівповною для безлічі натуральних чисел Q\subseteq \mathbb(N), якщо існує перелічена безліч формул W_0, W_1, \ldots,W_n,\ldots, Таке, що .

Визначення 37.3.Теорія T називається повною для Q якщо вона напівповна для Q і ми також маємо формулу \lnot W_n , яка інтерпретується як n\notin Q , і ми можемо довести, що \lnot W_n є теоремою теорії T тоді і тільки тоді, коли n\ notin Q. Іншими словами, теорія T повна для Q , якщо T для кожного п ми можемо встановити, належить воно Q чи ні. Точніше, це означає, що теорія T називається повною для безлічі натуральних чисел T якщо вона напівповна для Q і напівповна для його доповнення \overline(Q) .

Теорема 37.4. Якщо теорія T напівповна для множини Q , Q перелічимо.

Доведення.За визначенням напівповноти T для Q безліч Q є безліч номерів формул з деякої перелічуваної множини \(W_0,W_1,\ldots,W_n,\ldots\)формул, що є теоремами теорії T , тобто. належить і безлічі \operatorname(Th)(T). Таким чином, Q є безліч номерів всіх формул з множини \operatorname(Th)(T)\cap \(W_0,W_1,\ldots,W_n,\ldots\). Кожне з цих множин перелічимо: перше - за попередньою теореми 37.1, друге - за сказаним на початку доказу. Отже, та його перетин, по теоремі 35.5, перелічимо. Але тоді пере-ціслімо і безліч номерів тих формул, які входять до цього перетину.

Наслідок 37.5.Якщо Q перерахована, але нерозв'язна множина натуральних чисел, то ніяка формальна теорія не може бути повною для Q .

Доведення.Якщо множина Q перерахована, але нерозв'язна, то в силу теореми 35.6 його додаток \overline(Q) неперелічений. Тоді теорема 37.4 ніяка теорія T не є напівповною для \overline(Q) . Отже, ніяка теорія T є неповною для Q .

Від цього слідства до теореми Геделя зовсім недалеко. Для цього потрібно засобами деякої формальної теорії T розвинути теорію натуральних чисел, причому так, щоб належність чисел даній множині Q можна було трактувати адекватно (тобто число п належить Q тоді і лише тоді, коли деяка ефективно зіставлена ​​йому формула теорії T є теоремою цієї теорії). Це можливо тільки тоді, коли Q щонайменше перелічимо.

Формальна арифметика та її властивості

Формальна арифметика як формальна аксіоматична теорія будується з урахуванням формалізованого обчислення предикатів, розглянутого раніше. Предметні змінні тут називатимемо числовими, бо замість них підставлятимемо натуральні числа.

Предметна змінна називається вільною у формулі, якщо вона стоїть під знаком квантора (спільності чи існування), і пов'язаної - інакше. Формула називається замкнутою, якщо її предметні змінні пов'язані, і відкритої, якщо у ній є вільні змінні. Замиканням формули F називається формула C(F) , що виходить з F дописуванням спереду кванторів спільності по всіх змінних, вільних F . Зрозуміло, що для будь-якої формули F(F) замкнута. Якщо F замкнута, то C(F)=F.

Функція C(F) обчислювана. Звідси випливає, що клас замкнутих формул дозволимо, поскольку.Рему належить і тоді, коли C(F)=F , і розпізнавання цієї рівності існує обчислювальна процедура.

З поняттям підстановки у формулу ми вже знайомі. Якщо формулу F замість символу (слова) X скрізь, де він входить у F , вставити слово (формулу) H , то отримаємо нове слово (формулу), що позначається S_X^HF і називається результатом підставки F слова H замість слова X . Тоді ясно, що

\begin(gathered)S_X^H(\lnot F)\equiv \lnot S_X^HF;\qquad S_X^H(F\to G)\equiv S_X^HF\to S_X^HG;\\ \text(esli) ~ i\ne j,~ \text(to)~ S_(x_i)^N(\forall x_j)(F)\equiv (\forall x_j)S_(x_i)^NF,~ S_(x_i)^N(\ exists x_j)(F)\equiv (\exists x_j)S_(x_i)^NF. \end(gathered)

Маючи справу з натуральними числами, ми б мати можливість підставляти в формули формальної теорії (арифметики), тобто. мати можливість говорити про цифри мовою нашої формальної теорії. Для цієї мети у формальній теорії необхідно мати слова, які служили б назвами натуральних чисел. Такі слова називаються номерами. Нумерал числа п позначається n^(\ast). Вимога до цих назв (імен) цілком природне: різні числа мають називатися різними іменами, тобто. якщо m\ne n , то m^(\ast)\ne n^(\ast). (Ідея введення нумералів полягає в тому, щоб розділити речі та імена цих речей.)

Таким чином, у формули арифметики ми підставлятимемо замість числових змінних x_1,x_2,x_3,\ldotsне самі натуральні числа m,n,k,\ldots , які нумерали (імена) m^(\ast),n^(\ast),k^(\ast),\ldotsвідповідно.

Зрештою, ми можемо сформулювати останню вимогу (аксіому), яку ми висуваємо до формальної арифметики. Назвемо його аксіомою арифметики: якщо предметна змінна jc не пов'язана в F , то

\text((AA))\colon~ S_(x_i)^(n^(\ast))F\to (\exists x_i)(F).

Якщо ввести для S_(x_i)^(n^(\ast))Fпозначення F(n^(\ast)) , то ця аксіома набуває вигляду:

\text((AA))\colon~ F(n^(\ast))\to (\exists x_i)(F).

Це виключно природна вимога: якщо формула F перетворюється на справжнє висловлювання при підстановці в неї замість змінної x_i якогось натурального числа n^(\ast) , то істинно і висловлювання (\exists x_i)(F) .

Жодних інших обмежень на формалізацію арифметики не накладається. Неважливо, зокрема, як визначаються додавання та множення натуральних чисел, як вводиться відношення порядку, чим ми скрупульозно займалися при побудові теорії натуральних чисел на основі системи аксіом Пеано. Навіть за таких самих загальних припущень на формалізацію арифметики ця формалізація підпорядковуватиметься теоремі Геделя: якщо вона буде несуперечливою, вона буде неповною.

Отже, визначившись з поняттям формальної арифметики, присвятимо частину цього пункту, що залишилася, поняттям ю-непротиворечивості, адекватності і повноти цієї формальної теорії, що беруть участь у точному формулюванні теореми Гёделя.

Почнемо з поняття несуперечності. Як і будь-яка аксіоматична теорія, формальна арифметика називається несуперечливою, якщо у ній не можна довести будь-яке твердження та її заперечення, тобто. якщо немає такої формули F , що одночасно \vdash F і \vdash\lnot F .

Припустимо тепер, що для деякої формули G(x) , що містить вільно єдину предметну змінну х, встановлено, що для всіх натуральних чисел n=0,1,2,3,\ldots . Навіть якщо у формальній арифметиці неможливо довести \vdash (\forall x)(G(x))Ми звичайно ж можемо вважати це твердження наслідком наведеного списку теорем. Отже, якщо теоретично вдасться довести теорему , то таку формальну арифметику слід вважати суперечливою.

Визначення 37.6.Формальна арифметика називається ω-несуперечливою, якщо в ній немає такої формули G(x) з єдиною вільною предметною змінною x , що для всіх натуральних чисел n справедливі теореми \vdash G(n^(\ast))і \vdash\lnot (\forall x)(G(x)).

Теорема 37.7. Якщо формальна арифметика -несуперечлива, то вона несуперечлива.

Доведення.Справді, якби вона була суперечлива, то, як доведено в §27, після визначення 27.1, усі її формули були б теоремами, у тому числі й ті, які створюють ω-суперечність формальної арифметики, і остання була б ω-суперечлива .

Визначення 37.8. Назвемо n-місцевий предикат P(x_1,\ldots,x_n) над безліччю натуральних чисел N цілком представленим у формальній арифметиці, якщо існує така формула F(x_1,\ldots,x_n) , вільними предметними змінними якої є п змінних x_1,\ldots ,x_n (і тільки вони), що:

а) для кожного набору n натуральних чисел (a_1,\ldots,a_n) , для якого предикат P перетворюється на справжнє висловлювання P(a_1,\ldots,a_n) , має місце теорема: \vdash F(a_1^(\ast),\ldots,a_n^(\ast));

б) для кожного набору n натуральних чисел (a_1,\ldots,a_n) , для якого предикат P перетворюється на хибне висловлювання P(a_1,\ldots,a_n) , має місце теорема: \vdash\lnot F(a_1^(\ast),\ldots,a_n^(\ast)).

Таким чином, цілком уявність предикату у формальній арифметиці означає, що ми засобами цієї формальної теорії завжди можемо вирішити, перетвориться він на справжнє чи хибне висловлювання при підстановці замість усіх його предметних змінних тих чи інших натуральних чисел.

Роз'яснимо тепер поняття адекватності формальної арифметики, що бере участь у формулюванні теореми Ґеделя. Ми хотіли б мати можливість відповідати на запитання про множини в такій арифметиці. У теоремі 37.4 ми показали, що лише перелічені множини чисел можуть мати напівповне опис у формальній теорії, тобто. існує перелічена безліч формул W_0,W_1,W_2,\ldots, таке, що Q=\(n\colon \vdash W_n\). Адекватність нашої формальної теорії (арифметики) могла б означати, що вона є напівповною для кожного переліченого множини натуральних чисел, тобто. що в ній має напівповний опис всяка множина, яка взагалі може мати такий опис хоча б у якійсь теорії.

У теоремі 37.1 ми встановили, що багато всіх теорем фор. мальної теорії перелічимо, тобто. всі теореми і, отже, що приводять до них висновки (докази) можуть бути ефективно перенумеровані. Візьмемо наше безліч Q і відповідне йому безліч теорем \(W_0,W_1,W_2,\ldots\). Розглянемо наступний предикат P(x, y) \ colon "y - номер доказу теореми W_x". Якщо висловлювання P(m,n) істинно, це означає, що є номер виведення теореми W_m , що, своєю чергою, означає, що m\in Q , тобто. n є номер висновку у тому, що m\in Q . Назад, взявши конкретні числа m і n ми можемо ефективно побудувати теорему (формулу) W_m і ефективно побудувати n-й висновок, після чого ефективно визначити, чи є побудований висновок висновком теореми W_m , тобто. ефективно дізнатися, чи істинно висловлювання P(m,n). Отже, P(x,y) - такий обчислюваний предикат, що .

Сформулюємо тепер визначення.

Визначення 37.9. Формальна арифметика називається адекватною, якщо для кожної переліченої множини Q натуральних чисел існує цілком представлений у цій арифметиці предикат P(x,y) такий, що Q=\bigl\(x\colon (\exists y)(\lambda = 1)\bigr\).

Під повнотою формальної арифметики розумітимемо абсолютну повноту, тобто. якщо для кожної замкнутої формули F цієї теорії або вона сама, або її заперечення є теоремою цієї теорії: \ vdash F або \ vdash \ lnot F .

Тепер ми можемо перейти безпосередньо до формулювання та доказу теореми Геделя.

Теорема Геделя про неповноту

Теорема стверджує таке. Будь-яка ω-несуперечлива та адекватна формальна арифметика не є повною.

▼ Доказ

Відповідно до теореми 35.7, виберемо таку множину Q натуральних чисел, яке перелічимо, але не можна розв'язати. Оскільки наша формальна арифметика адекватна, існує цілком представимий у ній перидикат P(x,y) такий, що

Q= \bigl\(x\colon\, (\exists y)\bigl(\lambda = 1\bigr)\bigr\).

Цілком уявність предикату P(x,y) у формальній арифметиці означає, що знайдеться така формула F(x,y) цієї теорії, що містить лише дві вільні предметні змінні, що для кожної пари натуральних чисел (a,b) , для якої має місце теорема: \vdash F(a^(\ast),b^(\ast)), а кожної пари натуральних чисел (a,b) , для якої \lambda =1, має місце теорема: \vdash\lnot F(a^(ast),b^(\ast)).

Застосуємо до формули F(x,y) квантор спільності змінної y . Отримаємо формулу з єдиною вільною предметною змінною x\colon\, G(x)\equiv (\exists y)(F(x,y)). Покажемо, що

Q= \bigl\(x\colon\, \vdash G(x^(\ast))\bigr\).

Припустимо, що m\in Q . Тоді (згідно (*)) знайдеться таке натуральне n що висловлювання P(m,n) істинно. Отже, має місце теорема: \vdash F(m^(\ast),n^(\ast))З огляду на аксіоми арифметики \text(AA) маємо теорему:

\vdash F(m^(\ast),n^(\ast))\to (\exists y)\bigl(F(m^(\ast),y)\bigr).

З двох останніх теорем за правилом МР укладаємо:

\vdash (\exists y)\bigl(F(m^(\ast),y)\bigr), тобто .

Це означає, що m\in \bigl\(x\colon \vdash G(x^(\ast))\bigr\). Таким чином, Q \subseteq \bigl\(x\colon\vdash G(x^(\ast))\bigr\).

Назад, припустимо, що m\in \bigl\(x\colon\vdash G(x^(\ast))\bigr\), тобто \vdash G(m^(\ast)), тобто \vdash (\exists y)(F(m^(\ast),y)). Звідси, з відомого висловлювання (за законом де Моргана) квантора існування через квантор спільності, укладаємо, що

\vdash\lnot (\forall y)\bigl(\lnot F(m^(\ast),y)\bigr).

Оскільки наша формальна арифметика, крім того, со-непротиворечива, то, зважаючи на наявність в ній останньої теореми, має існувати таке натуральне число n_0, що формула - \lnot F(m^(\ast),n^(\ast)_0)не є теоремою цієї арифметики. А якщо так, то висловлювання P(m,n_0) істинно (якби воно було хибним, то ми мали б теорему \vdash\lnot F(m^(\ast),n^(\ast)_0), що не так). За визначенням (*) множини Q це означає, що m\in Q . Таким чином, \(x\colon\vdash G(x^(\ast))\)\subseteq Q. Отже, рівність (**) доведено.

Тепер з'ясуємо, в якому відношенні знаходяться між собою безліч \overline(Q) (додаток Q ) і \(x\colon\vdash G(x^(\ast))\). Нехай me m\in \(x\colon\vdash\lnot G(x^(\ast))\), тобто \vdash\lnot G(x^(\ast)). Тоді m\in \overline(Q) , бо якби m\in Q , то через силу (**) ми мали б \vdash G(m^(\ast))і наша формальна арифметика була б суперечливою, але це не так через її ©-несуперечність (за умовою) і теорему 37.7. Таким чином, \(x\colon\vdash G(x^(\ast))\)\subseteq \overline(Q).

Покажемо, що останнє включення є суворим. Нагадаємо, що ми вибрали безліч Q перерахованим, але не можна розв'язати. Тоді згідно з наслідком 37.5 з теореми 37.4, ніяка формальна теорія не може бути повною для Q . Рівність (**) говорить, що наша формальна арифметика напівповна Q . Якби мала місце рівність \overline(Q)= \(x\colon\vdash G(x^(\ast))\), Це означало б, що наша формальна арифметика напівповна і для \overline(Q) і, отже, вона була б повною для Q . Останнє неможливе через слідство 37.5 з теореми_37.4. Отже, \(x\colon\vdash G(x^(\ast))\)\ne \overline(Q).

Отже, \(x\colon\vdash\lnot G(x^(\ast))\)\subset \overline(Q). Отже, існує таке число m_0\in \overline(Q), що m_0\notin \(x\colon\vdash\lnot G(x^(\ast))\), тобто невірно, що \vdash\lnot G(m_0^(\ast)). У той же час неправильно також, що \vdash G(m_0^(\ast))оскільки це, в силу (**), означало б, що m_0\in Q , а це не так. Отже, ми знайшли формулу G(m_0^(\ast)) , таку, що вона сама, ні її заперечення є теоремами нашої формальної арифметики. Це означає, що ця формальна арифметика перестав бути повної.

Теорема Ґеделя повністю доведена.

Звернемося ще раз до висловлювання \lnot G(m_0^(\ast)). Відповідно до рівності (**), його можна інтерпретувати як m_0\on \overline(Q)і, отже, він обов'язково є "істинним" висловлюванням. Проте воно не є теоремою нашої формальної арифметики. Якщо додати формулу G(m_0^(\ast)) до списку аксіом і розглянути нову формальну арифметику, то положення не зміниться: для новоотриманої формальної арифметики вірні всі передумови, які привели нас до теореми Геделя. Отже, ми знову знайдемо таке число m_1, що висловлювання \lnot G(m_1^(\ast))істинно, але не теорема нової формальної арифметики і т.д.

Гедель та його роль у математичній логіці XX ст

Курт Ґедель народився 28 квітня 1906 р. у м. Брюнні (нині м. Брно у Чехії). Закінчив Віденський університет, де захистив докторську дисертацію та був доцентом у період 1933-1938 рр. Після окупації Австрії фашистською Німеччиною емігрував до США. З 1940 по 1963 р. Гедель працює в Прінстонському інституті вищих досліджень (з 1953 він професор цього інституту). Гедель - почесний доктор Єльського та Гарвардського університетів, член Національної академії наук США та Американського філософського товариства. У 1951 р. Гёдель удостоєний найвищої наукової нагороди США - Ейнштейнівської премії. У статті, присвяченій цій події, інший найбільший математик нашого часу Джон фон Нейман писав: "Внесок Курта Геделя в сучасну логіку воістину монументальний. Це більше, ніж просто монумент, це віха, що розділяє дві епохи... Без жодного перебільшення можна сказати, що роботи Геделя докорінно змінили сам предмет логіки як науки. Гедель заклав основи цілих розділів математичної логіки: теорії моделей (1930), конструктивної логіки (1932-1933), формальної арифметики (1932-1933), теорії алгоритмів та рекурсивних функцій (1934), аксіоматичної теорії множин (1938). Гедель помер у Прінстоні (США) 14 січня 1978 р.

на тему: «ТЕОРЕМА ГЕДЕЛЯ»

Курт Гедель

Курт Ґедель – найбільший фахівець із математичної логіки – народився 28 квітня 1906 р. у Брюнні (нині м. Брно, Чехія). Закінчив Віденський університет, де захистив докторську дисертацію, був доцентом у 1933–1938 роках. Після аншлюсу емігрував до США. З 1940 по 1963 р. Гедель працював у Прінстонському інституті вищих досліджень. Гедель – почесний доктор Єльського та Гарвардського університетів, член Національної академії наук США та Американського філософського товариства.

У 1951 р. Курт Ґедель був удостоєний найвищої наукової нагороди США – Ейнштейнівської премії. У статті, присвяченій цій події, інший найбільший математик нашого часу Джон фон Нейман писав: «Внесок Курта Геделя в сучасну логіку воістину монументальний. Це більше, ніж просто монумент. Це віха, яка розділяє дві епохи… Без жодного перебільшення можна сказати, що роботи Геделя докорінно змінили сам предмет логіки як науки».

Дійсно, навіть сухий перелік досягнень Геделя в математичній логіці показує, що їх автор по суті заклав основи цілих розділів цієї науки: теорії моделей (1930; так звана теорема про повноту вузького обчислення предикатів, що показує, грубо кажучи, достатність засобів «формальної логіки» » для доказу всіх висловлюваних її мовою істинних речень), конструктивної логіки (1932-1933 рр.., результати про можливість зведення деяких класів речень класичної логіки до їх інтуїціоністських аналогів, що започаткували систематичне вживання «занурювальних операцій», що дозволяють здійснювати таке систем один одному), формальної арифметики (1932-1933 рр.; результати про можливість зведення класичної арифметики в інтуїціоністську, що в певному сенсі показують несуперечність першої щодо другої), теорії алгоритмів і рекурсивних функцій (1934 р.; визначення поняття загальнорекурсивної функції, що зіграло вирішальну що у встановленні алгоритмічної нерозв'язності низки найважливіших проблем математики, з одного боку. І в реалізації логіко-математичних завдань на електронно-обчислювальних машинах - з іншого), аксіоматичної теорії множин (1938 р.; доказ відносної несуперечності аксіоми вибору і континуум-гіпотези Кантора від аксіом теорії множин, що започаткувало серію найважливіших результатів теоретико-множинних принципів).

Теорема Геделя про неповноту

Вступ

У 1931 р. в одному з німецьких наукових журналів з'явилася порівняно невелика стаття з досить жахливою назвою «Про формально нерозв'язні пропозиції Principia Mathematica та споріднених систем». Автором її був двадцятип'ятирічний математик з Віденського університету Курт Гедель, який згодом працював у Прінстонському інституті вищих досліджень. Ця робота відіграла вирішальну роль в історії логіки та математики. У рішенні Гарвардського університету про присудження Геделеві почесного докторського ступеня (1952) вона була охарактеризована як одне з найбільших досягнень сучасної логіки.

Однак у момент опублікування ні назва геделівської роботи. Ні зміст її нічого не говорили більшості математиків. Згадані в її назві Principia Mathematica – це монументальний тритомний трактат Альфреда Норта Уайтхеда та Бертрана Рассела, присвячений математичній логіці та основам математики; знайомство з трактатом не було необхідною умовою для успішної роботи здебільшого розділів математики. Інтерес до питань, що розбираються в роботі Геделя, завжди був долею вельми нечисленної групи вчених. У той самий час міркування, наведені Геделем у його доказах, були свого часу настільки незвичайними. Що для повного їх розуміння потрібно виняткове володіння предметом і знайомство з літературою, присвяченою цим вельми специфічним проблемам.

Перша теорема про неповноту

Перша теорема Геделя про неповноту, мабуть, є найбільш знаменним результатом у математичній логіці. Вона звучить так:

Для довільної несуперечливої ​​формальної та обчислюваної теорії, в якій можна довести базові арифметичні висловлювання, може бути побудовано істинний арифметичний вислів, істинність якого не може бути доведена в рамках теорії. Іншими словами, будь-яка цілком корисна теорія, достатня для представлення арифметики, не може бути одночасно несуперечливою та повною.

Тут слово «теорія» позначає «нескінченну безліч» висловлювань, деякі з яких вважаються істинними без доказів (такі висловлювання називаються аксіомами), інші (теореми) може бути виведені з аксіом, тому покладаються (доводяться) істинними. Словосполучення «доведений теоретично» означає «виводиться з аксіом і примітивів теорії (константних символів алфавіту) з допомогою стандартної логіки (першого порядку)». Теорія є несуперечливою (узгодженою), якщо в ній неможливо довести суперечливе висловлювання. Словосполучення "може бути побудоване" означає, що існує деяка механічна процедура (алгоритм), яка може побудувати висловлювання на основі аксіом, примітивів та логіки першого порядку. «Елементарна арифметика» полягає в наявності операцій складання та множення над натуральними числами. Результуюче істинне, але недоказне висловлювання часто позначається для заданої теорії як «послідовність Геделя», однак існує нескінченно кількість інших висловлювань у теорії, які мають таку ж властивість: істинність, що недоказується в теорії.

Припущення у тому, що теорія обчислима, означає, що у принципі можна реалізувати комп'ютерний алгоритм (комп'ютерну програму), яка (якщо їй можна обчислювати довільно довгий час, до нескінченності) обчислить перелік всіх теорем теорії. Фактично, достатньо обчислити лише список аксіом, і всі теореми можуть бути ефективно одержані з такого списку.

Перша теорема про неповноту була під назвою «Теорема VI» у статті Геделя від 1931 року On Formally Undecidable Propositions in Principia Mathematica and Related Systems I. В оригінальному записі Геделя вона звучала як:

«Загальний висновок про існування нерозв'язних пропозицій полягає в наступному:

Теорема VI .

Для кожного ω-узгодженого рекурсивного класу kФОРМУЛ існують рекурсивніЗНАКИ r такі, що не (v Gen r)ні ¬( v Gen r)не належать Flg (k)(де v єВІЛЬНА ЗМІННА r ) ».

Позначення Flgпоходить від нього. Folgerungsmenge- безліч послідовностей, Genпоходить від нього. Generalisation- Узагальнення.

Грубо кажучи, висловлювання Геделя Gстверджує: «істинність Gне може бути доведена». Якби Gможна було довести в рамках теорії, то в такому разі теорія містила б теорему, яка суперечить сама собі, а тому теорія була б суперечлива. Але якщо Gнедоведено, то воно істинне, а тому теорія неповна (висловлювання Gневиводимо в ній).

Це пояснення звичайною природною мовою, а тому не зовсім математично суворо. Для надання суворого доказу, Ґедель пронумерував висловлювання за допомогою натуральних чисел. І тут теорія, яка описує числа, також належить безлічі висловлювань. Питання доказованості висловлювань у цьому випадку у вигляді питань про властивості натуральних чисел, які мають бути обчислювані, якщо теорія повна. У цих термінах висловлювання Геделя говорить, що немає числа з певним певним властивістю. Число з цією властивістю буде доказом суперечливості теорії. Якщо така кількість існує, теорія суперечлива попри початкове припущення. Тож припускаючи, що теорія несуперечлива (як передбачається посилці теореми), виходить, що такого числа немає, і висловлювання Геделя істинно, але у межах теорії цього довести неможливо (отже, теорія неповна). Важливе концептуальне зауваження у тому, що слід припустити, що теорія несуперечлива, щоб оголосити висловлювання Геделя істинним.

Друга теорема Геделя про неповноту

Друга теорема Геделя про неповноту звучить так:

Для будь-якої формально рекурсивно перелічуваної (тобто ефективно генерованої) теорії T, включаючи базові арифметичні істиннісні висловлювання і певні висловлювання про формальну доказовість, дана теорія T включає твердження про свою несуперечність тоді і тільки тоді, коли теорія T суперечлива.

Іншими словами, несуперечність досить багатої теорії не може бути доведена засобами цієї теорії. Однак цілком може виявитися, що несуперечність однієї конкретної теорії може бути встановлена ​​засобами іншої більш потужної формальної теорії. Але тоді постає питання про несуперечність цієї другої теорії, і т.д.

Використовувати цю теорему для доказу того, що розумна діяльність не зводиться до обчислень, багато хто намагався. Наприклад, ще 1961 року відомий логік Джон Лукас (John Lucas) виступав із подібною програмою. Його міркування виявилися досить вразливими – проте він і завдання ставив ширше. Роджер Пенроуз використовує дещо інший підхід, який викладається у книзі повністю, «з нуля».

Дискусії

Наслідки теорем торкаються філософії математики, особливо такі формалізми, які використовують формальну логіку для визначення своїх принципів. Можна перефразувати першу теорему про неповноту в такий спосіб: « неможливо знайти комплексну систему аксіом, яка була б здатна довести Усематематичні істини, і жодної брехні». З іншого боку, з погляду суворої формальності, це переформулювання немає особливого сенсу, оскільки вона передбачає поняття «істина» і «брехня» певними у абсолютному сенсі, ніж у відносному кожної конкретної системи.