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

1.11 Аксиомы и правила вывода в ИП

назад | оглавление | вперёд

 

       Поскольку ИП является расширением ИВ, то и множество аксиом ИП является расширением множества аксиом ИВ. Логическими аксиомами для ИП являются аксиомы ИВ и аксиомы ИП:
       

       Правилами вывода в ИП служат:

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

Пример. Доказать выводимость в исчислении предикатов
       Следующий вывод доказывает выводимость данной формулы:
       
       Очень полезными оказываются производные правил вывода, которые позволяют сократить длину вывода формулы. Рассмотрим некоторые из них для исчисления предикатов.

Правило индивидуализации (ПИ). Если А(х) не содержит терм t, то .
Доказательство.
1. гипотеза
2. P1
3. MP 1,2
       Правило доказано.

Правило существования (ПС). Если терм t свободный для переменной х в формуле А(х), то .
Доказательство.
1. P1
2. - тавтология
3. MP 1,2
       Правило доказано.


назад | оглавление | вперёд