論理の用語法整理の試み

「原子」「複合」 を使う。次の表の欄に入る語は正式なテクニカルタームとして定義する。

	原子	(複合)	構成規則
項
論理式
証明
リーズニング

リーズニングが一番ゴタゴタで、

• 証明{図}?の構成規則の概念とかぶる。
• コンビネータ由来のリーズニングと、2-射由来のリーズニングがある。
• フォワードリーズニングとバックワードリーズニングがある。

テクニカルタームとしての定理は3種類。

1. 論理式定理： 論理式に名前を付けて、証明部として証明を付けたもの。
2. 証明定理： 証明に名前とプロフィールを付けて、証明部としてリーズニングを付けたもの。

論理式定理のとき：

• ステートメントとは論理式そのもの。
• 証明部は、結論がその論理式である絶対証明

証明定理のとき：

• ステートメントとはプロファイル〈2-プロファイル | シーケント〉のこと
• 証明部は、そのプロファイルがプロファイルであるリーズニング

ライブラリ：

• 論理式ライブラリは、論理式定理の集まり。インターフェイスは論理式定理のヘッドの集まり。
• 証明ライブラリは、証明定理の集まり。インターフェイスは証明定理のヘッド〈宣言〉の集まり。

日常語のテクニカルタームによる解釈

1. 命題 → 論理式
2. 命題 → 定理（日常語）
3. 定理 → 論理式定理（論理式ライブラリの要素）
4. 定理 → 証明定理（証明ライブラリの要素）
5. 公理 → 論理式定理で証明部が原子証明であるもの。
6. 公理 → 証明定理で証明部が原子リーズニングであるもの。

原子証明／原子リーズニングのためのキーワード。

• 事実〈fact〉
• 明らか〈obvious 'b'がある〉
• 自明〈trivial〉
• 後で〈deffered〉
• 信じろ〈believe | trust〉
• 神託〈oracle〉
• 仮定〈assume〉