Теорема Геделя про неповноту, пояснення (I)

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

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

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

Перш ніж пояснити, чому це так, нам потрібні три ідеї: про які системи ми говоримо; як дозволити системі «говорити» про власні твердження та докази; і як побудувати речення, яке, по суті, посилається на себе.

Формальні системи для арифметики

Формальна система — це точна система умов, і будь-який комп'ютерний алгоритм є формальною системою:

• Він має алфавіт основних знаків та ретельно визначену граматику для формування висловлювань (речень).

  
  

• Він має фіксований список аксіом (вихідних точок) та правил висновку , які підказують, як виводити нові твердження зі старих.

  
  

• Це фактично аксіоматично : ви, в принципі, могли б запрограмувати машину, щоб вона перевіряла, чи є рядок аксіомою, а послідовність рядків — правильним доказом.

  
  

• Він достатньо сильний, щоб виразити повсякденні факти про цілі числа: додавання, множення, порівняння та прості міркування про них.

«Несуперечливий» означає, що система ніколи не доводить одночасно твердження та його спростування. «Повний» (у сенсі Геделя) означає, що кожне істинне арифметичне твердження, виражене в системі, можна довести в ній.

Ключовий трюк: дозволити арифметиці говорити про синтаксис

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

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

• «Чи є цей рядок правильно сформованим реченням?» стає «Чи має це число арифметичну властивість, яка відповідає правильному сформуванню?»

  
  

• «Чи є цей список речень дійсним доказом цього речення?» стає «Чи відповідає ця пара чисел арифметичній схемі, яка кодує правильне співвідношення доказу?»

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

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

Дзеркало: побудова речення, що самореференційно

Наступний інгредієнт — це загальний метод створення самопосилання, який називається діагональною або фіксованою точкою . Ось ідея без символів.

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

«Це саме речення не піддається доказу в системі».

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

Чому G змушує до неповноти

Розглянемо, що станеться, якщо система буде узгодженою.

• Якщо система довела G, то G було б хибним (оскільки G стверджує, що його неможливо довести). Система довела б хибність, що суперечить узгодженості. Отже, припускаючи узгодженість, система не доводить G.

  
  

• Якщо система довела «не G» (що G хибний), то, розібравшись з тим, що каже G, система довела б, що «G можна довести». Але ми щойно стверджували, що в послідовній системі G неможливо довести. Доведення «не G» тим самим призведе до суперечності. Отже, знову ж таки, за звичайних м’яких припущень щодо системи, це також не доводить «не G».

Отже, G неможливо довести, і його заперечення також неможливо довести. Більше того, у світі цілих чисел, що розглядається, G насправді є істинним (оскільки, власне, немає жодного доказу цього, якщо система є несуперечливою). Ми знайшли істинне, але недоведене речення: система є неповною.

Це, по суті, перша теорема Геделя про неповноту.

Кілька слів про технічне вдосконалення (трюк Россера)

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

Чому система не може довести свою власну узгодженість

Друга теорема про неповноту використовує той самий механізм. Щойно система може говорити про власні докази, вона також може написати речення, яке виражає «немає доказу суперечності». Назвемо це твердженням про узгодженість системи.

Якби система могла довести власну несуперечливість, можна показати (все ще працюючи виключно в межах арифметики), що вона також довела б твердження Геделя G, наведене вище. Але ми вже бачили, що, припускаючи, що система несуперечлива, вона не може довести G. Отже, несуперечлива система не може довести власне твердження несуперечності.

Інтуїтивно: система не може зсередини засвідчити, що її механізм доказів ніколи не зійде з рейок — принаймні, якщо цей механізм достатньо потужний, щоб вловлювати звичайну арифметику та дотримуватися механічних правил. А тепер уявіть, що цим механізмом є будь-який сучасний комп'ютер, яким би складним він не був. Механізм не може довести, що він ніколи не зійде з рейок.

Що говорять (і чого не говорять) теореми

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

  
  

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

  
  

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

Чому це мало значення — і досі має

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

Короткий виклад стратегії доказування

1. Розробіть спосіб кодування кожного речення та доказу як унікального цілого числа.

2. Покажіть, що система може висловлювати твердження про ці коди, зокрема «x є доказом y».

3. Використайте метод фіксованої коми, щоб побудувати конкретне речення G, яке стверджує про себе, що в системі немає доказу його існування.

4. Стверджуємо: якщо система є несуперечливою, вона не доводить ні G, ні його заперечення; більше того, G істинна в стандартних цілих числах. Це призводить до неповноти.

5. Виразіть у межах системи твердження «немає доказів суперечності». Покажіть, що якби система могла довести це твердження, вона також довела б G, що суперечить кроку 4. Отже, несуперечлива система не може довести власну несуперечність.

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