17. Подстановка термов в формулы. Композиция подстановок. Понятие коллизии переменных.

Формальной подстановкой (или просто подстановкой) называется функция , определенная на конечном множестве переменных, перерабатывающая каждую переменную х из области определения  в некоторый терм. Другое обозначение подстановкимножество ={x₁/t₁, x₂/t₂,…,x_n/t_n}, где x_i и t_i, i являются соответственно переменными и термами. Выражение (атом, терм, формула) Т обозначает выражение, полученное путем подстановки на места свободных вхождений переменных x₁,…, x_n соответствующих термов t₁,…, t_n.

При выполнении подстановки терма в формулу, важно учитывать следующее:

1. Вместо связанных переменных ничего подставлять нельзя.

2. Нельзя допускать появления новых связанных вхождений какой-нибудь переменной, если их не было в исходной формуле.

3. Результат подстановки термов t₁ t₂ ... t_n в формулу Р вместо свободно входящих переменных х₁, х₂, ..., х_n обозначается или P{x₁/t₁,…x_n/t_n}, где {x₁/t₁,…, x_n/t_n} называется подстановкой.

Определение: переменная у свободна для переменной х в формуле Р, если в формуле Р отсутствуют свободные вхождения переменной х, находящиеся в области действия квантора по переменной у; терм t свободен для переменной х в формуле Р, если любая переменная терма свободна для х в формуле Р.

Следствия.

1. Постоянный терм свободен для любой переменной в любой формуле Р.

2. Если ни одна переменная терма не является связанной переменной формулы Р, то терм t свободен для любой переменной формулы Р.

Результатом подстановки в формулу терма t вместо свободно входящей переменной x, является предложение которое ложно в множестве действительных чисел R. В результате подстановки терма t в формулу вместо свободного вхождения переменной x произошла смена логического значения формулы. Такое событие называется коллизией переменных.

Основной операцией на множестве подстановок является композиция.

Пусть имеются две подстановки ={u₁/s₁,… ,u_m/s_m} и ={v₁/t₁,,…, v_n/t_n}.

Композицией  и  называется подстановка ={u₁/s₁,…, u_m/s_m, v₁/t₁, …, v_n/t_n} \ ({u_i/s_i | u_i=s_i}  {v_i/t_i | v_i{u₁,…, u_m}}).

При выполнении композиции подстановок сначала применяется подстановка  в термы s₁,…, s_m подстановки , а затем полученная подстановка дополняется элементами множества . При этом отбрасываются элементы вида u_i/s_i, если терм s_i совпадает с u_i, и элементы вида v_i/t_i, если v_i{u₁,…, u_n}.

18. Аксиоматические основания логики предикатов. Теорема универсальной конкретизации.

правила экзистенциальной конкретизации. Докажем общезначимость: если ╞(x((x)  )(x (x))).Данное выражение означает, что при любых логических значениях атомов, входящих в «большую» формулу, и в любой интерпретации формула остается истинной. В формулу (x) переменная x входит свободно, а формула  не содержит свободных вхождений переменной x. Если в «большую» формулу входят свободно другие переменные, по ним необходимо провести замыкание путем навешивания квантора общности по всем переменным, кроме переменной x. Введем обозначение Результатом замыкания будет новая формулировка теоремы: ╞x 

По определению истинна импликация с ложной посылкой или истинным заключением.

1. Если посылка импликации x ложна, то доказательство окончено, так как импликация с ложной посылкой истинна.

2. Если же посылка импликации x истинна, то в соответствии с правилом определения логического значения формулы, образованной квантором общности Если при этом I[]=1, то доказательство окончено. Если I[]=0, то тогда и только тогда, когда . Но при этом . Следовательно, I[ ]=1.

Теорема доказана.

Аксиоматические основания логики предикатов

Пусть х₁, х₂, ... ,хn_n - полный список свободных переменных формулы А.

Через обозначим формулу, в которой все свободные вхождения переменных связаны квантором общности. Такая формула называется замыканием А. Если формула А не содержит свободных переменных, то будем считать, что замыкание А совпадает с А. Заметим, что замыкание формулы является постоянной формулой. Аналогично через _{обозначим формулу x1 … xn A(x1,…,xn).}Формулу А будем называть общезначимой, если она истинна во всех моделях, т.е. в любой предметной области и в любой интерпретации. При этом замыкание А истинно.

Формула А называется выполнимой, если она истинна в какой-либо интерпретации и в какой-нибудь модели. Таким образом, формула общезначима, если , и выполнима, если . Очевидно, что всякая общезначимая формула выполнима. Обратное не справедливо. Действительно, рассмотрим постоянную формулу F= х у r⁽²⁾ (х, у) и две интерпретации II1₁ и II₂ , которым соответствуют предметные области DD₁=NN и DD₂ =RR (множества натуральных и действительных чисел, соответственно), а сигнатура содержит единственный предикатный символ r⁽²⁾, означающий £Ј. В интерпретации I₁ формула F означает: «существует наименьшее натуральное число», и она истинна. В интерпретации I₂ формула F означает: «существует наименьшее действительное число» - и она ложна. Следовательно, указанная формула выполнима, но не общезначима.

Общезначимая формула А обозначается: ╞ А. Например, ╞ (АА). Если формула А не выполнима ни в какой модели, т.е. ни в какой предметной области и ни в какой интерпретации, она называется противоречием. Например, А&&А.

В бескванторных формулах вопрос о логическом значении формулы решается непосредственным использованием правил определения логического значения связок &&,, , , . Для формул с кванторами процедура определения логического значения формулы осложняется тем, что предметные переменные имеют в общем случае бесконечные области определения. Поэтому прямой перебор всех значений невозможен и приходится использовать косвенные приемы.

Пример 1. Доказать общезначимость:

╞ ((($$xxPP((xx))))  ""xx (Р(х))).

 Пусть для некоторого предиката Р и предметной области DD левая часть эквивалентности истинна. Тогда в предметной области не существует ни одного элемента а  DD, для которого II[[PP((aa))]]=1. Следовательно, для всех аD формула Р(а) ложна. Иначе, II[[""xxùщPP((xx))]]=1.Таким образом, левая и правая части эквивалентности истинны, следовательно, формула истинна.

Пусть теперь левая часть эквивалентности ложна. Тогда в предметной области найдется хотя бы одно значение переменной х, равное а, при котором формула Р(а) истинна. Следовательно, отрицание формулы Р(а) будет ложно, и, следовательно, I[xP(x)]= 0. Следовательно, опять имеем I[11]=1.

Следовательно, рассматриваемая формула общезначима. 

Пример 2. Доказать общезначимость ╞ (х (Р₁(х) Р₂(х)) (хР₁(х)& хР₂(х))).

 Если I[x(P₁ (x) & P₂(x))]=0, то импликация истинна при любом логическом значении заключения импликации. Если же I[x(P(x)&Q(x))] =1, то импликация истинна только при истинном заключении. Истинность посылки импликации в данном случае означает, что в предметной области найдется хотя бы один элемент аD, на котором обе формулы Р(а) и Q(а) истинны одновременно. Но в этом случае каждая из подформул , входящих в конъюнкцию в заключении импликации окажется истинной, и, следовательно, заключение импликации также будет истинно. Следовательно, и в этом случае импликация истинна. Следовательно, данная формула общезначима. 

Для произвольных формул , ,  следующие формулы являются аксиомами:

1. ();

2. (())(()());

3. ()();

4. Правило вывода Modus Ponens: ,    ├ .

5. если free (x,t, ), то общезначимы следующие формулы:

• ╞(x(x)  (x/t)); (правило универсальной конкретизации)

• ╞( (x/t)  x(x)); (правило экзистенциального обобщения)

• ╞(  (x))  ╞ (  x (x));

• ╞((x)  )  ╞ (x (x)  ).

Следующие формулы выводимы в системе аксиом логики предикатов.

free (x, t, ) означает, что терм t свободен для переменной х в формуле .