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

первого порядка Эквациональная логика состоит из бескванторных терминов обычной логики первого порядка с равенством в качестве единственного символа-предиката . Модельная теория этой логики была развита в алгебру Биркгофом Гретцером , Коном и универсальную . в ветвь теории категорий Позже Ловер превратил ее («алгебраические теории»). ^[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]}$ .	$\vdash P\qquad \rightarrow \qquad \vdash P[x:=E]$
Лейбниц	Если ${\textstyle P=Q}$ это теорема, то и она ${\textstyle E[x:=P]=E[x:=Q]}$ .	$\vdash P=Q\qquad \rightarrow \qquad \vdash E[x:=P]=E[x:=Q]$
Транзитивность	Если ${\textstyle P=Q}$ и ${\textstyle Q=R}$ являются теоремами, то и ${\textstyle P=R}$ .	$\vdash P=Q,\;\vdash Q=R\qquad \rightarrow \qquad \vdash P=R$
Невозмутимость	Если ${\textstyle P}$ и ${\textstyle P\equiv Q}$ являются теоремами, то и ${\textstyle Q}$ .	$\vdash P,\;\vdash P\equiv Q\qquad \rightarrow \qquad \vdash Q$

^[2]

История [ править ]

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

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

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

Доказательство [ править ]

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

{\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)}$ покажите использование правила вывода Лейбница:

(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}$ , то есть

(\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 }$ , является теоремой, на что указывает подсказка справа от нее. Следовательно, по правилу вывода Невозмутимость, мы заключаем, что линия ${\textstyle (0)}$ это тоже теорема. И ${\textstyle (0)}$ это то, что мы хотели доказать. ^[2]

См. также [ править ]

Теория чистого равенства

Ссылки [ править ]

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

Внешние ссылки [ править ]

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

[1] эквациональная логика. (без даты). Бесплатный онлайн-словарь по информатике. Получено 24 октября 2011 г. с веб-сайта Dictionary.com: http://dictionary.reference.com/browse/equational+logic .

[gries-2] Jump up to: Перейти обратно: ^а ^б ^с ^д Грис, Д. (2010). Введение в эквациональную логику. Получено с http://www.cs.cornell.edu/home/gries/Logic/Equational.html. Архивировано 23 сентября 2019 г. на Wayback Machine.

[1]

[2]