Формализация в математике

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

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

Рассмотрим такой объект как математическое доказательство. Рассуждение становится доказательством в результате, по выражению Ю.И. Манина, «социального акта "принятия доказательства"». Несколько упрощая, можно сказать что доказательство становится доказательством, когда таковым его признает математическое сообщество. Доказательство публикуется, обсуждается математической общественностью и принимается или отвергается в зависимости от того, насколько оно соответствует принятым критериям доказательности. Это справедливо применительно не только к математике, но и к другим наукам. Критерии доказательности в математике практически всегда (по крайней мере, со времен Евклида) были достаточно высоки. В математической теории без доказательства принимаются аксиомы. Из них по явно сформулированным правилам выводятся теоремы. Чтобы доказать теорему, достаточно предъявить некоторый текст, который удовлетворяет определенным требованиям, позволяющим принять его в качестве доказательства. Хотя требования к доказательствам со временем эволюционировали (в направлении повышения уровня строгости), тем не менее основа оставалась более или менее неизменной. Ситуация изменилась, когда возникла необходимость доказать отсутствие доказательства. Без точно зафиксированного определения сделать это невозможно. Поясним это таким примером. Предположим, исследуется проблема присутствия на Земле инопланетян. Если кто-то сумеет предъявить сторукого обитателя летающей тарелки, это будет признано положительным решение проблемы. Давать при этом точное определение того, что такое инопланетянин, не потребуется. Для доказательства отсутствия инопланетян точное определение необходимо. К примеру, определение «инопланетянин – существо, прилетевшее на Землю из космоса» не сработает: под него подпадут космонавты. Уточнение определения можно продолжить, однако ясно, что выработка точного определения – дело не простое.

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

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

Пусть, например, требуется дать точное определение некоторого понятия или, что равносильно, точно описать класс объектов C, составляющий содержание рассматриваемого понятия. Прежде всего фиксируется математический язык, на котором будет дано описание – набор знаков (алфавит) и правила их комбинации (синтаксис). Объекты формализованной теории – это определенные языковые конструкции. Далее указываются примитивы и правила построения объектов класса C. Все примитивы принадлежат классу C по определению. Правила построения имеют следующий вид: объект O может быть построен из объектов O₁, O₂, …,O_k. При этом класс C считается замкнутым относительно правильных построений: если все объекты O₁, O₂, …, O_k содержатся в классе C, то и объект O содержится в классе C. Таким образом, в классе C содержатся все примитивы; объекты, которые могут быть построены из примитивов; объекты, которые могут быть построены из объектов, построенных из примитивов, и т.д. Никаких других объектов класс C не содержит. Объект O принадлежит классу C тогда и только тогда, когда имеется конечная цепочка объектов

O₁, O₂, …, O_n

такая, что O_n=O, и каждый объект в цепочке является примитивом или может быть построен из некоторых предшествующих ему объектов. Такое определение класса C называется рекурсивным.

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

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

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

Не нашли, что искали? Воспользуйтесь поиском: