Если в формулу F(х), содержащей свободную переменную x, выполнить всюду подстановку вместоx терма t , то получим формулу F(t).
Этот факт записывают так:
xòtF(x)
F(t).
Подстановка некоторого терма t в формулу F(x) вместо ее свободной переменной x состоит в замещении всех свободных вхождений этой переменной данным термом t. Такая подстановка называется правильной. Подстановка будет неправильной если в результате подстановки сколемовской функции свободная переменная окажется в области действия квантора.
Например,
1. x1òx2$x3( P21(x1, x3)® P2 (x2))
$x3( P21(x2, x3)® P2 (x2)).
Это правильная подстановка, т.к. x1 –свободная переменная.
2. x1òf(x2, t) $x3( P21(x1, x3)® P2 (x2))
$x3( P21(f(x2, t), x3)® P2 (x2)).
Это — правильная подстановка, т.к. x1 –свободная переменная.
3. x3òx2$x3( P21(x1, x3)® P2 (x2))
$x3( P21(x1, x2)® P2 (x2)).
Это — неправильная подстановка, т.к. x3 –связанная квантором $.
4. x2òx3$x3( P1(x1, x3)® P2 (x2))
$x3( P1(x1, x3)® P2 (x3)).
Это — неправильная подстановка, т.к. предикат P2 (x3) попадает в область действия квантора $.
Понятие правильной подстановки необходимо, например, для формулировки законов снятия квантора общности
«x F(x)
F(t)
и введения квантора существования
F(t)
$xF(x).