Логічний наслідок логіки предикатів

Означення 13.4. Формула G логіки предикатів називається логічним наслідком формули F, якщо при будь-якій інтерпретації, при якій формула F перетворюється в тотожно істинний предикат, формула G також перетворюється в тотожно істинний предикат. Цей факт записують так F ╞ G. Як і в алгебрі висловлень F ╞ G Û F ® G.

Дві формули рівносильні тоді й тільки тоді, коли кожна із них є логічним наслідком іншої.

Приклади логічних наслідків.

╞

╞

╞ ;

╞ ;

╞ ;

╞ .

Звернемо увагу на тавтології, які виражають закони вилучення квантора загальності й введення квантора існування ╞ , ╞ за умови, що предметна змінна у не входить вільно в формулу F(x). Із цих тавтологій одержуються наступні логічні наслідки: ╞ - правило вилучення квантора загальності (або правило універсальної конкретизації);

╞ - правило введення квантора існування (або правило екзистенціального узагальнення).