等式論理

一階等式論理は、通常の一階等式論理の量化子を含まない項で構成され、等号が唯一の述語記号である。この論理のモデル理論は、バーコフ、グレーツァー、コーンによって普遍代数に発展した。後にローヴェレによって圏論の一分野となった（「代数理論」）。^[1]

等式論理の項は、関数記号 (または演算) を使用して変数と定数から構築されます。

論理の推論規則は 4 つあります。は、式 の変数 に対する式のテキスト置換を表します。次に、 は、同じ型のとに対して等価性を表しますが、 、つまり同値性は、ブール型のとに対してのみ定義されます。ブール型のとに対して、と は同じ意味を持ちます。 ${\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}$

^[2]

等式論理は、効率的な操作や計算のスタイルの必要性を感じていたプログラムの形式開発の研究者によって、長年にわたり（1980 年代初頭から）開発されてきました。この研究に関わったのは、Roland Carl Backhouse、Edsger W. Dijkstra、Wim HJ Feijen、David Gries、Carel S. Scholten、Netty van Gasteren などの人々です。Wim Feijen は証明形式の重要な詳細を担当しています。

これらの公理は、ダイクストラとショルテンがモノグラフ『述語計算とプログラム意味論』 （Springer Verlag、1990 年）で使用した公理と似ていますが、提示の順序が若干異なります。

ダイクストラとショルテンは、そのモノグラフで、ライプニッツ、代入、推移性の3つの推論規則を使用している。しかし、ダイクストラ/ショルテンシステムは、論理学者が使用する言葉としての論理ではない。彼らの操作のいくつかは、関連する用語の意味に基づいており、明確に提示された操作の構文規則に基づいていない。それから本当の論理を作成する最初の試みは、離散数学への論理的アプローチに現れたが、そこには推論規則の平静さがなく、定理の定義はそれを説明するためにねじ曲げられている。平静さの導入と証明形式での使用は、グリースとシュナイダーによるものである。それは、例えば健全性と完全性の証明で使用され、離散数学への論理的アプローチの第2版に掲載されている。^[2]

^[明確化]の証明を用いて、4つの推論規則が証明でどのように使用されるかを説明します。論理記号と はそれぞれ「真」と「偽」を示し、 は「でない 」を示します。定理番号は「離散数学への論理的アプローチ」の定理を参照します。^[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{同一性}}\ \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)}$

最後に、直線 は、その右側のヒントに示されているように定理であることに注意してください。したがって、推論規則 Equanimity により、直線も定理であると結論付けられます。そしてが証明したかったことです。^[2]${\textstyle (4)}$${\textstyle \lnot \top \equiv \bot }$${\textstyle (0)}$${\textstyle (0)}$

• 純粋平等理論

• Sakharov, Alex. 「等式論理」。Eric W. Weisstein が作成した Wolfram Web リソース、MathWorld より。