数学の基礎

　直観主義論理に従う理論 T において、命題全体からなる集合を B₀ と書き、P, QÎ B₀ が同値であることを P = Q と書くことにすれば、“ = ”は明らかに B₀ 上の同値関係で、Q Ù P = P であることと P ® Q が定理であることは同値です。
　また、Ù と Ú をそれぞれ ò , ñ と書き直せば、本文第３節メタ定理22、メタ定理23及び (P Ú Q) Ù P と (P Ù Q) Ú P と P の同値性により、本文第14節 (14-79) が成り立ちます。
　すなわち、B₀ は、P, QÎB₀ に対する“sequent P ® Q は証明可能”という関係を擬順序とする束になっており、P Ú Q と P Ù Q はそれぞれ P と Q の上限と下限になっていることがわかります。しかも任意の命題 P に対して ^ ® P と P ® Ø ^ が共に成り立つので、B₀ は最小値 ^ と最大値 Ø ^ を持ちます。
　また、明らかに R ® P Þ Q が成り立つことと R Ù P ® Q 成り立つことは同値ですから、Þ を ð と書き直せば、これは第14節 (14-84) が成り立つことを意味するので、B₀ はHeyting代数になることがわかります。
　更に、排中律 (Ø P) Ú P が成り立つということは、命題 (P Þ ^) Ú P が定理 Ø ^ と同値であるという形、すなわち第14節 (14-86) の形に表現できますから、T が古典論理に従う場合は B₀ はBoole代数になることがわかります。

　次に T における項全体からなる集合を S₀ と書くことにします
　任意に P(x)ÎB₀ を取ると、すべての TÎS₀ に対し、始式 P(T ) ® P(T ) から ( " 左) により "xP(x) ® P(T ) が得られます。
　逆に RÎB₀ が、すべての TÎS₀ に対して R ® P(T ) が成り立つという性質を持つとします。このとき特に R に現れない変数 z を取ると、z も項ですから、仮定により R ® P(z) が成り立つので、( " 右) により R ® "xP(x) が得られます。
　すなわち

(A9-1a)  "xP(x) = inf{ P(T ) | TÎS0 }

が成り立っていることがわかりました。
　同様に、任意に P(x)ÎB₀ を取ると、すべての TÎS₀ に対し、始式 P(T ) ® P(T ) から ( $ 右) により P(T ) ® $xP(x) が得られます。
　逆に RÎB₀ が、すべての TÎS₀ に対して P(T ) ® R が成り立つという性質を持つとします。このとき特に R に現れない変数 z を取ると、z も項ですから、仮定により P(z) ® R が成り立つので、( $ 左) により $xP(x) ® R が得られます。
　すなわち

(A9-1b)  $xP(x) = sup{ P(T ) | TÎS0 }

が成り立っていることがわかりました。

　さて、以上のような直観主義論理や古典論理の持つ代数的な性質に基づいて、以下のようにしてモデルの概念を定義します。

　T を直観主義論理に従う理論で、Ù , Ú , Þ , ^ , " , $ 以外に論理記号を持たないものとします。
　ここで、集合 S と Heyting代数 B が与えられ、T の各変数 x に対して S の元 x* が与えられ、T の各関数記号 f に対して（その引数の個数を n とするとき）S ⁿ から S への写像 f* が与えられ、T の各述語記号 p に対して（その引数の個数を n とするとき）S ⁿ から B への写像 p* が与えられ、T の各命題 P に対して B の元 P* が与えられ、以下の条件が満たされているとき、B と S と * の組を、理論 T のHeytingモデルといいます。

(A9-2a)  ( f T1 ,¼, Tn )* = f*(T1*,¼, Tn*)

(A9-2b)  ( pT1 ,¼, Tn )* = p*(T1*,¼, Tn*)

(A9-2c)  ^* = 0

(A9-2d)  (P Ù Q)* = P* ò Q*

(A9-2e)  (P Ú Q)* = P* ñ Q*

(A9-2f)  (P Þ Q)* = P* ð Q*

(A9-2g)  ("xP)* = inf{ P* | x*ÎS }

(A9-2h)  ($xP)* = sup{ P* | x*ÎS }

　ただし、T_i は項を、P と Q は命題を、x は変数を表わし、ñ と ò はそれぞれ両辺の上限と下限を表します。

　また、T が古典論理に従うとき、B をBoole代数に置き換えたものを理論 T のBooleモデルといいます。この場合、 (A9-2) の性質により

(A9-3)  (Ø P)* = (P Þ ^)* = P* ð ^* = (ùP*) ñ ^* = (ùP*) ñ 0 = ùP*

が成り立つこともわかります。

　集合 S に対し、Heyting代数（Boole代数） B は、任意の写像 f : S ®B の像が必ず上限と下限を持つとき S-完備であるといい、任意の集合 S に対して S-完備であるとき単に完備であるといいます。S が有限集合なら、明らかに任意のHeyting代数（Boole代数）は S-完備です。

　順序集合 B は、任意の部分集合が上限を持ち、かつ任意の a, bÎB が aðb を持てば完備Heyting代数です。
　実際、A Ì B のとき、A のどの元 a に対しても b £ a となるような B の元 b 全体の集合の上限は A の下限になるので、B の任意の部分集合は下限を持ち、また B 自身の上限として最大値、B 自身の下限として最小値を持つからです。

　もし B が S-完備ならば、変数 x に対する x* と、関数記号 f に対する f* と、述語記号 p に対する p* さえ与えられれば（このとき論理式の解釈が与えられたといいます）、項 T に対する T*ÎS と命題 P に対する P*ÎB を (A9-2) によって順次定義していくことによって、理論 T のHeytingモデルを構成することができることに注意します。

　さて、T を直観主義論理（古典論理）の述語論理、すなわち Ù , Ú , Þ , ^ , " , $ 以外に論理記号を持たず、構造及び論理記号に関する推論規則以外に推論規則も公理も持たない理論とします。
　ここで T のHeytingモデル（Booleモデル）が与えられたとき、証明可能なsequent A₁ ,¼, A_n ® R に対して

(A9-4)   inf{A1* ,¼, An* } £ R*

が成り立つことを証明しましょう。そのために、証明文に現れる各sequentが、どんな解釈に対しても (A9-4) を満たすことを、上から順に確かめていくことにします。なお、簡単のため、(A9-4) の左辺を a と置きます。

　まず、当該sequentが推論規則 ( 同 一 ) を用いて得られた場合は、仮定より明らかです。

　次に、当該sequentが推論規則 ( 仮 定 ) を用いて得られた場合は、R は A_i のうちのいずれかですから明らかです。

　次に、当該sequentが ( 増 ) , ( 減 ) , ( 換 ) のいずれかを用いて得られた場合は、ある B₁ ,¼, B_m ® R が既に証明されていて、任意の B_j は、ある A_i に一致します。ゆえに a = inf{A₁* ,¼, A_n* } £ inf{B₁* ,¼, B_m* } で、仮定により inf{B₁* ,¼, B_m* } £ R* ですから (A9-4) が成り立ちます。

　次に、当該sequentが ( 切 断 ) を用いて得られた場合は、ある P に対して A₁ ,¼, A_n ® P と A₁ ,¼, A_n , P ® R が既に証明されているはずです。ゆえに仮定により inf{A₁* ,¼, A_n* } £ P* かつ inf{A₁* ,¼, A_n* , P* } £ R* ですから、(A9-4) は明らかに成り立ちます。

　次に、当該sequentが ( 代 入 ) を用いて得られた場合は、ある B₁ ,¼, B_n ® P が既に証明されていて、項 T が存在して A_i は (T | x)B_i で、R は (T | x)P です。すると仮定により、どんな解釈に対しても inf{B₁* ,¼, B_n* } £ P* が成り立つので、特に x* が値 T* をとっても成り立ちます。ところがこれは (A9-4) の成立を意味しています。

　次に、当該sequentが ( Ù 導入) を用いて得られた場合は、ある A₁ ,¼, A_n ® P と A₁ ,¼, A_n ® Q が既に証明されていて、R は P Ù Q です。すると仮定により a £ P* と a £ Q* が成り立つので a £ (P* òQ*) = R* が成立します。

　次に、当該sequentが ( Ú 導入) を用いて得られた場合は、ある A₁ ,¼, A_n ® P 又は A₁ ,¼, A_n ® Q が既に証明されていて、R は P Ú Q です。すると仮定により a £ P* 又は a £ Q* が成り立つので a £ (P* ñQ*) = R* が成立します。

　次に、当該sequentが ( Þ 導入) を用いて得られた場合は、ある A₁ ,¼, A_n , P ® Q が既に証明されていて、R は P Þ Q です。すると仮定により aòP* £ Q* が成り立つので、ð の定義により a £ (P* ðQ*) = R* が成立します。

　次に、当該sequentが ( " 導入) を用いて得られた場合は、ある A₁ ,¼, A_n ® P が既に証明されていて、R はこのsequentの左辺に現れない変数 x により "xP と書かれます。すると仮定により、どんな解釈に対しても a £ P* が成り立つので、特に x* がどんな値をとっても成り立ちます。ところが仮定により左辺は x* の値に依存しませんから、a £ inf{ P* | x*ÎS } = R* が成立します。

　次に、当該sequentが ( $ 導入) を用いて得られた場合は、ある A₁ ,¼, A_n ® (T | x)P が既に証明されていて、R はある変数 x により $xP と書かれます。すると仮定により、a £ ((T | x)P)* = (T* | x*)P* £ sup{ P* | x*ÎS } = R* が成立します。

　次に、当該sequentが ( Ù 消去) を用いて得られた場合は、ある A₁ ,¼, A_n ® P Ù Q が既に証明されていて、R は P 又は Q です。すると仮定により a £ (P Ù Q)* = P* òQ* £ R* が成立します。

　次に、当該sequentが ( Ú 消去) を用いて得られた場合は、ある A₁ ,¼, A_n ® P Ú Q と A₁ ,¼, A_n , P ® R と A₁ ,¼, A_n , Q ® R が既に証明されています。すると仮定により a £ (P Ú Q)* と aòP* £ R* と aòQ* £ R* が成り立ちます。
　ところで ð の定義により、後２者は P* £ (aðR*) 及び Q* £ (aðR*) が成立するので (P Ú Q)* = P* ñQ* £ (aðR*) となり、再び ð の定義により、aò(P Ú Q)* £ R* がわかりますが、a £ (P Ú Q)* により a = aò(P Ú Q)* となるので a £ R* が成立します。

　次に、当該sequentが ( Þ 消去) を用いて得られた場合は、ある A₁ ,¼, A_n ® P Þ R と A₁ ,¼, A_n ® P が既に証明されています。すると仮定により a £ (P Þ R)* = P* ðR* と a £ P* が成り立ちます。ところが前者は ð の定義により aòP* £ R* が成り立ち aòP* = a ですから a £ R* が成立します。

　次に、当該sequentが ( " 消去) を用いて得られた場合は、ある A₁ ,¼, A_n ® "xP が既に証明されていて、R は (T | x)P と書かれます。すると仮定により、a £ ("xP)* = inf{ P* | x*ÎS } £ (T* | x*)P* = R* が成立します。

　次に、当該sequentが ( $ 消去) を用いて得られた場合は、ある A₁ ,¼, A_n ® $xP と A₁ ,¼, A_n , P ® R が既に証明されていて、x は、R にも、どの A_i にも現れません。すると仮定により、任意の解釈に対して、特に x* がどんな値をとっても a £ ($xP)* と aòP* £ R* が成り立ちます。
　一方 ð の定義により後者は P* £ aðR* を意味し、仮定からこの右辺も a も x* に依存しないので、a £ ($xP)* = sup{ P* | x*ÎS } £ aðR* が成り立ち、再度 ð の定義により a = aòa £ R* が成立します。

　次に、当該sequentが ( ^ 消去) を用いて得られた場合は、A₁ ,¼, A_n ® ^ が既に証明されています。すると仮定により a £ ^* = 0 が成り立ちますが、0 は B の最小値なので a = 0 £ R* が成り立ちます。

　最後に、Booleモデルの場合で、用いた推論規則が排中律である場合は、sequent ® P Ú Ø P について (A9-4) を確かめればよく、その右辺は (A9-2e),(A9-3) 及び本文第14節 (14-88b) により (P Ú Ø P)* = P*ñ(ùP*) = 1 となるので明らかに成り立ちます。

　以上で (A9-4) は証明されました。

　以上の結果を用いると、特定のタイプの命題の証明不可能性を導くことができます。
　すなわち、Heytingモデル（Booleモデル）をうまく選んで (A9-4) が成り立たないようにできれば、そのsequentは直観主義論理（古典論理）の述語論理では証明不可能であることがわかるからです。特に

(A9-5a)   ® P が証明可能  Û  P* = 1

(A9-5b)   P ® Q が証明可能  Û  P* £ Q*

が成り立ちます。また

(A9-6)  (Ø^)* = (^ Þ ^)* = 0ð0 = 1

が成り立ちます。

　さて、以下では直観主義論理の体系 T とHeytingモデルのみを考えることにし、集合 S と S-完備Heyting代数の具体例を構成してみましょう。

　まず、S が有限集合の場合を考えます。この場合、B がHeyting代数であれば、S-完備性は自動的に成り立ちます。
　B を順序関係に関して排中律が成り立つ全順序集合とすれば、B はHeyting代数です。実際、x, yÎB に対し、

(A9-7a)  xñy = max{ x, y }

(A9-7b)  xòy = min{ x, y }

(A9-7c)  xðy =

ì í î

1       ( x £ y )  y       ( x > y )

となるからです。特に、

(A9-7d)  ~x :º xð0 =

ì í î

1       ( x = 0 )  0       ( x ¹ 0 )

が成り立ちます。このようなモデルの中で最も単純なのは B = { 0, c, 1 } だけからなる３値論理です。

　３値論理モデルに加えて 0 < a < c かつ 0 < b < c で相互に比較不能な a , b を B に追加すれば、これは全順序集合ではありませんが、

(A9-8a)  xñy =

ì í î

c        ( (x, y) = (a, b), (b, a) )  max{ x, y }      それ以外

(A9-8b)  xòy =

ì í î

0        ( (x, y) = (a, b), (b, a) )  min{ x, y }      それ以外

(A9-8c)  xðy =

ì ï ï í ï ï î

1       ( x £ y )  y       ( x ³ c　かつ　y < x)  b       ( x = a　かつ　y £ b)  a       ( x = b　かつ　y £ a)

となるので、やはりHeyting代数になります。これを便宜的に５値論理とよぶことにします。特に

(A9-8d)  ~x :º xð0 =

ì ï ï í ï ï î

1       ( x = 0 )  b       ( x = a )  a       ( x = b )  0       ( x ³ c )

(A9-8e)  ~~x =

ì í î

1       ( x = c )  x       ( x ¹ c )

が成り立ちます。以下５値論理で考えます（ a, b に言及していないものは３値論理でも成り立ちます）。
　まず

(A9-9a)  P* = c   ならば   (P Ú ØP)* = cñ(~c) = cñ 0 = c

(A9-9b)  P* = c   ならば   ((ØØP) Þ P)* = (~~c)ðc = 1ðc = c

(A9-9c)  P* = c   ならば   ((ØP) Ú (ØØP))* = (~c)ñ(~~c) = 0ñ1 = 1

(A9-9d)  P* = a   ならば   (P Ú ØP)* = añ(~a) = añb = c

(A9-9e)  P* = a   ならば   ((ØØP) Þ P)* = (~~a)ða = aða = 1

(A9-9f)  P* = a   ならば   ((ØP) Ú (ØØP))* = (~a)ñ(~~a) = bña = c

ですから、(A9-5) により

(A9-10a)  ®  (ØØP) Þ P　は証明できない（ ∵ (A9-9b) ）。

(A9-10b)  ®  (ØP) Ú (ØØP)　は証明できない（ ∵ (A9-9f) ）。

(A9-10c)  (ØP) Ú (ØØP)  ®  (ØØP) Þ P　は証明できない（ ∵ (A9-9b),(A9-9c) ）。

(A9-10d)  (ØØP) Þ P  ®  (ØP) Ú (ØØP)　は証明できない（ ∵ (A9-9e),(A9-9f) ）。

(A9-10e)  (ØP) Ú (ØØP)  ®  P Ú ØP　は証明できない（ ∵ (A9-9a),(A9-9c) ）。

(A9-10f)  (ØØP) Þ P  ®  P Ú ØP　は証明できない（ ∵ (A9-9d),(A9-9e) ）。

　一方、第３節メタ定理19、５により (A9-10e) の逆向きは証明可能です。またメタ定理33により (A9-10f) の逆向きも証明可能ですから、古典論理ではすべて同値な命題群：

	ä	(ØØP) Þ P	æ
(A9-11)  P Ú ØP				Ø^
	æ	(ØP) Ú (ØØP)	ä

が、直観主義論理では“命題 A から B へ矢印の向きに沿って到達できる場合の A ® B は証明できるが、そうでない場合は証明できない”ことがわかりました。
　このことから特に、直観主義論理では排中律は証明できない（つまり古典論理は直観主義論理より“真に”強い）ことがわかります。

　また、

(A9-12a)  P* = 1, Q* = c   ならば   (ØØ(P Þ Q))* = ~~(1ðc) = ~~c = 1

(A9-12b)  P* = 1, Q* = c   ならば   (P Þ Q)* = 1ðc = c

(A9-12c)  P* = Q* = c   ならば   (P Þ Q)* = cðc = 1

(A9-12d)  P* = Q* = c   ならば   ((ØØP) Þ Q)* = (~~c)ðc = 1ðc = c

(A9-12e)  P* = Q* = a   ならば   ((ØØP) Þ Q)* = (~~a)ða = aða = 1

(A9-12f)  P* = Q* = a   ならば   ((ØP) Ú Q)* = (~a)ña = bña = c

ですから、(A9-5b) により

(A9-13a)  ØØ(P Þ Q)  ®  P Þ Q　は証明できない（ ∵ (A9-12a),(A9-12b) ）。

(A9-13b)  P Þ Q  ®  (ØØP) Þ Q　は証明できない（ ∵ (A9-12c),(A9-12d) ）。

(A9-13c)  (ØØP) Þ Q  ®  (ØP) Ú Q　は証明できない（ ∵ (A9-12e),(A9-12f) ）。

　一方、第３節メタ定理19により (A9-13a) の逆向きは証明可能、メタ定理19、13により (A9-13b) の逆向きは証明可能、メタ定理15で P にØØP を代入してメタ定理20とメタ定理５を使えば (A9-13c) の逆向きは証明可能ですから、更にメタ定理38 (b) とメタ定理39 (b),(f) により、古典論理ではすべて同値な命題群：

	(ØØP) Þ (ØØQ)
	¯ｭ
	(ØQ) Þ (ØP)
	¯ｭ
(A9-14)  (ØP) Ú Q   ®   (ØØP) Þ Q   ®   P Þ Q   ®	ØØ(P Þ Q)
	¯ｭ
	Ø(P Ù ØQ)
	¯ｭ
	P Þ ØØQ
	¯ｭ
	ØØ((ØP) Ú Q)

が、直観主義論理では“命題 A から B へ矢印の向きに沿って到達できる場合の A ® B は証明できるが、そうでない場合は証明できない”ことがわかりました。

　また、

(A9-15a)  P* = 0, Q* = c   ならば   (P Ú Q)* = 0ñc = c

(A9-15b)  P* = 0, Q* = c   ならば   ((ØP) Þ Q)* = (~0)ðc = 1ðc = c

(A9-15c)  P* = 0, Q* = c   ならば   ((ØQ) Þ P)* = (~c)ð0 = 0ð0 = 1

(A9-15d)  P* = 0, Q* = c   ならば   ((ØØP) Ú (ØØQ))* =(~~0)ñ(~~c) = 0ñ 1 = 1

(A9-15e)  P* = 0, Q* = c   ならば   (ØØ(P Ú Q))* = ~~(0ñc) = ~~c = 1

(A9-15f)  P* = c, Q* = 0   ならば   (P Ú Q)* = cñ 0 = c

(A9-15g)  P* = c, Q* = 0   ならば   ((ØP) Þ Q)* = (~c)ð0 = 0ð0 = 1

(A9-15h)  P* = c, Q* = 0   ならば   ((ØQ) Þ P)* = (~0)ðc = 1ðc = c

(A9-15i)  P* = c, Q* = 0   ならば   ((ØØP) Ú (ØØQ))* =(~~c)ñ(~~0) = 1ñ 0 = 1

(A9-15j)  P* = c, Q* = 0   ならば   (ØØ(P Ú Q))* = ~~(cñ0) = ~~c = 1

(A9-15k)  P* = a, Q* = b   ならば   (P Ú Q)* = añb = c

(A9-15l)  P* = a, Q* = b   ならば   ((ØP) Þ Q)* = (~a)ðb = bðb = 1

(A9-15m)  P* = a, Q* = b   ならば   ((ØQ) Þ P)* = (~b)ða = aða = 1

(A9-15n)  P* = a, Q* = b   ならば   ((ØØP) Ú (ØØQ))* =(~~a)ñ(~~b) = añb = c

(A9-15o)  P* = a, Q* = b   ならば   (ØØ(P Ú Q))* = ~~(añb) = ~~c = 1

ですから、(A9-5b) に加えて、(A9-15k),(A9-15l) 又は (A9-15a),(A9-15c) 又は (A9-15f),(A9-15i) の組み合わせを考えることにより、

(A9-16a)  A　を　(ØP) Þ Q , (ØQ) Þ P , (ØØP) Ú (ØØQ)　のいずれかとするとき、A  ®  P Ú Q　は証明できない。

　また、(A9-5b) に加えて、(A9-15b),(A9-15c),(A9-15d) 又は (A9-15g),(A9-15h),(A9-15i) 又は (A9-15l),(A9-15m),(A9-15n) の組み合わせを考えることにより、

(A9-16b)  A, B　を　(ØP) Þ Q , (ØQ) Þ P , (ØØP) Ú (ØØQ)　の中から任意に選んだ異なる２命題とするとき、A  ®  B　は証明できない。

　また、(A9-5b) に加えて、(A9-15b),(A9-15e) 又は (A9-15h),(A9-15j) 又は (A9-15n),(A9-15o) の組み合わせを考えることにより、

(A9-16c)  B　を　(ØP) Þ Q , (ØQ) Þ P , (ØØP) Ú (ØØQ)　のいずれかとするとき、ØØ(P Ú Q)  ®  B　は証明できない。

　一方、第３節メタ定理26、19、５により (A9-16a) の逆向きは証明可能です。また Ø(P Ú Q) を仮定すると、メタ定理31により (A9-16c) の B とはいずれにせよ矛盾するので、(A9-16c) の逆向きも証明可能ですから、古典論理ではすべて同値な命題群：

		(ØP) Þ Q
	ä		æ
(A9-17)  P Ú Q	®	(ØØP) Ú (ØØQ)	®	ØØ(P Ú Q)  «  Ø((ØP) Ù (ØQ))  «  Ø((ØØØP) Ù (ØØØQ))  «  ØØ((ØØP) Ú (ØØQ))
	æ		ä
		(ØQ) Þ P

が、直観主義論理では“命題 A から B へ矢印の向きに沿って到達できる場合の A ® B は証明できるが、そうでない場合は証明できない”ことがわかります。ただし右の４個の命題の同値性は、メタ定理20とメタ定理31から従います。

　また、

(A9-18a)  P* = Q* = c   ならば   (P Ù Q)* = còc = c

(A9-18b)  P* = Q* = c   ならば   ((ØØP) Ù (ØØQ))* =(~~c)ò(~~c) = 1ò1 = 1

ですから、(A9-5b) により(ØØP) Ù (ØØQ)  ®  P Ù Q は証明できないことがわかります。
　一方、この逆向きは第３節メタ定理19、５により証明可能ですから、更にメタ定理38 (a) とメタ定理39 (b),(f) により、古典論理ではすべて同値な命題群：

	Ø((ØP) Ú (ØQ))
	¯ｭ
	Ø(P Þ (ØQ))
	¯ｭ
(A9-19)  P Ù Q  ®	(ØØP) Ù (ØØQ)
	¯ｭ
	Ø(Q Þ (ØP))
	¯ｭ
	ØØ(P Ù Q)

が、直観主義論理では“命題 A から B へ矢印の向きに沿って到達できる場合の A ® B は証明できるが、そうでない場合は証明できない”ことがわかりました。

　また、

(A9-20a)  P* = a, Q* = b   ならば   ((ØP) Ú (ØQ))* = (~a)ñ(~b) = bña = c

(A9-20b)  P* = a, Q* = b   ならば   (Ø(P Ù Q))* = ~(aòb) = ~0 = 1

ですから、(A9-5b) により Ø(P Ù Q)  ®  (ØP) Ú (ØQ) は証明できないことがわかります。
　一方、メタ定理15で Q に ØQ を代入し、メタ定理28を使えば、古典論理ではすべて同値な命題群：

	P Þ (ØQ)
	¯ｭ
(A9-21)  (ØP) Ú (ØQ)  ®	Ø(P Ù Q)
	¯ｭ
	Q Þ (ØP)

が、直観主義論理では“命題 A から B へ矢印の向きに沿って到達できる場合の A ® B は証明できるが、そうでない場合は証明できない”ことがわかりました。

　また、

(A9-22a)  P* = c, Q* = 0   ならば   (P Ù ØQ)* = cò(~0) = cò1 = c

(A9-22b)  P* = c, Q* = 0   ならば   (Ø(P Þ Q))* = ~(cð0) = ~0 = 1

ですから、(A9-5b) により Ø(P Þ Q)  ®  P Ù ØQ は証明できないことがわかります。
　一方、メタ定理19、５、34を使えば、古典論理ではすべて同値な命題群に対する関係：

	(ØØP) Ù (ØQ)
	¯ｭ
(A9-23)  P Ù (ØQ)  ®	Ø(P Þ Q)
	¯ｭ
	Ø((ØP) Ú Q)

が、直観主義論理では“命題 A から B へ矢印の向きに沿って到達できる場合の A ® B は証明できるが、そうでない場合は証明できない”ことがわかりました。

　さて、上記のモデルにおいて、更に S は２個の元からなる集合 {a, b} とします。このとき、("xP)* と (a | x*)P*ò(b | x*)P* および ($xP)* と (a | x*)P*ñ(b | x*)P* はそれぞれ等しいので、Ù と Ú に関する証明不可能性からそれぞれ " と $ に関する証明不可能性が導かれます。この事実を用いると、古典論理ではすべて同値な命題群：

(A9-24a)  $xP  ®  $xØØP  ®  ØØ$xP  «  Ø"xØP  «  Ø"xØØØP  «  ØØ$xØØP

(A9-24b)  "xP  ®  "xØØP  «  Ø$xØP

(A9-24c)  $xØP  ®  Ø"xP

が、直観主義論理では“命題 A から B へ矢印の向きに沿って到達できる場合の A ® B は証明できるが、そうでない場合は証明できない”ことがわかります。
　実際、証明不可能性の方は、(A9-17),(A9-19),(A9-21) がそれぞれ (A9-24a),(A9-24b),(A9-24c) に対応しています。
　一方、証明可能性の方は、(A9-24a) と (A9-24b) の最初の ® はメタ定理19により証明され、(A9-24a) の２番目の ® は、メタ定理6 (b) の P に Ø$P を代入したものとメタ定理37 (a) の対偶により証明され、(A9-24c) の ® はメタ定理37 (b) そのものであり、残る « は、メタ定理37 (a) とメタ定理20から証明されます。

　さて、(A9-17) と (A9-24a) により、(ØØP) Ú (ØØQ) と $xØØP は、いずれも二重否定を取ったものとそれ自身が同値でない（両者を Û で結んだ命題が証明できないことを意味することにします）ことがわかります。これは、付録２の記法でいうと P˜ Ú Q˜ と P˜ Ú˜ Q˜ が同値でなく、$xP˜ と $˜xP˜ が同値でないことを意味するので、付録２の (A2-25) は論理記号 s が Ú , $ の場合は成り立たないことがわかりました。

　次に第３節メタ定理39,40に掲げた残りの命題が直観主義論理で証明不可能であることを確かめます。

　まずメタ定理39 (h) の P Þ (Q Ú R) と (P Þ Q) Ú R の非同値性ですが、これらは Q に ^ を代入すると、それぞれ P Þ R と (ØP) Ú R になるので (A9-14) から明らかです。
　また、P* = a , Q* = b ならば、

(A9-25)  ((P Þ Q) Ú (Q Þ P))* = (aðb)ñ(bða) = bña = c

ですから、メタ定理39 (i) の (P Þ Q) Ú (Q Þ P) は直観主義論理では証明不可能です。
　また、(P Ú Q) Þ P と Q Þ P は同値ですから、上記の結果により ((P Ú Q) Þ P) Ú ((P Ú Q) Þ Q) は証明不可能です。よって、集合 S が２点からなるモデルで考えれば、(A9-24) の証明不可能性と同じ論法で、メタ定理40 (c) の命題 $x($xP Þ P) の証明不可能性がわかります。

　残るはメタ定理39 (k) の、x が Q に現れない自由変数のときの、("xP) Ú Q と "x(P Ú Q) の非同値性ですが、これを S が２点の集合のモデルを使って " を Ù の場合に還元して示そうとしても、対応する (P Ù P' ) Ú Q と (P Ú Q) Ù (P' Ú Q) が同値ですからうまくいきません。
　かといって S を無限集合にするのは、（メタ言語に排中律を仮定していないため）今度は B の S-完備性が保証されません。

　そこで位相モデルというものを導入します。B を位相空間 X の開集合全体からなる集合とし、包含関係で順序を入れます。すると、これは任意の部分集合に対して上限を持ちます。また、B の元 a , b に対し、

(A9-26)  aðb :º È{ cÎB | cÇa Ì b }

と置くと、第５節 (5-12a) により

(A9-27)  aÇ(aðb) = aÇ( È{ cÎB | cÇa Ì b }) = È{ aÇc | cÎB  Ù  cÇa Ì b } Ì b

が成り立つので、B は完備Heyting代数になります。このような B によるモデルを位相モデルといいます。
　位相モデルでは、A Ì B に対して sup A = ÈA であり、a, bÎB に対して inf {a, b} = aÇb ですが、inf A = (ÇA)° であることに注意します。

　早速 S を自然数の全体 N 、X を有理数の全体 Q として応用してみましょう。x は命題 P に現れる変数で、かつ命題 Q には現れないものとします。このとき各 x*ÎN に対して

(A9-28a)  P* :º { r ÎQ | r < 1/x* } ÎB

(A9-28b)  Q* :º { r ÎQ | r > 0 } ÎB

と置けば、

(A9-29a)  ("x(P Ú Q))* = ( Ç{ (P Ú Q)* | x*ÎN } )° = ( Ç{ P*ÈQ* | x*ÎN } )° = ( Ç{ Q | x*ÎN } )° = Q

(A9-29b)  (("xP) Ú Q)* = ( Ç{ P* | x*ÎN } )° È Q* = { r ÎQ | r < 0 } È { r ÎQ | r > 0 } = { r ÎQ | r ¹ 0 } ¹ Q

となり、"x(P Ú Q) と ("xP) Ú Q は直観主義論理では同値でないことがわかりました。

　もう一つの例として、"xØØP と ØØ"xP の非同値性を証明してみましょう。これも (A9-19) により、３値論理や５値論理のモデルで示すのは無理な例です。今度は S , X を共に Q とします。このとき各 x*ÎQ に対して

(A9-30)  P* :º { r ÎQ | r ¹ x* } ÎB

と置けば、

(A9-31a)  ~{ r ÎQ | r ¹ x* } :º { r ÎQ | r ¹ x* }ðÆ = Æ

(A9-31b)  ~Æ = ÆðÆ = Q

(A9-31c)  ~Q = QðÆ = Æ

ですから

(A9-32a)  ("xØØP)* = ( Ç{ (ØØP)* | x*ÎQ } )° = ( Ç{ ~~P* | x*ÎQ } )° = ( Ç{ Q | x*ÎQ } )° = Q

(A9-32b)  (ØØ"xP)* = ~~( Ç{ P* | x*ÎQ } )° = ~~Æ = Æ

となり、"xØØP と ØØ"xP は直観主義論理では同値でないことがわかりました。