В дополнение к этому правилу мы будем в процессе переработки равенств пользоваться известными свойствами отношения равенства —
V. Определения.
Записи вида (α ≡ β) и (α → β) суть сокращения для формул вида (~α V β)[10] и ((~α V β) & (α V ~β)).
Приведенное исчисление представляет собой исчисление равенств формул определенного вида — исчисление, которое в алгебраических терминах носит название исчисления равенств булевых выражений[11]. Оно сформулировано нами как неинтерпретированное исчисление, поскольку при его развертывании не было указано, из какой же области следует брать значения пропозициональных переменных, как следует понимать логические связки и константы 0 и 1, какой смысл имеют формулы и как нужно понимать содержание термина «верная формула».
Дадим теперь первую интерпретацию этого исчисления — функциональную.
Значения знаков → и ≡ вытекают из этих таблиц. В силу того, что (α → β) есть сокращение для (~α V β), (α ≡ β)—сокращение для ((~α V β) & (α V ~β)); можно считать, что знаки → и ≡ задаются таблицами 4 и 5 соответственно.
Поясним, как строится, например, табл. 5. Мы начинаем с того, что строим колонку для формулы ~а, пользуясь табл. 1, задающей операцию (функцию) отрицания; затем, пользуясь табл. 3, определяющей функцию, называемую дизъюнкцией, строим колонку для формулы (~α V β) аналогичным образом строится колонка для формулы (α V ~β) наконец, опираясь на табл. 2, задающую функцию, называемую конъюнкцией, мы строим колонку для конъюнкции ((~α V β) & (α V ~β)) Задание функции ≡ получено: его дают две первые левые (аргументные) колонки табл. 5 и ее крайняя правая колонка.
Задав описанным способом интерпретацию пропозициональных переменных и связок, мы тем самым получаем интерпертацию и для любой формулы[13]: каждая формула осмысливается как функция (таблица), которая может быть построена по данной формуле.
Возьмем, например, формулу (A1 & (A2 V ~A1)) и определим, какую функцию она задает, построив соответствующую таблицу (табл. 6).
Построим таблицу для формулы (А1& ~(А2 V A1))» проверку правильности которой мы выше предоставили читателю. Мы получим табл. 7.
Из нее видно, что эта формула принимает значение 0 при любых значениях своих аргументов. Она называется поэтому тождественно равной нулю. Если мы возьмем отрицание только что рассмотренной формулы, то есть формулу ~(А1 & ~(А2 V A1)), то очевидно, что она задает функцию, которая принимает значение 1 при любых значениях своих аргументов, то есть функцию, тождественно равную единице.
Функции, тождественно равные нулю, неотличимы друг от друга: ведь какие бы значения ни принимали аргументы (и сколько бы их ни было), функции эти все равно принимают одно и то же значение, то есть ведут себя как константы—постоянные. То же самое можно сказать и о функциях, тождественно равных единице. Учитывая это, функции, тождественно равные нулю, мы отождествим с константой 0, а функции, тождественно равные единице, с константой 1 (и, следовательно, будем считать, что значением первой константы является число 0, а второй — число 1).
Для завершения интерпретации нам осталось только установить, при каких условиях равенство α = β следует признать верным (истинным). Будем считать, что α = β есть верное равенство, если α и β задают одну и ту же функцию, то есть, что если построить таблицы, соответствующие формулам α и β, таблицы эти полностью совпадут[14].
Нетрудно проверить, что каждая из 17 схем аксиом задает верное равенство. Проверим это, например, для схемы аксиом 6 (табл. 8).
Мы видим, что колонки нулей и единиц для схем формул (α V (β & γ)) и ((а V β) & (α V γ)) создают, что означает: при любом выборе α, β, γ они переходят в пару формул, задающих одну и ту же функцию. Таким образец, можно сказать, что схема аксиом 6 в нашей интерпретации оказывается схемой верных равенств.
Наконец, нетрудно проверить (эту проверку мы предоставляем читателю), что, действуя по нашим правилам вывода, мы из верного равенства всегда будем выводить верное же равенство.