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

Содержание

0.1 Предмет математической логики

0.2 Пример формальной системы

0.3 Структура раздела

1 Аксиоматический метод

1.1 Аксиомы натуральных чисел

1.2 Начальные задачи

1.3 Сложение

1.4 Порядок

1.5 Наименьший элемент

1.6 Умножение

1.7 Системы Пеано

2 Логика высказываний

2.1 Объектный язык и метаязык

2.2 Пропозициональные формулы

2.3 Доказательство свойств формул по индукции

2.4 Разбор формул

2.5 Семантика

2.6 Нормальные формы

2.7 Выполнимость

2.8 Логическое следование

2.9 Пропозициональный вывод

2.10 Правила для конъюнкции и импликации

2.11 Правило введения посылки

2.12 Корректность правил вывода

2.13 Правила для отрицания и правила противоречия

2.14 Правила для дизъюнкции

2.15 Корректность и полнота логики высказываний

3 Логика предикатов

3.1 Язык логики предикатов

3.2 Свободные и связанные переменные

3.3 Представление предложений русского языка предикатными формулами

3.4 Подстановка

3.5 Семантика

3.6 Выполнимость

3.7 Логическое следование

3.8 Выводы в логике предикатов

3.9 Правила для кванторов всеобщности

3.10 Правила для кванторов существования

3.11 Корректность и полнота логики предикатов

3.12 Функциональные символы и равенство: синтаксис

3.13 Функциональные символы и равенство: семантика

3.14 Выводы в логике первого порядка

3.15 Теории первого порядка

3.16 Пример: Теория линейного порядка

3.17 Арифметика первого порядка

3.18 Нестандартные модели арифметики

3.19 Теорема неполноты Гёделя

Введение

Предмет математической логики

Основная идея математической логики – формализация знаний и рассуждений. Известно, что наиболее легко формализуемые знания – математические. Таким образом, математическая логика, по-существу, – наука о математике, или метаматематика. Центральным понятием математической логики является ``математическое доказательство''. Действительно, ``доказательные'' (иначе говоря, дедуктивные) рассуждения – единственный вид признаваемых в математике рассуждений. Рассуждения в математической логике изучаются с точки зрения формы, а не смысла. По-существу, рассуждения моделируются чисто ``механическим'' процессом переписывания текста ( формул). Такой процесс называют выводом. Говорят еще, что математическая логика оперирует только синтаксическими понятиями.

Однако обычно всё же важно, как соотносятся рассуждения с действительностью (или нашими представлениями). Поэтому, надо всё же иметь в виду некоторый смысл формул и вывода. При этом используют термин семантика (синоном слова ``смысл'') и чётко разделяют синтаксис и семантику.

Когда же действительно интересуются только синтаксисом, часто используют термин ``формальная система''. Мы будем использовать синоним этого термина – ``исчисление'' (используются ещё термины ``формальная теория'' и ``аксиоматика'').

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

Формальная система определена, если:

1. Задан алфавит (множество символов, используемых для построения формул).
2. Определено, какие именно строки считать формулами (остальные строки считаются просто бессмысленными).
3. Выделено множество формул, называемых аксиомами. Это – стартовые точки в выводах.
4. Задано множество правил вывода, которые позволяют из некоторой формулы (или множества формул) получать новую формулу.

Пример формальной системы

Рассмотрим пример простой, ``игрушечной'' формальной системы.

Пример формальной системы. Популярная формальная система (DH) определяется следующим образом:

1. Алфавит: {M,I,U}.
2. Формулы: любая последовательность символов данного алфавита.
3. Одна аксиома: MI.
4. Правила вывода:
   • правило 1: из формулы вида mI можно получить mIU.
   • правило 2: из формулы вида Mm можно получить Mmm.
   • правило 3: подстроку III можно заменить на U.
   • правило 3: подстроку UU можно заменить на пустую строку.
   символом m в первом и во втором правиле обозначается произвольное слово.

MI (аксиома), MII (правило 2), MIIII (правило 2), MIIIIU (правило 1), MIUU (правило 3), MI (правило 4).

Определите, можно ли получить формулу MU с помощью правил вывода из аксиомы.



Структура раздела

Раздел ``математическая логика'' состоит из трёх частей: по неформальному аксиоматическому методу, по логике высказываний и по логике предикатов (первого порядка).

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

По поводу используемой нотации. Текст построен на последовательности задач. Большинство задач состоит в доказательстве некоторых утверждений. Для некоторых задач имеются указания для решения. Для отдельных приведено решение. Некоторые задачи служат для подготовки читателя к следующим задачам – для номеров таких вспомогательных задач используется курсив. В тексте мы часто используем шаблон ``для <объекты> : <свойство>''. Здесь ``:'' является сокращением слов ``выполняется следующее:''.