- 184 名前：デフォルトの名無しさん mailto:sage [2005/04/29(金) 11:43:24 ]
- タイプ理論
20世紀初頭、集合論を使って数学の基礎を再構築する試みが開始された。
数学基礎論の源流には、以下の３つの流派があった。
（１）論理主義 （ラッセルに代表される考え方）
（２）形式主義 （ヒルベルトに代表される考え方）
（３）直観主義 （ブラウワーに代表される考え方）
ラッセルの提示したや り方が「タイプ（type）理論」（the theory of types）である
（ラッセルの提示したタイプ理論は「分岐タイプ理論」と云うが、
ラムゼー（Ramsey F.P.）は、それを簡素化して、単純タイプ理論にした）。
ラッセルの導入したタイプ理論を要約すれば、以下の２点が主張 である。
（１）モノは、（以下に記述するように）いくつもの階層（＝型）から構成されている
（これを、 「高階」の構成という）。
タイプ０：個体｛ａ, ｂ, ｃ,...｝
タイプ１：個体の性質 ｆ(x) [つまり、「関数」]
タイプ２：個体の性質の性質 ｇ(ｆ(x))[ つまり、「関数の関数」のこと ]
：
タイプ（Ｎ−１）
タイプＮ
（２）代入規則：タイプＮの 関数は、タイプ（Ｎ−１）の対象を代入項とする。
したがって、「Ｗ∈Ｗ」（同じレベルの代入）は無意味となる（「タイプ理論」ではＷ∈｛Ｗ｝が正しい扱いとなる）。
ちなみに、Ｗ＝｛Ｗ｝が成立することもある。これを「不動点」という。
数学者たちが、モノを「高次に（高階に）構成された構築物」と観る原点が、ここにある。
モノは「無定義語」であって、「関係 （関数）」のなかで扱われるパラメータ（項）に過ぎない。
|
 |
