Эссе Тьюринга

Доказательство вычислимости первой теоремы Гёделя о неполноте

«Любая непротиворечивая формальная система F, в рамках которой может быть проведена определенная элементарная арифметика, неполна; т.е. есть утверждения языка F, которые нельзя ни доказать, ни опровергнуть в F. »

Статья Гёделя 1931 года, содержащая доказательство его первой теоремы о неполноте, трудна для чтения. Он состоит из 26 страниц, содержит 46 предварительных определений и несколько важных положений, которые представлены в очень формальной форме (Nagel & Newman, 2001). Доказательство Гёделя должно было быть таким длинным, потому что оно было сформулировано до создания общей теории вычислимости (Turing, 1936; Church, 1936), и поэтому общая концепция формальной системы действительно еще не была сформулирована (Franzen, 2005).

Гёдель, следовательно, вместо этого доказал свою теорему о неполноте для формальной системы P, созданной им самим, и утверждал, что она содержит свойства, общие для широкого класса систем. Используя изобретение Тьюринга и Черча вычислимости, с помощью покойного великого Торкеля Франзена (2005) мы можем разработать схему доказательства вычислимости теоремы Гёделя о неполноте, которая столь же сильна, как и версия Гёделя, но гораздо проще выводить .

Обзор

Во-первых, давайте набросаем набросок того, что показал Гёдель в своем первом доказательстве неполноты, любезно предоставленном Эрнестом Нагелем и замечательной книгой Джеймса Р. Ньюмана Доказательство Гёделя:

Steps of Gödel's proof (Nagel & Newman, 2001)
In his proof, Gödel showed the following:
i) How to construct a formula G of Peano arithmetic (PA) that represents the statement: "The formula G is not demonstrable using the rules of Peano arithmetic"
ii) That G is demonstrable if and only if its formal negation not-G is demonstrable
iii) That although G is not formally demonstrable, it nevertheless is a true arithmetic statement
iv) That since G is both true and formally undecidable within Peano arithmetic, Peano arithmetic must be incomplete
v) How to construct a formula A of Peano arithmetic that represents the statement "Peano arithmetic is consistent" and that the formula A ⊃ G is formally demonstrable inside Peano arithmetic
vi) Finally, that the formula A is not demonstrable in Peano arithmetic

Чтобы построить набросок доказательства вычислимости, которое показывает то же самое, мы должны сначала определить несколько необходимых понятий. Следующий раздел основан на главе «Вычислимость, формальные системы и неполнота» в Franzén (2005).

Числовые строки

Большинство из нас знакомы с термином «строка» из информатики, термином, традиционно используемым для описания любой конечной последовательности символов. Числовые строки, в свою очередь, могут использоваться для описания строк, используемых в математике для обозначения натуральных чисел (неотрицательных целых чисел), таких как «0», «13» или «125 239». Альтернативный способ представления таких натуральных чисел в виде строк - в двоичной системе счисления, так что три числа выше вместо этого выражаются в системе счисления с основанием 2, в которой используются только два символа: «0», «1101», «11110100100110111».

Набор числовых строк имеет два свойства, которые имеют отношение к нашему исследованию теоремы Гёделя о неполноте (Franzen, 2005). Они есть:

  1. Должна существовать механическая процедура для генерации числовых строк, например, в двоичном случае, например, сначала записываются однозначные строки 0 и 1, затем двухзначные строки {00, 01, 10, 11 }, затем трехзначные строки {000, 001, 010, 100, 011, 110, 101, 111}, затем четырехзначные строки и так далее.
  2. Должен существовать алгоритм, который может решить, будет ли она, учитывая любую строку символов, когда-либо появляться в вычислимом перечислении набора. То есть должен существовать механизм для определения, появляется ли символ в числовой строке.

Перечислимость и разрешимость

Наборы числовых строк имеют два свойства, которые имеют особое значение для вычислимости и неполноты. Это перечислимость и разрешимость:

Enumerability 
A set E of strings is computably enumerable if it is possible to program a computer to compute and print out the members of E
Decidability
A set E of strings is computably decidable if it is possible to program a computer to decide, given any string s of symbols, whether or not is in E.

Задавать вопросы о том, является ли набор строк вычислимо перечислимым и / или разрешимым, имеет смысл только в том случае, если этому набору можно дать формальное математическое определение. То есть неформально это имеет смысл только в том случае, если мы знаем правила, которые генерировали элементы множества. Таким образом, «набор всех предложений на английском языке» нельзя считать ни перечислимым, ни разрешимым, поскольку мы не можем формально выразить, как английские предложения были и генерируются людьми достаточно систематическим образом.

Итак, чтобы продвинуться вперед, давайте займемся созданием наборов строк, которые нам интересны для целей доказательства неполноты формальных систем.

Гёделевская нумерация

Посмотрите на свою клавиатуру. Обратите внимание на то, что клавиши расположены в определенном порядке, и каждое вводимое вами предложение может быть представлено числовой цепочкой цифр, представляющих, в каком порядке вы нажимали клавишу. Длина строки соответствует длине любого предложения, которое вы вводите.

С самого начала должно быть тривиально заметить, что свойство, требуемое выше для генерации числовых строк (перечислимость), может быть изменено таким образом, чтобы генерировать все возможные строки (Franzen, 2005 ). Нумерация Гёделя, введенная в его статье 1931 года, - это способ представления произвольных строк, а не только числовых, числами. Формально,

A Gödel numbering is a function that assigns each symbol and a well-formed formula of some formal language a unique natural number called its Gödel number.

Стоит отметить, что эта гёделевская нумерация является лишь одним из бесконечных способов представления произвольных строк (символов, букв, цифр и т. Д.) Числами (Franzen, 2005). Также стоит отметить, что нумерация Гёделя удовлетворяет двум условиям:

  • Для любой строки мы можем механически вычислить ее число Гёделя, генерируя строки и считая их, пока не найдем строку, чье число Гёделя мы ищем;
  • С учетом числа, наоборот, мы можем решить, является ли это геделевским числом сгенерированной нами строки, и если да, то какой именно;

Примеры оригинального кодирования Гёделем символов, букв и целых чисел в числа Гёделя включены ниже в современной нотации:

Из его конструкции нумерации Гёделя мы знаем, что:

A set of strings is computably enumerable or decidable if and only if the set of Gödel numbers of strings in the set is computably enumerable or decidable.

То есть мы можем только сказать, может ли набор строк (представляющих, например, слова в предложении) быть механически вычислен (перечислимы) и / или может ли быть определено, принадлежат ли они данному набору (разрешимы) тогда и только тогда. если, набор чисел Гёделя, связанных со строками в наборе, сам по себе перечислим (может быть вычислен механически) и / или разрешим (можно определить, принадлежат ли они данному набору).

Давайте сделаем паузу и повторим еще раз. Каждое предложение, представленное символами (например, буквами), может быть представлено уникальной цепочкой (очень больших) чисел. Наборы строк, представляющие каждое предложение на английском (или любом другом) языке , могут быть механически вычислены, распечатаны и проверены на принадлежность к заданному набору, если соответствующие им числа Гёделя также могут быть механически вычислены, распечатаны и проверены. принадлежать к данному набору.

Другими словами, мы можем использовать числа Гёделя, связанные с наборами строк (например, предложениями), чтобы определить, является ли какое-либо предложение вычислимо перечислимым и / или разрешимым. Это важно.

Неразрешимые множества

Учитывая, что некоторые наборы строк разрешимы, очевидно, что другие наборы строк нет. Чтобы найти их, давайте сначала утвердим два фундаментальных свойства вычислимо разрешимых множеств (множества, которые могут быть определены с помощью вычислений как принадлежащие или не принадлежащие такому набору, как, например, формальная система) (Franzén, 2005):

  • Каждое вычислимо разрешимое множество вычислимо перечислимо
  • Множество E вычислимо разрешимо тогда и только тогда, когда и E, и его дополнение вычислимо перечислимы.

Первое свойство может быть легко получено из определения вычислимой перечислимости (если набор строк вычислимо разрешим, компьютер может определить, принадлежит ли он данному набору или нет, но компьютер может это сделать. Таким образом, члены набора, с которым сравнивается строка, также должны обладать тем свойством, что они могут быть произведены механически с помощью компьютера).

Второе свойство касается дополнения множества E, то есть всех строк, которых нет в множестве E. Во-первых, обратите внимание, что если E разрешимо, то также и дополнение к E (мы можем построить множество F всех строк которые, как показано, не принадлежат E).

Алан Тьюринг и Алонзо Черч в 1936 году оба независимо друг от друга доказали, что общее решение Entscheidungsproblem, которое сейчас известно как теорема неразрешимости, невозможно, а именно:

Undecidability Theorem (Turing, 1936; Church, 1936)
There are computably enumerable sets which are not computably decidable.

То есть есть строки символов, которые могут быть сгенерированы компьютером, но которые мы не можем определить, принадлежат ли они к данному набору.

Формальные системы

В математике формальная система, такая как арифметика Пеано (PA), на которой основана работа Гёделя, основана на формальном языке, наборе правил вывода и набор аксиом. В целом предполагается, что подмножество языка, состоящее из предложений, разрешимо. Подмножество предложений, которое, в свою очередь, включает аксиомы и правила вывода, необходимо определить таким образом, чтобы формальная система удовлетворяла следующему основному свойству формальных систем, а именно тому, что (Franzén, 2005):

Множество теорем формальной системы вычислимо перечислимо.

То есть теоремы, которые могут быть разработаны с помощью системы аксиом и правил вывода, выраженных предложениями на формальном языке, также должны быть механически вычислены компьютером. Таким образом, выбирая правильные аксиомы и правила вывода, мы можем построить формальную систему S, которая разрешима, и таким образом показать, что множество доказательств в системе также разрешимо. Другими словами, свойство подразумевает, что всегда можно искать доказательство данного предложения формальной системы механическим способом, и что, если такое доказательство существует, в конечном итоге оно будет найдено, и вычисление остановится ( быть конечным).

Первая теорема о неполноте.

«В соответствии с любой данной аксиоматизацией теории чисел, можно явно построить диофантово уравнение, которое не имеет решений, но такое, что этот факт не может быть доказан в рамках данной аксиоматизации»

Вышеупомянутая (более сильная) версия первой теоремы Гёделя о неполноте может быть получена из теоремы Матиясевича (иногда называемой теоремой Матиясевича-Робинсона-Дэвида-Патнэма), в которой говорится, что

Every computably enumerable set is Diophantine

То есть набор строк, которые можно запрограммировать на компьютер для вычисления и распечатки членов, можно выразить как полиномиальное уравнение с целыми коэффициентами и конечным числом неизвестных, которые принимают целочисленные значения. Иными словами, Матиясевич доказал (Franzén, 2005):

Не существует алгоритма, который бы определил, имеет ли какое-либо диофантово уравнение решение, имеет ли уравнение решение.

Когда было объявлено в 1970 году, результатом была решена десятая проблема Гильберта, в которой требовался общий алгоритм, который для любого диофантова уравнения (полиномиального уравнения с целыми коэффициентами и конечным числом неизвестных) может определять, имеет ли уравнение решение с все неизвестные принимают целочисленные значения.

То есть доказательство показало, что не может быть алгоритма, который при любом диофантовом уравнении D (x₁, x₂,… xᵢ) = 0 решал бы, имеет ли уравнение решение. Другими словами, система диофантовых уравнений неразрешима (см. Теорему о неразрешимости Тьюринга и Чёрча).

Доказательство подразумевает, что через наше второе указанное выше свойство неразрешимых множеств (Множество вычислимо разрешимо тогда и только тогда, когда оба и его дополнение вычислимо перечислимы) является его отрицание, диофантово уравнение D (x₁, x₂,… .xᵢ) = 0 имеет хотя бы одно решение также неразрешима. Это потому, что если нет, то для данной формальной системы S мы могли бы решить, имеет ли данное диофантово уравнение D (x₁, x₂,…. Xᵢ) = 0 решение, путем систематического поиска в S доказательства либо утверждение диофантово уравнение D (x₁, x₂,…. xᵢ) = 0 имеет хотя бы одно решение или его отрицание, и таким образом построить множество всех диофантовых уравнений с решениями. Алгоритм, проводящий этот поиск, нарушил бы результат Матиясевича о том, что такого алгоритма не может быть.

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

Предположим, что S - формальная система, которая содержит достаточно арифметики, чтобы доказать все истинные утверждения вида (Franzén, 2005)

D(x₁, x₂, …. xᵢ) = 0 has no solution

Если S непротиворечива, каждая такая теорема S верна. То есть, если нет таких утверждений A, что и A, и не-A доказуемы в S, то каждая такая теорема для S верна. Набор всех уравнений, для которых в S доказано, что они не имеют решения, является вычислимо перечислимым подмножеством уравнений, не имеющих решения (Franzén, 2005).

Однако, поскольку последнее не является вычислимо перечислимым (т. Е. Подмножество уравнений D, для которых может быть доказано отсутствие решений, не может быть вычислено с помощью механического процесса), отсюда следует, что существует бесконечно много уравнений D (x₁, x₂,…. Xᵢ ) = 0, которые не имеют решения, но которые мы не можем доказать, что они не имеют решений (должна существовать остальная часть системы уравнений D, не имеющих решений).

Таким образом, наша формальная система S должна быть неполной, поскольку она недостаточно сильна для доказательства всех теорем, выводимых из ее аксиом и правил вывода.

Интерпретация

Статья Гёделя 1931 года, которая включает его первый результат о неполноте, озаглавлена ​​Über form unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I («О формально неразрешимых положениях принципов математики и связанных систем»). Хотя работа Гёделя занимает десятки страниц (а точнее 26), она основана на удивительно простой идее, а именно на том, что (Sigmund, 2017):

"In any formal system, mathematical statements are simply strings of symbols. Gödel found a systematic way of turning any such string into a unique integer. The given string of symbols determined its integer uniquely, and vice versa - given a large integer, if it represented a string of symbols, then that string was uniquely determined."

Поскольку важная Principia Mathematica Уайтхеда и Рассела, да и вообще всякая полная формальная система, включая ее доказательства, должна строиться систематически, Гёдель заметил, что по существу можно представить любую формальную систему в виде целых чисел.

"Thus for any theorem there was a theorem-number that could be defined in terms of addition, multiplication, and other mathematical operations. Therefore, provability of a string in a formal system corresponded to a purely mathematical property of a very large number, and this property could be talked about using the notation of Principia Mathematica."

Подобно тому, как можно утверждать о числе N, что оно имеет такие свойства, как квадрат, квадратный корень, куб или простое число, и использовать эти свойства для построения доказательств различных гипотез, можно также утверждать, что для числа N это номер теоремы (т.е. он представляет собой строки из букв, символов и целых чисел, которые показывают, что сформулированные предположения логически гарантируют заключение предложенной гипотезы).

"Gödel's coup de grâce was the construction of a special mathematical proposition G that asserted that a certain string having Gödel number g is unprovable - meaning that it cannot be formally derived from the system of axioms of Principia Mathematica. And astonishingly, Gödel managed to arrange things so that the integer g was precisely the Gödel number of the statement G ("somewhat fortuitously", as he slyly noted)."
- Excerpt, "Exact Thinking in Demented Times" by Karl Sigmund (2017)

Тем, кто заинтересован в дальнейшем изучении природы результатов Гёделя о неполноте, рекомендуется получить книгу Торкеля Франзена (2005) Теорема Гёделя: неполное руководство по ее использованию и злоупотреблениям и книгу Вычислимость: Тьюринг, Гедель, Черч и не только под редакцией Коупленда, Поза и Шагрира (2015).

Это эссе является частью серии рассказов на математические темы, опубликованных в еженедельном издании Medium Cantor’s Paradise. Спасибо за чтение!