雑録

---

『量子論理の限界』について ( IV )

1. 形而上学（あるいは超‐物理学）　(Meta-physics)
2. 自然哲学者のための量子力学 ( I )　(Quantum mechanics for natural philosophers ( I ))
3. 波動‐粒子の２重性　(Wave-particle duality)
4. コペンハーゲン解釈 ( I )　(The Copenhagen interpretation ( I ))
5. コペンハーゲン解釈 ( II )　(The Copenhagen interpretation ( II ))
6. 自然哲学者のための量子力学 ( II )　(Quantum mechanics for natural philosophers ( II ))
7. 射影公準　(Projection postulates)
8. 非局所性と隠れた変数　(Nonlocality and hidden variables)
9. 使い勝手の量子論理　(A user-friendly quantum logic)
10. 量子論理　(Quantum logic: what it can and can't do)

*

　第九章では、「NDQL」と呼ばれる量子命題論理の形式系が導入される。論理の形式化には色々なやり方が在るが、ギビンズは、ゼクヴェンツを用いる自然演繹法を採用している。ここでは、直観的に把握しやすい（と思われる）証明図に依るスタイルで、それを定式化しなおしてみる。
　まず、Σ を適当な記号からなる可算無限集合として、Σ の要素を文記号と呼ぶことにする。（論理の形式系は汎用であるべきだから、ELQM の基本文のような具体的な文を所与の素材とする訳にはいかない。そこで、基本文のダミーとして文記号を用いる訳だ。）文記号と論理結合子「¬」、「∧」、「∨」、「⇒」、そして区切り記号としての括弧「 ( 」、「 ) 」が NDQL の基本記号だ。
　通常の文に相当するのは、基本記号を適宜組み合わせて得られる記号列だ。それらを「式」と呼ぶ。式は次のように帰納的に定義することができる。

• 文記号は式である。
• φ が式ならば ¬φ は式である。（つまり、式に「¬」を接頭したものもまた式である。）
• φ と ψ が式ならば (φ ∧ ψ ) は式である。（つまり、式と式を「∧」で接続し括弧でくくったものもまた式である。）
• φ と ψ が式ならば (φ ∨ ψ ) は式である。
• φ と ψ が式ならば (φ ⇒ ψ ) は式である。
• 以上によって得られるものだけが式である。

（この定義はボトムアップ流で構成的だが、式全体の集合を、いわば超越的に、基本記号からなる有限列全体の集合の或る特殊な部分集合として規定することもできる。）
　有限箇の式からなる（空であり得る）集合とひとつの式の順序対をゼクヴェンツと云う。（「ゼクヴェンツ」はドイツ語の「Sequenz」の音訳。この語は、もともと、ゲンツェンによって、式の有限列の順序対を表わすのに用いられたものだそうで、英語では、「sequence」が列を意味するため、「sequent」が当てられている。）ゼクヴェンツの第一の要素（つまり式の集合）を前提と云い、第二の要素を帰結と云う。
　以下では、式を「φ」等のギリシア小文字で表わし、有限箇の式からなる（空であり得る）集合を「Γ」等の大文字で表わす。特に空集合は「{ }」で表わす。このような、形式系の記号列等を代表する記号をメタ記号と云う。論理結合子および括弧に対しては、それら自体をメタ記号として流用する。また、前提 Γ と帰結 φ をもつゼクヴェンツを「Γ├ φ」と表わす。こうしたメタ記号からなる表現をスキーマと云う。（先の式の定義もスキーマに依っていた訳だ。）
　厳格な形式化は徒にことを煩瑣にしてしまうので、略式で行くことにすれば、NDQL の公理と推論規則は、スキーマを用いて次のように表わせる。

					A （公理スキーマ）						{φ }├ φ
					MP （モドゥス・ポネンス）						Γ├ (φ ⇒ ψ )　　Δ├ φ Γ ∪Δ├ ψ
					MT （モドゥス・トレンス）						Γ├ (φ ⇒ ψ )　　Δ├ ¬ψ Γ ∪Δ├ ¬φ
					DN （二重否定）						Γ├ φ　  Γ├ ¬¬φ Γ├ ¬¬φ  　Γ├ φ
					∧I （∧導入）						Γ├ φ　　Δ├ ψ   Γ ∪Δ├ (φ ∧ ψ )
					∧E （∧除去）						Γ├ (φ ∧ ψ ) Γ├ φ Γ├ (φ ∧ ψ ) Γ├ ψ
					∨I （∨導入）						Γ├ φ　　  Γ├ (φ ∨ ψ )  　　Γ├ ψ　　  Γ├ (φ ∨ ψ )
					∨E （∨除去）						Γ├ (φ ∨ ψ )　　{φ }├ χ　　{ψ }├ χ Γ├ χ
					CP （条件化）						{φ }├ ψ 　  { }├ (φ ⇒ ψ )
					RAA （帰謬法）						{φ }├ (ψ ∧ ¬ψ ) { }├ ¬φ
					D1 （定義 1）						(φ ⇒ ψ ) ≡def (¬φ ∨ (φ ∧ ψ ))
					D2 （定義 2）						(φ ⇔ ψ ) ≡def ((φ ⇒ ψ ) ∧ (ψ ⇒ φ ))

ちなみに、∨E、CP、RAA を、次の ∨ES、CPS、RAAS で置き換えれば、古典命題論理の自然演繹系が得られ、さらに、DN を ¬E で置き換えれば構成的命題論理――またの名を「直観主義命題論理」――の自然演繹系が得られる。

∨ES （標準的∨除去）

Γ├ (φ ∨ ψ )　　Δ├ χ　　Θ├ χ Γ ∪ (Δ - {φ }) ∪ (Θ - {ψ })├ χ

CPS （標準的条件化）

Γ├ ψ 　　　  Γ - {φ }├ (φ ⇒ ψ )

RAAS （標準的帰謬法）

Γ├ (ψ ∧ ¬ψ ) Γ - {φ }├ ¬φ

¬E （否定除去）

Γ├ (φ ∧ ¬φ ) Γ├ ψ

（ただし、「Γ - {φ }」は Γ に関する {φ } の補集合（つまり Γ から φ を除いた集合）を表わす。）公理スキーマは、そのスキーマの具体例であるゼクヴェンツ（つまり、ひとつの式だけからなる集合を前提としてもち、件の式と同一の式を帰結としてもつゼクヴェンツ）は何れも公理であることを表わしている。推論規則を表わしているのは、MP から RAA であり、これらの図は、横棒の上の一つないし三つのスキーマの具体例であるゼクヴェンツから、下のスキーマに当てはまるゼクヴェンツが導びけることを意味する。また、D1 は、「≡_def 」の両辺のどちらか一方のスキーマの具体例である式を帰結としてもつどんなゼクヴェンツについても、件の式を他方のスキーマに当てはまる式で置き換えていいということを表わしている。一方、D2 は、新たな記号「⇔」を導入し、「≡_def 」の右辺のスキーマの具体例である式の代替物として左辺のスキーマに当てはまる記号列を用いていいということを表わしている。なお、形式系に係わる定義は、通常、この D2 のように、基本記号ではない別の記号を導入するために設けられる。その点、D1 は基本記号にあらためて定義を与えていて変則的だ。そんなことをしなくても

Γ├ (φ ⇒ ψ ) 　　  Γ├ (¬φ ∨ (φ ∧ ψ ))

Γ├ (¬φ ∨ (φ ∧ ψ )) Γ├ (φ ⇒ ψ )

を推論規則として採れば済むように思えるのだが、ここはギビンズによる定式化に従っておいた。
　NDQL における証明は、公理を推論規則と定義 1 に従って変換していく有限のステップの有限の組み合わせからなる。形式的には、証明は、ゼクヴェンツによってラベル付けられた特殊なツリーとして規定できる。その葉のラベルは何れも公理で、ラベルの間には推論規則と定義 1 に則った関係が在って、それが対応する節の間の関係と同型になっているような有限ツリーだ。そうしたツリーを証明ツリーと云う。Γ├ φ を根のラベルとしてもつ証明ツリーが在るとき、Γ├ φ は証明可能であると云われ、{ }├ φ が証明可能なとき、 φ は証明可能であると云われる。
　証明ツリーを図式化すれば証明図が得られる。また、公理スキーマや推論規則を、個別のゼクヴェンツではなく、ゼクヴェンツのスキーマに適用した証明図を考えることもできる。例えば、排中律スキーマ「(φ ∨ ¬φ )」の証明図は次のようになる。（なお、以下では、式のスキーマの外側の括弧は省くことにする。） （左のブランチでは、公理スキーマが CP に則って変換され、さらに D1 に則って変換される。真ん中のブランチでは、（同一の式のスキーマを「├ 」の両辺にもつ点で）公理スキーマと同型のスキーマが ∨I に則って変換され、右のブランチでは、公理スキーマと同型のもうひとつのスキーマが ∧E に則って変換され、さらに ∨I に則って変換される。そして、三つの結果が ∨E に則って変換され、求めるスキーマが得られる。）この証明図は、排中律スキーマの具体例である（可算無限箇の）式の証明をひと括りに表わしているものと看做せる。もうひとつ、例として、ド・モーガンの法則のひとつを表わすスキーマ「¬(φ ∧ ψ ) ⇔ (¬φ ∨ ¬ψ )」の証明図をいくつかに分けて示してみる。 （まず、(a) では、左のブランチで公理スキーマと同型のスキーマが ∨I に則って変換され、さらに CP に則って変換される。そして、その結果と公理スキーマと同型のもうひとつのスキーマが MT に則って変換され、さらに DN に則って変換される。(b) も同様であり、それらの結果が (c) で ∧I に則って変換される。一方、(d) と (e) の結果は (f) で ∨E に則って変換される。そして、(c) と (f) の結果が (g) で ∧I に則って変換される。その結果に D2 を適用すれば、求めるスキーマが得られる訳だ。）ところで、一度このスキーマを証明してしまえば、それを介して（∧E と MP によって）Γ├ ¬(φ ∧ ψ ) から Γ├ ¬φ ∨ ¬ψ が導けるし、Γ├ ¬φ ∨ ¬ψ から Γ├ ¬(φ ∧ ψ ) を導くこともできる。そこで、そのことを、

Γ├ ¬(φ ∧ ψ ) Γ├ ¬φ ∨ ¬ψ

Γ├ ¬φ ∨ ¬ψ Γ├ ¬(φ ∧ ψ )

と表わして、推論規則のように考えることができる。こうした規則もどきを派生的規則という。（スキーマからなる証明図はあくまでインフォーマルな証明であり、派生的規則もまたインフォーマルな規則であることに注意しなければならない。）

　次はNDQL の意味論だ。ギビンズはそれをきちんと提示していないが、おおよそのことは示唆されているので、それをもとに、以下にひとつの意味論を定式化してみる。
　量子命題論理の意味論のためには、（古典命題論理の場合と違って）真理値表は役にたたないので、別の道具が要る。そのひとつが直モジュラ束だ。
　はじめに、NDQL では、{φ, ψ }├ χ が証明可能なことと {φ ∧ ψ }├ χ が証明可能なことは同等であり、また、{φ }├ ψ が証明可能なことと φ ⇒ ψ が証明可能なことと ((φ ∧ ψ ) ⇒ φ ) ∧ (φ ⇒ (φ ∧ ψ )) が証明可能なことは同等である一方、直モジュラ束 Ω においては、a ≦ b となることと a^⊥∨_Ω (a ∧_Ωb ) = 1 となることは同等であることを示しておく。
　まず、{φ, ψ }├ χ が証明可能だとすれば、証明ツリーの葉は何れも公理であり、その前提はひとつの式しかもたない訳だから、前提 {φ } をもつゼクヴェンツと前提 {ψ } をもつゼクヴェンツが MP か MT か ∧I の何れかによって前提 {φ, ψ } をもつゼクヴェンツに変換されるステップが在ることになる。それが、例えば、

{φ }├ α ⇒ β　　{ψ }├ α
{φ, ψ }├ β

という形だとすれば、これを で置き換え、さらに、後続のステップにおけるゼクヴェンツの前提 {φ, ψ } を {φ ∧ ψ } で置き換える。同様の操作を、前提 {φ } をもつゼクヴェンツと前提 {ψ } をもつゼクヴェンツが前提 {φ, ψ } をもつゼクヴェンツに変換される凡てのステップについて施せば、{φ ∧ ψ }├ χ の証明図が得られることになる。逆に、{φ ∧ ψ }├ χ が証明可能だとすれば、 よって、 {φ, ψ }├ χ が証明可能だ。また、{φ }├ ψ が証明可能ならば CP によって φ ⇒ ψ が証明可能であり、逆に、φ ⇒ ψ が証明可能ならば、これと {φ }├ φ から MP により {φ }├ ψ が証明可能だ。さらに、(φ ∧ ψ ) ⇒ φ は、{φ ∧ ψ }├ φ ∧ ψ から ∧E と CP によって、仮定なしに証明可能である一方、{φ }├ ψ が証明可能ならば、これと {φ }├ φ から ∧I と CP により φ ⇒ (φ ∧ ψ ) が証明可能だから、結局、{φ }├ ψ が証明可能ならば ((φ ∧ ψ ) ⇒ φ ) ∧ (φ ⇒ (φ ∧ ψ )) が証明可能であり、逆に、((φ ∧ ψ ) ⇒ φ ) ∧ (φ ⇒ (φ ∧ ψ )) が証明可能ならば、φ ⇒ (φ ∧ ψ ) が証明可能だから、これと {φ }├ φ から MP と ∧E により {φ }├ ψ が証明可能だ。次に、直モジュラ束 Ω において、a ≦ b とすれば、交わりの演算 ∧_Ω の属性（あるいは ≦ の定義）から a ∧_Ωb = a、よって、第六章に示されている直相補束の属性（９）と交換律から、

a^⊥∨_Ω (a ∧_Ωb ) = a^⊥∨_Ω a = 1

逆に、a^⊥∨_Ω (a ∧_Ωb ) = 1 とすれば、（７）と ∧_Ω の属性から

a ∧_Ω(a^⊥∨_Ω (a ∧_Ωb )) = a ∧_Ω1 = a

一方、束の属性（１）から a ∧_Ωb ≦ a、また、反射律から a^⊥≦ a^⊥、したがって、直モジュラ律により

a ∧_Ω(a^⊥∨_Ω (a ∧_Ωb )) = a ∧_Ωb

よって、a ∧_Ωb = a、したがって、（２）から a ≦ b。（直モジュラ律は、第六章において、

c ≦ a かつ b ≦ a^⊥ならば、a ∧ (b ∨ c ) = (a ∧ b ) ∨ (a ∧ c )

として定式化されていたが、b ≦ a^⊥ならば、∧ の属性から b ∧ a^⊥= b、よって、結合律と交換律そして（１０）と（８）から

b ≦ a^⊥ならば a ∧ b = a ∧ (b ∧ a^⊥) = b ∧ (a ∧ a^⊥) = b ∧ 0 = 0

また、c ≦ a ならば a ∧ c = c、よって、∨ の属性から

c ≦ a かつ b ≦ a^⊥ならば、(a ∧ b ) ∨ (a ∧ c ) = 0 ∨ c = c

したがって、直モジュラ律は、

c ≦ a かつ b ≦ a^⊥ならば、a ∧ (b ∨ c ) = c

として定式化することもできる。）
　そこで、f を文記号全体の集合 Σ から直モジュラ束 Ω への写像として、式全体の集合 Φ から Ω への写像 J_f を次のように定義する。

• φ が文記号ならば J_f (φ ) = f (φ )
• J_f (¬φ ) = J_f (φ )^⊥
• J_f (φ ∧ ψ ) = J_f (φ ) ∧_ΩJ_f (ψ )
• J_f (φ ∨ ψ ) = J_f (φ ) ∨_ΩJ_f (ψ )
• J_f (φ ⇒ ψ ) = J_f (¬φ ∨ (φ ∧ ψ ))

こうした写像を解釈と呼ぶことにすれば、式の恒真性は次のように定義できる。

φ が恒真であるとは、どんな直モジュラ束 Ω および Ω への解釈 J についても J (φ ) = 1 となることを云う。

また、ゼクヴェンツの恒真性を次のように定義する。

空でない前提をもつゼクヴェンツ {φ₁, . . . , φ_n }├ ψ が恒真であるとは、どんな直モジュラ束 Ω および Ω への解釈 J についても J (( . . . (φ₁∧φ₂) ∧ . . . ) ∧ φ_n ) ≦ J (ψ ) となることを云い、空な前提をもつゼクヴェンツ { }├ φ が恒真であるとは φ が恒真であることを云う。

（これらの定義が整合的なことは、先に示しておいたことがらから判る。）
　ちなみに、古典命題論理の形式系に関しても、直モジュラ束の替わりにブール束を採れば、上と同様に意味論が展開できるが、その場合には、しかし、式 φ の恒真性は、1 と 0 だけを要素としてもつブール束 B₂ へのどんな解釈 J についても J (φ ) = 1 となることに還元できる。これは、古典命題論理が真理値表だけですっかり規定できてしまうことに対応している。（否定および連言と選言についての真理値表は B₂ の直補演算および交わりと結びの演算を規定する表と同型だ。）
　一般に、論理の形式系は、それにおいて証明可能な式が凡て恒真であるとき健全であると云われ、恒真な式が凡て証明可能であるとき完全であると云われる。NDQL は健全かつ完全だ。健全性は、公理の恒真性および凡ての推論規則が恒真性を保存することを示すことによって証明できる。例として、MT をとってみれば次のようになる。
　ゼクヴェンツの前提がひとつの式からなる場合を考えれば十分だから、{α }├ φ ⇒ ψ と {β }├ ¬ψ が恒真、つまり、J を任意の解釈として次が成り立つとする。

J (α ) ≦ J (φ )^⊥∨_Ω (J (φ ) ∧_ΩJ (ψ )),　　J (β ) ≦ J (ψ )^⊥

すると、第六章に示されている束の属性（１）、（２）、（５）から

J (α ) ∧_ΩJ (β ) ≦ J (α ) ≦ J (φ )^⊥∨_Ω (J (φ ) ∧_ΩJ (ψ ))
J (α ) ∧_ΩJ (β ) ≦ J (β ) ≦ J (φ )^⊥∨_ΩJ (ψ )^⊥

さらに（３）から

J (α ) ∧_ΩJ (β ) ≦ (J (φ )^⊥∨_ΩJ (ψ )^⊥) ∧_Ω(J (φ )^⊥∨_Ω (J (φ ) ∧_ΩJ (ψ )))

ところが、J (φ ) ∧_ΩJ (ψ ) ≦ J (φ ) から、直相補束の属性（１１）により、J (φ )^⊥≦ (J (φ ) ∧_ΩJ (ψ ))^⊥、同様に、J (φ ) ∧_ΩJ (ψ ) ≦ J (ψ ) から J (ψ )^⊥≦ (J (φ ) ∧_ΩJ (ψ ))^⊥、よって、（６）により J (φ )^⊥ ∨_ΩJ (ψ )^⊥≦ (J (φ ) ∧_ΩJ (ψ ))^⊥、したがって、（１１）と（１２）から

J (φ ) ∧_ΩJ (ψ ) ≦ (J (φ )^⊥∨_ΩJ (ψ )^⊥)^⊥

一方、J (φ )^⊥≦ J (φ )^⊥∨_ΩJ (ψ )^⊥、よって 、直モジュラ律により

J (α ) ∧_ΩJ (β ) ≦ (J (φ )^⊥∨_ΩJ (ψ )^⊥) ∧_Ω(J (φ )^⊥∨_Ω (J (φ ) ∧_ΩJ (ψ ))) ≦ J (φ )^⊥

したがって、{α, β }├ ¬φ は恒真であり、 MT は恒真性を保存する。
　一方、完全性を証明するには、証明可能でない式は恒真でないこと、云い換えれば、式 φ が証明可能でないならば J (φ ) ≠ 1 となる解釈 J が在ることを示せばいい。それにはいわゆるリンデンバウム代数が利用できる。
　以下では「φ ⇔ ψ」をもっぱら「(φ ⇒ ψ ) ∧ (ψ ⇒ φ )」の略記として用いることにして、「φ ⇔ ψ が証明可能である」という関係を考えると、これは NDQL の式全体の集合 Φ 上の同値関係になる。そこで、Ω をこの関係による Φ の分割として、φ の同値クラスを「〔φ〕」と表わすことして、Ω 上の演算 ^⊥、∧_Ω、∨_Ωを次のように定義する。

〔φ〕^⊥= 〔¬φ〕,　　〔φ〕 ∧_Ω〔ψ〕 = 〔φ ∧ ψ〕,　　〔φ〕 ∨_Ω〔ψ〕 = 〔φ ∨ ψ〕

（これらの定義が有効なためには、φ ⇔ ψ が証明可能ならば、¬φ ⇔ ¬ψ も証明可能で、さらに α ⇔ β が証明可能ならば、(φ ∧ α ) ⇔ (ψ ∧ β ) および (φ ∨ α ) ⇔ (ψ ∨ β ) も証明可能であることが示される必要があるが、その辺は端折ることにする。） Ω 上の順序 ≦ は、通常の束の場合と同様、次のように定義できる。

a ≦ b ≡_def a ∧_Ωb = a

（ {φ }├ ψ が証明可能であることと (φ ∧ ψ ) ⇔ φ が証明可能であることは同等だから、〔φ〕 ≦ 〔ψ〕 となることと {φ }├ ψ が証明可能であることは同等だ。） また、文記号 σ をひとつ固定して、1 と 0 を次のように定義する。

1 = 〔σ ∨ ¬σ〕,　　0 = 〔σ ∧ ¬σ〕

すると、これらによって Ω は直モジュラ束となる。（一般に、このようにして論理の形式系から得られる代数系をリンデンバウム代数と云う。） Ω では直モジュラ律が成り立つことだけを次に示しておく。
　〔χ〕 ≦ 〔φ〕 かつ 〔ψ〕 ≦ 〔φ〕^⊥ とすれば、{χ }├ φ および {ψ }├ ¬φ が証明可能だから、 よって、〔φ〕 ∧_Ω(〔ψ〕 ∨_Ω〔χ〕) = 〔χ〕。
　これで完全性が示せる。まず、式全体の集合 Φ から Ω への写像 J を

J (φ ) = 〔φ〕

として定義すれば、J は解釈となる。そこで、ψ を証明可能でない式とすれば、ψ ⇔ (σ ∨ ¬σ ) は証明可能ではない。（ σ ∨ ¬σ は証明可能だから、もし (σ ∨ ¬σ ) ⇒ ψ が証明可能だとすれば、モドゥス・ポネンスにより ψ が証明可能となって矛盾をきたす。）したがって、J (ψ ) = 〔ψ〕≠〔σ ∨ ¬σ〕 = 1。

　なお、量子述語論理については、２４５から２４６ページ目にかけて、次のようなくだりがある。

古典論理のように、（量子的）普遍量化子 (universal quantifier) は連言のように振舞い、（量子的）存在量化子 (existential quantifier) は選言のように振舞う。「∧」と「∨」についての四つの導入規則と消去規則のうち、「∨E」だけが非古典的なので、量化子規則のうち、「存在量化子消去」だけが非古典的であろうことが考えられる。事実、量子論理において存在量化子消去は、「∨E」とまったく同じ仕方で制限されているのである。
　・ ・ ・ 古典的規則は、すでにあらたまってこういうには及ばない。すなわち、いくつかの前提 Γ に基づいて、存在的限量命題「(∃x )Px 」が証明されたと仮定せよ。換言すれば、Γ├ (∃x )Px が証明されたと仮定せよ、である。ゆえに Γ が与えられていれば、われわれが知らなくても、「P 」はある個体について真となるであろう。したがって、「P 」が真である個体を a とし、「a 」で表そう――「a 」は任意の名辞であり、変項のことも定項のこともまったく語っていない。「Pa 」を仮定したとき、もしわれわれが追加諸前提 Γ₁の（あるいは空）集合を用いて結論 C を導くことができるならば、われわれは Γ, Γ₁├ C を推論することができる。すなわち、Γ と Γ₁のどちらも与えられていれば、われわれは C を導くことができるのである。なぜなら、C の導出において、対象 a「P 」のどちらが真であったかは問題ではないからである。さらに、Γ₁に課される制限がある。すなわち、「a 」は Γ₁に現れるべきではない。
　最後の量子論理的制限はいままでと異なっており、より厳しいものである。それは、Γ₁が空でなければならないことである。すでに言及したことを思い出せば、∨E を制限することの意味は、分配律を導出できなくすることにある。
　存在量化子について制限することの意味は、存在量化子 (∃x )Px ∧ (∃y )Qy├ (∃x )(∃y )(Px ∧ Qy ) にかんして「∧」の分配を止められることにある。

　原文は次の通り。

As in classical logic, the (quantum) universal quantifier behaves like conjunction and the (quantum) existential quantifier like disjunction. Of the four introduction and elimination rules for & and ∨, only ∨E is nonclassical, so we can expect that of the quantifier rules only ‘existential quantifier elimination’ will be nonclassical. In fact, in quantum logic it is restricted in exactly the same way ∨E is.
　 The clasical rule . . . is already tedious enough to state: suppose you have proved an existentially quantified proposition (Ex )Px on the basis of some premises Γ. In other words, you have proved

Γ├ (Ex )Px

Then given Γ, P is going to be true of some individual though we do not know of which. So let the individual of which P is true be a, named by a where a is an arbitrary name, strictly speaking neither a variable nor a constant. If, having asuumed Pa, we can, with a set (possibly empty) of additional premises Γ₁, derive a conclusion C which is independent of a, then we can infer that

Γ, Γ₁├ C.

That is, given both Γ and Γ₁, we can derive C because in deriving C it does not matter which object a P was true of. There is a further restriction to be placed on Γ₁, namely that a should not occur in Γ₁.
　 The final quantum logical restriction is different, and more severe. It is that Γ₁ has to be empty. The effect of restricting ∨E is, as we recall, to make the distributive law underivable. The effect of the restriction on the existential quantifier is to block the distribution of & over the existential quantifier

(Ex )Px & (Ey )Qy├ (Ex )(Ey )(Px & Qy ). (p.140f)

　これは次のような意味だろう。（ただし、適宜修正を加えた。）

古典論理においてと同様、（量子的）普遍量化子は連言［の論理結合子］のように振る舞い、（量子的）存在量化子は選言のように振る舞う。∧ および ∨ に関する導入規則と除去規則で非古典的なのは ∨E だけだから、量化規則のうち「存在量化子除去」だけが非古典的なことが予想できる。実際、量子論理において、件の規則は ∨E の場合と全く同様に制限される。
　その古典的規則は ・ ・ ・ あらためて述べるまでもないが、次の通りだ。或る前提 Γ にもとづいて存在量化命題 ∃x Px が証明されているとする。云い換えれば、

Γ├ ∃x Px

が証明済みだとする。すると、Γ を仮定すれば、P は何らかの個体について、仮令その個体を我々が知らなくとも、真であることになる。件の個体を a とし、それを a と名付ける。a は任意の名辞であり、厳密に云えば、変数でも定数でもない。そこで、付加的前提の（空であり得る）集合 Γ₁とともに Pa を仮定して、a に依存しない結論 C を導くことができれば、

Γ, Γ₁├ C

と推論できる。つまり、P がどの対象 a について真なのかは C を導くのに関わらない訳だから、Γ および Γ₁を仮定すれば C を導くことができる。ただし、 Γ₁には、a がそこに現われてはならないという制限が加えられる必要がある。
　量子論理における最後の制限は、それとは別で、そして、もっと厳しい。それは、Γ₁が空でなければならないというものだ。承知のように、∨E に対する制限は分配律を導くことを不可能にする。存在量化子に対する制限は存在量化子を越えての ∧ の分配

∃x Px ∧ ∃y Qy├ ∃x ∃y (Px ∧ Qy )

を阻む。

　NDQL を述語論理に拡張するには、変数や述語記号等を導入し、式の定義を改めたりする必要があるが、その辺は一切端折って、以下に、量化子に関わる推論規則だけを挙げておく。（なお、話を簡単にするために、定数記号と関数記号は考えに入れないことにして、自由変数を「a 」、束縛変数を「x 」で表わす。）

∀導入

Γ├ φ(a )　  Γ├ ∀x φ(x )

（ただし、a は Γ に属すどの式にも含まれていてはならない。）

∀除去

Γ├ ∀x φ(x ) Γ├ φ(a )

∃導入

Γ├ φ(a )　  Γ├ ∃x φ(x )

∃除去

Γ├ ∃x φ(x )　　{φ(a )}├ ψ Γ├ ψ

（ただし、a は ∃x φ(x ) にも ψ にも含まれていてはならない。）

標準的∃除去

Γ├ ∃x φ(x )　　Δ├ ψ Γ ∪ (Δ - {φ(a )})├ ψ

（ただし、a は ∃x φ(x ) にも ψ にも Δ - {φ(a )} に属すどの式にも含まれていてはならない。）

２００４年秋　　大熊康彦

---

雑録　／　『量子論理の限界』について ( I ) ( II ) ( III ) ( IV ) ( V )