3.10.5. Анализ проведенных доказательств

Хотя приведенные доказательства не были вполне наглядными, тем не менее их легко перевести в обычную форму записи, начиная с заключения, например:

Множество других резолюций может быть выполнено, и много других путей ведет к пустому предложению. В общем случае выгодно иметь систему предложений с единственным предикатом, так как в этом случае увеличивается число возможных резолюций. Так, при рассмотрении второго доказательства можно обнаружить, что в конце концов оба предложения гипотез об инверсных не используются: все этапы, содержащие резолюции с или удалены. Программа, которая их не содержит, менее стеснена в выборе (например, необходимо более ста шагов, чтобы получить табл. 3.7). В доказательстве, отраженном в этой таблице, первым существенным этапом является этап который утверждает, что наряду с гипотезами имеется и выражение Этот результат представляет собой лемму, поскольку затем поиск вновь начинается в новом направлении, чтобы получить

Это приводит к противоречию, так как е.

Отметим, что умножение слева на с использовалось “интуитивно” в этой резолюции.