ハイティング代数

数学において，ハイティング代数(擬ブール代数)とは、有界束(結び ∨ と交わり ∧ の二種の演算と、最小元 0と最大元 1をもつ束)で，テンプレート:Nowrap ⇔ テンプレート:Nowrap を満たす含意演算子 テンプレート:Nowrap が定義されるものをいう。論理学の視点からは、A→B は、モーダスポネンスつまり推論規則 テンプレート:Nowrap が健全になるような最弱の命題を表す．ブール代数に似て，ハイティング代数は有限個の等式で公理化できるバラエティを成す．ハイティング代数は 1930年に直観主義論理を形式化するために アレン・ハイティングにより導入された。

ハイティング代数は束として分配的である。ブール代数は a→b を(通常そうされるように) テンプレート:Nowrap で定義することでハイティング代数の構造をもつ。同様に、完備な分配束で無限分配則(∧ と ∨ の片方にだけ無限個の演算を含む)を満たすものは、a→b を テンプレート:Nowrap を満たす c の上限をとることでハイティング代数になる。有限の場合は、任意の非空な分配束、特に非空な有限鎖は自動的に完備で分配的であり、ハイティング代数となる。

ハイティング代数の半順序に関して テンプレート:Nowrap は直観的には a から b が導けることを表している。特に最大元 1は恒真命題に対応し、定義より成り立つ不等式 テンプレート:Nowrap は矛盾 0 から任意の命題 a が導かれるという直観に対応する。否定演算 テンプレート:Nowrap は定義には含まれていないが、 テンプレート:Nowrap として構成できる。テンプレート:Nowrap の直観的内容は、a を仮定することで矛盾が導かれることである。この定義から テンプレート:Nowrap が判る。更に テンプレート:Nowrap が示されるが、その逆向きの不等式 テンプレート:Nowrap は一般には正しくない。つまり，ハイティング代数において二重否定の除去は一般には成立しない。

ハイティング代数は、ブール代数の一般化である。つまり、ハイティング代数に排中律 テンプレート:Nowrap、または二重否定の除去 テンプレート:Nowrap を課したものがブール代数である。ハイティング代数 H の テンプレート:Nowrap の形の元はブール束をなすが、それは一般に H の部分代数とはならない(以下で説明する)。

ハイティング代数は、ブール代数が古典論理のモデルとなるのと同じように、直観主義命題論理のモデルとなる。初等トポスの内部論理は、終対象 1の部分対象 (1 から テンプレート:仮リンク Ω への射と同値)に包含で順序をつけてできるハイティング代数を基にしている。

任意の位相空間における位相、つまり開集合の集合はテンプレート:仮リンクをなす。よって，完備ハイティング代数はテンプレート:仮リンクの中心的な対象である。

非最大元の集合が最大元をもつ(よってそれ自身ハイティング代数となる)ハイティング代数はテンプレート:仮リンクであり、一方で任意のハイティング代数は新たな最大元を追加することで subdirectly irreducible となる。よって有限ハイティング代数のなかにも subdirectly irreducible なものが無限個あり、それらは互いに異なるテンプレート:仮リンクを持つ。よって有限ハイティング代数の有限集合で non-laws of Heyting algebra の全ての反例を与えることはできない。このことはブール代数とは明確に対比できる点である。subdirectly irreducible なブール代数は二元からなるものだけであって、それが non-laws of Boolean algebra の反例すべてとなる。これは真理値表という単純な判定法の基盤である。 それにも関わらず、ある等式が全てのハイティング代数で成立するかどうかは決定可能である。

ハイティング代数は時折 擬ブール代数 または ブラウアー束 と呼ばれる。しかしブラウアー束という語は双対的な定義 または若干一般的な意味合いを含めて言及されることもある．

形式的定義

ハイティング代数 H は有界束であって、任意の a,b∊ H に対して

$a\wedge x\le b$

をみたす x の最大元が存在するものをいう。この元は a の b に関する相対的擬補元であり、a→b と書かれる。H の最大元と最小元をそれぞれ 1、 0 と書く。

ハイティング代数において、元 a の 擬補元 ￢a を ￢a=a→0 で定義する。定義から a∧￢a=0 であり， ￢a はこの等式を満たす最大の元である。しかし一般には a∨￢a=1 は成立しない。よって ￢ は(ブール代数で定義されるような)真の補元ではない。

テンプレート:仮リンク とは、完備束であるようなハイティング代数である。

ハイティング代数の部分代数とは、H の部分集合 H₁ であって 0 と 1を含み演算 ∧、∨、→ で閉じているものである(よって￢についても閉じる)。部分代数はそのハイティング代数構造をもとの代数から引き継ぐ。

別定義

圏論的定義

ハイティング代数 H は全ての冪対象を持つ有界束である。つまり、束 H を交わり ∧ が積であるような圏とみなしたとき、 H の任意の対象 Y と Z に対して冪対象 Z^Y が H に一意に存在することを意味する。

含意演算が冪に相当する。(写像や関手を表す → との重複を避けるために ⇒ を用いると) Y ⇒ Z は Z^Y の別表記と考えられる。冪の定義から含意 テンプレート:Nowrapは交わりテンプレート:Nowrapの右随伴であり $-\wedge Y⊣Y\Rightarrow -$ と書ける。つまり $$(-\wedge Y):H\stackrel{⟶}{\underset{⟵}{\mathrm{\top }}}H:(Y\Rightarrow -)$$ である。

束論的定義

ハイティング代数は固定した a∊H に対する次の写像を考えることでも得られる：

$\{\begin{array}{c}{f}_a:H\to H\\ f_a(x)=a\wedge x\end{array}$

有界束 H がハイティング代数をなす必要十分条件は、任意の f_a が単調なガロア接続の下方随伴であることである。この場合対応する上方随伴 g_a は、上で定義された → を用いて g_a(x)=a→x で与えられる。

更に、モノイド演算を ∧ とするテンプレート:仮リンクとして定義することもできる。モノイド演算の単位元は最大元 1である。モノイド演算の可換性から、二つの residual は a→b と一致する。

含意演算を持つ有界束

最大元 1と最小元 0をもつ有界束 A とその上の二項演算 → が以下の条件をみたすとき、ハイティング代数をなす：

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

ここで 4番目の等式は → に対する分配則を示している。

直観主義論理の公理を使った特徴づけ

直観主義論理を用いてハイティング代数を特徴づけると、直観主義命題論理の算術とハイティング代数の関係に関する基本的な事実を即座に証明できる(証明可能な等式節および普遍構成節を参照のこと)。ハイティング代数の最大元 $\mathrm{\top }$ は直観的には証明可能(恒真)な命題とみなせる。直観主義論理の公理と比較のこと。

三種類の二項演算 →、∧、∨ が定義された集合 A と元 $\mathrm{\perp }$ および $\mathrm{\top }$ が以下の条件をみたすとき、A はハイティング代数である(更に条件 $a\le b\Rightarrow a\to b=\mathrm{\top }$ により順序 ≦ が定まる)：

1. $x\le y$ かつ $y\le x$ ならば $x=y,$
2. $\mathrm{\top }\le y$ ならば $y=\mathrm{\top },$
3. $x\le y\to x,$
4. $x\to (y\to z)\le (x\to y)\to (x\to z),$
5. $x\wedge y\le x,$
6. $x\wedge y\le y,$
7. $x\le y\to (x\wedge y),$
8. $x\le x\vee y,$
9. $y\le x\vee y,$
10. $x\to z\le (y\to z)\to (x\vee y\to z),$
11. $\mathrm{\perp }\le x.$

そして，￢x を x→$\mathrm{\perp }$ で定義する。

条件 1は同値な式は等しいこと、条件 2は証明可能な式がモーダスポネンスで閉じていることを表す。条件 3, 4は「ならば」、条件 5,6,7は「かつ」、条件 8,9,10は「または」に関する条件であり、条件 11は「偽」に関する条件である。

もちろん、別の公理一式を論理学に使うのであれば、それに従って条件を変えなければならない。

例

一元生成のテンプレート:仮リンクハイティング代数(Rieger-Nishimura 束とも呼ばれる)

• 任意のブール代数は p→q を ￢p∨q で定義することでハイティング代数になる。
• 最小元 0と最大元 1をもつ任意の全順序は(束としてみると)ハイティング代数である。この場合 p→q は p≦q のもとで 1，それ以外では q に等しい。
• ブール代数ではないハイティング代数で最も単純なものは(束としてみた)全順序 {0, テンプレート:Sfrac,1} である。その演算は以下の表のとおり：

$a\wedge b$ テンプレート:Diagonal split header 0 テンプレート:Sfrac 1 0 0 0 0 テンプレート:Sfrac 0 テンプレート:Sfrac テンプレート:Sfrac 1 0 テンプレート:Sfrac 1

$a\vee b$ テンプレート:Diagonal split header 0 テンプレート:Sfrac 1 0 0 テンプレート:Sfrac 1 テンプレート:Sfrac テンプレート:Sfrac テンプレート:Sfrac 1 1 1 1 1

テンプレート:Nobold テンプレート:Diagonal split header 0 テンプレート:Sfrac 1 0 1 1 1 テンプレート:Sfrac 0 1 1 1 0 テンプレート:Sfrac 1

a ¬a 0 1 テンプレート:Sfrac 0 1 0

ここで テンプレート:Math となるので排中律をみたしていないことに注意。

• 任意の位相において、その開集合がなす束がハイティング代数となる。この場合、元 A→B は A の補集合 A^c と B の和の内部になる。全ての完備ハイティング代数が何らかの空間の位相から得られるわけではない。この問題はテンプレート:仮リンクで研究されており、そこではハイティング代数のことを フレーム(frame) または ロケール(locale)と呼ぶ。
• 任意のテンプレート:仮リンクにおいて open element の束がハイティング代数となる。任意のハイティング代数はこのようにして得られる。なぜならハイティング代数は有界分配束として自由なブール代数拡大をとりブール代数におけるテンプレート:仮リンクとみなせばブール代数に完備化されるからだ。
• 直観主義命題論理のテンプレート:仮リンクはハイティング代数。
• 初等トポスのテンプレート:仮リンクΩのテンプレート:仮リンク全体はハイティング代数をなす。これはトポスから誘導される高階直観主義論理の真理値からなる代数である。更に、一般にトポスの任意の対象 X の部分対象の集合はハイティング代数をなす。
• 任意の n に対してテンプレート:仮リンク LM_n もまたハイティング代数である (しかし n≧5 においてテンプレート:仮リンクではない)。

性質

一般的性質

ハイティング代数 H の順序 ≦ は演算 → から以下のように復元される：任意の元 a, b ∊ H に対して a≦b ⇔ a→b=1。

いくつかの多値論理とは異なり、ハイティング代数は以下の性質をブール代数と共有する：否定演算が不動点をもつ(つまり ￢a=a となる a が存在する)ならば、そのハイティング代数は一元からなる自明な代数である。

証明可能な等式

命題論理式(変数，論理結合子 ∧、∨、￢、定数 0,1 からなる式) $F(A_1,A_2,\dots ,A_n)$ に対して、次の二つの条件の同値性がハイティング代数研究の初期に示された：

P1: 論理式 $F$ は直観主義論理で証明できる。

P2: 任意のハイティング代数 H とその元 $a_1,a_2,\dots ,a_n$ に対して等式 $F(a_1,a_2,\dots ,a_n)=1$ が成り立つ。

このメタレベルの含意 テンプレート:Nowrapは非常に有用で、ハイティング代数における等式を示すための実践的かつ主要な方法である。実用の場では、そのような証明ではしばしば演繹定理が使われる。

ハイティング代数 H の元 a と b に対して a≦b と a→b=1 は成否が一致するので、テンプレート:Nowrap から論理式 $F\to G$ が証明可能ならば $F(a_1,a_2,\dots ,a_n)\le G(a_1,a_2,\dots ,a_n)$ が任意のハイティング代数とその元 $a_1,a_2,\dots ,a_n$ に対して成り立つ。(演繹定理から、(無条件に) F→G が証明可能であることと F から G を証明できること、つまり G が F の論理的帰結であること、は同時な条件である) 特に、F と G の同値性が証明できるならば、≦ が順序関係であることから $F(a_1,a_2,\dots ,a_n)=G(a_1,a_2,\dots ,a_n)$ である。

テンプレート:Nowrap の証明は、証明系の公理を調べ、任意のハイティング代数においてそれらの値が 1になり，また値 1の式に推論規則を適用しても値が保たれることを検証することで得られる。例として、推論規則としてモーダスポネンスだけを持ち、直観主義論理のヒルベルト流公理から構成される証明系を考えよう。すると、上述したハイティング代数の公理的定義から直接この事実を確かめられる。

テンプレート:Nowrap はまた、ある種の命題論理式が、古典論理においてはトートロジーだけれども、直観主義論理式としては証明できないことを示す手段をも与える。論理式 $F(A_1,A_2,\dots ,A_n)$ が証明不可能であることを示すためには、あるハイティング代数 H とその元 $a_1,a_2,\dots ,a_n\in H$ が存在して $F(a_1,a_2,\dots ,a_n)\ne 1$ であることをいえればよい。

もしも論理学への言及を避けたいのであれば、演繹定理の一例である補題を示さざるを得ない：ハイティング代数 H とその元 $a,b,c$に対し、$(a\wedge b)\to c=a\to (b\to c)$。

メタレベルの含意 テンプレート:Nowrap についてより深く知りたければ普遍構成節を参照のこと。

分配性

ハイティング代数はつねに分配的である。特に、次の等式はつねに成り立つ：

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

分配則はときに公理として述べられるが、実際のところ相対的擬補元の存在から従う。演算 ∧ はガロア接続の下方随伴であることから、上限を保つからである。分配性は結局二項の場合の上限が ∧ で保たれることを述べているに過ぎない。

似た議論によって、次のテンプレート:仮リンクが任意の完備ハイティング代数 H とその元 x および部分集合 Y について成り立つ：

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

逆に、この無限分配則をみたす任意の完備束は相対的擬補元を

$a\to b=\bigvee \{c\mid a\wedge c\le b\}$

で定めることで完備ハイティング代数になる。

Regular and complemented elements

ハイティング代数 H の元 x が以下の(同値な)条件のいずれかを満たすとき、regular と呼ぶ：

1. x = ¬¬x.
2. x = ¬y for some y in H.

これらの条件の同値性は、任意の x 属する H に対して ¬¬¬x = ¬x　が成立することと言い直せる。

ハイティング代数 H の元 x と y が x∧y = 0 と x∨y = 1 を満たすとき、それらを互いに 補元(complement)という。x の補元が存在するならば、それは一意に決まり ¬x に等しい。補元を持つ元を complemented と呼ぶ。x が complemented ならば ¬x もそうで、x と ¬x は互いに補元の関係にある。しかし、x が complemented でない場合でも ¬x が(x とは異なる)補元を持つ場合がある。任意のハイティング代数において、0 と 1は互いに補元の関係にある。例えば、0 以外の任意の x について ¬x が 0で、0の補元が 1であることもありうる。このとき 0と 1のみが regular な元になる。

ハイティング代数の complemented な元は regular であるが、一般にその逆は言えない。特に 0と 1は常に regular である。

任意のハイティング代数 H に対して，以下の三条件は同値である:

1. H はブール代数である;
2. H の任意の元 x は regular;
3. H の任意の元 x は complemented.

このとき，元 テンプレート:Nowrap は テンプレート:Nowrap　に等しい。

任意のハイティング代数 H の regular な元はブール代数 H_reg を構成し、演算 ∧, ¬, → および定数 0, 1は H のものと一致する(complemented な元からなる H_comp についても同様)。H_comp の場合は演算 ∨ も一致し、H_comp は H の部分代数となる。しかし一般には H_reg は H の部分代数にならない。それは演算 ∨_reg が ∨ とは異なるかもしれないからである。テンプレート:Nowrap に対して、テンプレート:Nowrap である。∨_reg が ∨ に一致するための必要十分条件は後続の記述を参照してほしい。

ハイティング代数におけるド・モルガン則

次のド・モルガンの法則は任意のハイティング代数で成立する：

$\mathrm{\forall }x,y\in H:\mathrm{\neg }(x\vee y)=\mathrm{\neg }x\wedge \mathrm{\neg }y$.

しかし、もう片方のド・モルガンの法則が成立するとは限らない。そのかわりに弱い形の等式が成立する：

$\mathrm{\forall }x,y\in H:\mathrm{\neg }(x\wedge y)=\mathrm{\neg }\mathrm{\neg }(\mathrm{\neg }x\vee \mathrm{\neg }y)$.

以下の条件は任意のハイティング代数 H で同値である：

1. H は二種類のド・モルガンの法則をみたす,
2. $\mathrm{\neg }(x\wedge y)=\mathrm{\neg }x\vee \mathrm{\neg }y$ ($x,y\in H$),
3. $\mathrm{\neg }(x\wedge y)=\mathrm{\neg }x\vee \mathrm{\neg }y$ ($x,y\in H$ は regular),
4. $\mathrm{\neg }\mathrm{\neg }(x\vee y)=\mathrm{\neg }\mathrm{\neg }x\vee \mathrm{\neg }\mathrm{\neg }y$ ($x,y\in H$),
5. $\mathrm{\neg }\mathrm{\neg }(x\vee y)=x\vee y$ ($x,y\in H$ は regular),
6. $\mathrm{\neg }(\mathrm{\neg }x\wedge \mathrm{\neg }y)=x\vee y$ ($x,y\in H$ は regular),
7. $\mathrm{\neg }x\vee \mathrm{\neg }\mathrm{\neg }x=1$ ($x\in H$).

2の条件は上で言及した「もう片方」のド・モルガンの法則である。6の条件はブール代数 H_reg の演算 ∨_reg が H の演算 ∨ と一致することを述べている。7の条件は regular な元が complemented であること、つまり H_reg = H_comp であることを述べている。

各条件の同値性は以下のように示される。テンプレート:Nowrap テンプレート:Nowrap および テンプレート:Nowrap は自明。テンプレート:Nowrap と テンプレート:Nowrap は(つねに成り立つ)ド・モルガンの法則と regular の定義からの帰結である。テンプレート:Nowrap は 6に現れる x と y にそれぞれ ¬x と ¬¬x をとり、テンプレート:Nowrap を適用する。テンプレート:Nowrap は(つねに成り立つ)ド・モルガンの法則から、テンプレート:Nowrap は 6, 7 に与えられた条件から部分代数 H_comp の演算 ∨ が H の ∨ の制限となることから従う。テンプレート:Nowrap は 5の x と y にそれぞれ ¬x と ¬y を代入して弱いド・モルガンの法則を適用すればよい。

上記の条件をみたすハイティング代数は、一般にハイティング代数が直観主義論理と関係づけられるのと同じ意味で、中間論理と関係づけられる。

ハイティング代数の射

定義

ハイティング代数 H₁ と H₂ と写像 テンプレート:Nowrap をとる。f が H₁ の任意の元 x と y に対して以下の条件をみたすとき、f をハイティング代数の射と呼ぶ。

1. $f(0)=0,$
2. $f(x\wedge y)=f(x)\wedge f(y),$
3. $f(x\vee y)=f(x)\vee f(y),$
4. $f(x\to y)=f(x)\to f(y),$

条件 2, 3, 4から f は増加関数であり、テンプレート:Nowrap のもとで テンプレート:Nowrap が成り立つ。

H₁ と H₂ が演算 →, ∧, ∨ (可能なら ¬も含む)および 0,1をもち、H₁ から H₂ への全射 f が条件 1から条件4を満たすとする。このとき、H₁ がハイティング代数であれば、H₂ もそうである。このことは、(半順序集合としてではなく代数構造として考えたときの)有界束で、ある等式をみたす演算 → をもつものの特徴づけから従う。

性質

任意のハイティング代数について、それ自身への恒等写像 テンプレート:Nowrap は(ハイティング代数の)射であり、射 f と g の合成 テンプレート:Nowrap も射である。よってハイティング代数全体は圏をなす。

例

任意のハイティング代数 H とその任意の部分代数 H₁ に対して包含写像 テンプレート:Nowrap は射である。

任意のハイティング代数 H に対して、写像 テンプレート:Nowrap は H をその regular な元からなるブール代数 H_reg への全射を定める。両者で演算 ∨ が異なる可能性があるので、この写像は H からそれ自身への(ハイティング代数の)射とは限らない。

ハイティング代数の商

ハイティング代数 H と部分集合 テンプレート:Nowrap をとる。F が以下の条件をみたすとき、H のフィルターと呼ぶ：

1. $1\in F,$
2. $x,y\in F$ ならば $x\wedge y\in F,$
3. $x\in F,y\in H,x\le y$ ならば $y\in F.$

H のフィルターたちの共通部分はまたフィルターである。よって、H の部分集合 S について、それを含む最小のフィルターが存在し、S から生成されたフィルターと呼ぶ。S が空集合の場合は テンプレート:Nowrap であり、そうでない場合は F は テンプレート:Nowrap が存在して テンプレート:Nowrap となる元 x ∊ H の全体となる。

H がハイティング代数で F がその上のフィルターであるとき、H に二項関係 ∼ を定めることができる：テンプレート:Nowrap ⇔ テンプレート:Nowrap と テンプレート:Nowrap が共に F の元。この関係 ∼ は同値関係であり、商集合 テンプレート:Nowrapが定まる。テンプレート:Nowrap には標準的全射 テンプレート:Nowrap がハイティング代数の射となるようなハイティング代数構造が一意に定まる。これを H の F による商と呼ぶ。

S をハイティング代数 H の部分集合とし、F を S から生成されるフィルターとする。このとき H/F は次に述べる普遍性をみたす：

任意のハイティング代数の射 テンプレート:Nowrap で任意の テンプレート:Nowrap に対して テンプレート:Nowrap をみたすものについて、f は標準的全射 テンプレート:Nowrap を用いて一意的に分解される。つまり射 テンプレート:Nowrap が一意的に存在して テンプレート:Nowrap となる。射 テンプレート:Prime は f から誘導されたという。

ハイティング代数の射 テンプレート:Nowrap をとる。 ker f と書かれる f の核は、テンプレート:Nowrap をみたす元の集合で、 H₁ のフィルターである。(注意すべきは、この定義はブール代数の射に適用すると，環の射としてみたときの射の核の双対になることだ) 前述のことにより、f は射 テンプレート:Nowrap を誘導する。これは テンプレート:Nowrap と H₂ の部分代数 f[H₁] との間の同型を与える。

普遍構成

直観主義論理を念頭においた命題論理式のハイティング代数

証明可能な等式節で述べたメタ含意 テンプレート:Nowrap は以下の構成自体からハイティング代数が導かれることから証明される。

1. A₁, A₂, ... , A_n を変数とする命題論理式の集合 L をとる。
2. L の前順序 ≦ を「 F ≦ G ⇔ G が F の(直観主義での)論理的帰結」で定義する。つまり、G が F から証明可能であるとき F≦G。
3. 前順序 ≦ から同値関係 ~ を「F~G ⇔ F≦G かつ G≦F」で定める。この同値関係は直観主義論理における論理的同値を表している。
4. H₀ を商 L/~ とする。これが求めるハイティング代数である。
5. 論理式 F の同値類を [F] と書くことにして、論理式 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] である。

公理的なハイティング代数の定義の場合と同じように、H₀ に順序 ≦を x≤y ⇔ x→y=1 で定義する。演繹定理により、論理式 F→G は G が F から証明できるとき、またそのときに限り証明できるのだから、[F]≤[G] は F≼G が成り立つとき、またそのときに限り成り立つ。つまり、≦ は L の前順序から導かれる L/~ の順序関係である。

ハイティング代数の自由生成

前節で述べたことは(有限個と限らない)生成元集合 {A_i : i∊I} に対しても実行できる。結果として得られる H₀ はこの生成元集合上の自由ハイティング代数という。「自由」とは以下のことを意味している：変数として 〈a_i: i∈I 〉 をもつ任意のハイティング代数 H に対し、射 f:H₀→H で f([A_i])=a_i をみたすものが一意に存在する。f の一意性は把握しづらく、また存在性は本質的に証明可能な等式節のメタ含意 テンプレート:Nowrap の系として得られる。つまり F と G が同値性を証明できる論理式とするとき，H の任意の元の族〈a_i〉に対して F(〈a_i〉)=G(〈a_i〉) である。

理論 T に関して同値な論理式のなすハイティング代数

変数 {A_i} をもつ論理式の集合 T を公理の集合とみなすと、同様の構成が行える。ただし L 上の関係 F≦G は G が F と T から証明可能であることを意味する。H_T を得られるハイティング代数としよう。H_T は H₀ と同じ普遍性をもつが、H と元の族 〈a_i〉 は T の公理 J(〈A_i〉) に対して J(〈a_i〉)=1 をみたすとする。(H_T 自身が元の族 〈[A_i]〉に対してこの性質をもつことを付記する) 普遍性を示す射の存在と一意性は H₀ と同じように証明されるが、証明可能な等式節の テンプレート:Nowrap で P1の条件を「T から証明できる」、P2の条件を「T の論理式をみたす任意の元 a₁, a₂,..., a_n 」と読み替える必要がある。

ハイティング代数 H_T は(同じ変数集合から定義される)自由なハイティング代数 H₀ の商とみなせる。実際 H_T と元の族 〈[A_i]〉 に関する H₀ の普遍性を適用すればよい。

任意のハイティング代数は H_T の形の代数に同型である。ハイティング代数 H とその生成系 <a_i: i∈I> に対し、〈A_i: i∈I〉 変数とする論理式 J(〈A_i〉) で J(〈a_i〉)=1 になるものを T とすればよい。すると明らかに全射となる f:H_T→H が H_T の普遍性から得られる。f が単射になるのを見るのは難しくない。

リンデンバウム代数との比較

本節で与えたハイティング代数に対する構成は、ブール代数に対するテンプレート:仮リンクとよく似た役割を果たす。実際、{A_i} を変数とし公理 T をもつリンデンバウム代数 B_T は H_T∪T1 である(T₁ は ￢￢F→F の形の論理式の集合)。これは追加した公理 T₁ が古典的な恒真命題を証明可能にするのにちょうど必要なものだからである。

直観主義論理とハイティング代数

直観主義論理の公理をハイティング代数の項と解釈すると、それらは任意のハイティング代数および論理式に現れる変数への任意の値の割当てのもとで最大元 1に評価されるだろう。例えば (P∧Q)→P は擬捕性の定義から $P\wedge Q\wedge x\le P$ であるような　x の最大のものになる。この不等式は任意の x で成立するのでその最大元は 1であることがわかる。

さらに、モーダスポネンスの法則によって、論理式 P と P→Q から論理式 Q が導出される。しかしハイティング代数においては、P と P→Q が共に 1であるならば　$P\wedge 1\le Q$ であり、さらに $1\wedge 1\le Q$ が導かれて Q の値も 1であることがわかる。

このことは論理式が直観主義論理の法則、つまりモーダスポネンス同様に直観主義論理の公理から導かれるとき、任意のハイティング代数で変数に任意の値を割り当てた状況でその論理式は常に値 1をもつ。しかし、パースの法則が値 1を持つとは限らないハイティング代数を構成できる。前述した三元集合 {0,テンプレート:Sfrac,1} において、テンプレート:Sfrac を P に、 0 を Q に割り当てると、パースの法則 ((P→Q)→P)→P の値は テンプレート:Sfracになる。これはパースの法則が直観主義的には導出できないことが理由である。型理論においてこれが何を示唆しているかという一般的な文脈を知るにはカリー＝ハワード同型対応の項目を参照すること。

逆も同様に証明される：論理式が常に値 1を取るならば、その論理式は直観主義論理の法則から導出される(だから直観主義的に妥当な論理式とは、まさしく常に 1をとる論理式であるといえる)。この状況は、古典論理的に妥当な論理式とテンプレート:仮リンクで 1をとる論理式(その変数には真または偽を任意に割り当てた)との対応と似ている。つまり、これらの論理式は通常の真理値表の意味で恒真である．論理学の視点に立つとハイティング代数は真理値による通常使われる系の一般化であり、最大元 1は真偽の真に対応する。通常の二値の論理系はハイティング代数の特別な場合であり、1(真)と 0(偽)だけから成るそれは非自明で最小なものになっている。

決定問題

与えられた等式が任意のハイティング代数で成立するかどうかが決定可能であることはソール・クリプキが 1965年に証明した。この問題の正確な計算複雑性については 1979年にテンプレート:仮リンクがPSPACE完全であることを確かめ、よって少なくともブール代数における等式の決定問題と同じくらい求解が困難で(1971年にスティーブン・クックが示した)、更に難しい問題だと予想されている。ハイティング代数の初等理論および一階述語理論は決定不能である。ハイティング代数のテンプレート:仮リンクまたはテンプレート:仮リンクが決定可能かどうかは未解決問題として残っている。語の問題に関して言うと、ブール代数とは対照的にハイティング代数は局所有限ではない(非空な有限集合から生成されるハイティング代数で有限になるものはない)ことが知られている。ブール代数は局所有限で語の問題は決定可能である。

位相的表現と双対性

任意のハイティング代数 テンプレート:Math はある位相空間テンプレート:Mathの開集合からなる有界部分束テンプレート:Mathと自然に同型である。ここでテンプレート:Mathの含意 $U\to V$ は $(X\setminus U)\cup V$ の内部で定義される。より正確には、テンプレート:Mathは有界束テンプレート:Mathの素テンプレート:仮リンクのテンプレート:仮リンクである。

一般には、ハイティング代数の圏はハイティング空間の圏と双対的に同値である。この双対性は分配的有界束からハイティング代数の(非充満的な)部分圏への対応を与える古典的なストーン双対性の制限とみることができる。

もしくは、ハイティング代数の圏はテンプレート:仮リンクの圏と双対的に同値である．これをテンプレート:仮リンクと呼ぶ。

関連項目

• 直観論理
• ブール代数
• ブラウワー代数
• 束論
• ストーン双対性
• テンプレート:仮リンク
• 中間論理
• テンプレート:仮リンク
• テンプレート:仮リンク

参考文献

• テンプレート:Cite book
• F. Borceux, Handbook of Categorical Algebra 3, In Encyclopedia of Mathematics and its Applications, Vol. 53, Cambridge University Press, 1994. テンプレート:ISBN テンプレート:OCLC
• G. Gierz, K.H. Hoffmann, K. Keimel, J. D. Lawson, M. Mislove and D. S. Scott, Continuous Lattices and Domains, In Encyclopedia of Mathematics and its Applications, Vol. 93, Cambridge University Press, 2003.
• S. Ghilardi. Free Heyting algebras as bi-Heyting algebras, Math. Rep. Acad. Sci. Canada XVI., 6:240–244, 1992.
• テンプレート:Citation
• テンプレート:Cite book
• テンプレート:Cite book
• テンプレート:Citation.

外部リンク

• テンプレート:PlanetMath

テンプレート:Normdaten テンプレート:Mathlogic-stub