$`x = y`$ と書かれていたら、「その意味は明らかだ」と多くの人は思うでしょう。が、イコール/等式の意味や用法はそんなに簡単でもないですよ。$`\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\mbf}[1]{\mathbf{#1}}
%\newcommand{\mfk}[1]{\mathfrak{#1}}
\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\In}{ \text{ in } }
\newcommand{\On}{ \text{ on } }
\newcommand{\id}{\mathrm{id} }
%\newcommand{\op}{\mathrm{op} }
\newcommand{\Iff}{\Leftrightarrow }
\newcommand{\twoto}{\Rightarrow }
%\newcommand{\T}[1]{\text{#1} }
`$
内容:
集合論のイコール/等式
現在の数学的議論は、建前としては集合論に帰着させることになっています(実際にそうするとは言ってない)。$`x = y`$ を集合論の意味で解釈するなら、次の命題〈論理式〉と同じです。
$`\quad x\subseteq y \land y \subseteq x`$
集合の包含関係を所属関係で書き下せば、以下のようになります。
$`\quad \forall z.\, z\in x \Iff z \in y`$
変数 $`z`$ が所属する集合が明示されてませんが、それは、$`z`$ が集合論の宇宙を走る変数だからです。通常は、作業用の小さな宇宙〈グロタンディーク宇宙〉の中で議論するので、現状の作業用宇宙〈current working universe〉を $`U`$ として、次のようにも書けます。
$`\quad \forall z\in U.\, z\in x \Iff z \in y`$
イコールがこの定義だと、「$`x, y`$ が集合でない場合はどうなるんだ?」と心配になりますが、現在の公理的集合論では「すべてのモノは集合」なので、そもそも「集合でない場合」は起こりえません。自然数の $`0`$ や $`7`$ も、実数の $`\sqrt{2}`$ や $`\pi`$ (円周率)も集合です。
「円周率 $`\pi`$ も集合」に違和感をいだくかも知れませんが、これは建前の話なので、非形式的に(気持ちとして)「円周率 $`\pi`$ は集合の気がしない」でも別にかまいません。
古典述語論理のイコール/等式
古典述語論理の「古典」は、「古くさい」とか「過去の」という意味は全然ありません。たくさんある論理のなかの特定の論理を識別する目印として「古典」が使われているだけです。現代の圧倒的主流の論理が古典論理です。
古典述語論理におけるイコール記号は二項述語記号〈関係記号〉の扱いです。その意味論には集合論を普通に使います。論域〈domain of discourse | 議論領域〉と呼ばれる集合 $`X`$ を取って、イコール記号が表す関数〈写像〉を次のように書きます。
$`\quad \mrm{eq}_X : X\times X \to \mbf{B}`$
$`\mbf{B}`$ は、二値古典真偽値 $`\mrm{True}, \mrm{False}`$ からなる二元集合です。
等式 $`x = y`$ の意味は関数呼び出し $`\mrm{eq}_X(x, y)`$ です。$`x = y`$ や $`\mrm{eq}_X(x, y)`$ を命題と呼んでもかまいませんが、命題の素朴な意味「真偽を判定できる文」と照らし合わせるとズレがあります。これらの等式は、ただちには真偽を判定できません。集合 $`X`$ を具体化して、要素 $`x, y`$ も具体的な要素として特定してはじめて等式の真偽が確定します。
ただし、「命題」は曖昧多義語で(「「命題」と「型」の曖昧性を図示」参照)、ゆるく使うのが習慣なので、「具体化すれば、真偽を判定できる文」を命題と呼んでも罪にはなりません。
$`\mrm{eq}_X(x, y)`$ には、論域(と呼ばれる集合)$`X`$ が含まれるのでイコール記号(横二本棒の記号)にも論域 $`X`$ を添えて、次のように書くのが正確です。
$`\quad x =_X y`$
まったく同じ意味で、僕は次のように書くこともあります。
$`\quad x = y \On X`$
圏論のイコール/等式
前節で $`x = y \On X`$ という書き方をしましたが、ときに次のように書くこともあります。
$`\quad x = y \In X`$
$`\text{on}, \text{in}`$ の区別は(実際のところ)気紛れとも言えますが、区別する基準はちゃんとあります。
$`\cat{C}`$ は圏とします。必ずしも1-圏とは限らず、高次射を持つ高次圏かも知れません。$`f`$ が $`\cat{C}`$ の1-射であることは次のように書きます。
$`\quad f: A \to B \In \cat{C}`$
$`\alpha`$ が $`\cat{C}`$ の2-射であることは次のように書きます。
$`\quad \alpha :: f \twoto g : A \to B \In \cat{C}`$
より短く(一部の情報を省略して)次のように書いてもかまいません。
$`\quad \alpha :: f \twoto g \In \cat{C}`$
$`\cat{C}`$ の1-射が特に恒等1-射であるときは次のように書くことにします。
$`\quad \id: A \to B \In \cat{C}`$
恒等2-射の場合でも、同じ綴り '$`\id`$' を使います。2-射であることはコロンの個数と矢印の“太さ”で分かるから問題ないでしょう。
$`\quad \id :: f \twoto g \In \cat{C}`$
2つのk-射のあいだに恒等(k+1)-射があることは、2つのk-射が等しいことなので、上記の $`\id`$ を用いた記述は、実は等式と同じことです。
- $`\cat{C}`$ において、$`A = B`$ とは、$`\quad \id: A \to B`$ のことである。
- $`\cat{C}`$ において、$`f = g`$ とは、$`\quad \id:: f \twoto g`$ のことである。
特に集合圏 $`\mbf{Set}`$ で考えると:
- 集合 $`A, B`$ に関して、$`A = B`$ とは、$`\quad \id: A \to B \In \mbf{Set}`$ のことである。
- 写像 $`f, g`$ に関して、$`f = g`$ とは、$`\quad \id:: f \twoto B \In \mbf{Set}`$ のことである。
1-圏である(と通常はみなす)集合圏に2-射があるのか? というと、2-射はあります。写像〈1-射〉のあいだのイコールがまさに2-射なのです。集合圏では、写像のイコール(それは恒等2-射)以外の2-射はありません。
したがって、集合圏では、以下の命題はすべて同じことです。
- $`f = g`$
- $`\id :: f \twoto g`$
- $`\alpha :: f \twoto g`$ ($`\alpha`$ は任意の2-射)
任意の2-射が恒等になりますが、任意の1-射が恒等になるわけではありません。対象〈集合〉に関しては、次の2つの命題が同じことです。
- $`A = B`$
- $`\id : A \to B`$
さて、$`X`$ が集合のとき、次は意味があるでしょうか?
$`\quad \id : x \to y \In X`$
そのままでは意味不明ですが、集合は規準的〈canonical〉に1-圏とみなせます。集合 $`X`$ に(規準的に)対応する圏を、ここだけの一時的記法として $`X^\uparrow`$ と書きます。圏 $`X^\uparrow`$ の対象は、集合 $`X`$ の要素です。圏 $`X^\uparrow`$ の射は、恒等射だけです。恒等射だけしか持たない圏は離散圏〈discrete category〉といいます。
離散圏 $`X^\uparrow`$ に対してなら次は意味があります。
$`\quad \id : x \to y \In X^\uparrow`$
2つのk-射のあいだに恒等(k+1)-射があることをイコール記号で書く、という約束を k = 0 として適用すると:
$`\quad x = y \In X^\uparrow`$
集合 $`X`$ と圏 $`X^\uparrow`$ の対応は規準的なので、集合と圏を同一視すれば:
$`\quad x = y \In X`$
まとめ
集合論的イコール、古典述語論理的イコール、圏論的イコールを、いつでも意識して区別しているわけではありませんが、区別したほうが良さそうな場面では、僕は次のように書き分けています。
- $`x = y`$ : 集合論的なイコール、宇宙のなかでの等しさ
- $`x = y \On X`$ : 古典述語論理的イコール、論域ごとにそれぞれのイコール述語
- $`x = y \In X`$ : 集合は離散圏とみなし、イコールは恒等1-射
他の解釈として; $`X`$ 上の二項述語〈関係〉は、直積集合 $`X\times X`$ の部分集合とみなすことがあるので、対角集合 $`\Delta_X \subseteq X\times X`$ をイコールの意味とすることもあります。$`\mbf{B}`$-値関数と部分集合の一対一対応があるので、古典述語論理的イコール述語と対角集合は次のように対応しています。
$`\quad \mrm{Map}(X\times X, \mbf{B}) \ni \mrm{eq}_X
\longleftrightarrow \Delta_X \in \mrm{Pow}(X\times X)
`$
$`\qquad \mrm{eq}_X(x, y)
\longleftrightarrow (x, y) \in \Delta_X
`$
イコール記号(横二本棒の記号)と、イコール記号を使った等式には、色々な解釈があります。ときに(いつでもとは言ってない)どんな解釈のもとで議論が進んでいるかを意識したほうがいいことがあります。