ヘイティング代数

ハイティング代数${\displaystyle H}$は、すべての指数オブジェクトを含む有界格子です。

格子${\displaystyle H}$は、​${\displaystyle \wedge }$は積です。指数条件は、任意のオブジェクトに対して、${\displaystyle Y}$そして${\displaystyle Z}$で${\displaystyle H}$指数関数${\displaystyle Z^{Y}}$オブジェクトとして一意に存在する${\displaystyle H}$。

ヘイティングの含意（多くの場合、${\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 -)}$$

ハイティング代数の同等の定義は、以下の写像を考慮することによって与えることができる。

$${\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でなければならない。このモノイドの可換性は、a → bのとき2つの残余が一致することを意味する。

最大要素が 1、最小要素が 0 である有界格子Aと二項演算 → が与えられたとき、これらがハイティング代数を形成するのは、以下の条件が満たされる場合に限る。

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は→の分配法則である。

このハイティング代数の特徴付けにより、直観主義命題論理とハイティング代数の関係に関する基本的事実の証明が直ちに可能となる。（これらの事実については、「証明可能な恒等式」および「普遍的構成」の項を参照のこと。）要素を考える際には、${\displaystyle \top }$直感的に言えば、「証明可能な真実」という意味である。直観主義論理の公理と比較せよ。

3つの二項演算 →、∧、∨ と2つの異なる要素を持つ集合Aが与えられた。${\displaystyle \bot }$そして${\displaystyle \top }$すると、Aはこれらの演算に対するハイティング代数であり、関係 ≤ は条件によって定義される。${\displaystyle a\leq b}$a → b =の場合${\displaystyle \top }$) 要素Aの任意の要素x、y、zに対して以下の条件が成り立つ場合に限ります。

1. ${\displaystyle {\mbox{If }}x\leq y{\mbox{ and }}y\leq x{\mbox{ then }}x=y,}$
2. ${\displaystyle {\mbox{If }}\top \leq y,{\mbox{ then }}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は、証明可能な論理式はモーダス・ポネンスの下で閉じていることを示しています。条件 3と4は、次の条件です。条件 5、6、7は、かつ条件です。条件 8、9、10は、または条件です。条件 11は、偽の条件です。

もちろん、論理学に別の公理系が採用された場合は、それに合わせて我々の公理系も修正することができる。

順序${\displaystyle \leq }$ハイティング代数Hでは、演算 → から次のように復元できます。Hの任意の要素a、bに対して、${\displaystyle a\leq b}$a → b = 1 の場合に限る。

一部の多値論理とは対照的に、ヘイティング代数はブール代数と次の性質を共有しています。否定が固定点を持つ場合（つまり、あるaに対して ¬ a = aとなる場合）、ヘイティング代数は自明な1要素ヘイティング代数になります。

数式が与えられた場合${\displaystyle F(A_{1},A_{2},\ldots ,A_{n})}$命題論理（変数に加えて、結合子も使用）${\displaystyle \land ,\lor ,\lnot ,\to }$（定数0と1を含む）ハイティング代数の研究では、次の2つの条件が同値であることが早い段階で証明されている。

1. 直観主義命題論理においては、式Fは証明可能な真である。
2. アイデンティティ${\displaystyle F(a_{1},a_{2},\ldots ,a_{n})=1}$これは任意のハイティング代数Hおよび任意の要素に対して真である。${\displaystyle a_{1},a_{2},\ldots ,a_{n}\in H}$。

最初の式が2番目の式を導くというメタ含意（これを1 ⇒ 2と表記する）は非常に有用であり、ハイティング代数における恒等式を証明する主要な実用的方法である。実際には、このような証明において演繹定理が頻繁に用いられる。

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

1 ⇒ 2 は、証明体系の論理公理を調べ、任意のハイティング代数においてその値が 1 であることを確認し、次にハイティング代数において値が 1 である式に推論規則を適用すると値が 1 になる式が得られることを確認することによって証明できます。たとえば、推論規則としてモーダス・ポネンスのみを持ち、公理が直観主義論理#公理化で示されているヒルベルト式のものである証明体系を選択してみましょう。すると、検証すべき事実は、上記で示したハイティング代数の公理のような定義から直ちに導かれます。

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

論理に言及することを避けたい場合、実際には、ハイティング代数に有効な演繹定理のバージョンを補題として証明する必要が生じる。ハイティング代数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. x = ¬ y （ yはHに含まれる）

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

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

ハイティング代数の補元は正則であるが、一般にその逆は成り立たない。特に、0と1は常に正則である。

任意のヘイティング代数Hに対して、以下の条件は同値である。

1. Hはブール代数である。
2. Hのすべてのxは正則である。^{[ 11 ]}
3. Hのすべてのxは補数である。^{[ 12 ]}

この場合、要素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).}$$

以下の記述は、すべてのハイティング代数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は、部分代数H _comp上の結合演算 ∨が、条件 6 と 7 の特徴付けを考慮すると、∨ のH _compへの制限にすぎないという事実から導かれることに注意する。メタ含意5 ⇒ 2は、5 のxとyの代わりに¬ xと ¬ yを取る弱いド・モルガンの法則の自明な帰結である。

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

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

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 ₁がハイティング代数であれば、H ₂もハイティング代数です。これは、ハイティング代数が、特定の恒等式を満たす演算 → を持つ有界束 (半順序集合ではなく代数構造として考えられている) として特徴付けられることから導かれます。

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

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

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

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

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

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

実際、前述の構成は任意の変数集合{ A _i  : i ∈ I } (無限集合の場合もある) に対して実行できます。このようにして、変数 { A _i } 上の自由ハイティング代数が得られ、これを再びH ₀と表記します。自由とは、任意のハイティング代数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 ⟩ ) = ₁という性質を満たす要素の族 ⟨ a i _⟩に関してである。 （ H _Tとその要素の族 ⟨[ A _i ⟩ は、それ自体でこの性質を満たすことに注意してください。）射の存在と一意性は、 H ₀の場合と同じ方法で証明されますが、 「証明可能な恒等式」のメタ含意1 ⇒ 2を修正して、1 を「 T から証明可能な真」、2 を「 T の式を満たすHの任意の要素a ₁、a ₂、...、a _n」とする必要があります。

先ほど定義したヘイティング代数H _Tは、 H _Tに関するH ₀の普遍性、およびその要素の族 ⟨[ A _i ]⟩ を適用することにより、同じ変数の集合上の自由ヘイティング代数H ₀の商として見なすことができます。

すべてのヘイティング代数は、 H _Tの形のものと同型である。これを確認するには、Hを任意のヘイティング代数とし、⟨ a _i : i ∈ I ⟩をHを生成する要素の族(例えば、任意の全射族) とする。ここで、変数⟨ A _i : i ∈ I ⟩に関する式J (⟨ A _i ⟩)の集合Tを考え、 J (⟨ a _i ⟩)=1とする。すると、 H _Tの普遍性により射f : H _T → Hが得られ、これは明らかに全射である。fが単射であることを示すのは難しくない。

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