Введение

Правило вывода в предикатной логике

В предикатной логике универсальное инстанцирование (UI; также называемое универсальной спецификацией или универсальным устранением, и иногда путают с dictum de omni) – это корректное правило вывода от истины о каждом элементе класса индивидов к истине об определенном индивиде этого класса. Оно обычно представляется как правило квантификации для универсального квантора, но также может быть закодировано в аксиоматической схеме. Это один из базовых принципов, используемых в теории квантификации. Пример: "Все собаки – млекопитающие. Фидо – собака. Следовательно, Фидо – млекопитающее". Формально правило как аксиоматическая схема задается следующим образом:

для любой формулы A и любого терма t, где – результат подстановки t вместо каждого свободного вхождения x в A. является инстанцией

А как правило вывода:

из следует

Ирвинг Копи отметил, что универсальное инстанцирование "вытекает из вариантов правил "естественного вывода", разработанных независимо друг от друга Герхардом Гентценом и Станиславом Яшковским в 1934 году".

Куин

Согласно Уилларду Ван Орман Куину, универсальная инстанциарность и экзистенциальная генерализация — это два аспекта единого принципа, поскольку вместо утверждения, что "∀x x = x" влечет "Сократ = Сократ", мы можем столь же корректно утверждать, что отрицание "Сократ ≠ Сократ" влечет "∃x x ≠ x". Принцип, лежащий в основе этих двух операций, представляет собой связь между квантификацией и сингулярными высказываниями, которые выступают в качестве их экземпляров. Однако это принцип лишь в переносном смысле. Он верен только в тех случаях, когда термин является именем и, кроме того, употребляется референциально.