構文領域と意味領域

思い付いたことを順不同にダダーっと箇条書きにする。後で整理する。まだごった煮。

先に意味領域：

1. 集合の集合がある。小さい具象圏の対象集合 ＝ Type ＝ |Sem|
2. 0, 1 はType内にある。0, 1∈Type
3. 型がAの個体〈individual〉とは、1からのAへの射のこと。
4. 関数はSemの射。個体は射の一種。
5. Semはデカルト閉圏。
6. Semは直和も持っている。
7. 圏Semは、コンテキスト領域〈議論の領域〉と代入（の意味である関数）の圏。
8. 構文領域〈semantic realm〉が決まれば、個体変数を使ってコンテキストを作れる。コンテキストは、Sem上のファイバーリング構造を持つ。
9. {個体}?定数記号、{個体間}?関数記号とその意味が決まれば、代入の意味も決まる。
10. 集合（＝コンテキスト領域）XごとにPow(X)を付ければハイパードクトリンになる。
11. 代入の意味である関数からなるSemの部分圏と、その上のPowハイパードクトリン（もとのハイパードクトリンの部分ハイパードクトリン）ができる。
12. 述語{定数}?記号〈関係{定数}?記号〉の意味が定まれば、論理記号の意味は固定だから、論理式の意味が決まる。
13. リスト（連言的リストと選言的リスト）の意味も決まる。意味＝真理集合＝一般化された真偽値は、リストの場合も、コンテキスト領域XのPow(X)の要素。
14. リストは、集合 1..n = {1, .., n} をインデックスとするインデックス族〈indexed family of popositions〉に連言マーカー、選言マーカーが付いたもの。
15. リスト（連言的リストと選言的リスト）の一般化として、連言的インデックス族と選言的インデックス族を考えることが出来る。
16. インデックスセットがXである連言的命題族は、連言的Xコンテキスト内に置かれた命題の集まり。インデックスセットがXである選言的命題族は、選言的Xコンテキスト内に置かれた命題の集まり。
17. コンテキスト領域という概念は、それ自体は意味側の単なる集合だが、構文側と意味側を繋ぐ役割を果たす。
18. 連言的Xインデックス付き命題〈論理式〉族と選言的Xインデックス付き命題〈論理式〉族に対する意味は集合論的に真理集合として定義できる。
19. そして、真理集合の包含関係として、シーケントの二値的真偽が定義できる。
20. シーケントの二値的でない真偽値＝真理集合も定義はできる。
21. シーケントの真偽値（二値または集合値）とは、推論の真偽値だから、さらにリーズニング（推論に対する推論 ＝ 2-推論）の真偽値も定義できる。

そうか、次元（次数）でいいのか：

1. 0-推論 ＝ 命題
2. 1-推論 ＝ 推論〈証明〉
3. 2-推論 ＝ リーズニング

次に構文領域：

1. 型： 型定数記号、型変数記号、型オペレーター記号（型値）がある。型定数記号の意味は決まっている。
2. 型： 型を表す形式的型表現が決まる。形式的型表現に名前を付けると名前付き型コンビネータができる。型コンビネータは型パラメータを持てる。型パラメータのソートはTypeである。
3. 個体： 個体定数記号、個体変数記号、個体オペレーター記号（個体値）＝関数記号 がある。個体定数記号の意味は意味領域の個体＝射として決まっている。
4. 個体： 個体を表す形式的個体表現が決まる（項）。形式的個体表現に名前を付けると名前付き個体コンビネータ（ユーザー定義関数）ができる。個体コンビネータは個体パラメータを持てる。個体パラメータのソートは型（意味は集合）である。
5. 個体変数記号と型定数記号によりコンテキストを構文的に定義できる。
6. 命題： 命題定数記号、命題変数記号、命題オペレーター記号（命題値）がある。命題定数記号の意味は決まっている。
7. 命題： 命題を表す形式的命題表現（それが論理式）が決まる。形式的命題表現に名前を付けると名前付き命題コンビネータができる。命題コンビネータは命題パラメータを持てる。命題パラメータのソートはProp[α]である。αはコンテキスト。
8. 推論： 推論定数記号、推論変数記号、推論オペレーター記号（推論値）がある。推論定数記号の意味は決まっている。
9. 推論： 推論を表す形式的推論表現（推論式、推件式）が決まる。形式的推論表現に名前を付けると名前付き推論コンビネータができる。推論コンビネータは推論パラメータを持てる。推論パラメータのソートは推論のプロファイルである。

構文領域にある集合：

1. TypeConstSymb, TypeVarSymb, TypeOperSymb, UserTypeOperSymb, TypeExpr, TypeSortExpr = {Type}
2. IndivConstSymb, IndivVarSymb, IndivOperSymb, UserIndivOperSymb, IndivExpr, IndivSortExpr = TypeExpr
3. PropConstSymb, PropVarSymb, PropOperSymb, UserPropOperSymb, PropExpr, PropSortExpr = TypeExpr
4. InferConstSymb, InferVarSymb, InferOperSymb, UserInferOperSymb, InferExpr, InferSortExpr = PropProfileExpr

	Const	Var	Oper	UserOper	Expr	Sort
型	型名	型変数	型構成子	型構成子	型式	型のカインド
個体	定数	変数	関数	関数	項	個体の余域型
命題	述語記号	命題変数	結合子	命題構成子	論理式	命題の域型
推論	推論定数	推論変数	リーズナー	タクティク	推論式	推論プロファイル

述語記号と総称性がうまく説明できてない。
コンテキスト＝インデックスセットも説明が必要だ。項変数は要らないのか？ 次が別に必要。

• 個体変数を持った命題 ＝ 命題関数 ＝ インデックス付き命題族
• 命題変数を持った推論 ＝ 総称的推論 ＝ 推論規則
• 個体変数を持った型 ＝ インデックス付き型族

有限	任意
インデックス i	自由変数 x
インデックスセット 1..n	コンテキスト領域 X
リスト (i∈1..n … )	コンテキスト付き論理式 (x∈X …)
リストからの成分 A[k]	ボックスからの具体化 A[a]
同一成分リスト	自由変数を持たない論理式が入ったボックス
n複製Δn	Xコンテキスト水増しΔX