「命題」の曖昧性
- 真偽値
- 述語
- 論理式
- （個体変数に関して）閉じた論理式
ところが、「論理式」が曖昧。
- テンプレート述語項構文木（リーフが穴、ノードが述語コネクティブ）
- テンプレート述語項構文木＋述語コンテキスト
- 評価値である述語
型理論のときも、型の意味が
- テンプレート型項構文木（リーフが穴、ノードが型コネクティブ）
- テンプレート型項構文木＋型コンテキスト
- 評価値である型
- 型そのもの（圏の対象）
- 型リテラル
- 型変数
一般に、次のものが混同される。
- モノそのもの〈シング〉
- モノを表すリテラル
- モノを代入できる型付き変数
- モノに対するコネクティブをノードとするテンプレートツリー構造
- 項 ＝ テンプレートツリー構造＋コンテキスト
- 項の評価値
対策： 次の概念を導入する。
- XXXを代入できる変数＝XXX変数 例：真偽値変数、述語変数、整数変数、ベクトル変数
- XXXを成分とするタプル〈部分ラベル付きリスト〉＝XXXコンテキスト 例：真偽値コンテキスト、述語コンテキスト
- XXXに作用するオペレーターを表すリテラル＝XXXコネクティブ 例：述語コネクティブ、実数コネクティブ、述語テンプレート・コネクティブ、型コンテキスト・コネクティブ
- XXXを表すテンプレートツリー＋XXXコンテキスト＝XXX項
