Главная arrow книги arrow Копия Глава 9. Логический вывод в логике первого п arrow Правило вывода в логике первого порядка
Правило вывода в логике первого порядка

В этом правиле имеется n+1 предпосылка: л атомарных высказываний рi' и одна импликация. Заключение становится результатом применения подстановки θ к следствию д. В данном примере имеет место следующее:

Можно легко показать, что обобщенное правило отделения — непротиворечивое правило логического вывода. Прежде всего отметим, что для любого высказывания ρ (в отношении которого предполагается, что на его переменные распространяется квантор всеобщности) и для любой подстановки θ справедливо следующее правило:

Это правило выполняется по тем же причинам, по которым выполняется правило конкретизации высказывания с квантором всеобщности. Оно выполняется, в частности, в любой подстановке θ, которая удовлетворяет условиям обобщенного правила отделения. Поэтому изможно вывести следующее: а из импликации— следующее:

Теперь подстановка θ в обобщенном правиле отделения определена так, что для всех i, поэтому первое из этих двух высказываний точно совпадает с предпосылкой второго высказывания. Таким образом, выражение Subst (θ, g) следует из правила отделения.

Как принято выражаться в логике, обобщенное правило отделения представляет собой поднятую версию правила отделения — оно поднимает правило отделения из пропозициональной логики в логику первого порядка. В оставшейся части этой главы будет показано, что могут быть разработаны поднятые версии алгоритмов прямого логического вывода, обратного логического вывода и резолюции, представленных в главе 7. Основным преимуществом применения поднятых правил логического вывода по сравнению с пропозиционализацией является то, что в них предусмотрены только те подстановки, которые требуются для обеспечения дальнейшего выполнения конкретных логических выводов. Единственное соображение, которое может вызвать недоумение у читателя, состоит в том, что в определенном смысле обобщенное правило вывода является менее общим, чем исходное правило отделения: правило отделения допускает применение в левой части импликации любого отдельно взятого высказывания a, а обобщенное правило отделения требует, чтобы это высказывание имело специальный формат. Но оно является обобщенным в том смысле, что допускает применение любого количества выражений pi'.