Меню
Главная
Авторизация/Регистрация
 
Главная arrow Математика, химия, физика arrow ДИСКРЕТНЫЙ АНАЛИЗ. ФОРМАЛЬНЫЕ СИСТЕМЫ И АЛГОРИТМЫ
Посмотреть оригинал

Аксиомы

Аксиом в ИВ бесконечно много. Чтобы задать бесконечное множество формул, мы используем схемы аксиом. Схема аксиом — это формула, переменные которой понимаются как произвольные формулы. Другими словами, мы сопоставляем каждой формуле Ф множество формул, которые получаются подстановкой в формулу Ф произвольных формул вместо переменных, входящих в формулу Ф.

В ИВ есть три схемы аксиом.

Определение 1.11. Формула ИВ является аксиомой, если её можно представить одним из следующих способов:

где А, В, С — произвольные формулы.

Правило вывода

Правило вывода в исчислении высказываний ровно одно. Оно называется modus ponens (правило отделения) и может быть формально записано как

Неформально эта запись означает утверждение «из выводимости формул А, А—>В следует выводимость формулы В».

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

Определение 1.12. Формула А называется выводимой в исчислении высказываний (или формальной теоремой исчисления высказываний), если существует последовательность формул (вывод)

в которой для любой формулы Ai выполнено хотя бы одно из двух условий:

  • Ai является аксиомой;
  • • найдутся такие j, k < i, что Ak = Aj —у Ai (т. е. ранее в последовательности формул встречались и формула Aj, и формула Aj-^Ai).

Для выводимости мы будем использовать специальное обозначение h А, означающее выводимость формулы А.

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

Пример вывода даёт следующая лемма.

Лемма 1.13. h (А—>А).

Доказательство. Приведём последовательность формул и проверим, что она является выводом:

Чтобы получить первую формулу из первой схемы аксиом, нужно подставить вместо В формулу (А—>А). Вторая формула получается из второй схемы аксиом подстановкой вместо В формулу (А-+А), а вместо С — формулы А. Третья и пятая формулы в выводе получаются применением правила modus ponens, что отмечено в правом столбце. Например, запись (МР 1,2) указывает, что третья формула вывода получена из первой и второй применением правила modus ponens. Наконец, четвёртая формула получается из первой схемы аксиом подстановкой формулы А вместо формулы В. ?

Задача 1.3. Существует ли формула исчисления высказываний, которая встречается ровно в двух выводах?

Кроме выводимости мы будем использовать выводимость из множества формул Г (по традиции формулы из этого множества называются гипотезами). Определение формулы, выводимой из множества Г, почти дословно повторяет определение выводимой формулы.

Определение 1.14. Формула А называется выводилюй в исчислении высказываний из множества гипотез Г, если существует последовательность формул

В которой ДЛЯ любой формулы Ai выполнено хотя бы одно из трёх условий:

Ai является гипотезой (принадлежит множеству Г);

  • Ai является аксиомой;
  • • найдутся такие j, к < г, что А^ = Aj —> Л*.

Для выводимости из множества Г используется обозначение Г Ь А. Например, {А, В} Ь С или Л, В Ь С (второе обозначение мы будем обычно использовать при записи выводимости из конечных множеств).

Выводимость из множества формул называется также условной выводимостью. Такое называние имеет понятный смысл: из Г I- А следует выводимость формулы А при условии, что любая формула из множества Г выводима.

Приведём простой пример условной выводимости.

Лемма 1.15. А Ь {В—>А).

(в условном выводе одним из обоснований формулы является принадлежность к множеству гипотез). ?

Доказательство.

Из леммы 1.15 следует, в частности, что после того, как доказана выводимость формулы А можно утверждать выводимость любой формулы вида [В—>А). Поэтому, в частности, из противоречия (т. е. формул А и 1 А) можно вывести любую формулу.

Лемма 1.16. Л,1Л Ь В.

Доказательство. Применяем дважды лемму 1.15 и схему аксиом (АЗ):

Мы привели сокращённую запись вывода. Для получения полной записи нужно вставить вместо ссылок на лемму 1.15 вывод из этой леммы. Нумерация строк служит для удобства и не указывает на место формулы в полном выводе. Такую сокращённую запись вывода мы будем использовать и дальше. ?

 
Посмотреть оригинал
< Предыдущая   СОДЕРЖАНИЕ   Следующая >
 

Популярные страницы