Математическая логика

«Если все вороны черные, то все нечерные предметы — не вороны». Это высказывание несомненно истинно, и, чтобы утверждать это, не нужно быть знатоком птиц. Точно так же не нужно быть специалистом в теории чисел, чтобы сказать, что если все совершенные числа четны, то все нечетные числа несовершенны. Мы привели примеры утверждений, истинных независимо от смысла входящих в них понятий (вороны, черные, совершенные, четные) — истинных уже в силу самой своей формы. Изучение такого рода утверждений входит в задачу логики. Более общо: логика изучает правильные способы рассуждений — такие способы рассуждений, которые приводят к верным результатам в тех случаях, когда верны исходные посылки.

Предметом математической логики служат в основном рассуждения. При их изучении она пользуется математическими методами. Разъясним сказанное.

Математики строят и развивают математические теории, дают определения, доказывают теоремы и т. п. Специалисты по математической логике, наблюдая за этим, анализируют, как математики это делают и что при этом получается. Образно говоря, соотношение между математикой и математической логикой похоже на соотношение между концертом и теорией музыки. Можно сказать, что математическая логика изучает основания математики, принципы построения математических теорий.

Установив, что изучает математическая логика, перейдем к тому, как она это делает. Нам уже известно, что она пользуется математическими методами. Объясним, что это значит. Как применяются математические методы, например, в физике? Строится математическая модель рассматриваемого физического процесса, отражающая какие‑то его существенные свойства. Математические методы могут применяться не только в физике, но и в других науках. Например, применение математических методов в биологии состоит в построении математических моделей биологических процессов. Можно строить математические модели и для процесса развития математических теорий. Это и делает математическая логика.

<addc>l</addc>

Как устроена математическая теория? Она содержит какие‑то утверждения. Некоторые из них принимаются без доказательств, другие удается доказать (в этом случае утверждения называют теоремами). Значение слов «утверждение» и «доказательство» в повседневной практике весьма расплывчато. Поэтому если мы хотим строить математическую модель, то первым делом нужно уточнить эти понятия, т. е. построить их формальные аналоги в нашей модели. Для этого математические логики придумали специальные формальные языки, предназначенные для записи математических утверждений. Утверждения, записанные на формальных языках, называют формулами, чтобы отличить их от предложений естественных языков. Построив формальный язык, мы получаем возможность записывать некоторые математические утверждения в виде формул. Этого, разумеется, еще не достаточно. Нам нужно уметь записывать формально не только утверждения, но и доказательства. Для этого математические логики придумали формальный аналог понятия «доказательство» — понятие вывода (доказательства, записанного на формальном языке). Формальным аналогом понятия «теорема» является понятие «выводимая формула» (т. е. формула, имеющая вывод). Формальный язык вместе с правилами построения выводов называется формальной системой.

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

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

Основным предметом математической логики, таким образом, является построение и изучение формальных систем. Центральным результатом здесь является доказанная в 1931 г. австрийским математиком К. Геделем теорема о неполноте, утверждающая, что для любой «достаточно разумной» формальной системы существуют неразрешимые в ней предложения, т. е. такие формулы [math]A,[/math] что ни сама формула [math]A,[/math] ни её отрицание не имеют вывода. Если отождествить формальную систему с соответствующей областью математики, то можно сказать, что в любой «достаточно разумной» области математики есть утверждения, которые нельзя ни доказать, ни опровергнуть. Мы не можем здесь точно сказать, что именно требуется от «достаточно разумной» формальной системы; отметим лишь, что большинство формальных систем (в том числе формальная арифметика и аксиоматическая теория множеств) удовлетворяют этим требованиям. На примере теоремы о неполноте мы видим, какую пользу приносит построение формальной системы: мы получаем возможность доказать, что какие‑то утверждения недоказуемы!

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

Многие знаки, придуманные логиками для построения формальных систем, постепенно вошли в общее употребление. К ним относятся логические связки [math]∧[/math] (конъюнкция, «и»), [math]∨[/math] (дизъюнкция, «или»), [math]⇒[/math] (импликация, «если… то…»), [math]¬[/math] (отрицание, «неверно, что») и так называемые кванторы [math]∀[/math] (всеобщности, «для всех») и [math]∃[/math] (существования, «существует»). Смысл логических связок, помимо указанных в скобках названий, разъясняется так называемыми таблицами истинности. Эти таблицы показывают, будет ли сложное утверждение, составленное с помощью логических связок из простых, истинно (И) или ложно (Л) в зависимости от истинности его составных частей. Приведем их.

[math]A[/math]	[math]B[/math]	[math]A∧B[/math]	[math]A∨B[/math]	[math]A⇒B[/math]	[math]¬A[/math]
И	И	И	И	И	Л
И	Л	Л	И	Л	Л
Л	И	Л	И	И	И
Л	Л	Л	Л	И	И

Например, пятый столбец показывает, что утверждение [math]A⇒B[/math] может быть ложно, только если [math]A[/math] истинно, а [math]B[/math] ложно. С помощью этих таблиц можно составить таблицу истинности и для более сложных утверждений, например для утверждения [math]((A∨B)∧(¬A))⇒B.[/math]

[math]A[/math]	[math]B[/math]	[math]A∨B[/math]	[math]¬A[/math]	[math](A∨B)∧(¬A)[/math]	[math]((A∨B)∧(¬A))⇒B[/math]
И	И	И	Л	Л	И
И	Л	И	Л	Л	И
Л	И	И	И	И	И
Л	Л	Л	И	Л	И

Составив её, мы увидим, что это утверждение (шестой столбец) всегда истинно, независимо от истинности утверждений А и В. Это не удивительно — ведь его можно прочитать так: «Если верно или [math]А,[/math] или [math]В[/math] и [math]А[/math] неверно, то верно [math]В[/math]». Как говорят, это утверждение является логическим законом, или тавтологией. Именно с таких утверждений мы начали обсуждение предмета математической логики.

Смысл кванторов [math]∀[/math] и [math]∃[/math] можно объяснить так. Если [math]A(x)[/math] — некоторое утверждение, истинность которого зависит от значения переменной x (например, утверждение «[math]x[/math] — четное число»), то утверждение [math]∀xA(x)[/math] гласит, что [math]A(x)[/math] верно при всех значениях [math]x,[/math] а утверждение [math]∃xA(x)[/math] означает, что найдется такое [math]x,[/math] при котором [math]A(x)[/math] верно. (В нашем примере первое из этих утверждений ложно, а второе — истинно.) Как и логические связки, кванторы можно использовать для записи логических законов. Например, оба утверждения, приведенные нами в начале статьи в качестве примеров, частные случаи закона

[math]∀x(A(x)⇒B(x))⇒∀x(¬B(x)⇒¬A(x)),[/math]

которые получаются, если подставить вместо [math]A(x)[/math] утверждение «[math]x[/math] — ворона», а вместо [math]B(x)[/math] — «[math]x[/math] — черная» или вместо [math]A(x)[/math] — «[math]x[/math] — совершенные», а вместо [math]B(x)[/math] — «[math]x[/math] — четные».