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

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

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

Силлогизм

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

Замена	Если ${\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}$$

^[2]

История

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

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

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

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

Мы объясняем, как четыре правила вывода используются в доказательствах, используя доказательство ${\textstyle \lnot p\equiv p\equiv \bot }$. В логические символы ${\textstyle \top }$ и ${\textstyle \bot }$ указывают "истина" и "ложь" соответственно, и ${\textstyle \lnot }$ означает "нет". Номера теорем относятся к теоремам Логический подход к дискретной математике.^[2]

$${\displaystyle {\begin{array}{lcl}(0)&&\lnot p\equiv p\equiv \bot \\(1)&=&\quad \left\langle \;(3.9),\;\lnot (p\equiv q)\equiv \lnot p\equiv q,\;{\text{with}}\ q:=p\;\right\rangle \\(2)&&\lnot (p\equiv p)\equiv \bot \\(3)&=&\quad \left\langle \;{\text{Identity of}}\ \equiv (3.9),\;{\text{with}}\ q:=p\;\right\rangle \\(4)&&\lnot \top \equiv \bot &(3.8)\end{array}}}$$

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

$${\displaystyle (0)=(2)}$$

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

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

$${\displaystyle (\lnot (p\equiv q)\equiv \lnot p\equiv q)[p:=q]}$$

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

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

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

Рекомендации

1. эквациональная логика. (нет данных). Бесплатный он-лайн словарь по вычислительной технике. Получено 24 октября 2011 г. с веб-сайта Dictionary.com: http://dictionary.reference.com/browse/equational+logic
2. Грис, Д. (2010). Введение в эквациональную логику. Извлекаются из http://www.cs.cornell.edu/home/gries/Logic/Equational.html

внешняя ссылка

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