В первой части свойства операций общего и частного следования рассматриваются детально, с доказательствами. Здесь мы только кратко перечислим
их специально для тех, кому лень продираться через нагромождения формул. За редким исключением свойства относятся к операции
общего следования, т.к. истинность частного следования тривиально зависит от общего.
Общее следование 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