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

Общее следование A B ложно в любом из этих случаев (но не только):

• A не содержит свободных переменных.
• B не содержит свободных переменных.
• A и B не содержат одноименных свободных переменных.
• A всегда равно true (независимо от значений переменных).
• A всегда равно false (независимо от значений переменных).
• B всегда равно true (независимо от значений переменных).
• B всегда равно false (независимо от значений переменных).
• A постоянная формула (т.е. всегда равна одному и тому же, независимо от значений переменных).
• B постоянная формула (т.е. всегда равна одному и тому же, независимо от значений переменных).

В перечисленных случаях может быть истинно частное следование A B.

Транзитивность: если A B и B C, то A C.

Транзитивность можно сформулировать и через вложенное общее следование, если для внешнего следования A, B, C считать переменными, область значений которых - класс предикатов, представимых в РБА:

((A B) & (B C)) (A C)

Обращение: A B = ~B ~A

Рефлексивность: A A, если A не является постоянной формулой.

Modus ponens: Если R' & (R S), то S'

- где R' получается из R подстановкой некоторых значений на место всех свободных переменных, а S' получается из S той же подстановкой. Замыкание справа нужно на тот случай, если в S' останутся переменные (в случае, если в S есть переменные, которых нет в R).

Modus tollens: Если ~S' & (R S), то ~R'

- где S' получается из S подстановкой некоторых значений на место всех свободных переменных, а R' получается из R той же подстановкой. Замыкание справа нужно на тот случай, если в R' останутся переменные (в случае, если в R есть переменные, которых нет в S).

Modus-ы можно сформулировать и через вложенное общее следование:

(R' & (R S)) S'

(~S' & (R S)) ~R'

Правило замены: если A B, то истинно также A' B', где A' получается из A заменой некоторой переменной x на формулу, которая дает все допустимые для x значения, и B' получается из B той же подстановкой.

С помощью этого правила замены можно доказывать сложные формулы на основе простых истинных общих следований:

x x

x & y x

x & y y

x x y

y x y