| 第二部 信仰と理性論 | 星加弘文 |
Chapter 2 信仰と理性の多対多関係 (26)
Hard study 5-5-4 ハイティング代数とクリプキ意味論
頁内目次
(1) クリプキ系Ⅰ／Ⅱ型証明表とハイティング代数の複数モデル
(2) 束とブール代数
(3) ハイティング代数
(4) ハイティング代数の定義
(5) ハイティング代数の候補束
(6) → をどう定義すればよいか
(7) 定義第1式 (ａ∧ｘ)≦ｂ の意味
(8) 定義第2式 ｘ≦ｃ の意味
(9) 3値ハイティング代数表
(10) 3値ハイティング代数グラフ
(11) ガロア接続
(12) ｃが存在する束、存在しない束とは
(13) ￢の複数定義
(14) クリプキ系証明表とハイティング代数モデル
(1) クリプキ系Ⅰ／Ⅱ型証明表とハイティング代数の複数モデル <↓>
Hard study 5-2-4 の冒頭に記した宿題は、そこで作成してきた1命題証明表を2命題証明表に拡大し、直観主義論理の定理、非定理を確認することであった。
また、その結果を通じて、野矢茂樹『論理学』に書かれている「直観主義論理の意味論を真理表で表わすことはできない」というのが、どういう事態を指すものかを理解したいということである。
この目標に向けて直観主義論理の意味論の一つであるハイティング代数に取り組む中、WEB上のある記事に「直観主義論理におけるすべての定理／非定理を表現できるモデルは存在しない」という一文を見つけた。
直観主義論理の定理／非定理をもれなく表現するためには複数のハイティング代数モデルを要するということらしい。
詳細は不明であるものの、これにより先の宿題の答えは予想がつくものになった。すべての定理／非定理を表現するような単独のハイティング代数がないということであれば、すべての定理／非定理を表現できる単独のクリプキ系証明表もないだろうということである。
そもそも私がこの課題を負うことになったのは『論理学』の以下の記述による。
Hard study 5-2-4 に紹介した「分子式の分析」を一通り終えたところで、直観主義論理の論理的真理に関して次の会話が置かれている。（p.177）
無門「すると、さらに何が言えれば論理的真理になるのかね。」
野矢「こんなモデルをいくら作っても、必ずそのすべての知識状態で（その論理式に⊩が）成立していることが示されればいいわけです。」
道元「つまり、すべての可能な認識史のあらゆる時代の知識状態で成立している、ということか。」
無門「そりゃまたずいぶんきつい条件じゃな。」
野矢「でも、真理表のすべての行で1になるというのと同じですよ。」
「こんなモデルをいくら作っても」とあるが、ここで「こんなモデル」というのは「分子式の分析」を行ってきたところの認識史K0（認識史01）を指すことが明らかで、その上で「すべての可能な認識史のあらゆる時代で論理式が成立していることが、真理表のすべての行で1になるのと同じ」と言われている。
するとこのところからは、認識史K0以外の認識史についても「分子式の分析」を継続していって、すべての認識史のすべての期を証明値で埋めれば、その「証明表」（この呼び名は『論理学』では使われていないが）は式の妥当／非妥当を示すものとなるはず、という理解に導かれる。それ以外には理解のしようがない。
「直観主義論理の意味論を真理表で表わすことはできない」と書かれていたのが、これに先立つわずか数頁前のことであって、したがって、「分子式の分析」によってできあがるであろう「証明表」という考えはその記述とつじつまが合わないと感じるのだが、「分子式の分析」の遂行によって「証明表」ができあがることはあまりにも明らかなことであるので、数頁前の「真理表（証明表）はできない」という記述を「鵜呑み」にすることの方がはるかに困難と感じられるのである。（ここで「鵜呑み」と言わなければならないのは、この記述に関係する説明が一切ないからである。）
そこで、Hard study 5-2-4で作成済みの1命題2期3行の￢の証明表に加えて、2命題4期9行からなるⅠ型基本証明表（∧、∨、⊃）を作成し、それを用いて12個の論理式を調べてみたわけだが、その結果2個について、Hard study 5-5-1に既述の通りⅠ型証明表はそれを正しく表示しないことが判明した。
上の『論理学』の会話から予想されるところからは、この状況は理解しがたいものである。Ⅰ型証明表はすべての認識史のすべての期の証明値、すなわち「道元」の言う「可能な認識史のあらゆる時代の知識状態」を明らかにしたものだからである。しかしとりあえず、そのうまくいっていない2個の解決のために、Ⅰα型証明表とⅡ型証明表を作成することにした。
このとき私は『論理学』から得た見通しに立ち続けたままなので、当然ながら、Ⅰα型証明表とⅡ型証明表を作成する根拠のようなものは見えていない。本来は、Ⅰ型証明表によって直観主義論理のすべての定理／非定理をきちんと表示できるはずだが、それができないということはこの証明表に何かしらの欠陥があり、それを解決する別の証明表を作成することで、その欠陥が見えてくるかもしれないといった見通しを持つだけだったのである。
全く新たに考案したⅡ型証明表については、当初、それがド・モルガン律(2)aを正しく表示することから、すべての論理式に使えるという期待を抱いたが、「プレ線型性」を正しく表示しないことが明らかになった時点で公表に価しないと判断した。このためさらに「プレ線型性」のためにⅠα型証明表を考案しなければならなかったのだが、Ⅱ型証明表についてはやはりド・モルガン律のためのアドホックなものにすぎないと判断したのである。（もっともⅠα型証明表はⅠ型証明表と同等であり、Ⅱ型証明表はⅠ型証明表の上位互換なので、「プレ線型性」を読みとるためのⅡα型証明表を作ることは容易なのだが。）
この結果を受けて、私は自らに課した宿題について「どうまとめたものか」という望まない思案に陥ることになった。
「直観主義論理におけるすべての定理／非定理を表現できるモデルは存在しない」という先の一文を目にしたのはその折りである。そこで私の「目の梁」は取り除かれた。そういうことであれば俄然状況は変わる。Ⅰ型証明表が12個の論理式全部を正しく表示しないのは当然のこととなり、Ⅱ型証明表はⅠ型を補完する証明表として機能している可能性が考えられてくるのである。
つまり「道元」の言う「可能な認識史のあらゆる時代の知識状態」とは、「一つの証明表の中の知識状態」の話なのではなく、別種の「証明表」や、あるいは「証明表」のような二次元マトリクスで表現できるものとも限らない、とにかく可能である限りのすべての知識状態を言うものであったというのが真相だったということである。（もっとも『論理学』の中ではとてもそのようには――つまり「真理表で表すことはできない」というのが「一つの真理表では表せない」という意味だとは――読めないのだが。）
そこでⅡ型証明表は複数のハイティング代数モデルが果たす役割と同じ役割を果たすものである、とまではおそらく言えないにしても、この証明表で何がなされようとしたかについての全体的な視点に立った見方が可能になった。
見るところでは、Ⅰ型証明表の行数と証明値は、{0, ½, 1} の3値からなる最も簡素な（とはいえ難しいが）ハイティング代数の真理表と全く同じであり、また、{0, ⅓, ⅓', ⅔, 1} の5値からなるハイティング代数はいくつかの点でⅡ型証明表と似ている。
というのは、5値ハイティング代数モデルは私のⅡ型証明表と同じく、ド・モルガン律(2)aの非定理性を示すために使われているからである。ド・モルガン律(2)aは3値ハイティング代数では非定理性を示せないのである。その上、この5値ハイティング代数は、後述のとおり、なんとⅡ型証明表と同様の3種類の偽を定義していると見えるのである。
このHard study 最終節では、これまで見てきたクリプキ意味論とは異なるアプローチを持つハイティング代数によって、直観主義論理意味論を改めて学んでみたい。
ハイティング代数はクリプキ意味論と並ぶ、直観主義論理のもう一つの意味論である。
古典論理の意味論は、論理記号（￢、∧、∨、⊃）で結ばれる分子命題の真偽を、原子命題の真偽のあり方に応じて0か1を与える真理表によって表現されていた（Easy study 5-2-1冒頭）。この古典論理の真理値の集合{0,1}は「ブール代数」と呼ばれる。
直観主義論理の真理値の集合は「ハイティング代数」と呼ばれ、ブール代数が古典論理の意味論すなわち真理表を形成するのと同様に、ハイティング代数は直観主義論理の意味論となる。
このハイティング代数が、これまでに見てきた論理式を含め、非定理のド・モルガン律とプレ線型性式をどのように表現するのか、その非定理性を示すことができるのかを確認したい。
ハイティング代数を学ぶにあたり、まず、より理解しやすいブール代数から見ていくことにする。
さて、代数というのは数字を文字で置き換えて演算規則などを考える「代数学」で使われる文字や数字のことで、ブール代数としては{0,1}の他にも、有限集合のべき集合などがある。
べき集合とは集合の部分集合全部を集めた集合のことで、例えば、集合{a,b}のべき集合は{{ab},{a},{b},{φ}}（φファイ＝空集合）であるが、これも後に述べるブール代数の要件を満たす集合となっている。（以下、べき集合の要素では集合記号 { } を省略する。）
代数は演算が可能であり、ブール代数{0,1}の演算が、古典論理の真理表に対応するものであることが下の真理表から確認できる。
真理表の0、1について、先の箇所（Easy study 5-2-1）では真理表の中では未定義であると述べた。真理値0、1は、哲学的な「真理の対応説（Easy study 1）」による意味付けを持つものとして理解されるからである。
例えば、二つの命題Ｘ、Ｙがあるとき、「『ＸかつＹ』は真」という言い方ができるのは、ＸとＹが共に真であるときだけで、事態がそれ以外の場合には「『ＸかつＹ』は偽」とする。これが上の真理表のｘ∧ｙ列の1行目から4行目の真理値1000に表現されていることである。
代数演算では分子命題の真理値を、原子命題Ｘ、Ｙの真理値を用いた計算によって求める。Easy Study 2-2で見た真理値分析では、基本の真理表を使いながら、分子命題の真理値を一つ一つ手計算していたが、ブール代数演算を使えばこれを機械化できるということである。
ただしこの演算式はいくらか難しいので、特に∨や⊃の計算がどうしてこの式になるのかを理解するには若干の労力を要する。その労力はわずかだが、ここで理解したい内容からは離れるので解説が載っている書籍の紹介にとどめる。
このブール代数演算は、論理記号が持つ「真理の対応説」的意味を工夫して計算式にしたものであって、真理値の定義という観点からは「真理の対応説」以上の意味を持つものではない。言いかえれば、論理計算の機械化に役立つこの演算は、少なくとも真理表を扱ってきた者に対しては真理値0、1に関する理解を深めるものではない。
一方、以下に見ようとするブール代数とハイティング代数についての定義は「真理の対応説」とは別の観点から行われていて、真理値0、1について新たな理解をもたらす。
ブール代数、ハイティング代数は「代数」と呼ばれることから、数字や英文字による演算の値としてのイメージがあるが、実は集合のことである。これらの「代数」は、集合のある特質として定義される。
これらの代数は「順序集合」という集合を出発点として定義される。（なお「順序集合」には「半順序集合」「部分順序集合」という別の呼び名もある。）
順序集合というのは、数字や文字列や集合を要素とする集合において、要素間に大小や含有、前後などの関係による序列がつけられた集合のことである。
例えば、集合{0,1}は≦（大小）によって順序付けられ、集合{a, b}のべき集合{ab, a, b, φ}は⊆（含有）によって順序付けられた順序集合である。
順序集合のうち、集合内の任意の2つの元が共通の「上界」を持ち、その共通の上界に「最小元」があるとき、これを2つの元の「上限」とする、という決まりがある。
数学用語が続出したがここは難しくない。「上界」というのはその元を含むそれよりも大きな元全部のことで、例えば、順序集合{0,1,2,3}において、1の上界は{1,2,3}、2の上界は{2,3}である。そこで、1と2の共通上界は{2,3}であり、この中の「最小元」2が、1と2の「上限」ということになる。
同様に、集合内の任意の2元が共通の「下界」を持ち、その共通下界に「最大元」があるとき、これをその2つの元の「下限」という。
順序集合{0,1,2,3}において、0の下界は0を含めたそれ以下の元のことなので{0}、2の下界は{0,1,2}である。そこで、0と2の共通下界は{0}であり、その「最大元」0が0と2の「下限」ということになる。
任意の2元に関してこの「上限」と「下限」が存在する順序集合を「束（そく）」という。つまり順序集合{0,1,2,3}は束であり、この束にさらにある規則が加わったものがブール代数となる、という流れである。
理解をなじませるために、束と束ではない順序集合について見ておくと、まず、集合{a, b}のべき集合{ab, a, b, φ}は束である。
この場合、4個の要素は{ab}を頂点とする◇型のような、途中で枝分かれする形に配置され、横に張り出したところに{a},{b}が位置し、下端に{φ}がくる。
したがって {a}, {b} 間には順序関係はつかないが、それらの共通上界は{ab}であり、また{ab}自身が共通上界の最小元なので{a}, {b}の上限は{ab}として存在する。また、共通下界は{φ}で、それ自身共通下界の最大元でありこれが下限である。このようにして、{a} と {b} 以外の組においても上限と下限が定まるので、これが束であることが確認できる。
束ではない順序集合というのは、例えば、4個の元からなる集合{a, b, c, d}が、Ｙの字に配置される場合（a, b がＹの2本の枝それぞれの上端、c がＹの中心、d がＹの下端）、上端のa, b には共通の上界が存在しないので（aの上界はa、bの上界はb）上限が定まらず、これは順序集合ではあるが束ではない。（下限についてはどの2元を取ってもcまたはdに定まるので、このような場合の順序集合は「下半束」と呼ばれる。）
なるほど形から見ても◇は束（たば）だがＹは束（たば）ではないといえる。
順序集合{0,1,2,3}のようにＩ型に1列に配置される順序集合は、◇型の{a}, {b}のように順序関係を持たない元の組がないため「全順序集合」と呼ばれる。そしてこの場合、「上限」「下限」は、上に述べた「共通上界の最小元」「共通下界の最大元」という面倒な言い方をしなくてもすむようになる。
Ｉ型順序集合における「上限」は、2元のうちの「大きい方」と言えばよい。下限も同様、2元のうちの「小さい方」ということで誤りなく指定できる。このため、古典論理の真理値の集合{0,1}が考えられているときは、これは全順序集合であるから、上限は2元のうちの大きい方、下限は小さい方という理解で賄うことができる。
このように順序集合に対して「上限」と「下限」という概念を加え、これを満たす順序集合、言いかえれば「上限」と「下限」が存在する順序集合が「束」である。
そしてこのとき、上限を求める操作、下限を求める操作は、それぞれ2元に対する計算であるということができ、上限を求める計算を∨演算、下限を求める演算を∧演算とみなすことができる。この点を真理表から確認してみる。
これまでの理解では、∧と∨の真理値は「真理の対応説」に基づくあり方として得られる真理値であった。∧言明はｘとｙが共に真であるとき真とするのが適切であり、∨言明はｘとｙのいずれかが真であるとき真とするのが適切であるという見通しから、∧と∨の真理値が定められていたのである。
厳密にはEasy Study 2-2で述べた通り、「論理記号の意味に合うように1と0を配置しているのではなく、1、0をそう配置することによって論理記号の意味を定めている」のであり、この点は⊃（条件法）と≡（同値）の区別や、∨（非排他的選言）と▽（排他的選言）の区別においては特に重視されなければならないことであった。
そもそも論理学とはただ「真理の整合説」にのみ依拠する体系であり、「現実との対応」つまり「意味内容」から独立したものだが、少なくとも古典論理においては、そこで使われる論理記号は日常言語を表現するものであることが求められてきたといえる。
しかしここではこういった「意味による理解」を一切考えない。単純に、ｘ、ｙの真理値と、∧、∨の真理値を比較してみると次のことに気がつく。
すなわち、∧の真理値というのはｘとｙの真理値のうち小さい方を採用したものであり、∨の真理値はｘとｙの真理値のうち大きい方を採用したものだということである。
つまり∧というのは2元の下限を求める演算であり、∨は上限を求める演算であったということである。
上限、下限の考えでいくと、1と1の下限は1で、上限も1である。これが上の真理表の1行目のｘ∧ｙ列と、ｘ∨ｙ列の値となっている。
同様に1と0の下限は0、上限は1で、これが2行目の∧列と∨列の値であり、3行目も同様である。4行目は、0と0の下限は0、上限は0、これが∧列と∨列の値である。
なお、順序集合{0,1}において1と1、0と0のように、同じ元を2つ考えることについて疑問が起こるかもしれないが、この点は順序集合の定義に、「反射律」（ｘ≦ｘ）、「非対象律」（ｘ≦ｙ、ｙ≦ｘならばｘ＝ｙ）という規則が含まれていることから説明される。反射律は、0や1についてもう一つ同じ元を考えてよいことを示すものといえる。これに「推移律」（ｘ≦ｙ、ｙ≦ｚならばｘ≦ｚ）を加えたものが、集合が順序集合であるための条件となっている。
そこで繰り返しの確認となるが、「順序集合」に∧演算と∨演算が加わったもの、すなわち任意の2元ついて「上限」と「下限」が存在しているのが「束」である。
ブール代数はこの「束」に「補元」という元が加わったものである。プール代数一般を考えるときには「補元」の他に、その束において分配律が成り立つ「分配束」という性質が必要になるが、ここではブール代数として束{0,1}だけを考えるので「分配束」については省略し、この束{0,1}が「補元」を持つものであるかを確認したい。
なお、束{0,1}が分配法則を満たす束であることは、0と1をあてがった8通りのｘ,ｙ,ｚの組み合わせの全てにおいて、ｘ∧(ｙ∨ｚ)＝(ｘ∧ｙ)∨(ｘ∧ｚ)が成り立つことを見ることで確認できる。（ここでは省略する。）
さて、「補元」とは、束{0,1}の任意の元ｘについて、次の性質を同時に満たす元ｙのことで、意味としてはｘの「否定」に相当する。
ｘ∧ｙ＝0
ｘ∨ｙ＝1
束{0,1}で考えると、ｘを0とすると、
0∧ｙ＝0
0∨ｙ＝1
となるようなｙのことである。ここでｙに1を与えると
0∧1＝0（0と1の小さい方は0）
0∨1＝1（0と1の大きい方は1）
であるから、1が0の補元であることが分かる。
そしてこの1は、言うまでもなく束{0,1}の元として存在するものである。
同様にｘを束{0,1}の1とした場合は、
1∧ｙ＝0
1∨ｙ＝1
となるｙは0である。すなわち、
1∧0＝0（1と0の小さい方は0）
1∨0＝1（1と0の大きい方は1）
であるから、0が1の補元となっている。
そして、この補元0は束{0,1}の元として存在している。
つまり束{0,1}においては、2元の双方が、互いの補元となっているということである。
そこで、このような性質を持つｘの補元ｙを￢ｘと書く。すると、
ｘ∧￢ｘ＝0 (矛盾律)「ｘかつ￢ｘである」ことはない
ｘ∨￢ｘ＝1 (排中律)「ｘまたは￢ｘ」という言明は常に真
という見慣れた論理式となる。
論理記号∧、∨が2項目演算であるのに対し、￢は1項目演算でありｘの値が決まることで￢ｘの値が定まることになる。先の「分配束」という条件は、このときｘの補元が一意に定まること、すなわち補元を￢という写像として表現できるための条件である。これについての証明は［注］資料参照。
以上をまとめると、束とは上限と下限が存在する順序集合のことで、ブール代数とはｘに対する￢ｘが定義できる束のことである、ということである。
なお、先にブール代数の要件を満たすと書いた、集合{a,b}のべき集合{ab, a, b, φ}について、その補元を確認しておくと次のようである。
集合を元とするブール代数の補元￢ｘは、ｘの差集合として定義される。したがってｘが{a}のとき、￢ｘは{ab, b, φ}である。
これが補元の性質を満たすことは次のように確かめられる。
順序関係が⊆である集合、つまり元が集合である集合の場合は、∧演算は集合の∩（共通集合）を求める演算であり、∨演算は集合の∪（和集合）を求める演算である。
ｘ∧￢ｘ：＝ｘ∩￢ｘ＝{a}∩{ab, b, φ}＝φ（空集合なので0相当）
ｘ∨￢ｘ：＝ｘ∪￢ｘ＝{a}∪{ab, b, φ}＝{ab, a, b, φ}（全体集合なので1相当）
（：＝は「定義」の意味）
ハイティング代数はブール代数よりも規則が緩い束である。古典論理の二重否定除去則を、より緩い否定除去に置き換えた直観主義論理（Hard study 5-3-2 注[5]）が難しいのと同じく、規則の緩いハイティング代数はブール代数よりも理解が難しい。
見てきたように、古典論理におけるブール代数は、順序集合に∧と∨を定義して束となったものに、補元による￢演算を加えたもので、古典論理の⊃は、この∧と￢を使って定義される。そしてこれが先に見たブール代数⊃演算の1－x＋x・yという式にもなっている。
また、補元￢ｘの存在によりブール代数は「ｘ∨￢ｘは常に真」という排中律が成立する代数になっている。 そこで、ハイティング代数がどういうものかを考える際には、ここまで直観主義論理が排中律を定理として持たないことを見てきたので、補元を定義できない束としてそれを考えることが我々にとっての近道となる。
このとき補元すなわち￢が定義できないということは、∧と￢を使った →（⊃のハイティング代数版）の定義ができないことを意味する。そのためハイティング代数では → の定義を独自に行うことになる。
補元による￢の定義に代えて、先に → を定義し、その後、この → を使って￢を定義しようというのがハイティング代数である。
したがって、独自に定義される直観主義論理の → は古典論理の⊃とは働きが違っており、その結果、この → を使って定義される直観主義論理の￢も古典論理の￢とは働きが違うものになる。
なお、→ 記号は、これまでの説明に用いていた⊃記号と同じ条件法の結合子だが、束論では → が多く使われているようなので、以下、ハイティング代数では → を使うこととする。以下に限り、⊃は古典論理の条件法、→ は直観主義論理の条件法を示すものと理解されたい。（これまでの記述では直観主義論理でも⊃記号を使ってきた。）
代数学の書籍やWEB文献に紹介されているハイティング代数の代表的な定義は以下である。
定義式①
束の任意の元 a, b, c, x があるとき、これらが
(ａ∧ｘ)≦ｂ ←→ ｘ≦ｃ （←→は双条件）
であるような元ｃが存在する束をハイティング代数と呼び、このｃをａ→ｂとする。
Easy study 5-2-1で見たクリプキ意味論は、初め何を言っているのか見当がつかないものだったがハイティング代数も同様である。上の定義に大まかな概念図が添えられていることがあるが、それが助けになるという人はまずいないだろう。
後ほど見る「ガロア接続」という写像概念を理解することで、その往復写像の図から上の定義をいくらかイメージできるようになる。しかしそこから明瞭な理解に至るためには「随伴」などの深遠な概念を知る必要があり、かなり遠回りしなければならない。
そこでここでは、理解しやすいと私が考える順序で、また言わずもがなであるが、私が理解している範囲でハイティング代数を説明していくことにする。
上の定義はひとまず置いておき、ハイティング代数が、排中律が成立しない直観主義論理の意味論を形成する代数であり補元のない束である、ということを出発点としよう。
正確に言えば、補元を持つブール代数はハイティング代数の特殊な場合であり、ハイティング代数の一種であるので、ハイティング代数に補元がある場合もあるというべきだが、ここではハイティング代数からブール代数を除いて考えることで、ハイティング代数独自の形式を捉えたい。
そこでとりあえず補元がない束というものを考えてみる。
束{0,1}に元½を加えた3値からなる全順序集合の束{0, ½, 1}はどうか。
0と1に関しては互いが補元となることを見てきたので、新たに加えた元½に補元となる元があるかを確認してみる。
補元は束の中に見い出されなければならないものなので、補元候補は0、½、1の3つである。
繰り返しになるが、補元とは、
ｘ∧ｙ＝0
ｘ∨ｙ＝1
を同時に満たすｙのことである。
そこでｘを½とした上で、ｙに3つの候補値を代入して確かめてみる。
ｙ＝0 としたとき、
ｘ∧ｙ＝½∧0＝0
ｘ∨ｙ＝½∨0＝½
ｙ＝½ としたとき、
ｘ∧ｙ＝½∧½＝½
ｘ∨ｙ＝½∨½＝½
ｙ＝1 としたとき、
ｘ∧ｙ＝½∧1＝½
ｘ∨ｙ＝½∨1＝1
である。
したがってｙがいずれであっても、上の補元の定義式は満たされない。
つまり束{0, ½, 1}は、任意の元において補元が存在するのではない束であり、ハイティング代数となる資格があるといえる。
次に、このハイティング代数の候補束{0, ½, 1}、つまり補元のない束に、補元（￢）に頼らずに → を定義することを考える。
ブール代数の箇所で見た通り、束においてはすでに∧と∨が定義されている。これに → を定義することでハイティング代数になるのである。
このとき参考にするのは当然のことながらブール代数の⊃である。というのは、→ をできるだけ⊃のように定義できれば、それは「うまく定義した」こととなって、この新たな代数においても、→ を古典論理の条件法に準じた扱いができるようになるからである。
Easy Study 2-1 の「Ａ⊃Ｂの真理表」を再掲して、古典論理の⊃の働きを確認してみる。
古典論理ではａ⊃ｂの真理値を、その対応説的意味から考えて、前件が真であるのに後件が偽であるときに偽、それ以外は真であるとした（Easy Study 2-1）。
しかしここでは、ａ⊃ｂの定義をａとｂの大小関係に注目して捉えてみる。それは、順序集合から束に至る過程での∧と∨の導入が、やはり2つの元の大小関係の演算として定義されたことに習うということである。
そこで⊃について同じようにやってみる。するとａ⊃ｂの真理表からは、次の規則を見いだすことができる。
ａ≦ｂのとき、ａ⊃ｂ＝１（1、3、4行目）
ａ＞ｂのとき、ａ⊃ｂ＝ｂ（2行目）
ａ＞ｂの場合はａ⊃ｂ＝０として捉えることもできるが、ａ＞ｂである行は1行しかないので規則の汎用性を考えて、特定の真理値ではなくｂの値としておきたい。
この規則に従って、束{0, ½, 1}でのａ→ｂの真理表を作ってみる。3値2命題真理表なので、3^2＝9行の真理表となる。
とりあえずａ→ｂの真理値が出た。
このａ→ｂの真理値が → に求められている働きをきちんと果たしているかを知るにはどうすればよいだろうか。 古典論理の⊃の働きを如実に表現するものとして前件肯定式がある。（Easy Study 2-2 より）
すなわち ａ∧(ａ⊃ｂ)⊃ｂ である。
この前件肯定式（MP＝Modus Ponens）は、古典論理における規則、定理であるにとどまらず、論理体系の無矛盾性や健全性などを、その論理体系の外からメタ論理として検証する際にも使用される最も基礎的な論理式である。
上に作成した「直観主義論理ａ→ｂの真理表」において、このMPが成立していれば、ａ、ｂの大小関係から導いた「ａ→ｂ」における「→」は「うまく定義されている」ということになるだろう。
そこで「ａ→ｂの真理表」から前件肯定式の左辺ａ∧(ａ→ｂ)を計算して、それをｂの値と比較してみる。（∧演算の値は両辺の小さい方）
ここで、全行で前件肯定式ａ∧(ａ→ｂ) → ｂが成立しているのは当然である。前件肯定式はａ∧(ａ→ｂ)の値が、ｂと等しいか小さいことで成立するが、上表はこの性質をａ⊃ｂの真理表からくみ取ってできあがったものだからである。
確認すると、ａ≦ｂ（1、4、5、7、8、9行目）の場合、ａ→ｂの値は最大値である1としたが、ａはｂより小さいので、たとえａ→ｂがどんな値であったとしてもａ∧(ａ→ｂ)はｂより小さいことになる。したがって前件肯定式が成り立つ。
ａ＞ｂの場合（2、3、6行目）、ａはｂより大きいが、ａ→ｂをｂの値としているので、ａがどんな値であったとしてもａ∧(ａ→ｂ)はｂの値を超えることはない。したがって前件肯定式が成り立つ。
このように上表全行でMPが成立することは当然のことにすぎないので、これをもってａ→ｂを古典論理のａ⊃ｂと同じように設定できたと見なすことは早計である。MPの性質をさらに詳しく見てみなければならない。
そこで先の「前件肯定式Ａ∧(Ａ⊃Ｂ)⊃Ｂの真理表」を見直して、ａ∧(ａ⊃ｂ)とｂの真理値関係から、MPで何が実現されているかを、もう一度捉え直してみる。特にａの真偽に注目するのは、ａはここで条件法の前件であり連言の単独要素でもあることから、いずれも式全体の真理値を決定づける役割をしているためである。
1行目 ａ＝1で、ａ∧(ａ⊃ｂ)＝1、ｂ＝1のとき、ａ⊃ｂは1である。
このとき、ａ∧(ａ⊃ｂ)＝ｂが成立している。
2行目 ａ＝1で、ａ∧(ａ⊃ｂ)＝0、ｂ＝0のとき、ａ⊃ｂは0である。
このとき、ａ∧(ａ⊃ｂ)＝ｂが成立している。
3行目、4行目 ａ＝0のときは、ａ∧(ａ⊃ｂ)とｂの真理値は一致したりしなかったりする。つまりａ＝0のときはａ∧(ａ⊃ｂ)＝ｂは成立しなくてよい。
前件肯定式の真理表ではａ∧(ａ⊃ｂ)⊃ｂだけではなく、ａが真の場合にａ∧(ａ⊃ｂ)＝ｂが成立している点が注目される。このことから、直観主義論理において実現されるべきａ→ｂを考えると、
1行目の考察から
① ａ∧(ａ→ｂ)＝1で、ｂ＝1のとき、ａ→ｂは1であってほしい。
そしてこのときａ∧(ａ⊃ｂ)とｂは同値であるべきである。
2行目の考察から
② ａ∧(ａ→ｂ)＝0で、ｂ＝0のとき、ａ→ｂは0であってほしい。
そしてこのときａ∧(ａ⊃ｂ)とｂは同値であるべきである。
3、4行目の考察から
③ ａ＝0のときは、ａ∧(ａ⊃ｂ)とｂの値は一致していなくてよい
ということになる。
ａ→ｂに関する上の要請が、先のａ∧(ａ→ｂ)の真理表で実現されているのかを確認してみる。ａ∧(ａ→ｂ)の真理表を再掲する。
①については、1行目がこれを満たしているので、①の印をつける。
②については、3行目と6行目がこれを満たしているので②の印をつける。
③については、7行目、8行目、9行目が該当しているので③の印をつける。
印がつかなかった残り3行についてはどうか。
2行目はａ∧(ａ→ｂ)＝½ 、ｂ＝½ で、ａ→ｂは½である。
5行目はａ∧(ａ→ｂ)＝½ 、ｂ＝½ で、ａ→ｂは1である。
いずれも①の前半の要件は満たしていないが、しかしａ∧(ａ⊃ｂ)＝ｂという前件肯定式において必須である後半の要件は満たしている。
したがって2行目と5行目において、ａ→ｂは前件肯定式に用いられてよい種類の式であるといえる。これらには①'の印をつけておこう。
4行目はａ∧(ａ→ｂ)＝½ 、ｂ＝1で、ａ→ｂは1である。これは①の前半を完全には満たさず、また、肝心のａ∧(ａ→ｂ)＝ｂが実現されていない。したがってこの4行目によって、ここに見てきた → は前件肯定式の重要な性質を完全には満たしていないということになる。
しかしここで、前件肯定式の近似式ａ∧(ａ→ｂ)＜ｂを考えれば、これについては満たしているといえる。このため4行目には①<という印をつけることにしよう。
こうして見てくると、束{0, ½, 1}の全体では、ａが0以外のときに前件肯定式における
ａ∧(ａ→ｂ)＝ｂ
ではなく、それふうの
ａ∧(ａ→ｂ)≦ｂ
が成立しているという結論となる。
残念な結果にも思えるが、しかしここまでくると、先にあげたハイティング代数の定義の意味が少し見えてくる。それは先の定義式は、この前件肯定式の近似を表現するものであったということである。再掲すると、
定義式①
束の任意の元 a, b, c, x について
(ａ∧ｘ)≦ｂ ←→ ｘ≦ｃ
であるような元ｃが存在する束をハイティング代数と呼び、このｃをａ→ｂとする。
（以下、←→ の左側の式を定義第1式、右側を定義第2式と呼ぶ）
ここで、第1式左辺のｘをａ→ｂに置き換えると、これは上で、束{0, ½ ,1}で成立を確認したａ∧(ａ→ｂ)≦ｂそのものである。つまり定義式のｘというのはａ→ｂの代用と解することができる。
このことから定義第1式左辺の前件肯定式風の式は、古典論理の前件肯定式の妥協版といえるが、しかしこれがハイティング代数の定義として述べられているとすれば、このａ∧(ａ→ｂ)≦ｂをもって直観主義論理の前件肯定式の内容とするということにほかならない。
そしてこのときに前件肯定式の近似として働いている → を古典論理の条件法⊃に代わる直観主義論理の条件法とするということである。
定義第2式についても同様にして調べてみよう。第2式 ｘ≦ｃ については次のように理解できる。
任意の整数ｐ,ｑに、常にｐ≦ｑの関係を成り立たせたい場合は、ｑをｐが取り得る値の最大の値にしておけばよい。
定義式第2式はこれを意味しており、上と同様にｘをａ→ｂに置き換えると、
(ａ→ｂ)≦ｃ
となるが、このｃはａ→ｂが取り得る値の最大を意味している。しかしａ→ｂの最大値をとるとはどういう意味なのか。
ここまで定義式のｘにａ→ｂを代入してきたが、実は、そのａ→ｂというのは、ここで最終的に定義されようとしている直観主義論理におけるａ→ｂそのものではない。そうではなくその「候補としてのａ→ｂ」である。
ハイティング代数定義の終わりに「このｃをａ→ｂとする」とある。つまり、真の「ａ→ｂ」はｘではなくｃである。
ｘ≦ｃを満たすようなｘすなわち「ａ→ｂの候補」は複数あり得るが、それら候補の中の最大のものをｃすなわち正規の「ａ→ｂ」とするというのが
ｘ≦ｃ
の意味である。
ここで最大値を採用するのは、ａ∧(ａ→ｂ)≦ｂをできるだけａ∧(ａ→ｂ)＝ｂに近づくものにしたいためである。
ここまでの状況をハイティング代数の表で確認してみよう。確認したいのはａ→ｂの候補としてのｘと、その最大値ｃの状況。また、ａが0以外のときにａ∧(ａ→ｂ)＝ｂあるいはａ∧(ａ→ｂ)≦ｂが成立している状況である。
ハイティング代数を{0, 0.5, 1}とすると、ａとｂが取る値はそれぞれ3個なので、そのすべての組み合わせを作ると9行の表となる。
→ 演算を「閉じている」、つまり、→ の演算結果が束 {0, 0.5, 1} 内にとどまるとすると、ａ→ｂすなわちｃの値は 0, 0.5, 1 のいずれかであり、ａ→ｂの候補としてのｘもこのいずれかである。
ただしここではｘに制約を設けず、ｘの値は0～1の間で無限にとることができると考える。ｘの数がある程度多い方がｘの最大としてのｃということがイメージしやすいからである。ここではａ→ｂの候補値を0から0.1刻みの1まで ｘ0～ｘ10 の11個のｘを設定し、ｘ0＝0、ｘ1＝0.1 ... ｘ9＝0.9、ｘ10＝1 のようにする。
例えば、
（1行目）ａ＝0、ｂ＝0のとき、ａ→ｂの値は 0, 0.1 .... 0.9, 1 のいずれかである
（2行目）ａ＝0、ｂ＝0.5のとき、ａ→ｂの値はやはり 0, 0.1 .... 0.9, 1 のいずれかである
:
ということである。
このようにして、ａ→ｂの候補値ｘすべてを書き出したのが下の表である。
さて、この中でどのｘがａ∧(ａ→ｂ)≦ｂというハイティング代数定義式の制約を満たすか、すなわちａ→ｂの候補となれるｘなのかを見てみる。
表(1)と表(2)の表内数値の関係を確認しておくと、表(1)は単に0から1の値を0.1刻みにｘに割り振ったものである。表(2)は表(1)のそれぞれのｘにおけるａとの下限（ａ∧ｘ）を示したものである。
そこで、どのｘがａ∧(ａ→ｂ)≦ｂを満たすかを見るために、まず表(2)でａ∧ｘとｂの大小関係を確認する。
ａ∧ｘの値（ａとｘ0～ｘ10 の小さい方）とｂを比較していくと、黄色のセルで(ａ∧ｘ)＞ｂとなり式が破られている。例えば、a＝1、b＝0.5の行では、ａ∧ｘが0.6になるところで、(ａ∧ｘ)＝(1∧0.6)＝0.6＞0.5＝ｂとなって(ａ∧ｘ)≦ｂが成立しなくなる。
この黄色の状況をそのまま表(1)に移すと、黄色のセルのｘが(ａ∧ｘ)≦ｂを破るｘであることになる。例えば、a＝0.5、b＝0の場合ではｘ1～ｘ10 にはａ→ｂの資格がないということである。
表(1)で黄色以外のセルが(ａ∧ｘ)≦ｂが成立しているｘであり、その最大を濃い緑色にしている。この濃い緑色の値がａ、ｂの状況に応じて定まるｃ、つまりａ→ｂの値である。
すなわち、ａ＝0のときは、すべて ｃ＝1
ａ＝0.5 ｂ＝0のとき、 ｃ＝0
ａ＝0.5 ｂ＝0.5のとき、ｃ＝1
ａ＝0.5 ｂ＝1のとき、 ｃ＝1
ａ＝1 ｂ＝0のとき、 ｃ＝0
ａ＝1 ｂ＝0.5のとき、ｃ＝0.5
ａ＝1 ｂ＝1のとき、 ｃ＝1
である。
ａとｂがこれら一連の値をとるときに上のｃの値となる演算を、→ 演算として定義したのが直観主義論理であるということになる。
前件ａ＝0のときはａ⊃ｂ＝1とし、前件ａ＝1で後件ｂ＝0のときａ⊃ｂ＝0とする古典論理の⊃の働きが保たれているのが分かる。ただし古典論理ではａが真の場合、すなわちａが0以外の場合にａ∧(ａ⊃ｂ)＝ｂが成立していたが、この点を表(2)で見てみると、ａ＝0.5、ｂ＝1の行には濃い青色のセルがない。つまり、このときａ∧ｘの最大は0.5止まりでありｂの値1に届いていない。（ａ＝0、ｂ＝0.5の行と、ａ＝0、ｂ＝1の行も濃い青色のセルがないが、これらはａが0なのでａ∧(ａ→ｂ)とｂの値は一致していなくてよい。）
3値ハイティング代数表はこのように、直観主義論理においてａが0以外の場合であってもａ∧(ａ→ｂ)＝ｂではなく、ａ∧(ａ→ｂ)≦ｂが成立するのみであることを示している。古典論理でａが0以外というのはａが真であることを意味するが、直観主義論理ではａが0.5の場合もあり、そのときたまたまｂが0.5であれば＝が成り立つが、ｂが1の場合にはそうならないということである。
また表(2)からは、先に「（ｘの）最大値を採用するのは、ａ∧(ａ→ｂ)≦ｂをできるだけａ∧(ａ→ｂ)＝ｂに近づくものにしたいため」と説明した状況も見てとれる。例えば、ａ＝0.5、ｂ＝0.5の行ではすべてのｘにａ→ｂの資格があるが、その中の最大であるｘ10 がｃに採用されていることでａ∧ｘの値がｂと等しくなっている。
前段のハイティング代数表では、ハイティング代数の定義が実際にどのように実現されているかを見たが、これをグラフに表すとｃの定義の成り立ちが分かり、定義式の意味をイメージできるようになる。次段に見る「ガロア接続」の予習にもなる。
以下、図1～図6で、縦軸ｘはａ→ｂの候補を示し、縦軸ａ∧ｘはａとｘの下限を示している。
3値ハイティング代数表と同様、ｘが取り得る値の範囲をｘ0～ｘ10 の11個としている。
→ の定義にMP（前件肯定式）を利用する。ａ∧(ａ→ｂ)＝ｂにおけるａ→ｂはこれから定義されようとしているものなので、これをｘとし、ａ∧ｘ＝ｂとなるｘをａ→ｂとして定めたい。しかし、ａ∧ｘ＝ｂとなるようなｘを定めることは望めないかもしれないので、その近似式ａ∧ｘ≦ｂを満たすｘをａ→ｂとすることにする。
ただしそのようなｘは複数あり得るのでａ∧ｘのｘはａ→ｂの候補であるにすぎない。ここでは0から0.1刻みで1までｘ0～ｘ10 の11個を考える。
定義の第一段階
ｘをａ∧ｘにする関数（写像）ｆを考える。（ｘ0 からの写像をｆ0 とし、以下同様。）
図1のａ＝0.5 ｂ＝1の場合、ａ∧ｘ0～ａ∧ｘ10 までのすべてがｂ以下の値となることがグラフで確認できる。
定義の第二段階
MPを満たす資格があるａ∧ｘの範囲が分かったところで、これら資格があるａ∧ｘについて、ａ∧ｘをｘに戻す逆写像ｆ-1 を考える。（図2）
この逆写像によって得られたｘは、MPを満たすａ∧ｘから作られたものなので、いずれもMPを満たすｘである。
ａ∧ｘにおいては、ａが何であれ、MPの資格を有するｘの最大のものがａ∧ｘをｂに近づかせるので、逆写像ｆ-1 から得られたｘの中の最大のものをａ→ｂとして定義する。このｘが定義式のｃに相当する。
写像ｆでａ∧ｘを得てそれをｂと比較することにより、MPの資格のあるａ∧ｘを限定しておいて（第一段階）、そこからの逆写像ｆ-1 でｘを復元することで、MPに最も近づくことができるｘを特定する（第二段階）。
図1、図2のａ＝0.5 ｂ＝1の場合は、すべてのａ∧ｘがｂ以下になるので、ｘを写像ｆでａ∧ｘとした後、そのａ∧ｘを逆写像ｆ-1で単に元に戻しているだけのように見えるが、ｘをａ∧ｘとする写像ｆによってMPの篩いにかけている。その篩いを通ったａ∧ｘだけを逆写像でｘに戻すということ。全部が篩いを通るのではない状況は、ａ＝1 ｂ＝0.5など、ａ＞ｂの設定で確認できる。（図5）
図1と図2の関係は「ガロア接続」と呼ばれる。通常、「ガロア接続」を説明する図では、図2のｆ-1 の過程を端折ったものになっているが、上図および後出する図ではｆ-1 の過程を表示している。
ａ＝0.5 ｂ＝1の場合は、「ガロア接続」の写像 g と、ａ∧ｘ10 からの逆写像ｆ-1 は一致しないが、これ以外のａ、ｂの値の場合はgとｆ-1 は一致することが確認できる。（この点は(6)での「直観主義論理ａ∧(ａ→ｂ)の真理表2」の4行目、また、3値ハイティング代数表(2)の6行目がMPでの＝を実現していないこととして確認していた。）
仮にａ、ｂの組み合わせすべてにおいて、gとｆ-1 が一致すれば図1と図2の関係は「同型写像」となるが、ａ＝0.5 ｂ＝1の場合は一致しないので、ハイティング代数は「ガロア接続」というより緩い関係にとどまる。
ここではgを、ｂをｃにする関数として理解しておく。（関数gの全体は次段で確認する。）
ｂは「理想のａ∧(ａ→ｂ)」であり（∵ａ∧(ａ→ｂ)＝ｂとなることが理想なので）、ｃは「正規のａ→ｂ」である。したがってgを言いかえれば「理想のａ∧(ａ→ｂ)」を「正規の(ａ→ｂ)」にする関数であり、gは「ａ∧」を取り去るｆ-1 と同種の関数といえる。
ガロア接続とは、対応する二つの集合間において、それぞれの順序関係が保たれるような写像（関数）でのやりとりが成立する状態をいう。
ある集合Ａ {a, b, c. d} を関数ｆによって、別の集合Ｂに {f(a), f(b), f(c), f(d)} として移行する。このとき集合Ａでの a, b, c, d の順序が、集合Ｂにおいて f(a), f(b), f(c), f(d) として保たれるとする。ここで集合Ｂの f(a), f(b), f(c), f(d) を逆関数ｆ-1によって元の集合Ａに戻せば、Ａ内に復元された a, b, c, d の順序は元のまま保たれる。このような二つの集合間のやりとりは「同型写像」と呼ばれる。
ガロア接続は、ＢからＡへの戻し写像が単純厳格な逆写像ｆ-1ではないが、ある写像、例えば何らかの工夫を凝らした写像ｇを使えば、Ａに戻したときの f(a), f(b), f(c), f(d) つまりg(f(a)), g(f(b)), g(f(c)), g(f(d))を、元の a, b, c, d の順序のまま保つことができるというものである。
式で表すと次のようになる。
Ａでの順序 Ｂでの順序
ｘ≦ｇ(ｙ) ←→ ｆ(ｘ)≦ｙ
言葉で言うと――Ａの任意の元ｘを関数ｆでｆ(ｘ)に変換してＢに移行した後、移行したそのｆ(ｘ)よりも大きいＢの元ｙを、ある関数ｇでｇ(ｙ)に変換してＡに戻す。このときＡでのそのｇ(ｙ)が初めの元ｘより大きくなるということが、すべてのｘ、ｙについて成り立つような関数の組ｆ、ｇが存在する――ということである。
ハイティング代数では、このガロア接続が成立している。
ｘ≦ｃ ←→ ａ∧ｘ≦ｂ あるいは
ｘ≦ａ→ｂ ←→ ａ∧ｘ≦ｂ
ａ∧ｘを、ｘが関数ｆによってａ∧ｘに変換されたもの、つまりｆ(ｘ)とみる。また、ａ→ｂを、ｂが関数ｇによってａ→ｂに変換されたもの、つまりｇ(ｂ)とみれば、(4)のハイティング代数の定義式①はガロア接続そのものである。というよりも、定義式①はガロア接続によるハイティング代数の定義なのである。
ハイティング代数では写像ｆについてはａをａ∧ｘにする関数、簡単に言えばａに∧ｘを付け加える関数であることが初めから定まっている。ただしｆはａ→ｂをｂにする関数でもあって、ａ→ｂとｂの関係は明らかではないので、この部分でｆは完全には明らかではない状況にある。
また、写像ｇもｆ(ｘ)については、ａ∧ｘをａに戻す、簡単に言えばａ∧ｘから∧ｘを取り去る関数であり、ｆの逆写像ｆ-1 であることが明らかである。しかしまたｇは、ｂをａ→ｂにする関数でもあって、ｆと同様、この部分については明らかではない。
したがってこの時点で、関数ｆもｇも、ａとｘに関しては働きが分かっているが、ただｂが関わる部分については別の働きをする関数であることが明らかであるものの、その内容は分かっていない。
以下では、ガロア接続が実現されるために写像ｇがｂについてどのように働かなければならないかを説明する。ｆはａ→ｂとｂに関して写像ｇの逆写像であるから、ｂに関する写像ｇの働きが明らかとなってｇの全体が分かればｆの全体も定まるので、ｆについては改めて述べない。
なお、ガロア接続は2つの集合間の関係だが、ハイティング代数でのガロア接続は自分自身への往復写像である。下図では、往復写像として描くと見づらくなるので、写像を左から右への移行として描いている。左端と右端の枠は同一枠の描画であり、中央の枠も自分自身である。
|
ａ≦ｂの場合、ａおよびｘがどんな値であっても、とにかくａがｂより小さいのでａ∧ｘは常にｂより小さい。すなわち、すべてのｘがａ∧ｘ≦ｂの関係を満たす。 したがってこの場合にｂをｃとして戻した先でｘ≦ｃを維持するためには、ｇはｂを、このときｘが取り得る最大の値である１の位置に戻してやらなければならない。この働きがｇ(ｂ)である。 すなわちｂについてｇ(ｂ)＝1＝ｃ＝(ａ→ｂ)。 ａ∧ｘをｘに戻す際は、逆写像ｆ-1によって元のｘの大小関係を保つことができるが、ｂについては別の扱いをしなければならない。このため、この対応は同型写像ではなくガロア接続となる。 ａ≦ｂでの写像ｇは、ｂを1に戻す働きと、f(x)をｆ-1によって元のｘの位置に戻す働きの二つを兼ね備えた写像となる。すなわちｘについてｇ(ｆ(ｘ))＝ｆ-1(ｆ(ｘ))＝ｘ。 |
|
ａ＞ｂの場合も、ａ∧ｘとｂの大小関係をｘとｃの関係において保つためには、ａ≦ｂの場合と同様に、ｂを、ａ∧ｘ≦ｂを保っている最大のｘの位置に戻してやればよい。 ただしａ＞ｂの場合は、ａ∧ｘ≦ｂの関係を満たすｘが限られる。ａ=0.5、ｂ=0の例では、ａ∧ｘ≦ｂを保っているのはｘ0 のみで、これが最大のｘである。 ａ＞ｂであり、ａ∧ｘ≦ｂが保たれるためには、すなわちａとｘの小さい方がｂより小さく保たれるためには（すでにａはｂより大きいので）ｘの方がｂより小さくなければならない。そのようなｘの最大はｘ＝ｂであるｘなので最大のｘの位置はｂである。したがってｂの位置にｂをｃとして戻してやればよい。 すなわちｂについてｇ(ｂ)＝ｂ＝ｃ＝(ａ→ｂ)。 ａ＞ｂでの写像ｇは、ｂを元のｂの位置に戻す働きと、ｂ以下であるf(x)すなわちａ∧ｘを逆写像ｆ-1によって元のｘの位置に戻す働きの二つを兼ね備えた写像となる。ｘについてのｇはａ≦ｂの場合と同じ。ただしａ＞ｂの場合、ｘ≦ｂを満たさないｘについては「ａ→ｂの候補」ではなくなりｘ自体存在しなくなるのでｇも存在しない。 これらのことから先の図と合わせたガロア接続の写像ｇは、ａ≦ｂの場合とａ＞ｂで動作を分ける働きを持つ関数である。 |
ガロア接続は、下のハイティング代数の定義［第1式左辺］ｘと［第2式左辺］ａ∧ｘを関数ｆによって関連づけ、［第2式右辺］ｂと［第1式右辺］ｃを関数ｇによって関連づけることによって、定義式が持つ性質を簡明に捉えている。
ｘ≦ｃ ←→ (ａ∧ｘ)≦ｂ
関数ｆ、ｇを使って表現すると、
ｘ≦ｇ(ｂ) ←→ｆ(ｘ)≦ｂ
となり、式からａとｃが消えてｘとｂの一種不思議な関係が浮かんでくる。先に(4)の段でこのガロア接続に触れたところで「『随伴』などの深遠な概念」と書いた「随伴」というのは、ｆとｇがもたらすこのｘとｂの関係のことである。
ここでｆ(ｘ)はａ∧ｘであり、ｇ(ｂ)はａ→ｂだが、「随伴」は∧と→ の関係の深さを示した概念といえる。実際、古典論理ではａが真のときａ∧ｂとａ→ｂは同じ真理値を持ち、直観主義論理においてもａが1のとき両者の真理値は同じである。意味を考えればさらに明らかである。「ａとｂが起こる」ということと「ａが起こればｂも起こる」ということは、ａが起きている状況では同じことである。
ここでのまとめとして、関数ｇとｆの働きを、a≦b と a＞b に区分けした3値ハイティング代数表で確認しておく。
まず、すべての行でｘ≦cが成立していることを確認する。ｃはｘの最大として設定されたものなので、これは当然のことだが、ａ≦ｂのときとａ＞ｂのときではｃの値の成立の仕方が違う。
定義第2式ｘ≦ｃが成立している行で（したがってすべての行で）、
ａ≦ｂの場合、
ｂをｃにする関数ｇとは、0、0.5、1であるｂをすべて1にしているのでｇ(ｂ)＝1である。
ａ＞ｂの場合、
ｂをｃにする関数ｇとは、ｂの値をもってｃとしているので、ｇ(ｂ)＝ｂである。
これらのときの定義第1式ａ∧ｘ≦ｂの成立有無を数値から確認すると、
ａ≦ｂのときは、
ｘをａ∧ｘにする関数ｆは、
ｘ≦ａの場合はｆ(ｘ)＝ｘ
ｘ＞ａの場合はｆ(ｘ)＝ａ
であることが確認できる。
つまりｘがａ以下ではｆ(ｘ)＝ｘだが、ｘがａを超えているときはｆ(ｘ)＝ａで、ｆ(ｘ)の最大はａである。また、ここではａ≦ｂが前提なので、これによりｆ(ｘ)≦ｂ、すなわちａ∧ｘ≦ｂが成立している。
ａ＞ｂのときは、
ｘをａ∧ｘにする関数ｆは、ａ≦ｂの場合と同様に、ａかｘの小さい方の値を採用するものとして働いている。ただしその最大はｂ止まりになっていることが確認できる。したがってｆ(ｘ)≦ｂ、つまりａ∧ｘ≦ｂが成立している。
以上によってガロア接続の関数ｇ、ｆが働いている状況で、ｘ≦ｃとａ∧ｘ≦ｂが同時に成り立っていることが確認できた。
以上、ハイティング代数 {0, ½, 1} の → の定義がどのように行われているかを見てきた。古典論理とは異なる条件法の定義についてとりあえず理解できたとしてよいだろう。
Hard study 5-2-4 で、「『論理学』では⊃の分子式の分析が慎重に避けられているように見える」と書いたが、実際にそうなのかはともかくとして、やはり直観主義論理の条件法には古典論理からの理解だけでは済まされない性質が含まれていたということである。
ただしハイティング代数を理解するということは、上で行ってきたように予めハイティング代数であるものを用意して、その性質を調べることから定義の成り立ちを理解するというだけでは十分ではない。
それ以前の問題として、ハイティング代数の前提となっている束の条件を理解する必要がある。ハイティング代数の外に出て、ハイティング代数が成立可能である束の範囲を知ることがハイティング代数の完全理解につながる。
この点は定義にも表明されている。
「元ｃが存在する束をハイティング代数とする」
上に見てきた「3値ハイティング代数表」では、ａ→ｂの候補としてのx1～x10には、その上限が0または0.5または1として存在した。この上限をａ→ｂとして定めたが、しかしこのような元ｃが必ず存在するとは限らないということである。
では、このようなｘからなる集合に上限が存在しない（共通上界がない、共通上界に最小元がない、上限が一意に定まらない等）とはどういう束であるのか。
ハイティング代数には、これまでに見てきた定義
① (ａ∧ｘ)≦ｂ ←→ ｘ≦ｃ あるいは
(ａ∧ｘ)≦ｂ ←→ ｘ≦ａ→ｂ
の他に、2つの定義がある。
束を{元∈束｜元の性質} と表記すると、その一つめは束Ｈにおいて、
② Max{ｘ∈Ｈ｜ａ∧ｘ≦ｂ}が存在し、これをａ→ｂとする
というものである。
これは、ａ∧ｘがｂ以下であるようなｘの最大値の存在を述べた定義である。つまり①の定義のｃの存在を述べたもので、①の第2式と第1式を合わせて1つの式に表現したものと解することができる。
二つめは、束Ｈの任意の元ａとＨの可算部分集合{ｂ}において、（可算部分集合とは、{b1},{b2}...のように番号を割り当てることができる部分集合。ここでは簡略にｂで表す。）
③ ａ∧Vｂ＝V(ａ∧ｂ) が成り立つ
というもの。ここで、Vは∨と同じ上限記号の一種で、集合のように一つの項において上限が存在するときの上限の書き方である。
また、{ｂ}が付番できる集合として指定されているのは、③ではこれまでに見てきた有限束ではなく、無限を要素に持つことができる「完備束」を前提しているためである。（束の定義が任意の2元について上限と下限が存在するということであるのに対し、完備束では任意の部分集合について上限と下限が存在するという定義が行われる。）ただしここでは、束の拡張に伴って出てきた完備性や可算部分集合については置いておき、以下に注目する。
③は完備ハイティング代数において分配律が成立することを述べたものである。この式自体の証明は①の定義式を使って行うことができる。証明内容をたどったものを注に挙げておく。
また、①と②が同等であることの証明と、②と③が同等であること（厳密には②の完備版の定義と③が同等であること）の証明が、注[22]に引用した同書 命題5.1と命題5.9で確認できる。こちらも証明内容をたどったものを注に挙げておく。
さて、課題は①の定義における「ａ∧ｘ≦ｂが成立するようなｘの集合において上限が存在しない束とはどのようなものか」を知ることだが、上の三個の定義は同等なので、このいずれかが成立しない束が分かればよいことになる。
ただし、これまでに見てきたＩの形の3値ハイティング代数モデル（次段(13)のハイティング代数モデル参照）では「上限が存在しない」ということはあり得ないので、したがってそれだけを見てきた我々としては、その事態をイメージできない状況にある。この点を考えれば、やはり定義①あるいは同じことを述べている②において、それが実現できない束というものを知りたい気がする。
『束論』（1966年初版）、『現代のブール代数』（1986年）などの古い書籍には、分配律やモジュラー律が成立しない束の具体例が掲載されている。モジュラー律というのは束特有の弱い分配律である。
したがって、ある束では定義③が成立しないことについてはこれらの書物に当たれば確認できるが、本来的には、その束において定義①②が成立しないことを理解したい。「上限ｃが存在しない」というのがどういう事態であるのかをイメージしたいためである。しかしとりあえずは、ある束では定義③が成立しないことを以下の通り確認しておこう。
分配律が成立しない束の一つは、いびつな五角形に5値が配されたもので、上端を1、下端を0とし、仮にこれをＤ形と呼ぶと、Ｄの弧上に相当する2つの頂点にａ、ｘが置かれ、直線的な縦棒の中程にｂが置かれている束である。いずれの2点をとっても上限、下限が存在し、したがってこれが束であることについては明らかである。
上図でａとｂ間、ｘとｂ間に順序関係はない。ａとｘの下限（a∧x）はｘとなるが、ｘとｂ間の大小比較ができないので、a∧x≦ｂというハイティング代数定義①の基準の論外的状況が生じている。
先に、上限が存在しない例として「共通上界がない」「共通上界に最小元がない」「上限が一意に定まらない」という思いつく限りのことを挙げていたが、考えてみれば前二者については「上限がない」ことになるので、そもそも束ではなく見当違いである。
そういうことではなく、上図のように束でありながら、a∧xとｂ間の順序関係が存在できない場合があり、「ｃが存在しない」少なくとも一つの例がこれだということである。
なお、先段(10)の図5では、ａ＞ｂかつｘ＞ｂのとき、ａ∧ｘのｘが、ａ→ｂの候補としての資格を失っていることを確認したが、その状況がｃが存在しないケースの一つであるというわけではない。そこでは、ただａ→ｂの候補ｘが、ａ≦ｂである場合や、ａ＞ｂだがｘ≦ｂである場合とは異なり、ａ∧ｘ≦ｂによって、すなわちａ∧ｘとｂの比較によって限定される事態が起きているということであり、これは候補ｘの中からａ→ｂを特定しようとする操作の過程で生じる除外であり、定義が実行できているその過程に生じる事態であるにすぎない。
これに対して、上の5角形の束で起きているのは、ａ∧ｘとｂの比較そのものができない、つまり定義が実行できないという事態である。
この束は、また、ハイティング代数定義③に表れているモジュラー律を満たさない。モジュラー律は、ｘ≦ａのときに、
(ｘ∨ｂ)∧ａ＝ｘ∨(ｂ∧ａ)
というように、左辺と右辺のｘ、ｂ、ａの並び順が同じ、∨と∧の位置も同じで、ただカッコだけがずれる形となるある種の分配律である。
上図で、ｘとｂの上限は1、したがって(ｘ∨ｂ)∧ａ＝ａ。ｂとａの下限は0、したがってｘ∨(ｂ∧ａ)＝ｘとなり、(ｘ∨ｂ)∧ａとｘ∨(ｂ∧ａ)は＝で結ばれない。
この束が一般の分配律を満たさないことも容易に見てとれる。分配律は、
ａ∧(ｂ∨ｘ)＝(ａ∧ｂ)∨(ａ∧ｘ)
だが、ｂ∨ｘ＝1なので、左辺は
ａ∧(ｂ∨ｘ)＝ａ∧1＝ａ
右辺の第1項はａ∧ｂ＝0。右辺の第2項はａ∧ｘ＝ｘなので、
(ａ∧ｂ)∨(ａ∧ｘ)＝0∨ｘ＝ｘ
したがって、左辺がａ、右辺がｘでモジュラー律と同じ結果となり分配律は成立していない。
先の『束論』に紹介されている分配律が成立しないもう一つの例は、◇の中央に縦棒があるモデルで、上端を1、下端を0とし、その中間位置にａ、ｂ、ｃを横並びに配置したものである。この束では、モジュラー律は成立するが、分配律は成立しないということである。
モジュラー律 (ｘ∨ｂ)∧ａ＝ｘ∨(ｂ∧ａ) では「ｘ≦ａのとき」という条件が付くので、ｘを0のところに配置して確認する。（ｘをａのところに置いても同様の結果となる。）
左辺(ｘ∨ｂ)∧ａ＝ｂ∧ａ＝ｘ
右辺ｘ∨(ｂ∧ａ)＝ｘ∨ｘ＝ｘ となり成立している。
分配律ａ∧(ｂ∨ｃ)＝(ａ∧ｂ)∨(ａ∧ｃ) では、
左辺ａ∧(ｂ∨ｃ)＝ａ∧１＝ａ
右辺(ａ∧ｂ)∨(ａ∧ｃ)＝ｘ∨ｘ＝ｘ となり成立しない。
縦棒ありの◇形束では、すべての元の比較ができるとしても（ａ、ｂ、ｃそれぞれを0.5の値を持つものとしても上の状況が成立する）、分配律が成立していないためにハイティング代数にならない。5角形束との共通点を考えれば、ハイティング代数にならない、すなわち「上限ｃが存在しない」というのは、元同士の比較ができないということであるよりも、分配律が成り立たないことにあるということになる。
先に挙げた見通しを拾うと、分配律が成立しないとは「上限が一意に定まらない」ということであり、それが「上限ｃが存在しない」ことの意味だと思われるが、確認ができれば追記したい。また、この2つの非分配束以外の例についても知りたいところだが、今回は以上で満足することとしたい。
ブール代数の補元に相当するハイティング代数の補元は「擬補元」と呼ばれ、次のように定義される。
￢ｘ：＝ｘ→ 0（：＝は定義の意味）
上の定義で使われている → は、ハイティング代数の定義で定めた → である。すなわち、ａ→ｂの候補ｘにおいて
ａ≦ ｂのとき、ｘ≦1
ａ＞ｂのとき、ｘ≦ｂ
が成り立つ最大のｘを正規の「ａ→ｂ」の値とするということであった。つまり、
ａ≦ ｂのとき、ａ→ｂ＝1
ａ＞ｂのとき、ａ→ｂ＝ｂ
である。ハイティング代数の最小元が0であることを踏まえて、このａ→ｂの定義をｘ→ 0 にそのまま置き換えると、
ｘ≦ 0のとき、すなわちｘ＝0のとき、ｘ→ 0＝1
ｘ＞0のとき、すなわちｘが0以外のとき、ｘ→ 0＝0
ということになる。
これによってハイティング代数 {0, ½, 1} の￢の真理表は以下になる。
ｘ＝½を意味づけして、例えば「現時点では未証明だがやがて証明される」と解すると、￢ｘ＝0は「現時点で未証明で将来的にも証明されない」といった意味合いになる。
これは3値ハイティング代数の½をクリプキ意味論の認識史01（α⊮、~β⊩）相当と見たものだが、「直観主義論理の￢Ｐの証明表」で確認すると（Hard study 5-2-4）、￢ｘの認識史01は確かにα⊮、~β⊮であり、「現時点で未証明で将来的にも証明されない」という上の解釈に一致している。
参考までに、ウカシェヴィチの三値論理の￢の真理表は以下のようである。
こちらはｘ＝½を「『彼は生きている』という情報はあいまいである」という意味に解すると、￢ｘは「『彼は死んでいる』という情報もまたあいまいである」という意味に解することができる。½の解釈にはいろいろな可能性がある。
さて、以上で、ハイティング代数の「擬補元」￢については一件落着とも思える。しかし一筋縄ではいかないのがハイティング代数である。
当節冒頭に紹介したWEB文献に掲載されているハイティング代数モデルは以下である。
左端のモデルはこれまでに扱ってきた {0, ½, 1} がＩ形に並んだもので、これをハイティング代数3値モデルと呼ぶことにする。
真中は5値からなるハイティング代数で5値モデル、右は6値モデルと呼ぶ。また、ここで新たに登場した真中と右のモデルがハイティング代数であることの確認は省略する。（分配律が成立していればハイティング代数である。）
注目したいのは、それぞれの否定のあり方である。
当該WEB文献では、
3値モデル ￢1＝0、￢½＝0、￢0＝1
5値モデル ￢1＝0、￢⅔＝0、￢⅓＝⅓'、￢⅓'＝⅓、￢0＝1
6値モデル ￢1＝0、￢¾＝0、￢½＝0、￢½'＝0、￢¼＝0、￢0＝1
となっており、続けて
「0以外の元の擬補元は0になることが多いようですが、例外もあります。」
とだけ書かれている。この他の説明はないので検討してみると以下のことが分かる。
まず、どのモデルにも、
￢1＝0、￢0＝1
というブール代数的な否定がある。
また、どのモデルにも、
￢½＝0、￢⅔＝0、￢¾＝0、￢¼＝0
のように、当段冒頭に見たハイティング代数の擬補元の定義から導かれている否定がある。もっともブール代数的否定もこの定義から導かれたものなので、両者を同等と見ることは可能である。
5値モデルには、ブール代数的でもハイティング代数的でもない否定
￢⅓＝⅓'、￢⅓'＝⅓
がある。これが先の説明で「例外もあります」と言われていたものである。
この⅓とシングルクォート付きの⅓'は、上に見たウカシェヴィチの三値論理の否定と同じ種類のもののようにも見えるが、ウカシェヴィチでは ½ → ½＝1で、5値モデルでは ⅓ → ⅓'＝0、 ⅓' → ⅓＝0として計算されるので両者は全く別種のものである。（5値モデルの計算については同WEB文献のプレ線型性式「A→B.∨.B→A」での計算参照。）
これについて理解できることを挙げてみる。まず ⅓ → ⅓'＝0 であることから、ここでの → 演算は、これまでに見てきた3値ハイティング代数の → 演算とは違っているように見える。前件が後件と同じか小さい値のときは式全体の値を1とするというのが → 演算の規則だからである。
しかし（おそらく）以下のように理解できる。上は ⅓'の値を ⅓ と同じと見た場合の見通しだったが、実は ⅓' がどんな値であるのかは分かっていないとするのが正しいということである。 ⅓' が0より大きく⅔ よりは小さい順序関係にあることは5値モデルの形から分かるが、しかし⅓ との大小関係は明らかではない。そのため ⅓ と ⅓' が混在する式は、前件後件の大小から値が決まる → 演算を行うことができないと見なければならない。 ⅓ → ⅓' はその種の式である。
そこで以下に注目してみる。5値モデルで◇の左右に配されている⅓と⅓'の下限（◇の下端）は 0 であるため、⅓∧⅓'＝0が成り立つ。そしてこのように、連言をとると偽になるということが、先に見たブール代数の補元の性質の一つであることに着目すると、⅓ と ⅓' は肯定と否定の関係にあると見ることができる。
このため ⅓ と ⅓' に関しては、わざわざハイティング代数の擬補元の定義を使わなくても、⅓' を ⅓ のブール代数的な補元すなわち￢⅓とみなすことができる。すなわち ￢⅓＝⅓' であり、これが「例外もあります」と言われていた ⅓ と ⅓' についての理解となる。
そしてここに、当段冒頭に紹介したハイティング代数の ￢ の定義を当てはめると、⅓ と ⅓' は否定の関係にあるので次が成り立つ。
⅓'＝￢⅓ ＝(⅓ → 0)
したがって、
⅓ → ⅓' ＝ ⅓ → (⅓ → 0) ＝ ⅓ → (0) ＝ 0
同じことが⅓'と⅓についても成り立つので、以下となる。
⅓' → ⅓ ＝ ⅓' → (⅓' → 0) ＝ ⅓' → (0) ＝ 0
⅓' の場合は ⅓' の値は不明だが0より大きいことは確かなので、⅓' → 0 ＝ 0 である。（ａ＞ｂのとき、ａ→ｂ＝ｂ）
あるいは、上で「⅓ と ⅓' は肯定と否定の関係にある」としたことは、ハイティング代数定義①を使って、次のように確認することもできる。
定義① (ａ∧ｘ)≦ｂ ←→ ｘ≦ａ→ｂ すなわち、
(⅓ ∧⅓' )≦0 ←→ ⅓' ≦ ⅓ → 0
このとき、どちらかの式で等号が成り立っていれば、もう一方の式でも等号が成り立っているとしてよいので、いま⅓と⅓'の下限が0なので、
(⅓ ∧⅓' )＝0 ←→ ⅓' ＝ ⅓ → 0
が成り立つ。この第2式はハイティング代数の擬補元の定義の形、すなわち ￢⅓ ＝ ⅓ → 0 の形なので、したがって⅓' ＝￢⅓ である。
なお、この5値モデルでＡ＝⅓、Ｂ＝⅓'と設定することで、当稿のⅠα型証明表で扱ったプレ線型性式は、 (Ａ→Ｂ)∨(Ｂ→Ａ)＝0∨0＝0となり、非定理であることが示される。
さて、注[22][23]で参照した『論理体系と代数モデル』では、直観主義論理の否定の性質が次のように書かれている。
「ハイティング代数ではｘ∧￢ｘ＝0はつねに成り立つが、ｘ∨￢ｘ＝1は一般には成り立たない。」
また、直観主義論理の否定について、次のように伝えているWEB文献がある。
「（直観主義で）2重否定の性質とド・モルガン律が成立するような否定を定義することは可能で，これは古典論的否定あるいは擬否定と呼ばれる．しかし，この擬否定の決め方は一意ではない。」
ここからは、直観主義論理における否定というのはｘ∧￢ｘ＝0が満たされることが唯一の条件であり、それを満たす複数の定義が可能であって、一般にハイティング代数の否定の定義として書かれている￢ｘ：＝ｘ→ 0は、そのような否定の決め方の一つであり、これとは別に「擬否定」という、二重否定除去則やド・モルガン律(2)aを成立させるような古典論理的な否定の定義もあるということが推察される。
ここで言われている「古典論的否定あるいは擬否定」というのは、先に「ブール代数的否定」として理解してきたものや、下限に0を持つ⅓ と ⅓' の関係を指すように思われ、そうであればその存在は確認してきたところである。
すでに(5)の段で「ブール代数はハイティング代数の一種なので、ハイティング代数に補元がある場合もある」と理解してきたところであり、5値ハイティング代数でのように、ハイティング代数的否定としての「擬補元」と、ブール代数的否定としての「補元」が同時に存在してもおかしなことではないということもとりあえずは納得できる。
確かにどのモデルの擬補元もｘ∧￢ｘ＝0が果たされている。多くの場合で￢ｘが0だからである。そして見てきたように、5値モデルでは ⅓ と ⅓' の下限が0なので ⅓∧⅓'＝0である。
なお、6値モデルの ½∧½' では、両者の下限が¼になっているので、5値モデルの⅓と⅓'とは異なり、この½と½'は相互否定の関係にはない。6値モデルでは￢½＝0，￢½'＝0であって、これはハイティング代数の擬補元の定義から導かれた否定である。
また当該WEB文献によると、6値モデルでは (½ → ¼)＝½' と計算される。ハイティング代数の → の定義を直接当てはめるなら ½ → ¼ はａ＞ｂのパターンであるからａ→ｂ≦ｂ、つまり ¼ となるはずなのでこれも確認を必要とする事態である。
5値モデルでの ⅓ と ⅓' がそうであったように、6値モデルでの ½ と ½' は◇形の下限 ¼ を持つ組み合わせである。ここからは現時点での見通しとしてしか述べられないが、このように◇形で存在する値を考える場合は、論理記号の定義順序により、ハイティング代数の → に先立って、束の下限∧の定義が優先されなければならないようである。つまり、
½ ∧ ½' ＝ ¼
が優先される。ここから、先と同様にハイティング代数定義①を当てはめて、
½' ＝ ½ → ¼
として、→ を持つ式が導かれ、これが当該WEB文献に記されている計算ということになる。
また、ここでハイティング代数定義①の式の不等号を等号として扱ってよいのは ½ → ¼ のようにａ≧ｂである場合は (ａ∧ｘ)≦ｂではなく (ａ∧ｘ)＝ｂが成立するためである。3値ハイティング代数でこれが成立していることは、前段の「3値ハイティング代数表(3)」で確認できる。
ついでに「ｘ∨￢ｘ＝1は一般には成り立たない」について確認しておくと、
3値モデル 元½ 擬補元0 ½∨0＝½
5値モデル 元⅓ 補元⅓' ⅓∨⅓'＝⅔
（⅓∨⅓'＝⅓ではなく、∨は上限を求める計算。）
6値モデル 元½ 擬補元½' ½∨½'＝¾
（½＋½＝1ではなく、∨は上限を求める計算。）
等々で、いずれも1にならないことが見てとれる。
これまで古典論理の「排中律」について「肯定と否定を合わせると全体を満たす」という言い方を何度かしてきたが、これら直観主義論理の擬補元では、もとの元と合せても1に満たないことが排中律の非成立を示している。ただ1と0の関係においてのみ例外的に排中律が成立しているのである。
したがって『論理体系と代数モデル』の先の文言が述べているのは、ハイティング代数は、否定に関して排中律は満たさなくてよいが矛盾律は満たさなければならないということである。
最後に、当稿で作成したクリプキ系証明表をハイティング代数モデルと比較して、現時点での評価を与えておきたい。
まず、ハイティング代数 {0, ½ ,1} の真理表はⅠ型証明表と同じであることを確認する。
Ⅰ型証明表はクリプキ意味論に基づいて16行からスタートしたが、「証明済」が「不証明」に変わる認識史はないということから9行に収まった（Hard study 5-5-1）。これにより11、10、01、00の4通りの認識史のうち10が除かれたので、Ａ、Ｂそれぞれは3通りの認識史を持つこととなり、(3認識史)^(2命題）＝9行となったのである。
一方、3値ハイティング代数の2命題真理表を作成すると(3値)^(2命題)でやはり9行となってⅠ型証明表と同じになる。
次にⅠ型証明表の証明値と3値ハイティング代数の真理値を確認してみると、Ⅰ型証明表の認識史11、01、00を3値ハイティング代数の1、½、0とみなしてよいことが分かる。
以下は、∧（下限の定義）、∨（上限の定義）、→（ハイティング代数定義）、￢（擬補元の定義）から計算した3値ハイティング代数の真理表である。
3値ハイティング代数真理表の真理値は、Hard study 5-5-1に示したⅠ型基本証明表の証明値との完全な一致がある。したがって認識史11、01、00は、それぞれ1、½、0相当である。
Ⅰ型証明表と3値ハイティング代数の値が一致するということは、それらの証明可能範囲も同じであることを意味している。
したがって、Hard study 5-5-2～3で扱った「プレ線型性」(Ａ⊃Ｂ)∨(Ｂ⊃Ａ) と、「ド・モルガン律(2)a」￢(Ａ∧Ｂ)⊃(￢Ａ∨￢Ｂ)は、3値ハイティング代数モデルでも非妥当性を示すことはできない。
ハイティング代数モデルを掲載している先のWEB文献で、「プレ線型性」と「ド・モルガン律(2)a」の非妥当性を示すための計算を、3値モデルではなく5値モデルで行っているのはそのためである。
次に、否定の種類について見てみると、Ⅰ型基本証明表では認識史01と00の2種の否定があるのに対し、3値モデルでは先に見たようにブール代数的否定とハイティング代数定義による否定というやはり2種の否定があり両者は一致している。（認識史01がハイティング代数定義による否定相当、認識史00がブール代数的否定相当）
以上のことから、Ⅰ型証明表と3値ハイティング代数は完全に同じであるという見方ができる。
ではⅡ型証明表と5値ハイティング代数についてはどうだろうか。これらは否定の種類だけを見れば一致しているといえそうである。
Hard study 5-5-3から再録すると、Ⅱ型証明表には
1. 認識史01での├/p 直観主義論理の「やがて証明されることになる未証明」
2. 認識史00での├/t 古典論理的「否定」
3. 認識史00での├/p 三値論理的「永遠の真偽不明」
の3種の否定がある。これらは5値ハイティング代数の
1. 擬補元 ￢ｘ：＝ｘ→ 0
2. ブール代数的否定 ￢1＝0、￢0＝1
3. 5値モデル的否定 ￢⅓＝⅓'、￢⅓'＝⅓
に相当するといえる。
これらの相似は驚くべきことに思われ、当節冒頭に述べたように、これがⅡ型証明表を生き返らせたのである。
さらに「ド・モルガン律(2)a」の非定理性を示す点においても両者は似ている。また、Ⅱ型証明表がそのために用いた「外部結合」という手法は、先に見た「ガロア接続」と似ている。
関数ｆを「￢」とし、逆向き関数ｇを「￢」とするとき、ｆ(ｘ)＝￢ｘ、ｇ(ｆ(ｘ))＝￢￢ｘであり、ガロア接続においては、この￢￢ｘがｘよりも大きいことが証明されることから、「外部結合」と「ガロア接続」の効果における類似性を指摘することができる。（いずれも否定における「不」と「否」の組み合わせに由来する効果といえるが詳細は省略する。）
しかし、それぞれの由来を考えるとこれらを同等とみなすことには無理がある。5値ハイティング代数モデルがハイティング代数の定義に由来する由緒正しいモデルであるのに対して、Ⅱ型証明表はクリプキ意味論を出自とするものの、その後、「ド・モルガン律(2)a」の非定理性を示すために技巧を加えて改変したものである。
さらに5値ハイティング代数が「ド・モルガン律(2)a」だけではなく、当考察でⅠα型証明表を使わなければならなかった「プレ線型性」の非妥当性に対しても有効であるということが、両者の決定的な差を示している。
もっとも、Ⅱ型証明表はいまのところⅠ型証明表の上位互換であると判断できるので、これにⅠα型証明表と同様の処理を施すことでⅡα型証明表とすることは容易であり、これをもってⅡ型証明表を「プレ線型性」に対応済みとみなすことは可能である。
しかしながら、Ⅱ型証明表の意義は、否定に複数の種別を設けるという考え方が直観主義論理を理解するための方向性として正しかったという点、および「外部結合」というデータベース演算が、否定が持つ範囲の差を示すのに有効であるという点に限られる、とする控えめの判断が現時点での結論としては妥当であるだろう。
なお、ハイティング代数がプレ線型性式と非定理のド・モルガン律をどのように表現するかについては、注[25]に挙げたWEB文献に示されているので省略する。（プレ線型性式については先段(13)に示した。）
そこでの方法は、2命題論理式のＡ、Ｂをハイティング代数3値モデル、5値モデルの2元に置き換えて論理演算を行った結果が1ではなくなるような元の組み合わせを見つけることで、その式の非定理性を示すということである。（ド・モルガン律(2)aについてもプレ線型性式と同様に、Ａ＝⅓、Ｂ＝⅓'と設定することで式全体の値が1にならないことが確認できる。）
したがってハイティング代数モデルは、それを用いることで即座にその式の定理／非定理が分かるというものではなく、認識史分析などの何らかの方法で非定理となる2元の組み合わせについての見通しを立てた上で、そのような元の組み合わせを実際に探すという手順を踏まなければならない。
この点ではⅡ型証明表は、当稿で扱った12個の式に関しては古典論理の真理表と同様に即座にその式の定理／非定理を示すことができる。しかし、当節冒頭に紹介したように、「直観主義論理におけるすべての定理／非定理を表現できるモデルは存在しない」ことは直観主義論理において原理的なことであるので、Ⅱ型証明表のようなものが万能の働きをすることは望めない。
定理／非定理についての感想を付け加えれば、古典論理で定理でありながら直観主義論理で非定理である論理式、例えば代表的な例で「排中律 Ａ∨￢Ａ」だが、これが直観主義論理で非定理であるというのは、直観主義論理においては否定の種類が複数存在するからに他ならない。
そのため排中律は、否定に関して認識史01と認識史00を持つⅠ型証明表で非定理として表示され、またブール代数的否定とハイティング代数的否定を持つ3値ハイティング代数においても、Ａを元½とすると￢Ａ＝0なので、Ａ∨￢Ａ＝½∨0＝½となり1とはならず、「Ａと￢Ａで全体を満たさない」ことによりその非定理であることが示される。
しかし、排中律のように複数の偽が存在するために非定理となる式、言いかえれば古典論理のようにそれらの偽をひとまとめにしてしまえば定理となるような非定理と、古典論理においてすでに非定理である非定理式は、非定理としての性質に違いがある。
もちろんそれが基づく公理系から導き出せるか否かが定理／非定理を分ける基準であり、これは直観主義論理においても古典論理においても同じであるから論理学的に不具合はなく、排中律を古典論理で定理、直観主義論理で非定理と呼ぶことには何の問題もない。
しかし排中律のような論理式では、直観主義論理において何によってそれが非定理となっているのかという性質が古典論理の非定理式、例えばＡ⊃Ｂなどの一般式とは異なるので、論理式の意味を重視したい立場としては、直観主義論理における非定理をすべてひとまとめにするのではなく、一般式としての非定理なのか、偽の複数性がもたらした非定理なのか、あるいはプレ線型性式のようにそのいずれとも言えない非定理なのかを区別することも重要な視点と思える。
さて、この「Hard Study」は直観主義論理における否定概念の追求として始まったので（Easy Study 5-1 最後から5行目の記述）、Ⅱ型証明表およびハイティング代数モデルにおける否定概念の概観を終えたことによってひとまず終わりを迎えた。