Подстановка термов в формулы

Формальной подстановкой (или просто подстановкой) называется функция J, определенная на конечном множестве переменных, перерабатывающая каждую переменную х из области определения J в некоторый терм формальную подстановку можно изображать в виде двумерной таблицы

,

где в верхней строке указана область определения функции J:

, и

J(x_i)=t_i.

Пусть Т –формула или терм логики предикатов и J-формальная подстановка . Через ТJ=Т =

Другое обозначение подстановки-множество q={x₁/t₁, x₂/t₂,…,x_n/t_n}, где x_i и t_i, iÎ являются соответственно переменными и термами.

Выражение (атом, терм, формула) Тq обозначает выражение, полученное путем подстановки на места свободных вхождений переменных x₁,…, x_n соответствующих термов t₁,…, t_n.

Если вместо переменных в выражение ничего не подставляется, то подстановка называется пустой. Пустая подстановка обозначается символом Е, E={ }.

Дадим индуктивное определение подстановки.

1.

2.

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

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 свободен для любой переменной формулы Р.

Практически это означает, что свободный для переменной х терм может быть подставлен в формулу Р вместо свободного вхождения переменной х, не изменив ее логического значения. Например, формула (x+y<0) содержит переменные х и у свободно. Логическое значение замыкания этой формулы получается навешиванием квантора общности по свободным переменным, в модели M=(R,<), где R-множество действительных чисел, I[ "х"у(x+y<0) ]=0. Пусть терм t=y²-y. Согласно определению терм t свободен для переменной х в этой формуле. Результатом подстановки будет формула (у²-у+у<0), логическое значение которой I["y(y² <0)]=0,и совпадает со значением формулы до подстановки.

Связав переменную у квантором существования, получим формулу $у(х+у<0). Логическое значение замыкания этой формулы I[ "x$y(x+y<0)]=1, т.е. высказывание: Для любого действительного числа х существует действительное число у, для которого х+у<0 - истинно на множестве действительных чисел R. Переменная у не свободна для переменной х в последней формуле. Результатом подстановки в формулу терма t вместо свободно входящей переменной x: , является предложение которое ложно в множестве действительных чисел R. В результате подстановки терма t в формулу вместо свободного вхождения переменной x произошла смена логического значения формулы. Такое событие называется коллизией переменных.

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