数理科学と日本古代史のブログ

　今日は、もう一つの量化記号 ∃ の定義です。

　今度は、ある公理系 Γ において、「命題 P(x) に項 T を代入した命題 P(T) が証明されている」という状態を考えます。
　ただし、この状態において、P(T) を満たす項 T の具体的な形には関心がなく、ただそれが命題 P を満たしている、という事実のみに関心があるとします。

　そこで、この状態すなわち「命題 P の変数 x に何か項を代入した命題が証明されている」という状態のことを、「P(x) を満たす x が存在する」あるいは略して ∃xP(x) と書くことにします。そして、論理記号 ∧ ∨ ⇒ ⊥ ∀ のときと同様なやり方で、この概念を形式化することにします。
　すなわち

(1) ∃xP(x) のとき、命題 R が定理として導かれる。

という性質を考え、

(2) 命題 P の変数 x に何か項を代入した命題が証明されているとき、命題 R が定理として導かれる。

と言い換えて、形式化の原理を発動します。
　すなわち、考えている理論に、∃ という量化記号を新規に追加し、更に (1) と (2) の同等性を、記号 ∃ に関する推論規則として同時に追加する、という形で理論を拡大します。

　実際に、(1) と (2) の同等性を導入規則、消去規則という形の推論規則に変形してみましょう。

　まず、R に ∃xP(x) を代入すると、(1) の言明は自明になります。従って (1) と (2) の同等性を仮定すると、(2) すなわち

(3) 命題 P の変数 x に何か項を代入した命題が証明されているとき、命題 ∃xP(x) が定理として導かれる。

という推論規則が得られます。これを (∃導入) といいます。

　逆に、(∃導入) を推論規則にすると、(1) から (2) が導出できます。
　実際、(1) を仮定し、(2) の前半を仮定すると、(2) の前半すなわち「命題 P の変数 x に何か項を代入した命題が証明されている」とき、(∃導入) により ∃xP(x) が得られ、更に (1) により R が得られますが、これは (2) の後半部分でもあります。
　すなわちこれは、(∃導入) を推論規則にしたとき、(1) から (2) が導けたことを意味します。

　次に消去規則に行く前に、前々回で、注意として挙げた次の性質：

(4)　一般に 公理系 Γ(x) のもとで P(x) という定理が得られたら、T を項とするとき、P(x) の x のところに項 T を代入して得られる命題 P(T) は、公理系 Γ(x) の x のところに項 T を代入して得られる公理系 Γ(T) のもとでの定理になる。

を思い出しましょう。このことに注意して、今

(5a) ∃xP(x) という命題が証明されている。

(5b) 自由変数 x を選んだとき、命題 P(x) を公理に付け加えた理論の中で、x を含まない命題 R が証明されている。

という２つの条件が成り立っているとします。

　この条件のもとで、更に (2) の前半の条件、すなわち「命題 P の変数 x に何か項を代入した命題が証明されている」が成り立っていると仮定します。
　すなわち、何か項 T があって、P(T) が証明されているとするのです。

　今、考えている理論の公理系を Γ とすると、(5b) の言っていることは、公理系 Γ,P(x) のもとで、定理 R が得られている、ということですから、ここで (4) を用いると、公理系 Γ,P(x) の x に T を代入して得られる公理系のもとで、命題 R の x に T を代入した命題が定理として得られることがわかります。
　ところが、x が公理系 Γ の自由変数であることから、x は Γ に含まれず、従って「公理系 Γ,P(x) の x に T を代入して得られる公理系」というのは、公理系 Γ,P(T) ということになります。
　一方、R が変数 x を含まないことから、「命題 R の x に T を代入した命題」とは、命題 R そのものです。
　すなわち、

(6) 公理系 Γ,P(T) において、命題 R が証明されている

わけです。言い換えると、

(6)' 考えている公理系に P(T) を追加した公理系で命題 R が証明されている

ということになります。

　ところが、仮定により P(T) は成り立っているのでしたから、これと (6)' を用いると、R が成り立つことになります。

　言い換えると、前提 (5a) と (5b) のもとで、(2) の前半の条件「命題 P の変数 x に何か項を代入した命題が証明されている」から R が導出できた、すなわち (2) が導出できたわけです。
　そこで、(2) と (1) の同等性を仮定すると、(1) が成り立つ、すなわち「∃xP(x) が得られていれば R が得られ」ます。
　ところが前提 (5a) により ∃xP(x) は定理なのですから、結局 R が得られることになります。

　以上により、次の推論規則が得られました：

(7) 前提 (5a) (5b) のもとで R が得られる。

　この推論規則のことを (∃消去) とよびます。

　今度は逆に、推論規則 (∃消去) を用いると、(2) から (1) が導出できることを証明しましょう。

　実際、(2) を仮定し、(1) の前提部分、すなわち ∃xP(x) が証明されていると仮定します。すなわち (5a) が成り立っていると仮定するわけです。
　x とは別に勝手な変数 z を選ぶとき、∃xP(x) と ∃zP(z) は同じ記号列です。従って、言明 (2) において、変数 x は R に含まれない自由変数であると仮定しても一般性は失われません。

　そこで、自由変数 x に対して命題 P(x) を公理に付け加えた理論を考えると、この理論では P(x) が成り立つので、変数 x を (2) の言明における項だと思えば、P(x) が成り立つので、(2) を仮定していることから R が導かれます。
　これは、(5b) が成り立っているということに他なりません。

　以上により、(5a) と (5b) すなわち (∃消去) の前提部分が成り立っていることがわかりました。

　従って、(∃消去) を用いると、R が導かれ、これは (1) の結論部分が成り立つということを意味します。

　以上で、(2) を仮定すると (1) が得られることがわかりました。

　以上を纏めると、次のようになります：

　「P(x) を満たす x が存在する」あるいは ∃xP(x) という概念は、「x に何らかの項を代入した命題が証明されている」という状態を形式化したものとして定義され、推論規則として

(∃導入) x に何らかの項を代入した命題が証明されているとき、命題 ∃xP(x) が得られる。

(∃消去) 条件 (5a) と (5b) が成り立っているとき、命題 R が得られる。

を持つ。