意味不明な言葉達

フントニモウ、ムカムカムカムカ、ムッキー！！ 矢鱈に同義語があったりする（例：論理AND、論理積、連言、合接、コンジャンクション）のに、肝心なモノ・コトに言葉がなかったり、曖昧過ぎて使いものにならなかったり。むっかー！

1. 定理
2. 証明
3. 公理と推論

定理

定理の全体構造は：

1. 名前またはラベルまたは番号
2. ステートメント、コンテキスト付きシーケントで記述
3. ヘッド＝名前＋ステートメント
4. ボディは本体
5. エンディングフレーム＝スチル
6. ムービーフィルム

どこを指して定理と呼ぶかが分からない。

証明

証明を大別すれば：

1. NKの意味での証明図 スチル方式
2. LKの意味での証明図 ムービー方式

今現在は、NKの意味の証明図を単に証明図と呼び、LKの意味での証明図（ムービーフィルム）はリーズニング図と呼んでいる。さらに、仮定のあるなしで、

1. 絶対証明図
2. 相対証明図

まとめると：

	NK証明図	リーズニング図
絶対	絶対証明図	絶対リーズニング図
相対	相対証明図	相対リーズニング図

さらに、総称か具体的かで、

	総称	具体的
絶対証明図	総称絶対証明図	具体的絶対証明図
絶対リーズニング図	総称絶対リーズニング図	具体的絶対リーズニング図
相対証明図	総称相対証明図	具体的相対証明図
相対リーズニング図	総称相対リーズニング図	具体的相対リーズニング図

公理と推論

語の運用をみて経験的に判断してみる。総称を命題総称と証明総称に分ける必要がある。組み込みとユーザー定義の別も必要になる。

NKレベルでは、

• 推論規則＝組み込み“命題総称”相対証明図 ＋名前
• 論理的公理＝組み込み“命題総称”絶対証明図 ＋名前
• 分野固有公理＝組み込み具体的絶対証明図 ＋名前

LKレベルでは、

• 推論規則＝組み込み“証明総称”相対リーズニング図 ＋名前
• 論理的公理＝組み込み“証明総称“絶対リーズニング図 ＋名前