Эквациональная логика - Equational logic

Эквациональная логика первого порядка состоит из бескванторных терминов обычной логики первого порядка с равенством в качестве единственного предикатного символа . Теория модели этой логики была разработана в универсальную алгебру по биркгофовому , Grätzer и Кон . Позже было сделано в отрасль теории категорий по Ловер ( «алгебраические теории»).

Термины эквациональной логики состоят из переменных и констант с использованием функциональных символов (или операций).

Силлогизм

Вот четыре логических правила вывода . обозначает текстовую замену выражения переменной в выражении . Далее, означает равенство для одного и того же типа, в то время как , или эквивалентность, определяется только для типа и типа boolean . For и типа boolean и имеют то же значение. ${\ textstyle P [x: = E]}$${\ textstyle E}$${\ textstyle x}$${\ textstyle P}$${\ textstyle b = c}$${\ textstyle b}$${\ textstyle c}$${\ textstyle б \ экв с}$${\ textstyle b}$${\ textstyle c}$${\ textstyle b}$${\ textstyle c}$${\ textstyle b = c}$${\ textstyle б \ экв с}$

Замена	Если это теорема, значит, так оно и есть . ${\ textstyle P}$${\ textstyle P [x: = E]}$	$${\ Displaystyle \ vdash P \ qquad \ rightarrow \ qquad \ vdash P [x: = E]}$$
Лейбниц	Если это теорема, значит, так оно и есть . ${\ textstyle P = Q}$${\ textstyle E [x: = P] = E [x: = Q]}$	$${\ Displaystyle \ vdash P = Q \ qquad \ rightarrow \ qquad \ vdash E [x: = P] = E [x: = Q]}$$
Транзитивность	Если и являются теоремами, то так и есть . ${\ textstyle P = Q}$${\ textstyle Q = R}$${\ textstyle P = R}$	$${\ Displaystyle \ vdash P = Q, \; \ vdash Q = R \ qquad \ rightarrow \ qquad \ vdash P = R}$$
Невозмутимость	Если и являются теоремами, то так и есть . ${\ textstyle P}$${\ textstyle P \ Equiv Q}$${\ textstyle Q}$	$${\ Displaystyle \ vdash P, \; \ vdash P \ Equiv Q \ qquad \ rightarrow \ qquad \ vdash Q}$$

История

Логика уравнений разрабатывалась на протяжении многих лет (начиная с начала 1980-х годов) исследователями формальной разработки программ, которые чувствовали необходимость в эффективном стиле манипуляции и вычислений. Были задействованы такие люди, как Роланд Карл Бэкхаус , Эдсгер В. Дейкстра , Вим Х. Дж. Фейен, Дэвид Грис , Карел С. Шолтен и Нетти ван Гастерен. Вим Фейен отвечает за важные детали формата доказательства.

Аксиомы аналогичны аксиомам, используемым Дейкстрой и Шолтеном в их монографии « Исчисление предикатов и семантика программ» (Springer Verlag, 1990), но наш порядок изложения немного отличается.

В своей монографии Дейкстра и Шолтен используют три правила вывода Лейбница, подстановку и транзитивность. Однако система Дейкстры / Шолтена не является логикой, как используют это слово логики. Некоторые из их манипуляций основаны на значениях используемых терминов, а не на четко представленных синтаксических правилах манипуляции. Первая попытка сделать из этого реальную логику появилась в «Логическом подходе к дискретной математике» . Однако здесь отсутствует правило вывода «Беспристрастность», и определение теоремы искажено, чтобы объяснить это. Введение Equanimity и его использование в формате доказательства принадлежит Грису и Шнайдеру. Он используется, например, в доказательствах правильности и полноты, и он появится во втором издании « Логического подхода к дискретной математике» .

Доказательство

Мы объясняем, как четыре правила вывода используются в доказательствах, используя доказательство . В логические символы и указывают на «истинно» и «ложно» , соответственно, и указывает на «нет» . Номера теорем относятся к теоремам логического подхода к дискретной математике . ${\ textstyle \ lnot п \ эквив р \ экв \ бот}$ ${\ textstyle \ top}$${\ textstyle \ bot}$${\ textstyle \ lnot}$

Во-первых, линии - показывают использование правила вывода Лейбница: ${\ textstyle (0)}$${\ textstyle (2)}$

это заключение Лейбница, и его посылка дается в Интернете . Таким же образом и равенство по строкам - обосновываются с помощью Лейбница. ${\ textstyle \ lnot (п \ эквив р) \ экв \ лнот р \ экв р}$${\ textstyle (1)}$${\ textstyle (2)}$${\ textstyle (4)}$

Предполагается, что "подсказка" в строке дает предпосылку Лейбница, показывая, какая замена равных вместо равных используется. Эта посылка является теоремой с заменой , т.е. ${\ textstyle (1)}$${\ textstyle (3.9)}$${\ textstyle p: = q}$

Это показывает, как подстановка правила вывода используется в подсказках.

Из и мы заключаем на основании правила вывода Транзитивность, что . Это показывает, как используется транзитивность. ${\ textstyle (0) = (2)}$${\ textstyle (2) = (4)}$${\ textstyle (0) = (4)}$

Наконец, обратите внимание, что строка , является теоремой, на что указывает подсказка справа от нее. Следовательно, по правилу вывода Беспристрастность, мы заключаем, что линия также является теоремой. И это то, что мы хотели доказать. ${\ textstyle (4)}$${\ textstyle \ lnot \ верх \ эквив \ бот}$${\ textstyle (0)}$${\ textstyle (0)}$

Ссылки

внешние ссылки

• Сахаров Алексей. «Эквациональная логика». Материал из MathWorld - веб-ресурса Wolfram, созданного Эриком Вайсштейном.