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

Рассмотрим некоторое истинное общее следование A B. В формулах A и B могут присутствовать свободные переменные. На место этих переменных можно подставить какие-нибудь формулы. В результате как раз и получится частное следование. А теперь дадим это определение строго.

Определим понятие подстановочной функции.

Функция Subst называется подстановочной, если:

1. Она преобразует одну формулу РБА X в другую формулу РБА X' (то есть, однозначно отображает тексты формул на тексты формул) путем замены некоторых (или всех) свободных переменных в X на другие формулы РБА.
2. Если переменная с одним и тем же именем встречается в формуле X несколько раз, то подстановочная функция заменяет все вхождения переменных на одну и ту же формулу.
3. Функция всегда заменяет переменную с тем же самым именем на ту же самую формулу. То есть, если применение подстановочной функции к формуле X заменило все вхождения переменной x на формулу Z, то применение подстановочной функции к любой другой формуле Y также заменит все вхождения переменной x на формулу Z.
4. Если подстановочная функция заменяет некоторую переменную x в формуле X на формулу Z, то множество значений формулы Z должна быть подмножеством области допустимых значений переменной x в формуле X.

Подстановочная функция описывается множеством упорядоченных пар вида (_γ, Ψ_), где γ - имя заменяемой переменной, и Ψ - текст подставляемой формулы.

Введем понятие операции частного следования:

A _Subst B = (Subst(A') = A) & (Subst(B') = B) & (A' B')    (1)

Запись A _Subst B означает, что при подстановке Subst истинно частное следование из A в B.

Будем также применять сокращенную запись, если функция подстановки оговорена заранее:

A B = A' B'

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

Мы не можем доказать, что формула A B частного следования истинна, если не указана соответствующая формула общего следования и функция подстановки. Однако в определенной ситуации мы можем доказать, что формула A B ложна, даже если не знаем соответствующей формулы общего следования и функции подстановки. А именно:

Теорема 11.0 Если (A & ~B), то A B = false    (2) или, что то же самое: Если ~(A B), то A B = false

Доказательство Возьмем произвольную формулу A' B' и произвольную подстановку Subst и докажем, что для них правая часть формулы (1): (Subst(A') = A) & (Subst(B') = B) & (A' B')    (3) ложна, если истинно (A & ~B).    (4) Рассмотрим (3). Если Subst(A') ≠ A, то (3) сразу ложна по закону поглощения для операции "&". Если Subst(B') ≠ B, то то же самое. Остается рассмотреть случаи, когда (Subst(A') = A) & (Subst(B') = B). Формула (3) означает, что есть некоторая комбинация переменных, при которой (A & ~B) = true. Теперь возьмем соответствующую комбинацию переменных для формул A' и B'. Должно получиться (A' & ~B') = true. Но тогда общее следование A' B' = false. По закону поглощения формула (3) дает false. Итак, для произвольно взятого общего следования и подстановки формула A B оказывается ложной. Значит, можно сказать, что это частное следование ложно "вообще", независимо от выбора подстановки и общего следования.

Здесь стоит пояснить, какая "соответствующая" комбинация переменных имелась в виду в доказательстве теоремы. Поясним это на примере.

Рассмотрим частное следование

A B = x & y x & y & z.    (5)

Существует комбинация переменных x = true, y= true, z = false, при которой левая часть равна A = x & y = true, B = x & y & z = false. Предположим, что формула (5) получилась из формулы:

A' B' = x x & y.    (6)

путем замены переменных:

x на x & y,

y на z.

Подстановочная функция для такой замены определяется двумя упорядоченными парами:

(_x, x & y_),

(_y, z_)

Соответствующую комбинацию переменных для формулы A' B' получим простой подстановкой значений из комбинации x = true, y= true, z = false, которую мы нашли для формулы A B. Значения будем подставлять в правую часть каждой упорядоченной пары и вычислять результат.

(_x, x & y = true & true = true_),

(_y, z = false_)

То есть, "соответствующая" комбинация для формулы A' B' - это x = true, y = false. Нетрудно убедиться, что при таких значениях переменных A' & ~B' = false. И так будет в любом случае, благодаря определению подстановочной функции.

Вслед за введением операции частного следования, можно ввести операцию двойного частного следования по аналогии с операцией двойного общего следования.

A _Subst B = (Subst(A') = A) & (Subst(B') = B) & (A' B')