ヘイティング代数

数学において、ヘイティング代数（ Heyting algebra 、擬似ブール代数^[1]とも呼ばれる）は、結合演算と会合演算が ∨ と ∧ と書かれ、最小元が 0 で最大元が 1 である有界格子であり、含意と呼ばれる二項演算a → bを備え、 ( c ∧ a ) ≤ bがc ≤ ( a → b )と同等である。 ^{[説明が必要]}論理的観点から、この定義により、 A → B は、モーダスポネンス、つまり推論規則A → B、A ⊢ Bが妥当である最も弱い命題である。ブール代数と同様に、ヘイティング代数は、有限個の方程式で公理化可能な多様体を形成する。ヘイティング代数は、直観論理を形式化するためにArend Heyting  (1930)によって導入された。

ヘイティング代数は分配格子である。a → bが ¬ a ∨ bと定義されるとき、すべてのブール代数はヘイティング代数であり、同様に、 a → bがc ∧ a ≤ bとなるすべてのcの集合の最大値とされるとき、片側無限分配法則を満たすすべての完全 分配格子もヘイティング代数である。有限の場合、すべての空でない分配格子、特にすべての空でない有限鎖は自動的に完全かつ完全に分配的であり、したがってヘイティング代数である。

定義から 1 ≤ 0 → aが成り立ち、これはあらゆる命題a は矛盾 0 を伴うという直観に対応します。否定演算 ¬ a は定義の一部ではありませんが、 a → 0として定義できます。 ¬ aの直観的な内容は、 a を仮定すると矛盾が生じるという命題です。定義はa ∧ ¬ a = 0 を意味します。さらに、 a ≤ ¬¬ aであることが示されますが、その逆 ¬¬ a ≤ aは一般には真ではありません。つまり、二重否定除去はHeyting 代数では一般には成立しません。

ヘイティング代数は、ブール代数がまさにa ∨ ¬ a = 1 (排中律) を満たすヘイティング代数、つまり ¬¬ a = a であるという意味において、ブール代数を一般化します。形式 ¬ aのヘイティング代数Hの要素はブール格子を構成しますが、一般にこれはHの部分代数ではありません(以下を参照)。

ヘイティング代数は、ブール代数が命題古典論理をモデル化するのと同じ方法で、命題直観論理の代数モデルとして機能します^{[要出典] 。}基本トポスの内部論理は、包含によって順序付けられた終端オブジェクト1のサブオブジェクトのヘイティング代数、つまり 1 からサブオブジェクト分類子Ω への射に基づいています。

任意の位相空間の開集合は完全な Heyting 代数を形成します。したがって、完全な Heyting 代数は無意味位相幾何学における中心的な研究対象となります。

最大元でない集合が最大元を持ち（そして別のヘイティング代数を形成する） 、あらゆるヘイティング代数は部分直接既約で、したがってあらゆるヘイティング代数は新たな最大元を付加することによって部分直接既約にすることができる。従って、有限ヘイティング代数の中にも部分直接既約なものが無限に存在し、そのうちの2つが同じ等式理論を持つことはない。したがって、有限ヘイティング代数の有限集合は、ヘイティング代数の非法則に対するすべての反例を提供することはできない。これはブール代数とは著しい対照をなす。ブール代数の唯一の部分直接既約なのは2元代数であり、したがってそれだけでブール代数の非法則に対するすべての反例に十分であり、これは単純な真理値表決定法の基礎となる。それでも、すべてのヘイティング代数について等式が成り立つかどうかは決定可能である。^[2]

ヘイティング代数は擬似ブール代数[ ^3]やブラウワー格子^[4]と呼ばれることはあまりないが、後者の用語は二重の定義^[5]を意味したり、もう少し一般的な意味を持つこともある^{[6] 。}

ヘイティング代数Hは有界格子であり、 Hの任意のaとbに対して、Hの最大元xが存在し、

${\displaystyle a\wedge x\leq b.}$

この元はbに関するaの相対擬似補元であり、a → bと表記される。 Hの最大元と最小元をそれぞれ 1 と 0 と表記する。

任意の Heyting 代数では、 ¬ a = ( a →0)と設定することにより、任意の元aの擬似補集合¬ aを定義します。定義により、、 ¬ a はこの特性を持つ最大の元です。ただし、一般には は真ではないため、¬ は擬似補集合にすぎず、ブール代数の場合のように 真の補集合ではありません。${\displaystyle a\wedge \lnot a=0}$${\displaystyle a\vee \lnot a=1}$

完全 Heyting 代数は、完全格子である Heyting 代数です。

ヘイティング代数Hの部分代数は、0 と 1 を含み、演算 ∧、∨、→ に関して閉じているHの部分集合H ₁です。したがって、これは ¬ に関しても閉じています。部分代数は、誘導演算によってヘイティング代数になります。

Heyting 代数は、すべての指数オブジェクトを持つ有界格子です。 ${\displaystyle H}$

格子は、 がを満たすカテゴリと見なされ、は の積です。指数条件は、指数内の任意のオブジェクトとに対して、内のオブジェクトとして一意に存在することを意味します。 ${\displaystyle H}$${\displaystyle \wedge}$${\displaystyle Y}$${\displaystyle Z}$${\displaystyle H}$${\displaystyle Z^{Y}}$${\displaystyle H}$

Heyting 含意 (多くの場合、関数 を示すためにを使用するなどの混乱を避けるためにまたはを使用して記述されます) は、指数関数です。は の別の表記法です。指数関数の定義から、含意 ( ) は( ) を満たす右随伴であることがわかります。この随伴は として記述することも、より完全には次のように記述することもできます。 ${\displaystyle \Rightarrow}$${\displaystyle \multimap }$${\displaystyle \to}$${\displaystyle Y\Rightarrow Z}$${\displaystyle Z^{Y}}$${\displaystyle \Rightarrow :H\times H\to H}$${\displaystyle \wedge :H\times H\to H}$${\displaystyle (-\wedge Y)\dashv (Y\Rightarrow -)}$$${\displaystyle (-\wedge Y):H{\stackrel {\longrightarrow }{\underset {\longleftarrow }{\top }}}H:(Y\Rightarrow -)}$$

Heyting 代数の同等の定義は、マッピングを考慮することによって与えられます。

${\displaystyle {\begin{cases}f_{a}\colon H\to H\\f_{a}(x)=a\wedge x\end{cases}}}$

H内の固定されたaに対して。有界格子Hがヘイティング代数となるのは、すべての写像f _aが単調ガロア接続の下随伴である場合に限ります。この場合、それぞれの上随伴g _{a は}g _a ( x ) = a → xで与えられ、→ は上記のように定義されます。

さらに別の定義は、モノイド演算が ∧ である剰余格子として定義されます。モノイド単位は最上位要素 1 でなければなりません。このモノイドの可換性は、2 つの剰余がa → bとして一致することを意味します。

最大要素 1 と最小要素 0 を持つ 有界格子Aと二項演算 → が与えられたとき、これらが Heyting 代数を形成するのは、次の条件が成立する場合のみです。

1. ${\displaystyle a\to a=1}$
2. ${\displaystyle a\wedge (a\to b)=a\wedge b}$
3. ${\displaystyle b\wedge (a\to b)=b}$
4. ${\displaystyle a\to (b\wedge c)=(a\to b)\wedge (a\to c)}$

ここで式4は→の分配法則です。

Heyting 代数のこの特徴付けにより、直観主義命題計算と Heyting 代数の関係に関する基本事実の証明が直接的になります。(これらの事実については、「証明可能な同一性」および「普遍的構成」のセクションを参照してください。) 要素は、直観的に「証明可能な真実」を意味するものと考える必要があります。直観主義論理の公理と比較してください。 ${\displaystyle \top}$

3 つの二項演算 →、∧、∨ と 2 つの区別される要素および を持つ集合Aが与えられたとき、Aがこれらの演算 (およびa → b = のときという条件によって定義される関係 ≤ ) に対する Heyting 代数であるためには、 Aの任意の要素x、y、zに対して次の条件が成り立つ必要があります。 ${\displaystyle \bot}$${\displaystyle \top}$${\displaystyle a\leq b}$${\displaystyle \top}$

1. ${\displaystyle {\mbox{}}x\leq y{\mbox{ かつ }}y\leq x{\mbox{ ならば }}x=y,}$
2. ${\displaystyle {\mbox{}}\top \leq y ならば{\mbox{ }}y=\top ,}$
3. ${\displaystyle x\leq y\to x,}$
4. ${\displaystyle x\to (y\to z)\leq (x\to y)\to (x\to z),}$
5. ${\displaystyle x\land y\leq x,}$
6. ${\displaystyle x\land y\leq y,}$
7. ${\displaystyle x\leq y\to (x\land y),}$
8. ${\displaystyle x\leq x\lor y,}$
9. ${\displaystyle y\leq x\lor y,}$
10. ${\displaystyle x\to z\leq (y\to z)\to (x\lor y\to z),}$
11. ${\displaystyle \bot \leq x.}$

最後に、¬ x をx →と定義します。 ${\displaystyle \bot}$

条件 1 は、同等の式が識別される必要があることを示しています。条件 2 は、証明可能な真の式は、modus ponens の下で閉じていることを示しています。条件 3 と 4 は条件です。条件 5、6、7 はand条件です。条件 8、9、10 はor条件です。条件 11 は偽の条件です。

もちろん、論理に別の公理のセットが選択された場合には、それに応じて私たちの公理を変更することができます。

• すべてのブール代数はヘイティング代数であり、p → qは¬ p ∨ qで与えられます。
• 最小元が 0 で最大元が 1 であるすべての全順序集合は、Heyting 代数です (格子として見た場合)。この場合、p≤qのときはp → q は1 に等しく、それ以外のときはqに等しくなります。
• ブール代数ではない最も単純なヘイティング代数は、全順序集合{0, ⁠1/2⁠ , 1}（格子として見ると）となり、次の演算が得られます。

  この例では、⁠1/2⁠ ∨¬ ⁠1/2⁠ = ⁠1/2⁠ ∨( ⁠1/2⁠ → 0) = ⁠1/2⁠ ∨0 = ⁠1/2⁠排中律を否定します。

• すべての位相は、その開集合格子の形で完全な Heyting 代数を提供します。この場合、要素A → B はA ^cとBの和集合の内部です。ここで、A ^{c は}開集合Aの補集合を表します。すべての完全な Heyting 代数がこの形式であるわけではありません。これらの問題は無点位相で研究され、完全な Heyting 代数はフレームまたはロケールとも呼ばれます。
• すべての内部代数は、その開元格子の形でヘイティング代数を提供します。すべてのヘイティング代数はこの形式です。ヘイティング代数は、その自由ブール拡張を有界分配格子として取り、それをこのブール代数の 一般化された位相として扱うことでブール代数に完成させることができるからです。
• 命題直観論理のリンデンバウム代数はヘイティング代数です。
• 基本的なトポスのサブオブジェクト分類子Ωのグローバル要素は、Heyting 代数を形成します。これは、トポスによって誘導される直観主義的高階論理の真理値の Heyting 代数です。より一般的には、トポス内の任意のオブジェクトXのサブオブジェクトのセットはHeyting 代数を形成します。
• Łukasiewicz-Moisil代数(LMn ₎も任意のnに対してHeyting代数である^{[7] （ただし}n≥5に対してはMV代数ではない^[8]）。

ヘイティング代数H上の順序は、次のように操作 → から復元できます。Hの任意の要素a、bに対して、a → b = 1のときのみ、それが成り立ちます。 ${\displaystyle \leq}$${\displaystyle a\leq b}$

いくつかの多値論理とは対照的に、Heyting 代数はブール代数と次の特性を共有します。否定が不動点を持つ場合(つまり、あるaに対して ¬ a = a )、Heyting 代数は自明な 1 要素 Heyting 代数です。

命題計算の式（変数に加えて、接続詞、定数 0 および 1 を使用）が与えられた場合、次の 2 つの条件が同等であることは、Heyting 代数の研究の早い段階で証明された事実です。 ${\displaystyle F(A_{1},A_{2},\ldots ,A_{n})}$${\displaystyle \land ,\lor ,\lnot ,\to }$

1. 式F は直観主義命題計算において真であることが証明できる。
2. この恒等式は、任意の Heyting 代数Hと任意の要素に対して成り立ちます。${\displaystyle F(a_{1},a_{2},\ldots ,a_{n})=1}$${\displaystyle a_{1},a_{2},\ldots ,a_{n}\in H}$

メタ含意1 ⇒ 2は非常に有用であり、Heyting 代数における恒等式を証明するための主要な実用的な方法です。実際には、そのような証明では演繹定理が頻繁に使用されます。

ヘイティング代数Hの任意のaおよびbに対して、 a → b = 1のときのみ成り立つので、 1 ⇒ 2から、式F → G が証明可能に真であるときはいつでも、任意のヘイティング代数H、および任意の要素に対して成り立つことがわかります。 （演繹定理から、 G がFから証明可能な場合、つまり、G がFの証明可能な帰結である場合に限り、 F → Gが（無条件に）証明可能であることがわかります。）特に、FとG が証明可能に同値である場合、 ≤ は順序関係であるため、 となります。${\displaystyle a\leq b}$${\displaystyle F(a_{1},a_{2},\ldots ,a_{n})\leq G(a_{1},a_{2},\ldots ,a_{n})}$${\displaystyle a_{1},a_{2},\ldots ,a_{n}\in H}$${\displaystyle F(a_{1},a_{2},\ldots ,a_{n})=G(a_{1},a_{2},\ldots ,a_{n})}$

1 ⇒ 2 は、証明体系の論理公理を調べ、任意の Heyting 代数でその値が 1 であることを確認し、次に Heyting 代数で値 1 を持つ式に推論規則を適用すると値 1 を持つ式が得られることを確認することで証明できます。たとえば、推論規則としてmodus ponensのみを持ち、その公理が直観主義論理#公理化で示されているヒルベルト スタイルのものである証明体系を選択しましょう。すると、検証される事実は、上記の Heyting 代数の公理のような定義からすぐにわかります。

1 ⇒ 2 は、特定の命題式が古典論理ではトートロジーであっても、直観主義命題論理では証明できないことを証明する方法も提供します。ある式が証明不可能であることを証明するには、ヘイティング代数Hととなる要素を示すだけで十分です。 ${\displaystyle F(A_{1},A_{2},\ldots ,A_{n})}$${\displaystyle a_{1},a_{2},\ldots ,a_{n}\in H}$${\displaystyle F(a_{1},a_{2},\ldots ,a_{n})\neq 1}$

論理について言及することを避けたい場合、実際には、Heyting 代数に有効な演繹定理のバージョンを補題として証明することが必要になります。Heyting 代数H の任意の要素a、b、cに対して、 が成り立ちます。 ${\displaystyle (a\land b)\to c=a\to (b\to c)}$

メタ含意 2 ⇒ 1 の詳細については、以下の「普遍的な構造」のセクションを参照してください。

ハイティング代数は常に分配的である。具体的には、常に次の恒等式が成り立つ。

1. ${\displaystyle a\wedge (b\vee c)=(a\wedge b)\vee (a\wedge c)}$
2. ${\displaystyle a\vee (b\wedge c)=(a\vee b)\wedge (a\vee c)}$

分配法則は公理として述べられることもありますが、実際には相対擬似補集合の存在から導かれます。その理由は、ガロア接続の下側随伴 が、すべての既存の最大値を保存するからです。分配法則は、 によるバイナリ最大値の保存に他なりません。 ${\displaystyle \wedge }$ ${\displaystyle \wedge }$

同様の議論により、任意の完全なヘイティング代数において 次の無限分配法則が成り立ちます。

${\displaystyle x\wedge \bigvee Y=\bigvee \{x\wedge y\mid y\in Y\}}$

Hの任意の元xとHの任意の部分集合Yに対して成り立つ。逆に、上記の無限分配法則を満たす任意の完全格子は完全ヘイティング代数であり、

${\displaystyle a\to b=\bigvee \{c\mid a\land c\leq b\}}$

相対的な擬似補数演算です。

ヘイティング代数Hの元x は、次の同値な条件のいずれかが成り立つ場合、 正則であるとされます。

1. x = ¬¬ x。
2. H内の何らかのyに対してx = ¬ y。

これらの条件の同値性は、単に ¬¬¬ x = ¬ xという恒等式として言い換えることができ、これはH内のすべてのxに対して有効です。

ヘイティング代数Hの元xとy は、 x ∧ y = 0 かつx ∨ y = 1の場合、互いに補数であるという。存在する場合、そのようなy は一意であり、実際に ¬ xと等しくなければならない。元xが補数を持つ場合、その元を補数と呼ぶ。 xが補数であれば¬ x も補数であり、その場合、xと ¬ x は互いに補数である。しかし、紛らわしいことに、xが補数でなくても、 ¬ x は補数（xと等しくない）を持つことがある。どのヘイティング代数でも、元 0 と 1 は互いに補数である。たとえば、 ¬ x は0 と異なるすべてのxに対して 0 であり、 x = 0 の場合は 1 である可能性があり、その場合、0 と 1 だけが正規の元である。

Heyting 代数の補元はどれも正則ですが、その逆は一般には成り立ちません。特に、0 と 1 は常に正則です。

任意のHeyting代数Hに対して、次の条件は同値である。

1. H はブール代数です。
2. Hのすべてのxは正則である。^[9]
3. Hの全てのxは補数である。^[10]

この場合、要素a → b は¬ a ∨ bに等しくなります。

任意のヘイティング代数Hの正則（それぞれ補元）はブール代数H _reg（それぞれH _comp）を構成し、そこでは演算 ∧、¬、→ および定数 0 と 1 がHのそれらと一致します。 H _compの場合、演算 ∨ も同じであるため、H _{comp は}Hの部分代数です。ただし、一般にH _{reg は}Hの部分代数にはなりません。これは、その結合演算 ∨ _{reg が}∨ と異なる可能性があるためです。x、y ∈ H _regに対して、x ∨ _reg y = ¬(¬ x ∧ ¬ y )が成り立ちます。∨ _{reg が}∨ と一致する ための必要十分条件については、以下を参照してください。

2つのド・モルガン法則のうちの1つは、すべてのヘイティング代数において満たされる。すなわち、

${\displaystyle \forall x,y\in H:\qquad \lnot (x\vee y)=\lnot x\wedge \lnot y.}$

しかし、他のド・モルガンの法則は常に成り立つわけではありません。代わりに弱いド・モルガンの法則があります。

${\displaystyle \forall x,y\in H:\qquad \lnot (x\wedge y)=\lnot \lnot (\lnot x\vee \lnot y).}$

次のステートメントはすべてのHeyting代数Hに対して同値です。

1. Hはド・モルガンの法則の両方を満たし、
2. ${\displaystyle \lnot (x\wedge y)=\lnot x\vee \lnot y{\mbox{ for all }}x,y\in H,}$
3. ${\displaystyle \lnot (x\wedge y)=\lnot x\vee \lnot y{\mbox{ for all regular }}x,y\in H,}$
4. ${\displaystyle \lnot \lnot (x\vee y)=\lnot \lnot x\vee \lnot \lnot y{\mbox{ for all }}x,y\in H,}$
5. ${\displaystyle \lnot \lnot (x\vee y)=x\vee y{\mbox{ for all regular }}x,y\in H,}$
6. ${\displaystyle \lnot (\lnot x\wedge \lnot y)=x\vee y{\mbox{ for all regular }}x,y\in H,}$
7. ${\displaystyle \lnot x\vee \lnot \lnot x=1{\mbox{ for all }}x\in H.}$

条件 2 は、もう 1 つのド・モルガンの法則です。条件 6 は、Hの正則元のブール代数H _{reg上の結合演算 ∨ reg が、} Hの演算 ∨ と一致することを述べています。条件 7 は、すべての正則元が補完的であること、つまりH _reg = H _{comp を}述べています。

同値性を証明する。明らかに、メタ含意1 ⇒ 2、2 ⇒ 3 、および4 ⇒ 5は自明である。さらに、3 ≡ 4および5 ≡ 6 は、第 1 ド・モルガン法則と正則元の定義から単純に生じる。6のxおよびy の代わりに¬ xおよび ¬¬ x を取り、恒等式a ∧ ¬ a = 0 を使用することで、 6 ⇒ 7 となることを示す。2 ⇒ 1 は第 1 ド・モルガン法則から導かれ、7 ⇒ 6 は、条件 6 および 7 について示した特徴付けを考慮すると、部分代数H _comp上の結合演算 ∨ が∨ のH _compへの制限にすぎないという事実から導かれることに注意してください。メタ含意5 ⇒ 2は、5 のxおよびyの代わりに¬ xおよび ¬ yを取るという、弱いド・モルガン法則の自明な帰結である。

上記の特性を満たすヘイティング代数は、ヘイティング代数が一般に直観主義論理と関係するのと同じように、 ド・モルガン論理と関係しています。

2つのヘイティング代数H ₁とH ₂および写像f  : H ₁ → H ₂が与えられたとき、H ₁の任意の元xとyに対して次が成り立つとき、 ƒ はヘイティング代数の射であるという。

1. ${\displaystyle f(0)=0,}$
2. ${\displaystyle f(x\land y)=f(x)\land f(y),}$
3. ${\displaystyle f(x\lor y)=f(x)\lor f(y),}$
4. ${\displaystyle f(x\to y)=f(x)\to f(y),}$

最後の 3 つの条件 (2、3、または 4) のいずれからも、fは増加関数であることがわかります。つまり、x ≤ yの場合は常にf ( x ) ≤ f ( y )となります。

H ₁とH _{2 が}、演算→、∧、∨ (およびおそらく ¬) と定数 0 と 1 を持つ構造であり、f が上記の性質 1 から 4 を持つH _1からH ₂への全射写像であると仮定します。 H _{1 が}Heyting 代数であれば、 H ₂もHeyting 代数です。 これは、Heyting 代数を、演算 → が特定の恒等式を満たす有界格子 (半順序集合ではなく代数構造として考えられます) として特徴付けることから生じます。

任意のHeyting代数からそれ自身への恒等写像f ( x )= xは射であり、任意の2つの射fとgの合成g∘fも射である。したがってHeyting代数はカテゴリを形成する。

ヘイティング代数Hと任意の部分代数H ₁が与えられたとき、包含写像i  : H ₁ → Hは射である。

任意のヘイティング代数Hに対して、写像x ↦ ¬¬ x はHからその正則元のブール代数H _regへの射を定義します。これは一般にHからそれ自身への射ではありません。なぜならH _regの結合演算はHのものと異なる場合があるからです。

H をヘイティング代数とし、F ⊆ Hとする。Fが以下の性質を満たす場合、 それをH上のフィルターと呼ぶ。

1. ${\displaystyle 1\in F,}$
2. ${\displaystyle {\mbox{If }}x,y\in F{\mbox{ then }}x\land y\in F,}$
3. ${\displaystyle {\mbox{If }}x\in F,\ y\in H,\ {\mbox{and }}x\leq y{\mbox{ then }}y\in F.}$

H上の任意のフィルター集合の共通部分もフィルターです。したがって、Hの任意の部分集合Sが与えられた場合、 S を含む最小のフィルターが存在します。これをSによって生成されたフィルターと呼びます。Sが空の場合、F = {1} です。それ以外の場合、F はH内のxの集合に等しく、 y ₁、y ₂、...、y _n ∈ Sが存在し、 y ₁ ∧ y ₂ ∧ ... ∧ y _n ≤ xであるものになります。

Hがヘイティング代数でF がH上のフィルタである場合、 H上の関係 ~ を次のように定義します。x → yとy → x が両方ともFに属する場合は常にx ~ yと書きます。すると、 ~ は同値関係であり、商集合をH / Fと書きます。 H / Fには、標準全射p _F  : H → H / Fがヘイティング代数射となるような一意のヘイティング代数構造があります。ヘイティング代数H / F をHのFによる商と呼びます。

S をHeyting 代数Hのサブセットとし、F を S によって生成されるフィルタとします。このとき、H / F は次の普遍的性質を満たします。

任意のy ∈ Sに対してf ( y ) = 1 を満たすヘイティング代数f  : H → H ′の任意の射が与えられたとき、f は標準射影p _F  : H → H / Fにより一意に因数分解されます。つまり、f ′ p _F = f を満たす一意の射f ′  : H / F → H ′が存在します。射f ′ はfによって誘導されると言われています。

f  : H ₁ → H ₂をヘイティング代数の射とする。 fの核はker fと書かれ、集合f ⁻¹ [{1}] である。これはH ₁上のフィルターである。(この定義をブール代数の射に適用すると、環の射として見たときの射の核と呼ばれるものと双対になるため注意が必要である。) 前述のように、f は射f ′  : H ₁ /(ker f ) → H ₂を誘導する。これはH ₂の部分代数f [ H ₁ ]へのH ₁ /( ker f )の同型である。

「証明可能な恒等式」のセクションのメタ含意2 ⇒ 1は、次の構成の結果がそれ自体 Heyting 代数であることを示すことによって証明されます。

1. 変数A ₁、A ₂、...、A _nにおける命題式の集合Lを考えます。
2. G がFの（直観主義的）論理的帰結である場合、つまりG がFから証明可能である場合、 F ≼ Gを定義してLに事前順序 ≼ を付与します。≼ が事前順序であることは明らかです。
3. 前順序 F≼G によって誘導される同値関係F ~ Gを考えます。(これは、 F ≼ GかつG ≼ Fの場合にのみ、F ~ Gによって定義されます。実際、 ~ は (直観主義的) 論理同値関係です。)
4. H _{0 を}商集合L /~ とします。これが目的の Heyting 代数になります。
5. 式Fの同値類を[ F ]と書きます。演算 →、∧、∨、¬ はL上で明白に定義されます。式FとGが与えられた場合、同値類 [ F → G ]、[ F ∧ G ]、[ F ∨ G ]、[¬ F ] は [ F ] と [ G ]のみに依存することを検証します。これにより、商集合H ₀ = L /~上の演算 →、∧、∨、¬ が定義されます。さらに、1 を証明可能に真のステートメントのクラスとして定義し、0=[⊥] と設定します。
6. H ₀がこれらの演算とともにヘイティング代数であることを確認します。これは、ヘイティング代数の公理のような定義を使用して行います。与えられた形式のすべての式は直観主義論理の公理であるため、 H ₀は条件 THEN-1 から FALSE を満たします。MODUS-PONENS は、式 ⊤→ F が証明可能に真である場合 (⊤ が証明可能に真である場合)、F も証明可能に真である (推論法則の適用により) という事実から生じます。最後に、EQUIV は、F → GとG → Fの両方が証明可能に真である場合、FとG は互いに証明可能である (推論法則の適用により) という事実から生じ、したがって [ F ]=[ G ] となります。

いつものように、Heyting 代数の公理のような定義の下で、x → y =1の場合に限りx ≤ yであるという条件によってH _{0上の ≤ を定義します。}演繹定理により、式F → Gが証明可能であるのは、G がFから証明可能である場合のみであるため、 F≼G の場合に限り [ F ]≤[ G ] が成り立ちます。言い換えると、 ≤ は、L上の前順序 ≼ によって誘導されるL /~ 上の順序関係です。

実際、前述の構成は、任意の変数集合 { A _i  : i ∈ I } (無限の場合もある)に対して実行できます。このようにして、変数 { A _i } 上の自由Heyting 代数が得られます。これを再びH ₀で表します。これは、任意の Heyting 代数Hとその元の族 〈a _i : i ∈ I 〉 が与えられたときに、 f ([ A _i ])= a _{i を}満たす唯一の射f : H ₀ → Hが存在するという意味で自由です。 fの一意性は簡単に理解でき、その存在は本質的に、上記のセクション「証明可能な恒等式」のメタ含意1 ⇒ 2から生じます。メタ含意とは、FとGが証明可能に同値な式である場合、 H内の任意の元の族 〈a _i 〉 に対してF (〈a _i〉)= G (〈a _i 〉) であるという帰結の形で生じます。

変数 { A _i } の式集合Tを公理として考えると、 L上で定義された関係F ≼ Gに関して同じ構成を実行でき、G はFと公理集合Tの証明可能な帰結であることを意味する。このようにして得られた Heyting 代数をH _Tで表すことにする。すると、 H _Tは上記のH ₀と同じ普遍的性質を満たすが、Heyting 代数Hと、 _T内の任意の公理J (〈A _i 〉)に対してJ ( 〈a _i〉)=1という性質を満たす元 〈 a i 〉の族に関してである。 （H _{T は}、その元の族 〈[ A _i ]〉とともに、それ自体がこの性質を満たすことに注意してください。）射の存在と一意性は、 H ₀の場合と同じ方法で証明されます。ただし、「証明可能な恒等式」のメタ含意1 ⇒ 2 を修正して、 1 が「 T から証明可能に真」になり、 2 が「T の式を満たすHの任意の元a ₁、a ₂、...、a _n 」になる必要があります。

先ほど定義したヘイティング代数H _Tは、 H _{0の普遍的性質を}H _Tとその元の族 〈[ A _i ]〉に適用することで、同じ変数の集合上の自由ヘイティング代数H ₀の商として見ることができます。

あらゆる Heyting 代数は、形式H _Tのいずれかに同型です。これを確かめるために、H を任意の Heyting 代数とし、〈a _i : i ∈I〉 をH を生成する元の族（たとえば任意の射影族）とします。ここで、J (〈a _i 〉)=1となるような変数 〈A _i : i ∈I〉 における式J (〈A _i 〉)の集合T を考えます。すると、 H _Tの普遍的性質により射f : H _T → Hが得られ、これは明らかに射影的です。fが単射であることを示すのは難しくありません。

先ほど示した構成は、リンデンバウム代数がブール代数に関して果たす役割とまったく同様の役割をヘイティング代数に関して果たします。実際、公理Tに関する変数 { A _i } のリンデンバウム代数B _Tは、T _{1 が¬¬} F → F の形式を持つすべての式の集合であるH _{T ∪ T 1}にほかなりません。これは、 T ₁の追加の公理だけが、すべての古典的なトートロジーを証明可能にするために追加する必要がある公理だからです。

直観主義命題論理の公理を Heyting 代数の項として解釈すると、式の変数に任意の値を割り当てることで、任意のHeyting 代数の最大要素 1 に評価されます。たとえば、擬似補集合の定義により、( P ∧ Q )→ Pは、となる最大の要素xです。この不等式は任意のxに対して満たされるため、そのような最大のxは 1 です。 ${\displaystyle P\land Q\land x\leq P}$

さらに、モーダスポネンスの規則により、式PとP → Qから式Q を導くことができます。しかし、どの Heyting 代数でも、P の値が 1 で、P → Q の値が 1 の場合、 となり、したがってQの値が 1 である ことしかあり得ません。${\displaystyle P\land 1\leq Q}$${\displaystyle 1\land 1\leq Q}$

これは、ある式が直観主義論理の法則から演繹可能であり、その公理からモーダスポネンスの規則によって導かれる場合、その式の変数にどのような値を割り当てても、すべてのヘイティング代数で常に値 1 を持つことを意味します。ただし、パースの法則の値が常に 1 ではないヘイティング代数を構築することもできます。3 要素代数 {0, ⁠を考えてみましょう。1/2⁠ ,1}を上記のように代入します。⁠1/2⁠ をPに、 0 をQにすると、パースの法則 (( P → Q )→ P )→ Pの値は⁠1/2⁠。したがって、パースの法則は直観的に導くことはできない。これが型理論において何を意味するかについての一般的な文脈については、カリー・ハワード同型性を参照のこと。

逆もまた証明できる。つまり、ある式の値が常に 1 であれば、それは直観主義論理の法則から演繹可能であるため、直観主義的に有効な式とは、まさに常に値が 1 である式である。これは、古典的に有効な式とは、式の変数に真と偽のあらゆる可能な割り当ての下で2 要素ブール代数で値が 1 である式である、つまり、通常の真理値表の意味でトートロジーである式であるという概念に似ている。したがって、Heyting 代数は、論理的観点からは、通常の真理値体系の一般化であり、その最大要素 1 は「真」に類似している。通常の 2 値論理体系は Heyting 代数の特殊なケースであり、代数の要素が 1 (真) と 0 (偽) のみである最小の非自明な代数である。

与えられた方程式がすべてのヘイティング代数で成り立つかどうかという問題は、1965年にソール・クリプキによって決定可能と示された。 ^[2]問題の正確な計算複雑性は、1979年にリチャード・スタットマンによって確立され、彼はそれがPSPACE完全であることを示した^[11]ため、少なくともブール代数の方程式を決定するのと同じくらい困難であり（1971年にスティーブン・クックによってcoNP完全であることが示された）^[12]、それよりもかなり困難であると推測された。ヘイティング代数の基本理論または第1階理論は決定不可能である。^{[13]ヘイティング代数の}普遍ホーン理論、または単語問題が決定可能かどうかは未解決のままである。^[14] 単語問題に関しては、局所有限で単語問題が決定可能なブール代数とは対照的に、ヘイティング代数は局所有限ではない（有限の空でない集合によって生成されるヘイティング代数は有限ではない）ことが知られている。単一の生成元の場合を除いて、自由ヘイティング代数が新しいトップを付加することで自明に完了可能である場合を除いて、自由完全ヘイティング代数が存在するかどうかは不明である。

あらゆるヘイティング代数H は、位相空間Xの開集合の有界部分格子Lに自然に同型であり、ここでLの含意はの内部によって与えられる。より正確には、X は有界格子Hの素イデアルのスペクトル空間であり、L はXの開集合と準コンパクト部分集合の格子である。 ${\displaystyle U\to V}$${\displaystyle (X\setminus U)\cup V}$

より一般的には、ヘイティング代数のカテゴリはヘイティング空間のカテゴリと双対的に同値である。^{[15]この双対性は、有界分配格子の古典的な}ストーン双対性をヘイティング代数の（非完全）サブカテゴリに 制限したものと見ることができる。

あるいは、ヘイティング代数のカテゴリは、エサキア空間のカテゴリと双対的に同値です。これはエサキア双対性と呼ばれます。

• アレクサンドロフ位相幾何学
• 超直観主義（中間的）論理
• ブール代数のトピックのリスト
• オッカム代数

• ラザフォード、ダニエル・エドウィン (1965)。格子理論入門。オリバーとボイド。OCLC 224572  。
• F. Borceux,カテゴリー代数ハンドブック 3 ,数学とその応用百科事典、第 53 巻、ケンブリッジ大学出版局、1994 年。ISBN 0-521-44180-3 OCLC  52238554 
• G. Gierz、KH Hoffmann、K. Keimel、JD Lawson、M. Mislove、DS Scott、「連続格子と領域」、Encyclopedia of Mathematics and its Applications、第93巻、Cambridge University Press、2003年。
• S. Ghilardi.自由 Heyting 代数を双 Heyting 代数として、Math. Rep. Acad. Sci. Canada XVI.、6:240–244、1992 年。
• Heyting, A. (1930)、「Die formen Regeln der intuitionistischen Logik. I、II、III」、Sitzungsberichte Akad。ベルリン: 42–56、57–71、158–169、JFM  56.0823.01
• ディックマン、マックス; シュワルツ、ニールス; トレスル、マーカス (2019)。スペクトル空間。新しい数学モノグラフ。第35巻。ケンブリッジ：ケンブリッジ大学出版局。doi :10.1017 / 9781316543870。ISBN 9781107146723. S2CID  201542298。