記事タイトルの「述語論理」は、昨日の記事「圏論的述語論理とお絵描き」で紹介した、ハイパードクトリンによる圏論的述語論理のことです。このスタイルの述語論理に関係する話題には、記事タイトル冒頭に「述語論理：」を付けるつもり。
ハイパードクトリンは、2つの圏 $`\mathcal{C}, \mathcal{L}`$ とそのあいだの反変関手 $`\mathrm{Pred}:\mathcal{C}^\mathrm{op} \to \mathcal{L}`$ で構成されます。今日は、ハイパードクトリンの構成素である2つの圏について考えてみます。$`
%\newcommand{\Imp}{\Rightarrow }
\newcommand{PPB}{\diamondsuit} % Predicate Pull Back
\newcommand{\cat}[1]{\mathcal{#1} }
%\newcommand{\op}{\mathrm{op} }
\newcommand{\mrm}[1]{\mathrm{#1}}
\newcommand{\In}{\:\text{ in } }
%\newcommand{\id}{\mathrm{id} }
%\require{color}
%\newcommand{\Keyword}[1]{ \textcolor{green}{\text{#1}} }%
%\newcommand{\For}{\Keyword{For } }%
%\newcommand{\Define}{\Keyword{Define } }%
%\newcommand{\Where}{\Keyword{Where } }%
`$
内容：
ハブ記事：
ベース圏
ハイパードクトリン $`(\cat{C}, \cat{L}, \mrm{Pred})`$ における圏 $`\cat{C}`$ を（ハイパードクトリンの）ベース圏〈base category〉と呼ぶことにします。
「圏論的述語論理とお絵描き」では、ベース圏はデカルト閉圏だと仮定しましたが、仮定を弱めてデカルト圏でも構いません。ベース圏がデカルト圏であるハイパードクトリンを一階ハイパードクトリン〈first-order hyperdoctrine〉といいます。
ベース圏が単なるデカルト圏だと高階関数に相当するものは出てきません。高階述語（述語に関する述語）を定義するスベもありません。型（ベース圏の対象）、関数（ベース圏の射）、型ごとの述語達が相互依存的に絡み合うことはなく、レイヤーに分けて取り扱うことができます。その意味で、一階ハイパードクトリンは比較的に単純な構造になります。
ベース圏がデカルト閉圏ならば高階関数（相当物）を扱えるにようになります。関数引数の関数（相当物）や関数戻り値の関数（相当物）も作れます。述語が“関数で表現可能”なら、高階述語も扱えます。高階述語を扱えるハイパードクトリンは高階ハイパードクトリン〈higher-order hyperdoctrine〉と言うこともあります。
ベース圏に、デカルト閉圏より複雑な構造を仮定することもあります。例えば、直和による余デカルト構造を要請してみます。すると、ベース圏はデカルト積〈直積〉と余デカルト積〈直和 | 余直積 | デカルト余積〉の2つのモノイド積を持つ圏になります。データ型で言えば、ペア型、指数型〈関数型 | アロー型〉以外にタグ付きユニオン型も持つことになります。直積、指数、直和を持つベース圏の上のハイパードクトリンはより豊かになりますが、より複雑にもなります。
ここまで、ベースであるデカルト圏に構造を追加する方向で考えてきました。デカルト圏より弱い構造、例えばマルコフ圏をベース圏にしたらどうでしょう？ デカルト圏で出来たことが出来なくなるんで辛いですが、確率的述語論理のひとつの定式化を与えるかも知れません。
論理代数の圏
ハイパードクトリン $`(\cat{C}, \cat{L}, \mrm{Pred})`$ における圏 $`\cat{L}`$ のほうは論理代数の圏〈category of logical algebras〉と呼びましょう。
“論理代数”の確たる定義があるわけではありません。ハイパードクトリンの構成素（の役割名）として“論理代数の圏”を導入しただけです。“論理代数”は、“論理代数の圏”の対象を指しているだけです。
具体的な状況で、実際の論理代数として選ばれる代数構造・順序構造には次のようなものがあります。
- 順序集合
- ハイティング代数
- ブール代数
- デカルト閉圏
- 余完備デカルト閉圏
- 完備ハイティング代数〈とてもやせた余完備デカルト閉圏〉
- BI代数*1
例えば、ハイティング代数と準同型写像の圏を論理代数の圏に選ぶならば、
$`\quad \cat{L} := {\bf HytAlg}`$
として具体的なハイパードクトリンを定義します。
論理代数が実際に何であるかは、具体的な状況ごとに変わりますが、論理代数の圏として共通に要求される性質に次があります。
- ハイパードクトリンの論理代数の圏 $`\cat{L}`$ は、忘却関手 $`U:\cat{L} → {\bf Cat}`$ を持つ。
別な言い方をすると、
- 圏 $`\cat{L}`$ の対象は圏とみなせる。
- 圏 $`\cat{L}`$ の射は圏のあいだの関手とみなせる。
なぜこの条件が要求されるかというと、圏論的随伴の概念を使うからです。限量子は、射影から作った $`\PPB_X^Y`$ の右随伴関手／左随伴関手として定義される（「圏論的述語論理とお絵描き」参照）ので、随伴関手の概念がないと限量子が定義できません。
例えば、論理代数＝順序集合 とした場合なら、圏論的随伴はガロア接続のことです（「ガロア接続（順序随伴系）の簡単な例」参照）。他の場合でも、論理代数は自然に圏だとみなせます。
ハイパードクトリンの反変関手 $`\mrm{Pred}`$ と忘却関手 $`U`$ をこの順に結合した関手を $`\mrm{PredCat}`$ とします。
$`\xymatrix {
{\cat{C}^\mrm{op}} \ar[r]^{\mrm{Pred}} \ar[rd]_{\mrm{PredCat}} & {\cat{L}} \ar[d]^{U}\\
{} & {{\bf Cat}}
}`$
$`\mrm{PredCat} : \cat{C}^\mrm{op} \to {\bf Cat}`$ はインデックス付き圏〈indexed category〉になります。必要があれば、インデックス付き圏に関する技法、例えばグロタンディーク構成（「 インデックス付き圏のグロタンディーク構成 」参照）を使うことが出来ます。
グロタンディーク構成を通じて、ハイパードクトリンをファイバー付き圏〈{fibred | fibered} category〉とみなすと、ベースの対象 $`X`$ 上の論理代数 $`\mrm{Pred}[X]`$ はファイバーになります。なので、$`\mrm{Pred}[X]`$ を（ハイパードクトリンの）ファイバー〈fibre | fiber〉とも呼びます。
ハイパードクトリンは、ベースの各点〈各対象〉から論理代数であるファイバーが“生えた”構造を持ちます。
*1:https://cs.au.dk/~birke/papers/categorical-logic-tutorial-notes.pdf の Definition 4.11 参照。BI は bunched implication から。
