型理論の歴史

バートランド・ラッセルは、ゴットロープ・フレーゲへの手紙（1902年）の中で、フレーゲの『概念書』におけるパラドックスの発見を発表した。^{[ 1 ]}フレーゲはすぐに返信し、問題を認め、「レベル」に関する技術的な議論の中で解決策を提案した。フレーゲの言葉を引用すると次のようになる。

ちなみに、「述語はそれ自身について述語化される」という表現は正確ではないように思われます。述語は原則として第一レベルの関数であり、この関数は引数として対象を必要とし、引数（主語）として自身を持つことはできません。したがって、「概念はそれ自身の外延について述語化される」と言う方が適切だと思います。^{[ 2 ]}

彼はこれがどのように機能するかを示そうとするが、そこから後退しているように見える。ラッセルのパラドックスとして知られるようになった結果、フレーゲとラッセルは印刷所に持っていた著作を急いで修正しなければならなかった。ラッセルが『数学原理』 （1903年）に付け加えた付録Bには、彼の「暫定的な」型の理論が見られる。この問題はラッセルを約5年間悩ませた。^{[ 3 ]}

ウィラード・クワイン^{[ 4 ]}は、型の理論と「分岐型」型の理論の起源に関する歴史的概要を提示している。ラッセルは、型の理論を放棄することを検討した後（1905年）、3つの理論を次々と提案した。

クワインは、ラッセルが「見かけ上の変数」という概念を導入したことで、次のような結果が生じたと指摘している。

「すべて」と「どれでも」の区別：「すべて」は、ある型の範囲を指す全称量化の束縛（「見かけ上の」）変数によって表現され、「どれでも」は、型に関係なく、特定されていないあらゆるものを概略的に指す自由（「実在の」）変数によって表現される。

クワインはこの「束縛変数」の概念を「型の理論のある側面を除いては無意味」として退けている。^{[ 5 ]}

クワインは分岐理論を次のように説明しています。「関数の型は、引数の型と、引数の型を超える場合の、関数（またはその式）に含まれる見かけ上の変数の型の両方に依存するため、このように呼ばれています。」 ^{[ 5 ]}スティーブン・クリーネは、1952年の著書『メタ数学入門』^{[ 6 ]}で、型の分岐理論を次のように説明しています。

主要な対象または個体（つまり、論理分析の対象とならない与えられたもの）は、1 つの型（たとえば型 0）に割り当てられ、個体のプロパティは型 1に、個体のプロパティのプロパティは型 2などに割り当てられます。そして、これらの論理型の 1 つに該当しないプロパティは認められません（たとえば、これにより「述語可能」と「述語不可能」というプロパティは論理の範囲外に置かれます）。より詳細な説明では、他の対象に認められる型を関係とクラスとして記述します。次に、型内の非述語的定義を除外するために、型 0 より上の型はさらに順序に分けられます。したがって、型 1 の場合、全体性に言及せずに定義されたプロパティは順序 0に属し、特定の順序のプロパティの全体性を使用して定義されたプロパティは次の上位の順序に属します。...しかし、この順序への分離により、上で見たように非述語的定義を含むおなじみの分析を構築することが不可能になります。この結果を回避するために、ラッセルは還元可能性の公理を提唱した。この公理は、最も低い位より上位の位に属するあらゆる性質に対して、位数0の同程度の性質（つまり、まったく同じ対象が持つ性質）が存在すると主張する。定義可能な性質のみが存在すると考えられる場合、この公理は、与えられた型内のすべての非述語的定義に対して、同等の述語的定義が存在することを意味する（クリーネ 1952:44–45）。

しかし、分岐理論の規定は（クワインの言葉を借りれば）「煩雑」であることが判明したため、ラッセルは1908年の著書『型理論に基づく数理論理学』^{[ 7 ]}で還元可能性の公理も提案した。1910年までに、ホワイトヘッドとラッセルは『プリンキピア・マテマティカ』で、この公理を行列の概念でさらに拡張した。行列とは、関数の完全な外延的仕様である。行列から関数は「一般化」の過程によって導出でき、その逆もまた同様である。つまり、2つの過程は可逆的である。（i）行列から関数への一般化（見かけ上の変数を使用）、および（ii）見かけ上の変数に対する引数の値のコース置換による型の還元という逆過程。この方法により、非述語性を回避することができた。^{[ 8 ]}

1921年、エミール・ポストは「真理関数」とその真理表の理論を発展させ、見かけ上の変数と実在する変数の概念を置き換えた。彼の「序論」（1921年）より：「ホワイトヘッドとラッセルの完全な理論（1910年、1912年、1913年）では、命題の表明に実在する変数と見かけ上の変数が必要であり、これらは個体と様々な種類の命題関数を表し、結果として煩雑な型の理論を必要とするが、この部分理論では実在する変数のみを使用し、これらの実在する変数は、著者らが基本命題と呼ぶことにした一種類の実体のみを表す。」^{[ 9 ]}

ほぼ同時期に、ルートヴィヒ・ヴィトゲンシュタインは1922年の著作『論理哲学論考』の中で同様の考えを展開した。

3.331 この観察から、ラッセルの類型論についてさらに理解を深めることができる。ラッセルの誤りは、彼が記号規則を作成する際に、記号の意味について語らなければならないという事実によって明らかになる。

3.332 命題はそれ自身について何も言うことができない。なぜなら命題記号はそれ自身の中に包含されることができないからである（これが「型の理論」全体である）。

3.333 関数は、それ自身の引数になることはできません。なぜなら、関数記号は既にそれ自身の引数のプロトタイプを含んでおり、それ自身を含むことはできないからです。

ウィトゲンシュタインも真理表法を提案した。彼の4.3から5.101にかけて、ウィトゲンシュタインは無制限のシェファーストロークを基本的な論理的実体として採用し、2変数関数の16個すべてを列挙している（5.101）。

行列を真理値表として扱うという概念は、1940年代から1950年代にかけてタルスキの研究に現れ、例えば彼の1946年の索引「行列、参照：真理値表」^{[ 10 ]に見られる。}

ラッセルは1920年の著書『数学哲学入門』の中で、「無限公理と論理型」という章を丸ごと割いて、次のように懸念を述べている。「型の理論は、我々の主題の完成された確実な部分に属するものでは決してありません。この理論の多くはまだ未熟で、混乱していて、不明瞭です。しかし、何らかの型の教義が必要であることは、その教義がどのような形をとるべきかという点よりも疑わしいことが少なく、無限公理と関連して、そのような教義の必要性が特に容易に理解できます。」^{[ 11 ]}

ラッセルは還元公理を放棄する。 『プリンキピア・マテマティカ』第2版（1927年）で、彼はウィトゲンシュタインの議論を認めている。^{[ 12 ]}序論の冒頭で、「実変数と見かけ変数の区別は必要ない…ことは疑いの余地がない…」と宣言している。^{[ 13 ]}ここで彼は行列の概念を完全に受け入れ、「関数は値を通してのみ行列に現れることができる」と宣言している（ただし、脚注で「これは還元公理の代わりを（十分ではないが）取るものである」と異議を唱えている）。 ^{[ 14 ]}さらに、彼は「行列」の新しい（簡略化され、一般化された）概念、すなわち「定数を含まない論理行列…」という概念を導入している。したがって、p | qは論理行列である。^{[ 15 ]}このようにラッセルは事実上還元公理を放棄したが、^{[ 16 ]}最後の段落で「現在の原始的な命題」からは「デデキン関係と整列関係」を導き出すことはできないと述べ、還元公理に代わる新しい公理があるならば「それはまだ発見されていない」と指摘している。^{[ 17 ]}

1920年代に、レオン・チウィステック^{[ 18 ]}とフランク・P・ラムジー^{[ 19 ]}は、悪循環の原理を放棄するならば、「分岐型理論」における型の階層構造を崩壊させることができることに気づいた。

結果として得られる制限された論理は、単純型の理論^{[ 20 ]}または、より一般的には単純型理論^{[ 21 ]}と呼ばれています。単純型理論の詳細な定式化は、1920 年代後半から 1930 年代前半にかけて、R. Carnap、F. Ramsey、WVO Quine、A. Tarski によって発表されました。1940 年に、Alonzo Church はそれを単純型付きラムダ計算として（再）定式化し[ ^{22 ] 、} 1944 年に Gödel によって検討されました。これらの発展の概説は Collins (2012 ) にあります^{[ 23 ] 。}