レベルごとの演算子

演繹システムのパート分類（モジュラー／レイヤード設計・実装のため）：

1. 分野固有パート
2. 論理パート（分野によらない共通パート）

分野固有パートは：

1. 個体レベル
2. 型レベル

論理パート

1. 命題レベル
2. 推論レベル

システムが単ソート〈single{- | }sort{ed}?〉だとして、型レベルの議論は除く。また分野はN算術とする。

1. 個体レベル： 算術式←→構文解析木←→算術式の構成図
2. 命題レベル： 論理式←→構文解析木←→論理式の構成図
3. 推論レベル： 推論式←→構文解析木←→推論式の構成図

共通して：

1. 構文解析木のノードは演算子
2. 構文解析木の末端は定数生成ノード
3. 構文解析木の枝（ワイヤー）は中間部分式

用語法が乱れていて

1. 個体レベル： 項←→構文解析木←→項の構成図(呼び名なし)
2. 命題レベル： 論理式←→構文解析木←→論理式の構成図(呼び名なし)
3. 推論レベル： 推論図(証明図)←→構文解析木←→リーズニング図(証明図)

推論レベルになると、テキストによる式では表現が難しいので、図になる。

演算子：

1. 個体レベル： +, ×, 単項-, (-)², sqrt
2. 命題レベル： ∧, ∨, ¬, ⇒, ∀, ∃
3. 推論レベル： ;, , , ◇, □, Λ

定数（定数という言葉は誤解されるかも）：

1. 個体レベル： 個体変数ではない数値定数
2. 命題レベル： 命題変数ではない基本{アトミック | 原子}論理式、個体変数は含んでよい。
3. 推論レベル： 推論変数ではない基本{組み込み | プリミティブ}推論式、命題変数、個体変数は含んでよい。

「プリミティブなナントカ式」「ナントカ式のプリミティブ」がいいかも。

1. 算術式のプリミティブ + 算術式の{オペレーター|演算子|コンビネータ}
2. 論理式のプリミティブ + 論理式の{オペレーター|演算子|コンビネータ}
3. 推論式のプリミティブ + 推論式の{オペレーター|演算子|コンビネータ}

どのレベルでもオペレーターがあり、オペレーターには必ずプロファイルがある。

1. 算術オペレーターのプロファイル Nから構成される
2. 論理オペレーターのプロファイル Propと集合から構成される
3. 推論オペレーターのプロファイル 推論のプロファイルから構成される

(1)プリミティブ、(2)オペレーター、(3)オペレーターのプロファイル、この3つの概念とその定義をシッカリ追う。

---

リストの記法

1. プレーンリストは丸括弧
2. 連言と選言のマークは左肩に付ける。マーク付きリスト。
3. マークではなくて区切り記号で区別する場合はブラケットにする。
4. 無限リスト＝族 でも同じ記法を使う。区切り記号による区別は使えないので、プレーンな族にマークを付ける。
   1. ^∧(A₁, ..., A_n) = [A₁, ..., A_n]
   2. ^∨(A₁, ..., A_n) = [A₁| ...| A_n]
   3. ^∧(x∈X | A[x])
   4. ^∨(x∈X | A[x])
   5. ^∧() = T
   6. ^∨() = ⊥
   7. ^∧(x∈∅ | A[x]) = ^∧() = T
   8. ^∨(x∈∅ | A[x]) = ^∨() = ⊥