Обратите внимание на то, что все вхождения переменной должны быть заменены на новую формулу. Если переменная встречается несколько раз, мы не можем заменить только некоторые вхождения (как в предыдущем правиле замены подформулы). Когда мы вычисляем таблицу истинности для t(x,...), то мы во все места, где встречается переменная x, подставляем одно и то же значение истинности, взятое из одной определенной ячейки таблицы истинности. Что, если мы заменим только часть вхождений переменной? Тогда там, где переменная не была заменена, мы будем по-прежнему брать значения из таблицы, а там, где была заменена - из формулы f(...). Процесс вычислений изменится и может привести к результату false.

Простейший пример. Формула X ~X - тавтология. При X = true она дает true. Заменим только первое вхождение переменной X на формулу ~X. Получим ~X ~X. Эта формула при X = true дает false.

Когда мы заменяем переменную на формулу, то процесс вычисления, конечно, изменится по сравнению с тем, что было до замены. При этом после вычисления формулы f(...) может получиться результат true или false. Дальнейшие вычисления будут соответствовать какой-нибудь строке в таблице истинности t(x,...). Рассмотрим пример. Возьмем тавтологию

A B B A    (1)

и составим для нее таблицу истинности. Заменим в ней A на (C & ~A) и получим формулу

(C & ~A) B B (C & ~A)    (2).

Составим и для нее таблицу истинности, и покажем схематично, как вычисление очередной строки таблицы формулы (2) ведет к вычислению одной из строк таблицы формулы (1).

Примечание: иногда доказательство данной теоремы дается "по индукции", такой подход более строг, но прежде нам пришлось бы объяснять, что же это за индукция такая, и с чем ее едят.

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

Для нейтральных формул подобное правило не работает. После замены нейтральная формула может остаться нейтральной, но может превратиться и в тавтологию, и в невыполнимую формулу. Все зависит от того, на какие строки таблицы t(x, ...) мы будем попадать, вычисляя строки таблицы t(f(...),...). Например, если мы будем попадать всякий раз на строки, где стоит true, то получим тавтологию.

Другие примеры. Из тавтологии

(X & Y) (Y & X)

можно получить тавтологии:

(X & X) (X & X) - путем замены Y на X.
(Y & Y) (Y & Y) - путем замены X на Y.
(A & Y) (Y & A) - путем замены X на A.
(false & Y) (Y & false) - путем замены X на false.
(~A & Y) (Y & ~A) - путем замены X на ~A.
(~((X & X) (X & X)) & Y) (Y & ~((X & X) (X & X))) - путем замены X на ~((X & X) (X & X)).

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

(X & Y) (Y & X) - исходная тавтология.
(X & Q₁) (Q₁ & X) - путем замены Y на Q₁
(Q₂ & Q₁) (Q₁ & Q₂) - путем замены X на Q₂
(Q₂ & Y) (Y & Q₂) - путем замены Q₁ на Y
(Y & X) (X & Y) - путем замены Q₂ на X

- здесь мы за 4 шага поменяли местами переменные X и Y. Таким образом можно при желании заменять переменные сразу "пачками".

Уточним различия между правилами замены подформулы и переменной:

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

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