19/03/21 18:10:31.17 L2G86nzK.net
>>614
関連
URLﾘﾝｸ(m-hiyama.hatenablog.com)
檜山正幸のキマイラ飼育記 (はてなBlog)
2017-08-24
述語論理とインデックス付き圏と限量随伴性
命題論理の圏論的対応物としてデカルト閉圏やその拡張があります。述語論理の圏論的対応物はトポスだと思っている方が多いでしょう。確かにトポスがあれば（高階の）述語論理の入念な議論ができますが、トポスは複雑で難しいです。もう少し簡単な圏論的構造で（一階の）述語論理を展開できないでしょうか -- ここでは、インデックス付き圏（indexed category）による述語論理の定式化を紹介します。
(抜粋)
内容：
1.命題論理
2.連言含意論理とデカルト閉圏
3.述語論理
4.インデックス付き圏としての述語モデル
5.シンタックスとセマンティクス
6.変数の型、inとonと変数注釈の使い方
7.全称限量子
8.直積の射影に沿った述語論理
9.随伴の単位と余単位
10.述語論理におけるニョロニョロ
11.おわりに
一階述語論理の概念／用語と圏論の概念／用語の対応は次のようになります。
一階述語論理 圏論
解釈領域X ベース圏Bの対象X（Xは集合）
X上の述語P デカルト閉圏Pred[X]の対象P
X上の述語のあいだの証明／導出 デカルト閉圏Pred[X]の射
解釈領域のあいだの写像f ベース圏Bの射f（fは写像）
写像fによる述語の引き戻し デカルト閉圏のあいだの閉関手f*
真偽値 デカルト閉圏Pred[1]の対象
連言 デカルト閉圏の直積
含意 デカルト閉圏の指数
論理定数の真 デカルト閉圏の単位対象（＝終対象）
演繹定理 カリー同型Λ
命題論理とは、特定の集合X上のデカルト閉圏Pred[X]だけを考えることです。
つづく