Натуральное исчисление предикатов

⇐ ПредыдущаяСтр 14 из 32Следующая ⇒

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

Кванторные правила вывода

– правило введения квантора общности ( β – абсолютно ограничено, а – ограничения);

– правило исключения квантора общности;

– правило введения квантора существования;

– правило введения квантора общности ( – абсолютно ограничено, а – ограничения).

Как видно из приведенных правил, их применение требует выполнения ряда условий. Во-первых, выражение является результатом правильной подстановки
в формулу вместо всех свободных вхождений переменной терма t. Выражение – метаязыковая запись результата правильной подстановки в выражение вместо всех свободных вхождений переменной индивидной переменной .
Подстановка является правильной в том случае, если число вхожденийлюбой связанной переменной, определенное для формулы , остается неизменным и после подстановки.

Во-вторых, как мы уже знаем, свободные индивидные переменные трактуются как пробегающие по некоторому универсуму рассуждения U и принимающие любые значения на нем. Но в составе формул индивидные переменные не всегда являются знаками, обозначающими произвольный объект универсума. Свободная индивидная переменная употреблена в некоторой формуле в интерпретации всеобщности, если она в составе формулы понимается как знак, обозначающий произвольный объект из универсума.
Если выведение истинного предложения из некоторой высказывательной формы необходимо ограничить возможными значениями индивидных переменных, то говорят, что переменная использована в условной интерпретации. В случае условной интерпретации переменных выбор значений для одной переменной (абсолютное ограничение – абс. огр.) ограничивает выбор значений для других свободных переменных, входящих в это выражение (ограничение – огр.).

Правило исключения квантора общности ( ) разрешает осуществить переход от формулы вида к формуле . При этом устраняется квантор общности, а в формуле необходимо осуществить подстановку терма t вместо всех свободных вхождений переменной .

Правило введения квантора существования ( ) позволяет осуществить переход от формулы к формуле . При этом посылка должна быть результатом правильной подстановки вместо всех свободных вхождений переменной терма t в формулу .

Правило исключения квантора существования ( ) разрешает осуществить переход от формулы к формуле . В посылке правила утверждается наличие в универсуме объекта, удовлетворяющего условию , что, в свою очередь, позволяет считать таковым объект, обозначенный свободной переменной . Иными словами, необходимо осуществить выбор такого значения для , что утверждение будет истинно. Переменная абсолютно ограничена, и ее следует рассматривать как такое имя объекта, которое удовлетворяет условию . Выбор значения для ограничивает возможные значения для остальных свободных индивидных переменных . Таким образом,
в данном правиле переменные – это все те свободные индивидные переменные, которые входят в выражение .

Правило введения квантора общности ( ) позволяет перейти от формулы к формуле . Однако в данном случае мы имеем две возможности. Во-первых, переменная при данных фиксированных значениях входит в формулу в интерпретации всеобщности. В таком случае переход от к формуле является вполне допустимым. Во-вторых, формула может принимать значение «ложь» при каких-то фиксированных значениях и при некоторых значениях . Тогда следует выбрать одно из таких значений для переменной . Это сделает переменную абсолютно ограниченной, а все остальные свободные переменные ограниченными. Формула является при таком выборе ложной. Но, как нам известно, из ложного высказывания следует все, что угодно, а значит, будет следовать и выражение . В данном правиле переменные – это все свободные переменные формулы .

Применение кванторных правил позволяет как менять подкванторные индивидные переменные на новые переменные, так и обходиться без их замены.

Выводом в натуральном исчислении предикатов первого порядка называется
непустая конечная последовательность формул , которая должна удовлетворять условиям:

– каждая является посылкой либо получена из предыдущих формул по одному из правил вывода;

– в случае если применялись правила введения импликации или введения отрицания, то исключаются из дальнейших шагов построения вывода все формулы, начиная с последней посылки и вплоть до результата применения данного правила;

– ни одна индивидная переменная не может быть абсолютно ограничена дважды;

– ни одна переменная не может ограничивать сама себя;

– только наличие завершенного вывода гарантирует, что между посылками и заключением имеется отношение логического следования.

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

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

Говоря о правилах (эвристиках) выбора посылок в натуральном исчислении предикатов, следует помнить об эвристиках, сформулированных в отношении натурального исчисления высказываний. К ним добавляется еще одна, касающаяся квантифицированных формул.

Четвертая эвристика. Если в результате применения первой эвристики удалось дойти до формулы, имеющей вид или , то можно далее продолжить выбор посылок из формулы A по первой или второй эвристикам, не обращая внимания на наличие кванторов.

Пример 6. Обоснуем выводимость вида :

(1) – посылка;

(2) – к (1);

(3) – посылка;

(4) – modus ponens к (2), (3);

(5) – к (3), (4);

(6) – к (5).

Все условия вывода в данном случае соблюдены, вывод является завершенным.

Пример 7. Докажем выводимость вида :

(1) – посылка;

(2) – к (1), x – абс. огр.;

(3) – к (2);

(4) – к (2);

(5) – к (3), (4).

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

Пример 8. Докажем теорему :

(1) – посылка по 1-й эвристике;

(2) – посылка по 1-й эвристике;

(3) – к (1);

(4) – к (1);

(5) – к (4);

(6) – modus ponens к (5), (2);

(7) – к (3);

(8) – modus ponens к (7), (6);

(9) – к (2), (8);

(10) – к (9), x – абс. огр;

(11) – к (1), (10).

Данный вывод является завершенным доказательством. Причем на шаге (2) доказательства применялась четвертая эвристика к формуле .

В целом для натурального исчисления предикатов справедливым является метаутверждение: завершенный вывод имеет место тогда и только тогда, когда . Это говорит об адекватной формализации логики предикатов первого порядка в натуральном исчислении предикатов.

⇐ Предыдущая 9 10 11 12 131415 16 17 18 Следующая ⇒