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

Начнем с кванторов всеобщности. Предположим, что база знаний содержит следующую стандартную аксиому, которая передает мысль, содержащуюся во многих сказках, что все жадные короли — злые:

В таком случае представляется вполне допустимым вывести из нее любое из следующих высказываний:

Согласно правилу конкретизации высказывания с квантором всеобщности

(сокращенно UI — Universal Instantiation), мы можем вывести логическим путем любое высказывание, полученное в результате подстановки базового терма (терма без переменных) вместо переменной, на которую распространяется квантор всеобщности1. Чтобы записать это правило логического вывода формально, воспользуемся понятием подстановки, введенным в разделе 8.3. Допустим, что обозначает результат применения подстановки θ к высказыванию а. В таком случае данное правило для любой переменной ν и базового терма д можно записать следующим образом: