「命題」という言葉は極めて曖昧な言葉です。曖昧だから色々な意味で使えて便利ということでもあります。使う場面・文脈により次のような意味があります。
- 真偽値
- 述語
- 論理式
- 定理
- （国語辞書的意味で）課題、使命、目標など
この曖昧性については、「Propositions-As-Typesを曲解しないで理解するために // 「命題」を排除したい！」で書きました。
曖昧多義語の使用は、コミュニケーションに支障をきたす問題はあるのですが、なんらかの共通性を持つから同じ言葉で一括りにしている、ということもあります。国語辞書的意味は除いて、「真偽値、述語、論理式、定理」という意味での「命題」の用法は、論理の前層意味論の枠組みでチャンと解釈できます。$`\newcommand{\mrm}[1]{ \mathrm{#1} }
\newcommand{\In}{\text{ in }}
%\newcommand{\o}[1]{\overline{#1}}
\newcommand{\hyp}{\text{－} }
\newcommand{\twoto}{\Rightarrow }
%\newcommand{\Imp}{\Rightarrow }
\newcommand{\cat}[1]{\mathcal{#1}}
%\newcommand{\msf}[1]{\mathsf{#1}}
\newcommand{\mbf}[1]{\mathbf{#1}}
%\newcommand{\mbb}[1]{\mathbb{#1}}
%\newcommand{\doct}[1]{\mathbb{#1}}
%\newcommand{\M}{\text{-} }
%\newcommand{\T}[1]{\text{#1} }
\newcommand{\id}{\mathrm{id} }
\newcommand{\op}{\mathrm{op} }
%\newcommand{\dimU}[2]{{#1}\!\updownarrow^{#2}}
%\newcommand{\ClassOf}[1]{ \{\!| {#1} |\!\} }
%\newcommand{\CatOf}[1]{ \langle\!| {#1} |\!\rangle }
%\newcommand{\Opt}[1]{ \{\!/ {#1} /\!\} }
`$
内容：
二値真偽値の集合
真偽値と言えば、通常は「真」と「偽」の二値〈ふたつの値〉ですね。二値真偽値の集合を $`\mbf{B}`$ と書きましょう。'B' は、Boole（人名 George Boole）、Boolean（形容詞）からです。「真」と「偽」をどう書くかは好みと流儀があるので、以下のような候補があります。
- $`\mbf{B} = \{1, 0\}`$
- $`\mbf{B} = \{\mrm{True}, \mrm{False}\}`$
- $`\mbf{B} = \{\mrm{T}, \mrm{F}\}`$
- $`\mbf{B} = \{\text{true}, \text{false}\}`$
- $`\mbf{B} = \{\top, \bot \}`$
ここでは、$`1`$ と $`0`$ を使います（それが僕の好みなので）。
$`\mbf{B}`$ を単なる集合と考えることもありますが、順序集合やブール代数だと考えることもあります。その場合でも、同じ呼び名〈固有名〉 '$`\mbf{B}`$` を使いまわし〈オーバーロードし〉ます。紛らわしいときは次のような明示的な書き方をするのが良いでしょう。
- $`(\mbf{B} \text{ as Set})`$ （二値真偽値の集合）
- $`(\mbf{B} \text{ as Ordered Set})`$ （二値真偽値の順序集合）
- $`(\mbf{B} \text{ as Boolean Algebra})`$ （二値真偽値のブール代数）
- $`(\mbf{B} \text{ as Semiring})`$ （二値真偽値の半環）
- $`(\mbf{B} \text{ as Category})`$ （二値真偽値の圏）
- $`(\mbf{B} \text{ as Cartesian Closed Category})`$ （二値真偽値のデカルト閉圏）
例えば、$`(\mbf{B} \text{ as Category})`$ の場合、$`\mbf{B}`$ は次のような圏を表します。
- 対象の集合： $`|\mbf{B}| = \{0, 1\}`$
- ホムセット：
- $`\mbf{B}(0, 0) = \{\id_0\}`$
- $`\mbf{B}(0, 1) = \{ \mrm{t} \}`$
- $`\mbf{B}(1, 0) = \{ \} = \emptyset`$
- $`\mbf{B}(1, 1) = \{ \id_1 \}`$
過度なオーバーロードが諸悪の根源だと僕は思うのだけど ‥‥ グチグチ愚痴愚痴 ‥‥（言ってもしょうがないか）
二値真偽値をとる述語
「命題」の意味として、よくある説明は「真偽が判定できる文のことである」です。これは間違いではありません。例えば、次のような文を考えてみます。
- 彼は背が高い。
これは命題でしょうか？ キチンと状況設定すれば、命題になります。
まず、「彼」の候補となる人間の集合 $`H`$ を考えます。集合 $`H`$ の要素を「彼」に代入できます。例えば、男性の人間「鈴木一郎」（特定の文脈では一意的に人間を識別する固有名）さんが集合 $`H`$ の要素だとして、「彼」を具体化した文は次のようになります。
- 鈴木一郎さんは背が高い。
「背が高い」の定義を、「身長が178cm以上」だと定義します。cm単位で身長を測る操作は次の関数だとします。
$`\quad \mrm{height} : H \to \mbf{N} \In \mbf{Set}`$
この関数と不等号（関係記号のひとつ）を使えば、「彼は背が高い」は次の論理式で表現できます。
- $`\mrm{height}(x) \ge 178`$
変数 $`x`$ は集合 $`H`$ 上を走る変数だとして、この論理式は次の関数を定義します。
$`\quad \lambda\, x\in H.(\mrm{height}(x) \ge 178 \;\in \mbf{B})`$
型付きラムダ記法で書かれた関数なので、そのプロファイル（域と余域）はすぐに読み取れます。プロファイルは：
$`\quad H \to \mbf{B} \In \mbf{Set}`$
この関数に $`\mrm{tall}`$ という名前を付けましょう。
$`\quad \mrm{tall} := \lambda\, x\in H.(\mrm{height}(x) \ge 178 \;\in \mbf{B})\\
\quad \mrm{tall} : H \to \mbf{B} \In \mbf{Set}
`$
代名詞「彼」は、自然言語における変数だと思えば、自然言語の命題と論理式は次のように対応します。
- 彼は背が高い。←→ $`\mrm{height}(x) \ge 178`$ ←→ $`\mrm{tall}(x)`$
- 鈴木一郎さんは背が高い。←→ $`\mrm{height}(\text{鈴木一郎}) \ge 178`$ ←→ $`\mrm{tall}(\text{鈴木一郎})`$
$`\mrm{tall}(\text{鈴木一郎})`$ の値が $`1`$（真）か $`0`$（偽）かは、身長を測ってみないとわかりませんが、いずれにしても次は確実です。
$`\quad \mrm{tall}(\text{鈴木一郎}) \in \mbf{B}`$
この例において、次の言い方はいずれも許容できます（望ましくはない！）。
- 「彼は背が高い。」は命題である。
- $`\mrm{height}(x) \ge 178`$ は命題である。
- $`\mrm{tall}(x)`$ は命題である。
- $`\mrm{tall}`$ は命題である。
- $`\mrm{tall}(\text{鈴木一郎})`$ は命題である。
丁寧に言えば次のようです。
- 「彼は背が高い。」は、適切なセッティングのもとで、真偽が判定できる文となる。
- $`\mrm{height}(x) \ge 178`$ は、論理式である。
- $`\mrm{tall}(x)`$ は、関数名 '$`\mrm{tall}`$' を式内で使用しているが、上とまったく同義な論理式である。
- $`\mrm{tall}`$ は、述語（$`\mrm{B}`$ を余域とする関数）である。
- $`\mrm{tall}(\text{鈴木一郎})`$ は、述語の値なので二値真偽値（$`\mrm{B}`$ の要素）である。
曖昧多義語「命題」を使うより、「真偽が判定できる文」「論理式」「述語」「二値真偽値」といったテクニカルタームを使うほうがクリアな表現となるので望ましいです。曖昧多義語だと承知のうえで「命題」を使うのを禁止はしませんが（自分も使っているし）。
真偽値と論理圏
真偽値は二値真偽値（$`\mbf{B}`$ の要素）のことだ、と多くの人が想定しているでしょうから、デフォルトの真偽値は二値でいいと思います。
しかし、真偽値の概念は一般化されることがあります。
- 台集合が二値〈二元〉とは限らないブール代数やハイティング代数（の台集合）の要素を真偽値と呼ぶことがある。（この記事では扱わない。）
- 意味的には二値（真と偽の2つだけ）なのだが、便宜上たくさんの値を使うことがある。
ニ番目の用法の例として、例えば、“真偽値”として非負実数（$`\mbf{R}_{\ge 0}`$ の要素）を使うことがあります。
- ゼロでない非負実数（つまり正実数）はすべて真とみなす。
- ゼロは偽とみなす。
これで何が便利かというと、論理ANDに普通の掛け算、論理ORに普通の足し算が使えるのです。
別な例として、“真偽値”として集合（$`|\mbf{Set}|`$ の要素）を使うことがあります。
- 空でない集合はすべて真とみなす。
- 空集合は偽とみなす。
この場合は、論理ANDに集合の直積、論理ORに集合の直和が使えます。さらに、含意〈implication〉には関数集合〈関数空間 | 写像集合〉$`\mrm{Map}(\hyp, \hyp)`$ を使えます。否定は含意を使って掛けるので、集合としての真偽値 $`A`$ の否定は次のようになります。
$`\quad \mrm{Map}(A, \emptyset)`$
全称限量子としてはパイ型、存在限量子としてはシグマ型を使えるので、述語論理まで含めて論理演算の代わりに集合演算が使えて大変に便利です。ソフトウェアを作る立場だと、集合演算さえ実装すれば論理演算にそのまま流用できるので、これはとてもアリガタイことになります。
真偽値としての集合達を圏に仕立てたものが $`\mbf{Logic}`$ です。圏 $`\mbf{Logic}`$ については以下の記事で書いています。
要約しておくと：
- $`|\mbf{Logic}| = |\mbf{Set}|`$ 、したがって、対象は集合
- $`\mbf{Logic}`$ はやせた圏。したがって、2つの対象のあいだの射はあってもひとつ。
- $`X \ne \emptyset`$ のとき $`\mbf{Logic}(X, \emptyset)`$ は空集合。それ以外のホムセットは単元集合。
圏 $`\mbf{Logic}`$ に呼び名を付けていませんでしたが、論理圏〈logic category〉と呼ぶことにします。命題の圏〈category of propositions〉と呼ばれることもありますが、「命題」が曖昧多義語なので使用を避けたい。
述語とは
真偽値を二値真偽値だとするならば、述語とは次のような関数（集合圏の射）です。
$`\quad p : X \to \mbf{B} \In \mbf{Set}`$
述語（余域が $`\mbf{B}`$ である関数）を定義するために、論理式を使う場合が多いですが、論理式を使わなくても別にかまいません。関数が定義できりゃなんでもいいです。例えば、$`X`$ の部分集合 $`A \subseteq X`$ を取って、次のように関数を定義できます。
$`\text{For }x\in X\\
\quad p(x) := (\text{if }x \in A \text{ then } 1 \text{ else } 0)
`$
上記の関数定義の右辺も「論理式だ」と言い張られると、「論理式を使わなくてもいい」の事例になりませんが、「どこまで論理式と呼ぶか？」のような自転車置き場の議論に付き合う気はありません。構文的に決めりゃいいだけのことなので。
さて、真偽値の集合を $`|\mbf{Logic}|`$ とすると、述語は次の形になります。
$`\quad p : X \to |\mbf{Logic}| \In \mbf{SET}\\
\quad \text{where }X \in |\mbf{Set}|
`$
この場合、述語は“ファミリー”と言ったほうが適切かも知れません。ただし、「ファミリーであって、関数ではない」とかバカなことは言わないように。
二値真偽値の述語は、ファミリーとしての命題とみなすことができます。なぜなら、二値真偽値を論理圏 $`\mbf{Logic}`$ の対象とみなす写像があるからです。
$`\quad \mbf{B}\ni 0 \mapsto \mbf{0} \in |\mbf{Logic}|`$ （偽には空集合を割り当てる）
$`\quad \mbf{B}\ni 1 \mapsto \mbf{1} \in |\mbf{Logic}|`$ （真には特定された単元集合を割り当てる）
この“みなす写像”を使えば、二値真偽値を論理圏の対象とみなせるので、二値真偽値への述語をファミリーとしての述語とみなすことができます。
さらに、集合 $`X`$ を離散圏（という、特別な圏）とみなすと、述語は次の形だとみなせます。
$`\quad p: (X \text{ as Category}) \to \mbf{Logic} \In \mbf{CAT}`$
つまり、述語とは論理圏への関手だという見方ができます。
ここで一歩踏み出して、離散圏とは限らない任意の圏 $`\cat{C}`$ に対して、次のような反変関手を考えます。
$`\quad p: \cat{C}^\op \to \mbf{Logic} \In \mbf{CAT}`$
そして改めて、この形の関手を述語〈predicate〉と定義します。今まで知っていた“述語”は、新しく定義した“述語”の特殊ケースとなります。無理やり一般化した印象があるかも知れませんが、新しいステージに移行するときはちょっとした飛躍は必要です。
「$`\cat{C}`$ になんで $`{^\op}`$ が付いているんだ？」と不思議に思うでしょう。これは偶然そうなっているだけで意味はありません。歴史的経緯、あるいは習慣の問題です。$`{^\op}`$ を除いた形で述語を定義しても別にかまいません。習慣により多数派ではないだけです。
次の形の関手を一般に前層〈presheaf〉と呼びます。
$`\quad P: \cat{C}^\op \to \mbf{Set} \In \mbf{CAT}`$
圏 $`\mbf{Set}`$ から圏 $`\mbf{Logic}`$ への関手で identy-on-objects なものがただひとつだけあります。その関手を使うと、次のような関手圏のあいだの関手を作れます。
$`\quad [\cat{C}^\op, \mbf{Set}] \to [\cat{C}^\op, \mbf{Logic}] \In \mbf{CAT}`$
これは何を意味するかというと； 任意の前層を述語とみなすことができる。
雑な言い方をすれば、「任意の前層は述語である」となります。曖昧多義語「命題」を使って言えば「任意の前層は命題である」です。
定理とは
数学の教科書などでは、定理を「命題 1.5」「命題 2.1」のように呼んでいることがあります。この場合、「命題」とは「定理」のことです。論理式や述語では、偽（評価した値が $`0`$ や $`\mbf{0}`$）の場合もあるのですが、定理が偽のことはありません。このことから、「命題」を「真な命題」のことだと思い込んでいる人もいます。定理のことを「命題」と呼ぶのは「よろしくないなー」と僕は思います。
さてところで、定理とは何でしょうか？ 国語辞書を引いたり、言葉の運用を分析してみても迷宮に迷い込むだけです。印象や感情を根拠にしないで（根拠にならんし）、定理とは何かを考えてみましょう。
Propositions-As-Types の立場（「Propositions-As-Typesを曲解しないで理解するために」参照）では、命題とは型のことであり、証明とは関数を表す項です。と言ってみても、「命題」が曖昧多義語なので、なんだかよくわかりません。
今ここの文脈での「命題」は論理式や述語のことです。論理式や述語が「型」だとは、圏の対象とみなせるということです。「型」という言葉は圏の対象を指します。証明は型と型〈対象と対象〉をむすぶ射となります。
前節で実際に、述語は圏 $`[\cat{C}^\op, \mbf{Logic}]`$ の対象だと定義しました。となると、証明は圏 $`[\cat{C}^\op, \mbf{Logic}]`$ の射ということになります。圏論の言葉では、自然変換です。
まとめると：
- 述語とは、圏 $`[\cat{C}^\op, \mbf{Logic}]`$ の対象（関手）のことである。
- 証明とは、圏 $`[\cat{C}^\op, \mbf{Logic}]`$ の射（自然変換）のことである。
「証明」と「定理」は事実上同義語です。印象や感情からは同義語に思えないでしょうが、上記の射を「証明」と呼んでも「定理」と呼んでも好みの問題です。強いて印象・感情の違いを言えば：
- 定理は、証明に名前を付けている印象がある。
- 証明は、定理の具体的な記述を指すような印象がある。
「関数 ： 関数の計算手順 ＝ 射 ： 射の具体的記述 ＝ 定理 ： 証明」という“比例式”で考えると納得がいくでしょう。証明を伴った定理とは、具体的記述をともなった射のことなので、計算手順を伴った関数と同じことです。
この解釈では、定理は次の形に書けます。
$`\quad \alpha : P \to Q \In [\cat{C}^\op, \mbf{Logic}]`$
圏 $`\mbf{CAT}`$ 内で見ると：
$`\quad \alpha :: P \twoto Q : \cat{C}^\op \to \mbf{Logic} \In \mbf{CAT}`$
特定の対象 $`a\in |\cat{C}|`$ における自然変換の成分は次のようになります。
$`\quad \alpha_a : P(a) \to Q(a) \In \mbf{Logic}`$
$`P(a)`$ が前提で $`Q(a)`$ が結論です。これらの成分の束が、$`P`$ を前提として $`Q`$ を結論とする定理となります。
おわりに
最後のほうは駆け足でしたが、「命題」の曖昧性から生じる多様な意味「真偽値、述語、論理式、定理」についてザッと説明しました。結局、「命題とは圏 $`[\cat{C}^\op, \mbf{Logic}]`$ の対象または射」と解釈できます。対象は0-射、射は1-射なので、「命題とは圏 $`[\cat{C}^\op, \mbf{Logic}]`$ のk-射」の一言で片付きます。
曖昧多義語「命題」も、非常に高水準な立場からはひとつの概念を指している、と言えなくもないでしょう（ほぼコジツケだけど）。
