＊＊＊＊ この記事は書きかけ、今後、追加・修正・変更をして本編記事にする予定。本編に移したらこのエントリーは削除します。 ＊＊＊＊
含意演算と論理順序の違いをどう書き分けるか？ この問題は、もう何年も、いやっ、何十年も困っています。
関連する話題をこのブログ内に書いたこともあるし（例えば「矢印の混乱に対処する： デカルト閉圏のための記法 // 矢印記号の憂鬱」）、口頭でも幾度となくしゃべっています。原理的に解決策がないので、結論は常に「どうにもならない、致し方ない」です。
現状を追認して妥協するしかないと諦めてはいますが、事情を明らかにした上で、追認と妥協の行為にも理由を付けておきたいと思います。長年悩まされているこの問題に、追認と妥協という形ではありますが、一応の決着を付けるのがこの記事の目的です。$`\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\cat}[1]{\mathcal{#1}}
%\newcommand{\twoto}{\Rightarrow }
\newcommand{\Imp}{\Rightarrow }
\newcommand{\In}{\text{ in } }
\newcommand{\Iff}{\Leftrightarrow }
\newcommand{\hyp}{\text{－} }
% \newcommand{\op}{\mathrm{op} }
% \newcommand{\id}{\mathrm{id} }
\newcommand{\T}{\mathrm{True} }
\newcommand{\F}{\mathrm{False} }
\newcommand{\BR}[1]{ \left[\!\left[ {#1} \right]\!\right] }
\require{color} % 緑色
\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }%
\newcommand{\Holds}{\Keyword{Holds } }%
\newcommand{\DoHolds}{\Keyword{Holds! } }%
\newcommand{\IN}{\Keyword{ In } }%
\newcommand{\For}{\Keyword{For } }%
\newcommand{\Define}{\Keyword{Define } }%
\newcommand{\Where}{\Keyword{Where } }%
\newcommand{\Subject}{\Keyword{Subject } }%
`$
内容：
はじめに
論理記号として出てくる矢印っぽい記号
- $`\to`$
- $`\Imp`$
- $`\supset`$
- $`\vdash`$
- $`\models`$
などは、それぞれ別な意味があります。が、人によって使い分けが違うので、状況は混沌としています。そのことは何度もブログ記事にしています。古い順からリストにすると：
- 含意＜がんい＞から伴意＜ばんい＞へ 2005 *1
- さまざまな「ならば」達 2006
- 論理記号のいろいろ 2006
- 論理におけるさまざまな「矢印」達 2016
- 論理／メタ論理の記法をどうするか 2018
- 論理／メタ論理の記法をどうするか 2: 悟りへの道 2018
- 互換な演繹システムとシーケント、そして矢印記号 2020
- 矢印の混乱に対処する： デカルト閉圏のための記法 2023
矢印っぽい記号に関する内容的説明は、過去記事を参照してください。様々な矢印記号を使い分けるのが難しいのは事実です。「構文論 vs. 意味論」「オブジェクトレベル vs. メタレベル」「証明論 vs. モデル論」などの対比的構造を考慮する必要があります。
なので、細かい分類と使い分けは出来なくても／やらなくてもいいだろう、とは思います。しかし、矢印記号 '$`\Imp`$' を演算子記号と関係記号の両方の意味で使い回す（オーバーロードする）のはちょっと、いや、だいぶ困ります。僕が「困ります」と言ったところで何か変わるわけもないので、諦めて、「矢印記号 '$`\Imp`$' を演算子記号と関係記号の両方の意味で使い回す」という事実は受け入れましょう。
そして、矢印記号 '$`\Imp`$' のオーバーロードを合理化*2できる三種類の場合を説明します。
- 台集合が $`{\bf B} = \{\T, \F\}`$ の場合
- 全称限量子記号 '$`\forall`$' を使っている場合、省略されている場合
- 証明可能性メタ記号 '$`\vdash`$' が省略されている場合
これら三種類の場合は、相互に関連します。
命題とその真偽
命題とは何かについて、みんな知っている（おそらく学校で習う）次の定義を採用します。
- 命題とは、真偽を判定できる文である。
これはもちろん、インフォーマルな定義ですが、この定義を出発点にします。注意すべきは、命題が真だとは限らないことです。偽〈ウソ〉と評価される命題もあります。「定理」の意味で「命題」という言葉を使うことがあるので、「命題とは真な文」と誤解している人もいますが、そうじゃないです。
命題を $`p, q`$ などで表すことにします。命題 $`p`$ の真偽を判定した値（$`\T`$ または $`\F`$）を次のように書きます。
$`\quad \BR{p}`$
二値真偽値の集合を $`{\bf B} = \{\T, \F\}`$ とすれば、
$`\quad \BR{p} \in {\bf B}`$
命題の真偽は絶対的・一意的に決まるものではありません。例えば、「$`1 + 1 = 0`$」という命題は、定数を “$`{\bf N}`$ の要素”、プラス記号とイコール記号を“$`{\bf N}`$ の通常の足し算”と“$`{\bf N}`$ 上の等値” と解釈すれば偽です。しかし、$`{\bf Z}_2 = {\bf Z}/2{\bf Z}`$ 上で解釈すれば真です。
命題を解釈するための背景／環境／文脈などを、$`\sigma, \tau`$ などで表すとすると、真偽値は $`\sigma, \tau`$ などに影響されます。次のようなことが起こり得ます。
$`\quad \BR{p}_\sigma = \F\\
\quad \BR{p}_\tau = \T
`$
今 $`\sigma, \tau`$ などで表現した背景／環境／文脈などを総称して状況〈situation〉またはセッティング〈setting | 場面〉と呼びましょう。
命題 $`p`$ が、状況 $`\sigma`$ で真であること（成立していること）を次のように書きます。
$`\quad \Holds p \IN \sigma`$
例えば、命題「$`1 + 1 = 0`$」に対して、$`{\bf N}`$ 上で解釈する状況を $`\alpha`$ 、$`{\bf Z}_2`$ 上で解釈する状況を $`\beta`$ とすると：
$`\quad \Holds 1 + 1 = 0 \IN \beta`$
です。緑のキーワード $`\Holds`$は、命題からメタ命題（命題に関する命題）を作ります。メタ命題といえども偽〈ウソ〉のことはあります。次のメタ命題は偽です。
$`\quad \Holds 1 + 1 = 0 \IN \alpha`$
メタ命題の真偽をメタメタ命題で表すなら：
$`\quad \Holds (\lnot \Holds (1 + 1 = 0) \IN \alpha)\\
\quad \Holds (\Holds 1 + 1 = 0 \IN \beta)
`$
ここで、$`\lnot \Holds`$ は「成立しない」という意味です。
さて、命題、メタ命題、メタメタ命題、‥‥ とメタレベルの階層を上げていったらきりが無いのでは？ と不安になるでしょう。実際、きりがありません。
そこで、あるコミュニケーション内でのトップレベルの命題〈toplevel proposition〉を想定します。これは、一番外側の〈outermost〉／一番上位の〈topmost〉メタレベルで提示〈発話〉される命題です。トップレベルの命題は、提示〈発話〉されたら自動的に真だとみなします。トップレベルの命題かどうかはコミュニケーションの文脈により判断されます。
トップレベルの命題を想定することは、何かを“それ以上の保証なし”に信じることなので、疑心暗鬼な気分になるかも知れません。例えば、次の会話：
- A：「俺の言うことがホントだ、Bの言うことは信用するな」
- C：「うん、わかった。」
- B：「いいか、これから言うことはホントだ。Aはウソツキだ。」
- C：「‥‥」
とはいえ、トップレベルの命題を想定しないかぎり、まともなコミュニケーションが出来ません。想定せざるを得ないのです*3。
命題の同値性
2つの命題 $`p, q`$ が同値であることを、
$`\quad p \equiv q`$
と書きます。2つの命題の同値性を主張する $`p \equiv q`$ も命題に関する命題なのでメタ命題です。
同値性を主張する記号 '$`\equiv`$' は使い勝手がいいメタ記号です。なぜかと言うと、命題の真偽には言及してないからです。$`p \equiv q`$ は、$`p, q`$ の真偽値が一致すると言っているだけで、$`p, q`$ が両方とも偽でもかまいません。
記号 '$`\equiv`$' を使って次が言えます。
$`\quad p \equiv (\Holds p)\\
\quad (p \equiv q) \equiv ( (\Holds p)\equiv (\Holds q) )
`$
これらの命題自体はトップレベルの命題だと解釈して下さい。つまり、書いてある時点でホントだと信じてください。
状況〈セッティング〉を考慮して命題の同値性を述べると：
$`\quad (\Holds p \equiv q \IN \sigma) \equiv (\Holds \BR{p}_\sigma = \BR{q}_\sigma)`$
トップレベル命題 $`p \equiv (\Holds p)`$ から言えることは、$`p`$ が（ある状況で）真なら、次の命題はすべて真になることです。
- $`p`$
- $`\Holds p`$
- $`\Holds (\Holds p)`$
- $`\Holds (\Holds (\Holds p))`$
- ‥‥
$`p`$ が偽なら、上記の命題はすべて偽になります。また、$`p`$ が偽なら、次の命題はすべて真になります（古典論理に基づいて判断するなら）。'$`\lnot`$'（論理否定の記号）が移動できるのでややこしくなります。
- $`\lnot p`$
- $`\Holds \lnot p`$
- $`\lnot\Holds p`$
- $`\Holds (\Holds \lnot p)`$
- $`\Holds (\lnot\Holds p)`$
- $`\lnot\Holds (\Holds p)`$
- ‥‥
命題と述語
$`{\bf B} = \{\T, \F\}`$ の要素をブール値〈Boolean value〉ともいいます。集合 $`X`$ から集合 $`Y`$ への写像〈関数〉の集合は $`\mrm{Map}(X, Y)`$ と書きます。
$`\mrm{Map}(X, {\bf B})`$ の要素を述語〈predicate〉と呼びます。つまり、述語とはブール値関数〈Boolean-valued function〉のことです。集合 $`X`$ は特に制限はないので、$`X = {\bf B}^n`$ のときも $`\mrm{Map}({\bf B}^n, {\bf B})`$ の要素は定義上“述語”です。が、用途が違うことから、$`{\bf B}^n \to {\bf B}`$ という関数はn項のブール演算〈n-ary Boolean operation〉とも呼びます。否定は単項〈1項の〉ブール演算、連言〈論理AND〉は2項ブール演算です。
「命題関数〈propositional function〉」「真理関数〈truth function〉」という言葉もあります。が、僕は「命題関数」「真理関数」は使いません。使わない理由は、述語やブール演算とは違う微妙なニュアンスを付ける人がいて、そういう曖昧性が嫌いだからです。多くのケースでは、「命題関数 ＝ 述語」「真理関数 ＝ ブール演算」です -- そのときは、「述語」「ブール演算」があるのでやっぱり使いません。
述語（値がブール値な関数）とは別に、構文的対象物〈syntactic object〉としての命題を値とする写像を考えるなら、それは命題値関数〈proposition-valued function〉と呼ぶことにします。状況〈セッティング〉$`\sigma`$ で解釈可能〈真偽判定可能〉な命題の集合を $`\mrm{Prop}_\sigma`$ として*4、集合 $`X`$ 上の命題値関数は次の形です。
$`\quad f:X \to \mrm{Prop}_\sigma`$
形式言語とそのセマンティクスを定義するお作法に則れば、$`\mrm{Prop}_\sigma`$ と $`{\BR{\hyp}}{_\sigma}`$ を形式的〈フォーマル〉に定義することは可能です。
命題値関数 $`f`$ から述語 $`\bar{f}`$ を定義できます。次の図式が可換になるように定義します。
$`\quad \xymatrix{
X \ar[r]^{f} \ar[dr]_{\bar{f}}
& \mrm{Prop}_\sigma \ar[d]^{ {\BR{\hyp}}{_\sigma} }
\\
{}
& {\bf B}
}\\
\quad \text{commutative}
`$
$`\bar{f}`$ の定義をちゃんと書けば次のとおりです。（$`\Subject`$で、定義すべきモノを宣言してから実際の定義を続けます。）
$`\For f \in \mrm{Map}(X, \mrm{Prop}_\sigma)\\
\Subject \bar{f} \in \mrm{Map}(X, {\bf B})\\
\Define \bar{f} := \lambda\, x\in X.(\,\BR{f(x)}{_\sigma} \;\in {\bf B}\,)
`$
$`f \mapsto \bar{f}`$ という対応は次の関数を定義します。
$`\quad \bar{(\hyp)}\, : \mrm{Map}(X, \mrm{Prop}_\sigma) \to \mrm{Map}(X, {\bf B})`$
構文的対象物である $`\mrm{Prop}_\sigma`$ の要素（文としての命題）に興味がないなら、命題値関数の代わりに対応する述語を考えれば十分です。多くの場合、命題値関数と対応する述語は暗黙に同一視されます。しかし、命題値関数と述語が一対一に対応しているわけではないので注意してください*5。
ちなみに、「命題関数」「真理関数」という言葉が曖昧に使われてしまう理由は、「命題」という言葉がそもそも曖昧に使われることが要因でしょう。
- 構文的対象物〈文〉を命題と呼ぶ。
- ブール値〈真偽値〉を命題と呼ぶことがある。
- 構文的対象物とブール値を暗黙に同一視して、それを命題と呼ぶ。
ここでは（というか、僕の習慣として）、命題は構文的対象物〈文〉のことで、ブール値ではありません。
述語と部分集合
$`\mrm{Pow}(X)`$ は、集合 $`X`$ のベキ集合だとします。
$`\quad S\in \mrm{Pow}(X) \equiv S \subseteq X`$
今書いた命題の同値性はホントのことなので、「成立する／ホントだよ」の意味を強調したいなら：
$`\quad \Holds S\in \mrm{Pow}(X) \equiv S \subseteq X`$
トップレベル命題であることを明示するために $`\DoHolds`$という記号を使うなら次のようです。
$`\quad \DoHolds S\in \mrm{Pow}(X) \equiv S \subseteq X`$
ビックリマークが付いていたら、「ホントだ！ 有無を言わずに信じろ」ということになります。ただし、いちいち「ホントだよ」「信じろ」を付けるのは面倒過ぎるので、常識的に省略します。
なお、'$`\equiv`$' を使って '$`\Iff`$' を使わなかったのには理由があります。そのことは、この記事の主題に関係します。
ベキ集合と述語の集合は同型になります。
$`\quad \mrm{Pow}(X) \cong \mrm{Map}(X, {\bf B})`$
この同型は次の写像〈関数〉で与えられます。
$`\quad \chi : \mrm{Pow}(X) \to \mrm{Map}(X, {\bf B})\\
\quad \BR{\hyp} : \mrm{Map}(X, {\bf B}) \to \mrm{Pow}(X)
`$
スコットブラケット記号 '$`\BR{\:}`$' はオーバーロードしています。また、$`\chi, \BR{\hyp}`$ に、集合 $`X`$ を（例えば下付きで）添えるべきですが省略しています。
$`\chi, \BR{\hyp}`$ の定義は以下のとおり。
$`\Subject \chi : \mrm{Pow}(X) \to \mrm{Map}(X, {\bf B})\\
\quad \For S \in \mrm{Pow}(X)\\
\quad \Define \chi_S := \lambda\, x\in X.(\, \text{if }x\in S \text{ then }\T \text{ else }\F \,)
`$
$`\Subject \BR{\hyp} : \mrm{Map}(X, {\bf B}) \to \mrm{Pow}(X)\\
\quad \For p \in \mrm{Map}(X, {\bf B})\\
\quad \Define \BR{p} := \{ x\in X \mid p(x) = \T\}
`$
$`\chi, \BR{\hyp}`$ が互いに逆なのは比較的簡単に示せます。
$`\chi_S`$ を $`S`$ の 指示関数〈indicating function〉または特性関数〈characteristic function〉と呼びます。$`\BR{p}`$ を $`p`$ の外延〈extension〉または真理集合〈truth set〉と呼びます。
連言含意系
連言含意系〈conjunction-implication system〉は、ブール代数〈Boolean algebra〉やハイティング代数〈Heyting algebra〉の連言と含意に関する部分だけを抜き出した順序代数系です。それは $`(U, \le, \land, \top, \triangleleft)`$ と書けます。構造の各構成素は次のとおりです。
- $`U`$ は、台集合
- $`(U, \le)`$ は、順序集合
- $`\land`$ は、順序に対するミート（小さいほう）になっている二項演算
- $`\top`$ は、順序に対する最大元で、ミート演算の単位元
- $`\triangleleft`$ は、順序とミートに関する指数演算（すぐ後に説明）
$`\triangleleft`$ が指数演算〈exponentiation operation〉であるとは、次が成立することです。
$`\For a, b \in U\\
\quad a \land b \le c \equiv a \le b \triangleleft c
`$
記号の優先順位が分かりにくい人のために括弧を付ければ：
$`\quad ( (a \land b) \le c) \equiv ( a \le (b \triangleleft c) )`$
圏論を知っているなら、連言含意系が“とてもやせた小さいデカルト閉圏〈very thin small Cartesian closed category〉”の同義語だと分かるでしょう。圏論の記法では $`b \triangleleft c`$ を $`[b, c]`$ と書くのが普通です。ここでは、$`\le`$ と $`\triangleleft`$ が似た形になるように記号を選びました（似てなくても別にいいのだけど）。
$`A`$ が連言含意系〈とてもやせた小さいデカルト閉圏〉のとき、次のように書けば辻褄が合っています。
$`\quad A = (U_A, \le_A, \land_A, \top_A, \triangleleft_A)`$
しかし、記号の乱用と省略により次のように書くのが普通です。
$`\quad A = (A, \le, \land, \top, \triangleleft)`$
さて、連言含意系の実例としては、ベキ集合 $`\mrm{Pow}(X)`$ に必要な関係と演算を入れたものがあります。
| $`\text{一般論}`$ | $`\text{事例}`$ | $`\text{事例への備考}`$ |
|---|---|---|
| $`U`$ | $`\mrm{Pow}(X)`$ | ベキ集合 |
| $`\le`$ | $`\subseteq`$ | 集合の包含関係 |
| $`\land`$ | $`\cap`$ | 集合の共通部分 |
| $`\top`$ | $`X`$ | 全体集合 |
| $`\triangleleft`$ | $`\hyp^c \cup \hyp`$ | 合併と補集合を使って定義 |
合併と補集合を使って定義した指数演算に対する指数演算の法則は次のように書けます。
$`\For A, B \in \mrm{Pow}(X)\\
\quad A \cap B \subseteq C \equiv A \subseteq (B^c \cup C)
`$
記号の優先順位が分かりにくい人のために括弧を付ければ：
$`\quad ( (A \cap B) \subseteq C) \equiv ( A \subseteq (B^c \cup C) )`$
一般論としての連言含意系に関して重要なことは、
- 順序関係 $`\le`$ と二項演算 $`\triangleleft`$ は、記号の形が似ているが全然別物である
ことです。二項関係のオフィシャルな定義は直積の部分集合なので、
$`\quad (\le) \subseteq U\times U`$
ですが、部分集合と述語の一対一対応から、関係は述語とみなしてもかまいません。
$`\quad (\le) : U\times U \to {\bf B}`$
どちらかと言うと、関係を述語とみなしたほうが気持ちいい（感情の問題）でしょう。
一方で、二項演算は次の形の関数です。
$`\quad (\land) : U\times U \to U\\
\quad (\triangleleft) : U\times U \to U
`$
順序関係を表す述語とは別物です。
が、順序関係を表す述語と二項演算がたまたま一致してしまうことがあります。それは $`U = {\bf B}`$ の（標準的順序と演算の）場合です。
$`\quad (\le) : {\bf B}\times {\bf B} \to {\bf B}\\
\quad (\land) : {\bf B}\times {\bf B}\to {\bf B}\\
\quad (\Imp) : {\bf B}\times {\bf B} \to {\bf B}
`$
集合 $`{\bf B}`$ に標準的に備わった順序は $`\F \lt \T`$ で決まり、指数演算は（論理の）含意〈implication〉と呼ばれて、多数派の記号は '$`\Imp`$' です。これらは、$`{\bf B}`$ 上に連言含意系の構造を定義します。
| $`\text{一般論}`$ | $`\text{事例}`$ | $`\text{事例への備考}`$ |
|---|---|---|
| $`U`$ | $`{\bf B}`$ | ブール代数〈真偽値〉の集合 |
| $`\le`$ | $`\le`$ | 標準的な順序 |
| $`\land`$ | $`\land`$ | 論理AND |
| $`\top`$ | $`\T`$ | 真 |
| $`\triangleleft`$ | $`\Imp`$ | 論理の含意 |
$`{\bf B}`$ 上では、$`(\le)`$ と $`(\Imp)`$ はまったく同じ関数になります。が、これは特例中の特例です。
この節のオマケとして、連言含意系と圏論的対応物の表を挙げておきます。$`\newcommand{\Obj}[1]{ |#1| }`$
| $`\text{連言含意系}`$ | $`\text{圏論}`$ |
|---|---|
| $`U`$ | $`\Obj{\cat{C}}`$ |
| $`a \le b`$ | $`f: A \to B`$ |
| $`a \land b`$ | $`A \times B`$ |
| $`\top`$ | $`{\bf 1}`$ |
| $`a \triangleleft b`$ | $`[A, B]`$ |
述語の集合における論理記号
前々節で次の同型について述べました。
$`\quad \mrm{Pow}(x) \cong \mrm{Map}(X, {\bf B})`$
前節で、ベキ集合 $`\mrm{Pow}(X)`$ を台集合とする連言含意系について述べました。それは、記号の乱用で次のように書けます。
$`\quad \mrm{Pow}(X) = (\mrm{Pow}(X), \subseteq, \cap, X, \triangleleft)`$
'$`\triangleleft`$' は一般論の記号をそのまま拝借して、ベキ集合における指数演算の意味だとします。
$`\quad A \triangleleft B := A^c \cup B`$
ベキ集合 $`\mrm{Pow}(X)`$ と同型な集合である $`\mrm{Map}(X, {\bf B})`$ にも連言含意系の構造を載せることができます。一般論と事例の対応は次の表のようになります。
| $`\text{一般論}`$ | $`\text{事例}`$ | $`\text{事例への備考}`$ |
|---|---|---|
| $`U`$ | $`\mrm{Map}(X, {\bf B})`$ | 述語の集合 |
| $`\le`$ | $`?`$ | 述語のあいだの論理順序関係 |
| $`\land`$ | $`\land`$ | 述語の論理AND |
| $`\top`$ | $`\T_X`$ | 定数関数 |
| $`\triangleleft`$ | $`\Imp`$ | 述語の含意演算 |
順序関係の記号が「$`?`$」なのは、合意された記号がないからです。仮に記号 '$`\sqsubseteq`$' を使うことにします。
述語の集合 $`\mrm{Map}(X, {\bf B})`$ 上の載った順序関係、二項演算、特定要素、二項演算を手短に書けば以下のようです。記号のオーバーロードに注意しながら見てください。
$`\For p, q \in \mrm{Map}(X, {\bf B})\\
\quad p \sqsubseteq q \equiv \forall x\in X.\, p(x) \le q(x)\\
\quad p \land q := \lambda\, x\in X.\, p(x)\land q(x)\\
\quad \T_X := \lambda\, x\in X.\, \T\\
\quad p \Imp q := \lambda\, x\in X.\, p(x) \Imp q(x)
`$
$`X`$ は一般的に様々な集合を表します。一般的には、順序関係 $`\sqsubseteq`$ と二項演算 $`\Imp`$ はまったく別物です。
今で出てきた、連言含意系の3つの例を一覧表にまとめます。
| $`\text{一般論}`$ | $`\text{事例 1}`$ | $`\text{事例 2}`$ | $`\text{事例 3}`$ |
|---|---|---|---|
| $`U`$ | $`\mrm{Pow}(X)`$ | $`{\bf B}`$ | $`\mrm{Map}(X, {\bf B})`$ |
| $`\le`$ | $`\subseteq`$ | $`\le`$ | $`\sqsubseteq`$ |
| $`\land`$ | $`\cap`$ | $`\land`$ | $`\land`$ |
| $`\top`$ | $`X`$ | $`\T`$ | $`\T_X`$ |
| $`\triangleleft`$ | $`\triangleleft`$ | $`\Imp`$ | $`\Imp`$ |
同じ記号（オーバーロードされた記号）でも意味はそれぞれ違います。
$`{\bf 1}`$ を単元集合として、
$`\quad {\bf B} \cong \mrm{Map}({\bf 1}, {\bf B})`$
なので、$`{\bf B}`$ と $`\mrm{Map}({\bf 1}, {\bf B})`$ を一律に扱うこともできます。だとすると、変わった記号 '$`\sqsubseteq`$' を導入したのはあまり意味がないのですが、述語の集合の上にも順序があることを強調するために目立たせている、と思ってください。
論理式と論域
＊＊＊＊＊ 未完 ＊＊＊＊＊
| 構文論 | 意味論 |
|---|---|
| 命題〈閉じた論理式〉 | ブール値 |
| 論理式 | 述語 |
$`\Holds \forall x\in X. P(x) \equiv \T_X \sqsubseteq \lambda\, x\in X. P(x)`$
*1:「伴意」の読み方に関しては「伴意は「ばんい」じゃなくて「はんい」と読む」に書いてあります。「はんい」と読む人がいますが、結局僕は「ばんい」と読んでいます。
*2:かなり強引な合理化、コジツケと言えるかも知れません。
*3:「誰の言うことも一切信じない」人がいたとして、彼は誰とどんな会話をしたところで真偽情報を受け取りません。だとすると、あらゆる会話は（少なくとも真偽情報の交換としては）無意味なので、誰とも何も会話しないのと同じです。
*4:証明支援系で使う型宇宙である $`\mrm{Prop}`$ とは違います。ここでの $`\mrm{Prop}`$ は閉じた論理式〈closed formula〉の集合です。
*5:$`\BR{\hyp}{_\sigma}`$ は単射であるとも全射であるとも仮定できません。その意味では、構文的な命題〈論理式〉と述語を同一視するのはけっこう無茶やってます。
