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

　ここまでで論理接続詞 ∧ ∨ ⇒ と論理定数 ⊥ と量化記号 ∀ ∃ （これらはまとめて論理記号とよばれます）を、形式化の原理によって“定義”してきました。
　今回は等号 ＝ を同様な方法で“定義”します。

　今までの議論は、命題（群）から命題を作る話でしたが、今回の対象は、項（群）から命題を作る述語記号の一つである等号の定義です。

　２つの項 S と T が与えられたとき、これらが「記号列として同じものである」という性質は、論理記号を導入する際に考えた「命題 P と命題 Q が共に証明されている」とか「命題 P を公理に追加した体系の下で命題 Q が証明されている」などと同様な、与えられた記号列に関する性質です。
　そこで、この「項 S と項 T は同じ記号列である」という性質を S=T と略記して、この概念を論理記号のときと全く同様に形式化の原理によって形式化してみましょう。
　すなわち、

(1a) S と T が同じ記号列のとき定理 R が得られる。

という主張の前半を省略記法 S=T を使って

(1b) S=T のとき定理 R が得られる。

と書き直したとき、S=T をメタ言語の省略記号とはみなさないで、新たに２変項述語記号 = を理論に追加し、(1a) と (1b) が等価になる、すなわち「(1a) が成り立つときは (1b) が成り立ち、逆に (1b) が言えるときは (1a) が成り立つ」という推論規則を同時に追加します。

　ただし、この形に表現された推論規則では扱いにくいので、論理記号のときと同じように、これを導入規則と消去規則の形に定式化し直してみましょう。

　まず、(1b) の R に S=T を代入すると、これは自明に成り立ちますから、(1b) から (1a) が言えることから (1a) が成り立ちます。すなわち次の推論規則が得られます：

(2) S と T が同じ記号列のとき定理 S=T が得られる。

　これを等号の導入規則といい、（=導入）と名付けることにします。

　ところで (2) はちょっとまだるっこしい言い方で、「S と T が同じ記号列のとき」っていうのは、要するに S が T だということなんですから、(2) は端的に言えば

(2)' T=T の形の命題は必ず定理である。

と表現することができます。

　さて、推論規則 （=導入） を用いると、逆に (1b) から (1a) を導くことができるのは、今までの議論と同様です。
　すなわち (1b) が成り立つと仮定し、(1a) の前提部分が成り立つとき、すなわち「S と T が同じ記号列」であるとき、（=導入） により S=T が成り立つので、(1b) が成り立つという仮定から R が得られ、これは (1a) の結論部分でもありますから、結局 (1a) が得られたことになります。

　次に、今度はある定理 R が成り立っていると仮定し、更に勝手な項 S を考えます。
　命題 R は項 S を含んでいるかもしれないので、この R のことを R(S) と書くことにします（ただしこう書いたからといって、R は S を含んでいるとは限りません）。

　ここで、もし (1a) の前提、すなわち「S と T が同じ記号列である」ということが成り立っているなら、R は R(T) とも書けますから、R(T) は定理です。
　すなわち (1a) の R を R(T) に置き換えたものが成り立ちます。
　そこで、(1a) と (1b) の同等性を用いると、(1b) の R を R(T) に置き換えたものが成り立ちます。すなわち

(3) S=T のとき R(T) が成り立つ。

　ところで、(3) を導いた上記の議論では、最初に R(S) が成り立っているという前提を置いていましたから、

(4) R(S) と S=T から R(T) が導かれる。

ということがわかります。この推論規則 (4) を （=消去） といいます。

　次はこの逆です。すなわち （=消去） を用いて (1a) から (1b) を導きます。
　そのために、(1a) を仮定します。
　この (1a) の下段の命題 R には S と T が含まれている可能性がありますから、この R を R(S,T) と書くことにします（もちろんこう書いたからといって R が必ず S も T も含んでいる必要はありません。S のみを含む、あるいは T のみを含む、あるいはそのいずれも含んでいなくてもかまいません）。

　ここで R すなわち R(S,T) の中の T と書かれている部分を自由変数 x に置き換えて得られる命題 R(S,x) を P(x) と書くことにすれば、R すなわち R(S,T) は P(T) と書くことができます。

　さて、仮定により (1a) が成り立っているのですから、もし T が S と同じ項なら R すなわち R(S,T) が成り立ちます。これは言い換えると、R(S,S) が成り立つ、ということです。ところが R(S,S) というのは P(S) に他なりません。つまり P(S) は定理です。
　そこで (1b) の前提部分、すなわち S=T が成り立っていると仮定すると、これと P(S) に対して推論規則 （=消去） を適用すれば、P(T) が得られますが、これは R(S,T) すなわち R つまり (1b) の下段に他なりません。
　以上で (1a) から (1b) が導出できることが証明されました。

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

　「S と T は等しい」あるいは S=T という概念は、「項 S と項 T は同じ記号列である」という状態を形式化したものとして定義され、推論規則として

(=導入) 項 S と項 T が同じ記号列であるとき、命題 S=T が得られる。

(=消去) R(S) と S=T が証明されているとき、R(T) が得られる。

を持つ。

　ちなみに、等号に関する推論規則 （=導入） と （=消去） についても局所整合性と局所完全性が成り立ちます。

　実際、（=消去） の S=T のところを （=導入） の前提、すなわち S と T が同じ記号列であるという事実で置き換えると、R(S) が成り立つということと R(T) が成り立つことは同じことですから、これは （=消去） の下段の式が成り立っていることを意味し、局所整合性が成り立つことがわかりました。

　また、（=導入） のかわりに

(='導入) 項 S と項 T が同じ記号列であるとき、命題 S='T が得られる。

を仮定し、これと （=消去） を用いると、S=T から S='T が得られます。
　なぜなら、S に含まれない自由変数 x を取り、S='x という命題を R(x) と書くと、（='導入） により S='S が成り立ちますが、これは R(S) とも書くことができます。
　そこで （=消去） を用いると、R(S) と S=T から R(T) すなわち S='T が得られます。以上で （='導入） と （=消去） を用いて S=T から S='T が導かれたので、局所完全性も成り立つことが確かめられました。