ハイティング代数
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2025/07/26 01:25 UTC 版)
数学において，ハイティング代数(擬ブール代数[1])とは、有界束(結び ∨ と交わり ∧ の二種の演算と、最小元 0と最大元 1をもつ束)で，c∧a ≦ b ⇔ c≦ a→b を満たす含意演算子 a→b が定義されるものをいう。論理学の視点からは、A→B は、モーダスポネンスつまり推論規則 A→B,A ⊢ B が健全になるような最弱の命題を表す．ブール代数に似て，ハイティング代数は有限個の等式で公理化できるバラエティを成す．ハイティング代数は 1930年に直観主義論理[2]を形式化するために アレン・ハイティングにより導入された。
ハイティング代数は束として分配的である。ブール代数は a→b を(通常そうされるように) ￢a∨b で定義することでハイティング代数の構造をもつ。同様に、完備な分配束で無限分配則(∧ と ∨ の片方にだけ無限個の演算を含む)を満たすものは、a→b を c∧a≦b を満たす c の上限をとることでハイティング代数になる。有限の場合は、任意の非空な分配束、特に非空な有限鎖は自動的に完備で分配的であり、ハイティング代数となる。
ハイティング代数の半順序に関して a≦b は直観的には a から b が導けることを表している。特に最大元 1は恒真命題に対応し、定義より成り立つ不等式 1≦0→a は矛盾 0 から任意の命題 a が導かれるという直観に対応する。否定演算 ￢a は定義には含まれていないが、 a→0 として構成できる。￢a の直観的内容は、a を仮定することで矛盾が導かれることである。この定義から が判る。更に a≦￢￢a が示されるが、その逆向きの不等式 ￢￢a≦a は一般には正しくない。つまり，ハイティング代数において二重否定の除去は一般には成立しない。
ハイティング代数は、ブール代数の一般化である。つまり、ハイティング代数に排中律 、または二重否定の除去 を課したものがブール代数である。ハイティング代数 H の ￢a の形の元はブール束をなすが、それは一般に H の部分代数とはならない(以下で説明する)。
ハイティング代数は、ブール代数が古典論理[3]のモデルとなるのと同じように、直観主義命題論理のモデルとなる。初等トポスの内部論理は、終対象 1の部分対象 (1 から subobject classifier Ω への射と同値)に包含で順序をつけてできるハイティング代数を基にしている。
任意の位相空間における位相、つまり開集合の集合は完備ハイティング代数をなす。よって，完備ハイティング代数はpointless topologyの中心的な対象である。
非最大元の集合が最大元をもつ(よってそれ自身ハイティング代数となる)ハイティング代数はsubdirectly irreducibleであり、一方で任意のハイティング代数は新たな最大元を追加することで subdirectly irreducible となる。よって有限ハイティング代数のなかにも subdirectly irreducible なものが無限個あり、それらは互いに異なる等式理論を持つ。よって有限ハイティング代数の有限集合で non-laws of Heyting algebra の全ての反例を与えることはできない。このことはブール代数とは明確に対比できる点である。subdirectly irreducible なブール代数は二元からなるものだけであって、それが non-laws of Boolean algebra の反例すべてとなる。これは真理値表という単純な判定法の基盤である。 それにも関わらず、ある等式が全てのハイティング代数で成立するかどうかは決定可能である[4]。
ハイティング代数は時折 擬ブール代数[5] または ブラウアー束[6] と呼ばれる。しかしブラウアー束という語は双対的な定義[7] または若干一般的な意味合いを含めて言及されることもある[8]．
形式的定義
ハイティング代数 H は有界束であって、任意の a,b∊ H に対して
-
一元生成の自由ハイティング代数(Rieger-Nishimura 束とも呼ばれる) - 任意のブール代数は p→q を ￢p∨q で定義することでハイティング代数になる。
- 最小元 0と最大元 1をもつ任意の全順序は(束としてみると)ハイティング代数である。この場合 p→q は p≦q のもとで 1，それ以外では q に等しい。
- ブール代数ではないハイティング代数で最も単純なものは(束としてみた)全順序 {0, 1/2,1} である。その演算は以下の表のとおり：
この項目は、数理論理学に関連した書きかけの項目です。この項目を加筆・訂正などしてくださる協力者を求めています。
- ハイティング代数のページへのリンク
