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

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

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

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

Замена	Если — теорема, то и .${\textstyle П}$${\textstyle Р[х:=Е]}$	$${\displaystyle \vdash P\qquad \rightarrow \qquad \vdash P[x:=E]}$$
Лейбниц	Если — теорема, то и .${\textstyle Р=Q}$${\textstyle E[x:=P]=E[x:=Q]}$	$${\displaystyle \vdash P=Q\qquad \rightarrow \qquad \vdash E[x:=P]=E[x:=Q]}$$
Транзитивность	Если и являются теоремами, то также является .${\textstyle Р=Q}$${\textstyle Q=R}$${\textstyle П=Р}$	$${\displaystyle \vdash P=Q,\;\vdash Q=R\qquad \rightarrow \qquad \vdash P=R}$$
Невозмутимость	Если и являются теоремами, то также является .${\textstyle П}$${\textstyle P\equiv Q}$${\textstyle В}$	$${\displaystyle \vdash P,\;\vdash P\equiv Q\qquad \rightarrow \qquad \vdash Q}$$

^[2]

Этот раздел мог быть скопирован и вставлен из другого места, возможно, с нарушением политики Википедии в отношении авторских прав . Пожалуйста, просмотрите https://web.archive.org/web/20191022153744/http://www.cs.cornell.edu/home/gries/Logic/Equationalhistory.html  ( Copyvios ) и исправьте это, отредактировав эту статью, чтобы удалить любой несвободный контент, защищенный авторским правом, и правильно указав бесплатный контент или отметив контент для удаления. Пожалуйста, убедитесь, что предполагаемый источник нарушения авторских прав сам по себе не является зеркалом Википедии . ( Декабрь 2024 )

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

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

В своей монографии Дейкстра и Шолтен используют три правила вывода: Лейбниц, Подстановка и Транзитивность. Однако система Дейкстры/Шолтена не является логикой в ​​том смысле, в каком логики используют это слово. Некоторые из их манипуляций основаны на значениях задействованных терминов, а не на четко представленных синтаксических правилах манипуляции. Первая попытка сделать из этого настоящую логику появилась в A Logical Approach to Discrete Math , однако правило вывода Equanimity там отсутствует, а определение теоремы искажено, чтобы учесть его. Введение Equanimity и его использование в формате доказательства принадлежит Грайсу и Шнайдеру. Оно используется, например, в доказательствах обоснованности и полноты, и оно появляется во втором издании A Logical Approach to Discrete Math . ^[2]

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

$${\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 р:=q}$

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

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

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

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

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

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