タイプ理論（読み）タイプりろん（英語表記）theory of types

改訂新版　世界大百科事典

タイプ理論 (タイプりろん)
theory of types

B.A.W.ラッセルが1901年に発見したいわゆる〈ラッセルのパラドックス〉を解決しようとして提出した理論（1908）と，その単純化，制限の解除，および変形の総称。階型理論ともいう。大ざっぱにいえば，ある言語に登場する名辞は一般に階層組織を持ち，ある階層に属する名辞にはそれよりも高い階層の名辞しか帰属しないという思想にもとづいて論理学と数学の言語を再構成し，その言語中ではパラドックスが生じないようにする理論である。ラッセルは〈ある要素集合はその集合によって初めて定義されるものを要素とすることはできない〉という悪循環原理vicious-circle principleにもとづいてこれを行った。こうして，個体集合はそれ自身個体ではなく，個体集合の集合はそれ自身個体集合ではないことになる。しかし彼は，〈エピメニデスのパラドックス〉を初めとする意味論的パラドックスもこの原理にもとづいて解決されるべきだと信じたため，最初提出された理論は分岐タイプ理論ramified theory of typesというきわめて複雑なものであった。彼はあとで意味論的パラドックスを別に扱うべき異種のものであることを認めてこの理論を単純タイプ理論simple theory of typesに簡単化し，《プリンキピア・マテマティカ》の第2版でこれを採用した。タイプ理論のあとの発展は，理論の存在論的な面をいかに形式的な統語論に再構成するか，統語論的階層制限をどれほどゆるめ，あるいは変形してもパラドックスを生じないかということであった。しかし日常言語における語句の階層的構造は明確には認められず，悪循環原理は哲学的な存在論，カテゴリー論において生かされるべきものとされる。
→パラドックス
執筆者：中村 秀吉

出典　株式会社平凡社「改訂新版　世界大百科事典」

ブリタニカ国際大百科事典 小項目事典

タイプ理論
タイプりろん
theory of types

初期の集合論にみられたパラドックス，「すべての順序数の集合」に関するチェザーレ・ブラリ＝フォルティのパラドックス，「すべての集合の集合」に関するゲオルク・F.L.P.カントルのパラドックスなどを避けるためにバートランド・A.W.ラッセルが提唱，導入した概念。階型理論ともいう。ラッセルは「自己自身をメンバーとしないすべての集合の集合」という叙述に含まれる，自己否定を含む全体という観念によるパラドックスを解決するには「すべての集合を含むものは，その集合の一つであってはならない」という循環論法の原理を守ればよいとした。この矛盾を排除するためにたてた理論がタイプ理論である。すなわち，ある Xが有意味であるような対象の領域を限定して，これをタイプ（階型）と呼び，直接の対象である個物を第1のタイプ，個物の集合（関数）を第2のタイプ，集合の集合を第3のタイプとし，タイプの異なるものを混同してはならないとした。このタイプ理論はラッセル自身によってほかの意味論的・認識論的パラドックス（エピメニデスの嘘つきのパラドックスや，ベリーのパラドックス）にも適用され，のちの数学基礎論や意味論に影響を与えた。（→逆理）

出典　ブリタニカ国際大百科事典 小項目事典

世界大百科事典（旧版）内のタイプ理論の言及

【パラドックス】より

…これは順序数や基数の概念も必要としない純粋に論理的なパラドックスで，以後の論理学と数学基礎論の発展に大きな影響を与えた。このパラドックスをラッセルはタイプ理論によって解決したが，公理論的集合論を構成してその中に矛盾が生じないようにして解く方法も案出された。【中村 秀吉】。…

【ラッセル】より

…これはのちの論理学，数学基礎論，意味論の動向に大きな影響を及ぼすものであった。ラッセルはタイプ理論の案出によってこのパラドックスを解決し(1908)，師A.N.ホワイトヘッドとともに大著《プリンキピア･マテマティカ》(1910‐13)を著して数理論理学と数学を論理学に還元する論理主義の金字塔を建てた。一方，いわゆる〈記述〉理論を発表して(1905)，見かけ上の主語‐述語形式言明を存在言明におきかえる方策を案出，これをもとに存在の種類をできるだけへらす唯名論的な存在論を完成せんとした。…

※「タイプ理論」について言及している用語解説の一部を掲載しています。

出典｜株式会社平凡社「世界大百科事典（旧版）」