Аналогично будут пониматься и более длинные цепочки. Так, запись
= = = имеет смысл
= , = , = [5]
IV. Постулаты.
[а]. Схемы аксиом.
1. ( & ) = ( & ) (закон коммутативности для конъюнкции).
2. ( V ) = ( V ) (закон коммутативности для дизъюнкции).
3. (( & ) & ) = ( & ( & )) (закон ассоциативности, или сочетательности, для конъюнкции).
4. (( V ) V ) = ( V ( V )) (закон ассоциативности для дизъюнкции).
5. ( & ( V )) = (( & ) V ( & )) (закон дистрибутивности, или распределительности, конъюнкции относительно дизъюнкции).
6. ( V ( & )) = (( V ) & ( V )) (закон дистрибутивности дизъюнкции относительно конъюнкции).
7. ( & ( V )) = (первый закон поглощения).
8. ( V ( & )) = (второй закон поглощения).
9. ~( & ) = (~ V ~) (первый закон Де Моргана).
10. ~( V ) = (~ & ~) (второй закон Де Моргана).
11. ( & ) = (закон идемпотентности для конъюнкции).
12. ( V ) = (закон идемпотентности для дизъюнкции).
13. ~~ = (закон снятия двойного отрицания).
14. ( & 1) = (закон отбрасывания единицы).
15. ( V 0) = (закон отбрасывания нуля).
16. ( & ~) = 0 (закон противоречия, выраженный в форме приравнивания противоречия нулю).
17. ( & ~)=1 (закон исключенного третьего, выражений в форме равенства).
Перечисленные постулаты[6] являются не аксиомами, а схемами аксиом. Это значит, что, каждый постулат задает бесконечное множество аксиом определенной структуры. Так, схема аксиом 1 задает аксиомы: (А1 & А2) = (A2 & A1), ((А1 V ~A2) & ~A1) = (~A1 & (A1 V ~A2)) и т.д.; аксиомы — это равенства, принимаемые в качестве исходных.
Схемы аксиом 1 и 2 задают свойство перестановочности членов в конъюнктивных и дизъюнктивных формулах. Схемы аксиом 3 и 4 выражают ассоциативные законы, подобные ассоциативным законам школьной алгебры, где, как известно,
В данной же системе обе операции, конъюнкция и дизъюнкция, дистрибутивны одна относительно другой (схемы аксиом 5 и 6). Смысл законов Де Моргана[7] (схемы аксиом 9 и 10) можно передать фразами: «Отрицание конъюнктивной формулы означает дизъюнкцию отрицаний ее членов»; «Отрицание дизъюнктивной формулы означает конъюнкцию отрицаний ее членов». Смысл схем аксиом, выражающих остальные законы, непосредственно ясен. Заметим лишь, что они служат эффективным средством упрощения формул рассматриваемой формальной системы, то есть построения по данной формуле таких равных ей формул, которые проще, чем исходная (в том смысле, что содержат меньшее число вхождений логических связок); ср. ниже, с. 75—76.
[b]. Правила вывода.
Если верно равенство = , то верно и равенство Ф[] = Ф[]. Здесь Ф[] есть произвольная формула, содержащая в качестве своей части, формулу (аналогично понимается и Ф[]). Это —
В дополнение к этому правилу мы будем в процессе переработки равенств пользоваться известными свойствами отношения равенства —
V. Определения.
Записи вида и ( -> ) суть сокращения для формул вида (~ V )[10] и ((~ V ) & ( V ~)).
Приведенное исчисление представляет собой исчисление равенств формул определенного вида — исчисление, которое в алгебраических терминах носит название исчисления равенств булевых выражений[11]. Оно сформулировано нами как неинтерпретированное исчисление, поскольку при его развертывании не было указано, из какой же области следует брать значения пропозициональных переменных, как следует понимать логические связки и константы 0 и 1, какой смысл имеют формулы и как нужно понимать содержание термина «верная формула».
Дадим теперь первую интерпретацию этого исчисления — функциональную.