Языки и исчисления


Аксиомы и правила вывода - часть 5


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

Поясним интуитивный смысл этих правил. Первое говорит, что если из следует , причем в есть параметр , которого нет в , то это означает, что формула истинна при всех значениях параметра , если только формула истинна.

Используя первое правило Бернайса, легко установить допустимость правила обобщения

(если в исчислении предикатов выводима формула сверху от черты, то выводима и формула снизу). В самом деле, возьмем какую-нибудь выводимую формулу без параметров (например, аксиому, в которой вместо , и

подставлены замкнутые формулы). Раз выводима формула , то выводима и формула (поскольку

является тавтологией и даже аксиомой). Теперь по правилу Бернайса выводим и применяем правило MP к этой формуле и к формуле .

Правило (Gen) (от Generalization — обобщение) кодифицирует стандартную практику рассуждений: мы доказываем какое-то утверждение со свободной переменной , после чего заключаем, что мы доказали , так как было произвольным.

Второе правило Бернайса также вполне естественно: желая доказать в предположении , мы говорим: пусть такое существует, возьмем его и докажем (то есть докажем

со свободной переменной ).

94. Покажите, что класс выводимых в исчислении предикатов формул не изменится, если мы вместо правил Бернайса добавим туда правило обобщения и две аксиомы

и

(в которых требуется, чтобы переменная не была параметром формулы ).

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




- Начало -  - Назад -  - Вперед -



Книжный магазин