4. 2. 2. Исчисление предикатов

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

Для того чтобы формализовать процесс вывода необходимо также выделить классы фор­мул по кванторам. Дополнительные пра­вила, аксиомы и законы необходимы для оценки возможного введения и удаления, подстановки и замeны только кванторов.

Под интерпретацией формул следует понимать систему, состоящую из не­пустого множества V, называемого универсумом, и отображения предиката P⁽ t₁,t₂, t_n) на двухэлементное множество {и; л}. Предметные постоянные t_i и функциональные символы f_i(t₁, t₂,...) есть элементы tV, а предметные переменные есть обычные переменные, заданные на универсуме. Символы логических и кванторных операций приобретают также обычный смысл. Тогда каждому предикату P(t₁,t₂, t_n), принявшему значение “и” или “л”, ставится в соот­ветствие n-местное отношение на множестве V.

Например, если V есть множество целых чисел, то в формуле

xyz(P(x;+(y, z))):= “существует число x, которое меньше суммы чисел y и z" при х=5, у=1, z=3 имеем двухместную операцию +(1, 3) и двухместное отношение между числом 5 и значением операции +(1,3)=4. Отображение P(5;4) на двухэлементное множество дает значение “л”. При х=5, у=2, z=4 имеем +(2,4)=6 и P(5; 6)=”и”.

Другими словами, интерпретация функциональных символов опре­деляется по значениям функции на универсуме, а интерпретация предикатных символов по отображению на множество {и; л}.

Выделяют три класса формул: тождест­венно истинные, тождественно ложные и выводимые.

Тождественно истинные формулы - это особый класс формул, которые принимают значение “истины” для всех интерпретаций предметных постоянных, функциональных и предикатных символов; это - аксиомы исчисления предикатов.

Например, формула x(F(x))x(F(x)):= формула ”существуют x, для которых F(x)=и”, эквивалентна формуле “не для всех x F(x)=л””. Это тождественно истинная формула.

Тождественно ложные формулы - это особый класс формул исчисления предикатов, которые принимают значение “ложь” для всех интерпретаций входящих в нее предметных постоянных, функциональных и предикатных символов.

Например, формула _x(F(x))_x(F(x)):=“существуют x, для которых формула F(x)=и, и для всех x формула F(x)=л” является тождественно ложной.

Выполнимые формулы - это особый класс формул исчисления преди­катов, которые принимают значение “истина” не для всех интерпретаций входящих в нее предметных постоянных, функциональных и предикатных символов.

Например, формула _x(F(x))_x(F(x)):=” если существует x, для которого F(x)=и, то не для всех х универсума F(x)=и”.

Вывод заключения из множества посылок есть:

F₁;F₂;F_n B,

где слева от знака “” записывают множество посылок и необходимых аксиом F₁;F₂;F_n, а справа – заключение B.

Другая форма записи вывода заключения:

F₁; F₂;F_n

B,

где над чертой записывают множество посылок и аксиом F₁;F₂;F_n, а под чертой - заключение B.

Логический вывод заключения есть теорема:

F₁&F₂&&F_nB,

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