Формальные доказательства

Материал из synset
Перейти к: навигация, поиск
Доказательство от противного << Оглавление >> Вычислимые функции и их алгоритмы

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

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

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

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

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

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

Сущности могут вступать между собой в некоторые отношения, в результате чего возникают высказывания о них. Высказывания могут быть константными: "", брадобрей — мужчина: "", или переменными: , некоторый житель деревни мужчина "". В последнем случае они называются предикатами. Любые высказывания считаются либо истинными либо ложными. В случае предикатов, при одних они истинны, а при других ложны. Для натуральных чисел 0,1,2,... предикат истинен при , и ложен при всех остальных. Равенство это тоже предикат, истинный когда сущности и совпадают.

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

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

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

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

Рассмотрим теперь парадокс брадобрея. Утверждение о том, что "некий бреет -ка" обозначим предикатом . В этом случае означает, что " бреет сам себя". Введём константу "" — имя брадобрея (фиксированный объект) и запишем аксиомы теории:

Первая аксиома гласит: "если любой сам себя не бреет, то его бреет ". В силу принципиальности брадобрея, считается верной и вторая аксиома: "любой кого бреет брадобрей не бреет себя".

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

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

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

Однако, даже если критянин один (т.е. вместо предикатов стоит просто высказывания , ), определённые проблемы вызывает запись заявления о том, что "произносит эту фразу". Можно, например, определить сущность (чем бы она не являлась) при помощи 3-х аксиом:

 : если истинно(лжец), то не истинна,

 : если (не лжец), то его фраза истинна,

 : констатация факта, что это критянин.

Эти три аксиомы противоречивы и из них одновременно следует и . Хотя попарно, они являются вполне допустимыми системами.

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

Надо понимать, что это Игра, которая имеет свои Правила. Играющие должны их придерживаться. Вот и всё. Второй вопрос — "почему эта Игра позволяет предсказывать затмения Солнца или поведение пыльцы под микроскопом?" Но это уже вопрос из совершенно другой Игры.

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

В предыдущем разделе, аналогично, при помощи рекурсии был определён объект . Но, в отличие от функции сложения это определение некорректно, так как не содержит выхода из рекурсии типа . Это несколько иная алгоритмическая некорректность.

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

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

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


Доказательство от противного << Оглавление >> Вычислимые функции и их алгоритмы

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