Лекция
Эквациональная логика ( эквивалентная логика ) первого порядка состоит из бескванторных терминов обычной логики первого порядка , где единственным предикатным символом является равенство .
Теория моделей этой логики была развита в универсальную алгебру Биркгофом , Гретцером и Коном .
Позднее Ловером она была преобразована в раздел теории категорий («алгебраические теории»).
Термины эквациональной логики строятся из переменных и констант с использованием функциональных символов (или операций).
Вот четыре правила вывода логики.
обозначает текстовую замену выражения 
для переменнойхв выражении
. Следующий,
обозначает равенство, поскольку 
и 
того же типа, в то время как 
, или эквивалентность, определяется только для и типа boolean . Для и типа boolean, и имеют одинаковое значение.
| Замена (Substitution) | Если является теоремой, то и . |
 |
|---|---|---|
| Лейбниц | Если  является теоремой, то и . |
 |
| Транзитивность | Если и являются теоремами, то так же и . |
 |
| Невозмутимость (Equanimity) | Если и являются теоремами, то так же иВ . |
 |
Мы объясняем, как четыре правила вывода используются в доказательствах, используя доказательство
.
Логические символы 
и
указывают «истина» и «ложь» соответственно, и¬означает « не ».
Номера теорем относятся к теоремам из книги «Логический подход к дискретной математике» .
Во-первых, линии(0) –(2) показать использование правила вывода Лейбница: (0)=(2)
является заключением Лейбница и его предпосылкой
дается онлайн(1).
Таким же образом, равенство на прямых(2)–(4)обосновываются с помощью Лейбница.
«Подсказка» на линии(1) Предполагается, что это будет предпосылка Лейбница, показывающая, какая замена равных на равные используется. Эта предпосылка – теорема.(3.9)с заменой 
, то есть
Здесь показано, как правило вывода «Замена» используется в подсказках.
От (0)=(2) и (2)=(4), мы заключаем по правилу вывода Транзитивность, что (0)=(4). Это показывает, как используется транзитивность.
Наконец, обратите внимание на эту строку(4),
, является теоремой, как указано в подсказке справа.
Следовательно, по правилу вывода «Невозмутимость» мы заключаем, что строка(0)это тоже теорема. И(0) это то, что мы хотели доказать
Комментарии