- リテラルは、シングの束縛〈割り当て | 結びつき〉を持つ名前〈ラベル〉
- 宣言文は名前〈ラベル〉へのプロファイルの割り当て
- ソフト定義文は名前〈ラベル〉へのコンビネーション〈項〉の割り当て、マクロ・ラベルを生成する。
- ハード定義文は名前〈ラベル〉へのシング〈項〉の割り当て、リテラルを生成する。
- 宣言文のバンチを指標と呼ぶ。型コンテキスト、タイピング・コンテキストともいう。
- ソフト定義文のバンチを構成手続きと呼ぶ。ソフト環境ともいう
- ハード定義文のバンチをモデルと呼ぶ。ハード環境ともいう
知識ベースには次のものが含まれる。
- 型リテラル Nat, Bool, Real, 1 など
- 型構成子コネクティブ ×, [,] など
- 値リテラル〈型付き値定数〉 0, 1, true など
- 関数リテラル＝値構成子コネクティブ +, *, ^ など
- 述語リテラル（関数リテラルの特殊ケース） =, ≦ など
- 述語コネクティブ＝論理コネクティブ ∧, ∨, ￢ など
- 保証リテラル 公理論理式と |- で書く
- プリミティブ導出リテラル MP など
- プリミティブ・リーズニング・リテラル ConjIntro, LCurry など
- プリミティブ・メタリーズニング・リテラル APPLY, COMP, PROD など
グルーピング／組織化の手法として
- 指標デビジョン
- モデル・デビジョン
- 手続き・デビジョン
- 一般デビジョン
$`\mathscr{K}`$ が知識ベースなら、構文ベースのハイパードクトリン／インスティチューションを生成するので、それを $`\mathscr{K}^*`$ と書く。問題は、$`\mathscr{K}^*`$ の構造と意味論。
