命題／命題関数と論域

http://d.hatena.ne.jp/m-hiyama-memo/20181102/1541141733の最後の余談を敷衍する。

domain of discourse の訳語に論域を使う。すると、命題関数の域は論域となる。「論域＝命題関数の域」で事情が少しハッキリする。シーケントにおける自由変数の指定は、論域の指定なので、命題関数が定義される準備ができる。

命題と命題関数を区別しろ言われても無理があるので、

1. 確定命題： 他の情報なしでも真偽が二値で確定する命題
2. 命題関数： 論域の値ごとに真偽が二値で確定する命題
3. 命題：確定命題または命題関数。ただし、確定命題も論域が単元集合である命題関数。

命題Aの真偽値を、スコットブラケットを使って〚A〛と書く。

1. Aが確定命題のときは、〚A〛は、真か偽の二値のどちらかである。〚A〛∈ B
2. Aが論域X上の命題関数のときは、〚A〛は、Xの部分集合である。〚A〛∈ Pow(X)

B = Pow(1) であることから、統一的に

• 〚A〛∈Pow(Aの論域)

論域は普通の域に過ぎないので、

• 〚A〛∈Pow(dom(A))

〚A〛が集合なので、真理集合という言葉もあるようだが、真理値〈真偽値〉か真理集合〈真偽集合〉なのかを区別してもしょうもないので、別にどうでもいい。「真理」と「真偽」の訳語の揺れも鬱陶しいのー。命題が等式・不等式のときは、真理集合を解集合と呼び、場合により代数多様体と呼んだりもする。外延も同じ意味だし、、、(ため息)

論域がXである命題（うるさく言えば命題関数）の全体をProp[X] = Map(X, Prop) とすると、限量子〈量化子 | 限定作用素〉は、

• ∀, ∃:Prop[X]→Prop

となる。さらに次の図を考える。

           Q
   Prop[X] → Prop
     |         |
 Deno|     Deno|
     v     Q   v
   Pred[X] → Bool

ここで、Qは限量子、Denoはスコットブラケット〈デノテーション〉。

Pred[X] Pow(X) を使って、下側のQを具体的に書くと

• ∀(A) = if (A = X) then 1 else 0
• ∃(A) = if (A ≠ 0) then 1 else 0

Prog[X]はFormula[X]と同じなので構文的概念、ただし、Xは外延としての集合なので、意味的概念も必然的に混ざり込む。Pred[X] = Pow(X) （同一視）は意味的概念。構文的／意味的の区別なく記述するにはインデックス付き圏を使う。Denoはインデックス付き圏のあいだの関手。随伴付きのインデックス付き圏がローヴェアのハイパードクトリン。

• 述語論理とインデックス付き圏と限量随伴性 - 檜山正幸のキマイラ飼育記
• 『圏論による量子計算と論理』はエキサイティングだ (1/2) - 檜山正幸のキマイラ飼育記
• プログラム意味論の書き方サンプル： UMiToL - 檜山正幸のキマイラ飼育記