論理の用語法整理の試み 3

まだまだ改善の余地がある。

コンパクト論理に限定するとして、

• 論理式＝生成対象の集合 F から作った自由コンパクト圏
• 原子証明＝生成射＝シーケントの集合 S から作った自由コンパクト圏

コンパクト圏〈コンパクト閉圏〉は、射の同値書き換え〈equivalent rewrite〉により2-圏となる。コンパクト2-圏がモデルとなる圏（より正確にはモデルのターゲット圏）。

日常語 → テクニカルターム

1. 命題 → 論理式
2. 命題 → シーケント
3. 命題 → 定理のステートメント（論理式、シーケント）
4. 命題 → 定理
5. 証明 → 証明図（ストリング図）
6. 証明 → 証拠式
7. 証明 → 定理の保証部〈warranty〉
8. 証明 → リーズニング図（横棒図）
9. 推論{規則}? → 原子証明{図}?
10. 推論{規則}? → 原子リーズニング{図}?
11. 公理 → 原子証明{図}?
12. 公理 → 原子証拠{式}?
13. 公理 → 絶対原子証明{図}?
14. 公理 → 絶対原子証明{図}?の結論命題〈余域対象〉
15. 公理 → 保証部〈warranty〉が原子証明{図}?である定理
16. 公理 → 定理ライブラリのインターフェイス〈指標〉の宣言

テクニカルタームの省略・短縮

1. 証明図 ← グラフィカル形式証明
2. 証拠式 ← テキスト形式証明
3. 証明 ← 証明図 ← グラフィカル形式証明
4. 証拠 ← 証拠式 ← テキスト形式証明
5. 証拠記号 ← 原子証拠式 ← 原子テキスト形式証明
6. リーズニング ← リーズニング図
7. 保証 ← 定理の保証部〈warranty part〉

定理の分類基準

1. 名前があるかないか（なくてもよい） → 名前付き、無名
2. ステートメントは論理式かシーケントか → 論理式、シーケント
3. 保証部は証明図かリーズニング図か → 証明定理、リーズニング定理、どこまでリーズニングを書くかが程度問題
4. 保証部は原子的か → 公理か否か

定理が公理であるとは、リーズニング定理なら保証部が原子リーズニング図、証明定理なら保証部が原子証明図であるもの。

定理の構成素〈部位〉：

1. 名前、なくてもよい
2. ステートメント部
3. 保証部〈ボディ〉
4. 所属しているライブラリ
5. 使用しているライブラリ

ライブラリ〈パッケージ、モジュール、セオリー〉構成も重要。従来、セオリー〈クライスリ射〉とセオリーのコドメインが混同されていた気がする。