Формулы арифметики их номера

Материал из synset
Перейти к: навигация, поиск
Существуют ли несчетные множества? << Оглавление >> Теорема Гёделя о неполноте

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

Формальная теория — это множество утверждений относительно некоторых предметных сущностей, которые записаны на специальном, формальном языке. В арифметике этими сущностями являются натуральные числа . Через , , ... обозначаются некоторые не определённые числа (предметные переменные), а при помощи цифр их конкретные реализации (предметные константы). Мы считаем, что есть предметные функции от чисел, которые снова дают числа. Например или . Такие предметные функции мы обозначаем маленькими буквами со скобками. Кроме этого, вводятся логические утверждения относительно сущностей — предикаты. Это тоже функции, аргументами которых являются числа, но их значения равны "истина" или "ложь". Предикаты обозначаются большими буквами. Например, может значить утверждение " равно ", и чаще кратко обозначается, как , а — " меньше ". Если предикат зависит от переменной, то говорят, что она свободна. При одних её значениях предикат истинен, а при других — ложен. Например, это истина, а — ложь.

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

Кроме предикатов вводятся логические связки, заменители слов "не" (), "или" (), "и" (), "если , то " (), эквивалентно ():

На месте рукописных заглавных букв могут находится либо предикаты, либо составные формулы, состоящие из предикатов и логических связок. На самом деле связки — это функции, принимающие на вход значение истина "И" или "Л", и их же сообщающие на выходе. Так,

И это Л, Л это И Л И это И, Л Л это Л, и т.д.

Такие определения смысла логических связок называются таблицами истинности.

Логические связки позволяют из элементарных предикатов (базовых высказываний) создавать более сложные. Например, предикат неравенства определяется так . Естественно, если составные высказывания содержат свободную переменную, то при одних её значениях они истинны, а при других ложны:

Так, ложно всегда, а истинно только если . Если мы смогли приписать элементарным предикатам истинностные значения (например, это "И", а это "Л"), то составные высказывания также приобретают значение "И" или "Л". В результате, мы можем говорить об истинности данной формулы.

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

Фраза "утверждение справедливо для любого " обозначает, что истинно и , и , и , и, так далее, т.е. выполняется для всех натуральных чисел. Аналогично существующий делает справедливым (истинным) высказывание хотя бы для одного (или нескольких ), что выражается бесконечной цепочкой логических "или". Например, Великую Теорему Ферма можно записать следующим образом:

где конечно, предполагается, что арифметическая функция возведения в степень определена через другие (например, сложение).

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

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

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

где — это любая конкретная предметная константа (например, 0). Стрелочка "" означает что из одной формулы получается (выводится) другая, например .

Ещё одно правило вывода:

означает, что если есть формула , которая считается истинной, и формула в которую входит отрицание , то можно вывести формулу (так как Невозможно разобрать выражение (синтаксическая ошибка): {\displaystyle \textstyle Л\vee И} это И, а Невозможно разобрать выражение (синтаксическая ошибка): {\displaystyle \textstyle Л\vee Л} это Л, то Невозможно разобрать выражение (синтаксическая ошибка): {\displaystyle \textstyle Л\vee \mathcal B} это просто ).

Третье правило вывода двойного отрицания позволяет перед любым предикатом поставить или убрать их. Наконец, в четвёртом разрешено переставлять формулы вокруг логического "или" .

Рассмотрим теперь систему аксиом Пеано для арифметики:

которые определяют свойства предметной функции , имеющей смысл получения следующего числа [в более привычной записи ]. При этом предполагается, что есть только одна явно представленная предметная константа "0". Все остальные получаются (определяются) при помощи 0 и функции . Так, , , и т.д.

Аксиома утверждает, что не существует чисел "предшествующих" нулю, а аксиома наделяет арифметику свойством бесконечности предметных констант. Докажем, например, что :

Первый вывод использует правило подстановки в аксиому вместо константы и определение предиката неравенства . Во втором выводе проводится подстановка в вместо : , а вместо : 0. Затем, перед ставится двойное отрицание. Эти две формулы содержат подформулу и её отрицание. Значит её можно выбросить, и вывести , что учитывая сокращения для констант имеет вид .

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

Для этого символы (буквы) формального языка определённым образом кодируются при помощи целых чисел. Обычно алфавит языка выбирается конечным. Для этого любые переменные задаются при помощи только одного, при необходимости повторяющегося символа . Тогда — это , — это , и т.д. Аналогично, для выражения бесконечного числа предметных констант достаточно символа "0" и предметной функции дающей следующее после число. Ещё более кратко мы можем писать , , , т.е. при помощи символа штриха и константы 0 выражать любое натуральное число.

Далее поступим также, как и при нумерации программ. Присвоив каждому символу целочисленный номер (написанный под символом):

мы можем выразить любую формулу в виде последовательности чисел, которые, при помощи набора простых чисел, можно превратить в одно число, равное гёделевскому номеру формулы. Для формулы с символами берём последовательных простых чисел, возводим их в степени, соответствующие коду символа и перемножаем:

Функция получает на вход строку символов, выражающих данную формулу , и на выходе даёт число, равное гёделевскому номеру . Если термин "символы" смущает для арифметической функции, можно считать, что она сразу получает набор целочисленных кодов. Выше это , где 0 зарезервирован для конца строки.

Функция всюду определена, и более того — обратима. Т.е. существует , которая по номеру формулы, разложив его на простые множители, записывает в памяти набор чисел эквивалентных символьной записи формулы.

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


Существуют ли несчетные множества? << Оглавление >> Теорема Гёделя о неполноте

Истинность и доказуемость - о конструктивной математике, Канторе и Гёделе