コラム 項の略記の導入

Last-modified: Sun, 19 Nov 2017 10:17:29 JST (1476d)
Top > コラム 項の略記の導入
等号の定義へ戻る。

\( \Phi(x) \)量化の有界な論理式とします。これに対し、\( \{a \mid \Phi(a) \} \)という表記を導入したのですが、そもそも項を表すことが出来る文字列は形式言語の段階で決まっていたため、そのような表記を正当化する必要があります。

まずクラスに対する分出公理そのものに対応する論理式は\( \exists ! A (\forall a ( ( (\Phi(a) ) \to (a \in A) ) \wedge ( (a \in A) \to (\Phi(a) ) ) ) ) \)であり、論理式はただの文字列なので、いくら「ただ1つのクラス\( A \)が存在し」と読むと言っても、その読み方に従った意味付けが自動的に付与されるわけではありません。なので、「そのような\( A \)\( \{a \mid \Phi(a) \} \)と表記する」という表現は「文字通りに」受け取ってしまうと厳密には不正確です。従ってそのような表現は正確には何か文字通りでない意味を持っていると考えるべきでしょう。そのような正当化の仕方は一意ではないですが、1つの方法を紹介します。

ここで実際に行っていることは論理式の略記の導入に過ぎない、と考えましょう。例えば\( x \in \{ a \mid \Phi(a) \} \)という論理式は\( \forall A ( (\forall a ( ( (\Phi(a) ) \to (a \in A) ) \wedge ( (a \in A) \to (\Phi(a) ) ) ) ) \to (x \in A) ) \)という論理式を表し、\( \{ a \mid \Phi(a) \} \in x \)という論理式は\( \forall A ( (\forall a ( ( (\Phi(a) ) \to (a \in A) ) \wedge ( (a \in A) \to (\Phi(a) ) ) ) ) \to (A \in x) ) \)という論理式を表します。\( \{a \mid \Phi(a) \} \)を用いた議論は、これらの略記にクラスに対する分出公理\( \exists ! A (\forall a ( ( (\Phi(a) ) \to (a \in A) ) \wedge ( (a \in A) \to (\Phi(a) ) ) ) ) \)を組み合わせ、各種演繹規則を適用したものとなります。

更に、「\( \{a \mid \Phi(a) \} \)\( A \)と略記する」という表現をすることがあります。これも論理式の略記の導入という同様の解釈で正当化することが出来ます。例えば\( x \in A \)という論理式は\( x \in \{a \mid \Phi(a) \} \)という論理式を表し、これは既に導入されている論理式の略記なので問題がないことが分かります。略記の中に略記を用いることも同様に再帰的に正当化され、例えば\( \{a \mid \neg (a \in A) \} \)\( A \)という略記が外延的記法による略記の右側に現れますが、これはまず\( A \)の略記を展開して全体を\( \{a \mid \neg (a \in \{a' \mid \Phi(a') \} \}) \)と直し*1、更に\( \{a' \mid \Phi(a') \} \)の略記を展開して適切な論理式\( \Psi \)を得て全体を\( \{a \mid \Psi(a) \} \)の形に直す、という流れで一意的に処理することが出来ます。このような略記の反復は数学の至るところで行われますが、一度その正当化を1つ理解しておけば、その正当化の方法に一々立ち返らないでも自然にかつ厳密に解釈で出来るようになると思います。




*1 略記の展開で&mathjax{a};が来るべきところに&mathjax{a'};が来ていますが、どちらも等価な外延的記法です。しかしながら&mathjax{a};を用いてしまうと外延的記法の外側に出現する&mathjax{a};と記号が被ってしまい読みにくいので、文字を変えることが慣例です。これは論理式に量化子をつける時の慣例と同様です。例えば&mathjax{\forall x( (P) \wedge (\exists x(Q) ) )};という論理式を扱いたい場合にその代わりとして、&mathjax{P};にも&mathjax{Q};にも出現しない変項&mathjax{y};と&mathjax{P};に自由に出現する&mathjax{x};を全て&mathjax{y};に置き換えた論理式&mathjax{(P)[x/y]};を用いて、論理式&mathjax{\forall y( ( (P)[x/y]) \wedge (\exists x(Q) ) )};を扱うことが多いですね。変項への代入操作についてはコラム 代入の定義を参照して下さい。