По аналогии с предикатами будем называть формулы РБА общезначимыми, невыполнимым, и т.д. Например, постоянная формула - это формула,
значение которой всегда равно
Теорема 07.0
Если один или оба операнда операции следования - постоянные формулы, то | ||||||||||||||||||||
Доказательство Возьмем таблицу истинности:
По ней видно, что если хотя бы одна из двух формул постоянна и всегда равна |
Наличие зависимости между операндами - важнейшее отличие операции общего следования от материальной импликации. Эта зависимость обеспечивается наличием одноименных переменных в операндах и тем, что истинность операндов зависит от этих переменных определенным образом. Если же одноименных переменных нет, то и зависимости быть не должно. Докажем это строго.
Теорема 07.1
Если операнды операции следования не содержат одноименных свободных переменных, то |
Доказательство Если хотя бы один из операндов постоянный, то следование ложно по теореме 07.0. Поэтому остальная часть доказательства посвящена случаю, когда оба операнда переменные.
Поскольку формулы
Поскольку обе формулы переменные, то можно найти такие комбинации значений свободных переменных, при которых
|
Наиболее простой случай, когда между формулами есть нужная зависимость - это когда формулы одинаковы, но не постоянны. Докажем это строго.
Теорема 07.2
Если |
Доказательство
Поскольку формула |