4.Правила вывода:

1. правило заключения (Modus Ponens) – то же, что и в исчислении вы­сказываний;

2. правило обобщения (  - введения) :

F  G ( х )

F   х G ( х )

где G( х ) содержит свободные вхождения х, а F их не содержит;

3) Правило  - введения:

G ( х )  F



 х G ( х )  F

при тех же требованиях к F и G, что и в предыдущем правиле.

Нарушения этих требований могут привести к ложным выводам из ис­тинных высказываний. Пусть, например, Р ( х ) – предикат „ х делится на 6“ , Q ( х ) - предикат „ х делится на 3 .“ Высказывание Р ( х ) → Q ( х ) , оче­видно, истинно для любого х , однако применение к нему правила обоб­щения дает высказывание Р ( х ) →  х Q ( х ) , не являющееся всегда ис­тинным.

Если же к Р ( х )  Q ( х ) применить правило  - введения, то получим  х Р ( х )  Q ( х ) , из которого путем ( уже корректного  ) применения правила обобщения получим высказывание  х Р ( х )   х Q ( х ) , лож­ное на множестве натуральных чисел.

Рассмотрим примеры формальных систем.

Исторически формальные системы создавались с конкретной целью бо­лее точного обоснования методов построения математических теорий. Од­нако постепенно стало ясно, что на основе тех же принципов – исходного набора аксиом, правил вывода и понятия выводимости – можно описывать не только множество выражений, интерпретируемых как высказывания, но и перечислимые множества объектов произвольной формы. Основы теории таких формальных систем были заложены Э. Постом. Эту теорию можно называть абстрактной или общей, так как она - в отличие от исчисления высказывания - не рассматривает свойства формальных систем относи­тельно их конкретных интерпретаций, а изучает их внутренние синтаксиче­ские свойства.

Рассмотрим примеры формальных систем абстрактного типа.

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

Пример 2. Рассмотрим абстрактное определение ориентированной двух­полюсной схемы. Два варианта таких схем показан на рис. 4.1.

Рис. 4.1 - Двухполюсные схемы.

Аксиомы такой системы - элементы с выделенными полюсами, правила вывода - правила соединения элементов в схему.

Интерпретация - электрическая схема, график и прочее.

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

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

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

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

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

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

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 с помощью правил вывода из аксиомы.



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

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

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

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