バートランド・ラッセルとタイプ理論：Bertrand Russell and Type theory

バートランド・ラッセルとタイプ理論

Bertrand Russell and Type theory

★ ラッセルは、アリストテレス以来の伝統的論理学では疑われることのなかった三段論法のほかに多くの推理形式があることを明らかにしたことで、アリストテレス以来最大の論理学者と評価される[2]。その業績は、従来の体系におけるパラドックスの発見と、その解決の探求のなかで成し遂げられた。特にラッセルのパラドックスで知られる。

ラッセルのパラドックスの発見は、19世紀末から20世紀初頭にかけて、ドイツの哲学者・数学者・論理学者であるフレーゲの研究と関係がある。フレーゲは、数学は論理に帰着しうる（論理主義）と考え、その思想を現実化する一歩として、論理上で実際に数学を展開するという野心的な著作『算術の基本法則』( Grundgesetze der Arithmetik ) を上梓した。1901年、ラッセルは、この『算術の基本法則』で示された体系で、パラドックスを示せることを発見し、フレーゲにその発見を伝える書簡を送った。このパラドックスは、のちに「ラッセルのパラドックス」と呼ばれるようになった。この手紙は、フレーゲの悲痛なコメントとともに『算術の基本法則 II』( Grundgesetze der Arithmetik II ) に収録されている。

この時期、ラッセル自身もまた、ホワイトヘッドとともに、論理主義の立場から論理上で実際に数学を展開するという事業に取り組んでいたが、このラッセルのパラドックスのために、約2年間の停滞を余儀なくされている。さらに、このパラドックスは、同時期に発見された類似の他のパラドックスとともに、数学の基礎に存在する深刻な問題と受け取られ、いわゆる「数学の危機」の震源となり、その解決をめぐって、ヒルベルトの「形式主義」やブラウワーの「直観主義」の誕生の切っ掛けとなった。

ラッセルは他にもパラドックスを発見したが、通常ラッセルの名を冠して呼ばれるものは一つだけである。他のパラドックスには、例えばブラリ＝フォルティのパラドックスはラッセルの発表中に脚注で「ブラリ＝フォルティの論文に示唆された」とあるためこの名が冠せられた。ところがブラリ＝フォルティの論文を見てもそのパラドックスは載っていないという[3]。

ラッセル自身のパラドックス解決の試みは、1903年、「階型理論」(theory of types) の発見により成功をおさめた。ラッセルは、この成功を礎に、階型理論に基づく高階論理上で全数学を展開するという一大事業を押し進め、その努力は、『数学原理』Principia Mathematica（1911-1913年）として結実した。（→以上「バートランド・ラッセル」日本語ウィキペディア）

☆ 数学および理論計算機科学において、タイプ理論（型理論）とは特定の型システムの形式的な提示である。

In mathematics and theoretical computer science, a type theory is the formal presentation of a specific type system.[a] Type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a foundation of mathematics. Two influential type theories that have been proposed as foundations are: Typed λ-calculus of Alonzo Church Intuitionistic type theory of Per Martin-Löf Most computerized proof-writing systems use a type theory for their foundation. A common one is Thierry Coquand's Calculus of Inductive Constructions.	数学および理論計算機科学において、タイプ理論（型理論）とは特定の型システムの形式的な提示である。いくつかの型理論は、数学の基礎としての集合論に代わるものである。基礎として提案された2つの影響力のある型理論がある：アロンゾ・チャーチの型付きλ微積分 Per Martin-Löfの直観主義型理論コンピュータによる証明書作成システムの多くは、その基礎に型理論を用いている。一般的なものとしては、ティエリー・コカンの帰納的構成論がある。
History Main article: History of type theory Type theory was created to avoid a paradox in a mathematical equation based on naive set theory and formal logic. Russell's paradox (first described in Gottlob Frege's The Foundations of Arithmetic) is that, without proper axioms, it is possible to define the set of all sets that are not members of themselves; this set both contains itself and does not contain itself. Between 1902 and 1908, Bertrand Russell proposed various solutions to this problem. By 1908, Russell arrived at a ramified theory of types together with an axiom of reducibility, both of which appeared in Whitehead and Russell's Principia Mathematica published in 1910, 1912, and 1913. This system avoided contradictions suggested in Russell's paradox by creating a hierarchy of types and then assigning each concrete mathematical entity to a specific type. Entities of a given type were built exclusively of subtypes of that type,[b] thus preventing an entity from being defined using itself. This resolution of Russell's paradox is similar to approaches taken in other formal systems, such as Zermelo-Fraenkel set theory.[3] Type theory is particularly popular in conjunction with Alonzo Church's lambda calculus. One notable early example of type theory is Church's simply typed lambda calculus. Church's theory of types[4] helped the formal system avoid the Kleene–Rosser paradox that afflicted the original untyped lambda calculus. Church demonstrated[c] that it could serve as a foundation of mathematics and it was referred to as a higher-order logic. In the modern literature, "type theory" refers to a typed system based around lambda calculus. One influential system is Per Martin-Löf's intuitionistic type theory, which was proposed as a foundation for constructive mathematics. Another is Thierry Coquand's calculus of constructions, which is used as the foundation by Coq, Lean, and other computer proof assistants. Type theory is an active area of research, one direction being the development of homotopy type theory.	沿革主な記事型理論の歴史型理論は、素朴な集合論と形式論理に基づく数学方程式におけるパラドックスを回避するために作られた。ラッセルのパラドックス（ゴットロープ・フレーゲの『算術の基礎』で初めて説明された）とは、適切な公理がなければ、自分自身のメンバーではないすべての集合の集合を定義することが可能であるというものである。1902年から1908年にかけて、バートランド・ラッセルはこの問題に対する様々な解決策を提案した。 1908年までにラッセルは、還元可能性の公理とともに、両者とも1910年、1912年、1913年に出版されたホワイトヘッドとラッセルの『プリンキピア・マテマティカ』に登場する、両者とも「反復された型の理論」に到達した。この体系では、型の階層を作り、具体的な数学的実体をそれぞれ特定の型に割り当てることで、ラッセルのパラドックスが示唆する矛盾を回避している。与えられた型の実体はその型の部分型だけで構成され[b]、実体がそれ自身を用いて定義されることを防いだ。このラッセルのパラドックスの解決は、ツェルメロ＝フレンケル集合論など、他の形式システムで取られたアプローチと類似している[3]。型理論は、特にアロンゾ・チャーチのラムダ計算と関連して人気がある。型理論の初期の顕著な例として、チャーチの単純型付きラムダ計算がある。チャーチの型理論[4]は、型付けされていないオリジナルのラムダ計算を苦しめていたKleene-Rosserのパラドックスを回避するのに役立った。チャーチはそれが数学の基礎として機能することを示し[c]、高次論理学と呼ばれるようになった。現代の文献では、「型理論」はラムダ計算を中心とした型付きシステムを指す。構成的数学の基礎として提唱されたペール・マルティン＝レフの直観主義的型理論もその一つである。もうひとつはティエリー・コカンの構成論であり、Coq、Lean、その他のコンピュータ証明支援システムで基礎として使われている。型理論は活発な研究分野であり、その一つの方向性はホモトピー型理論の発展である。
History of Type Theory The type theory was initially created to avoid paradoxes in a variety of formal logics and rewrite systems. Later, type theory referred to a class of formal systems, some of which can serve as alternatives to naive set theory as a foundation for all mathematics. It has been tied to formal mathematics since Principia Mathematica to today's proof assistants. 1900–1927 Origin of Russell's theory of types In a letter to Gottlob Frege (1902), Bertrand Russell announced his discovery of the paradox in Frege's Begriffsschrift.[1] Frege promptly responded, acknowledging the problem and proposing a solution in a technical discussion of "levels". To quote Frege: Incidentally, it seems to me that the expression "a predicate is predicated of itself" is not exact. A predicate is as a rule a first-level function, and this function requires an object as argument and cannot have itself as argument (subject). Therefore I would prefer to say "a concept is predicated of its own extension".[2] He goes about showing how this might work but seems to pull back from it. As a consequence of what has become known as Russell's paradox both Frege and Russell had to quickly amend works that they had at the printers. In an Appendix B that Russell tacked onto his The Principles of Mathematics (1903) one finds his "tentative" theory of types. The matter plagued Russell for about five years.[3] Willard Quine[4] presents a historical synopsis of the origin of the theory of types and the "ramified" theory of types: after considering abandoning the theory of types (1905), Russell proposed in turn three theories: the zigzag theory theory of limitation of size, the no-class theory (1905–1906) and then, readopting the theory of types (1908ff) Quine observes that Russell's introduction of the notion of "apparent variable" had the following result: the distinction between 'all' and 'any': 'all' is expressed by the bound ('apparent') variable of universal quantification, which ranges over a type, and 'any' is expressed by the free ('real') variable which refers schematically to any unspecified thing irrespective of type. Quine dismisses this notion of "bound variable" as "pointless apart from a certain aspect of the theory of types".[5] The 1908 "ramified" theory of types Quine explains the ramified theory as follows: "It has been so called because the type of a function depends both on the types of its arguments and on the types of the apparent variables contained in it (or in its expression), in case these exceed the types of the arguments".[5] Stephen Kleene in his 1952 Introduction to Metamathematics describes the ramified theory of types this way: The primary objects or individuals (i.e. the given things not being subjected to logical analysis) are assigned to one type (say type 0), the properties of individuals to type 1, properties of properties of individuals to type 2, etc.; and no properties are admitted which do not fall into one of these logical types (e.g. this puts the properties 'predicable' and 'impredicable' ... outside the pale of logic). A more detailed account would describe the admitted types for other objects as relations and classes. Then to exclude impredicative definitions within a type, the types above type 0 are further separated into orders. Thus for type 1, properties defined without mentioning any totality belong to order 0, and properties defined using the totality of properties of a given order belong to the next higher order. ... But this separation into orders makes it impossible to construct the familiar analysis, which we saw above contains impredicative definitions. To escape this outcome, Russell postulated his axiom of reducibility, which asserts that to any property belonging to an order above the lowest, there is a coextensive property (i.e. one possessed by exactly the same objects) of order 0. If only definable properties are considered to exist, then the axiom means that to every impredicative definition within a given type there is an equivalent predicative one (Kleene 1952:44–45). The axiom of reducibility and the notion of "matrix" But because the stipulations of the ramified theory would prove (to quote Quine) "onerous", Russell in his 1908 Mathematical logic as based on the theory of types[6] also would propose his axiom of reducibility. By 1910 Whitehead and Russell in their Principia Mathematica would further augment this axiom with the notion of a matrix — a fully extensional specification of a function. From its matrix a function could be derived by the process of "generalization" and vice versa, i.e. the two processes are reversible — (i) generalization from a matrix to a function (by using apparent variables) and (ii) the reverse process of reduction of type by courses-of-values substitution of arguments for the apparent variable. By this method impredicativity could be avoided.[7] Truth tables In 1921, Emil Post would develop a theory of "truth functions" and their truth tables, which replace the notion of apparent versus real variables. From his "Introduction" (1921): "Whereas the complete theory [of Whitehead and Russell (1910, 1912, 1913)] requires for the enunciation of its propositions real and apparent variables, which represent both individuals and propositional functions of different kinds, and as a result necessitates the cumbersome theory of types, this subtheory uses only real variables, and these real variables represent but one kind of entity, which the authors have chosen to call elementary propositions".[8] At about the same time Ludwig Wittgenstein developed similar ideas in his 1922 work Tractatus Logico-Philosophicus: 3.331 From this observation we get a further view – into Russell's Theory of Types. Russell's error is shown by the fact that in drawing up his symbolic rules he has to speak of the meanings of his signs. 3.332 No proposition can say anything about itself, because the propositional sign cannot be contained in itself (that is the whole "theory of types"). 3.333 A function cannot be its own argument, because the functional sign already contains the prototype of its own argument and it cannot contain itself... Wittgenstein proposed the truth-table method as well. In his 4.3 through 5.101, Wittgenstein adopts an unbounded Sheffer stroke as his fundamental logical entity and then lists all 16 functions of two variables (5.101). The notion of matrix-as-truth-table appears as late as the 1940–1950s in the work of Tarski, e.g. his 1946 indexes "Matrix, see: Truth table"[9] Russell's doubts Russell in his 1920 Introduction to Mathematical Philosophy devotes an entire chapter to "The axiom of Infinity and logical types" wherein he states his concerns: "Now the theory of types emphatically does not belong to the finished and certain part of our subject: much of this theory is still inchoate, confused, and obscure. But the need of some doctrine of types is less doubtful than the precise form the doctrine should take; and in connection with the axiom of infinity it is particularly easy to see the necessity of some such doctrine".[10] Russell abandons the axiom of reducibility: In the second edition of Principia Mathematica (1927) he acknowledges Wittgenstein's argument.[11] At the outset of his Introduction he declares "there can be no doubt ... that there is no need of the distinction between real and apparent variables...".[12] Now he fully embraces the matrix notion and declares "A function can only appear in a matrix through its values" (but demurs in a footnote: "It takes the place (not quite adequately) of the axiom of reducibility"[13]). Furthermore, he introduces a new (abbreviated, generalized) notion of "matrix", that of a "logical matrix . . . one that contains no constants. Thus p\|q is a logical matrix".[14] Thus Russell has virtually abandoned the axiom of reducibility,[15] but in his last paragraphs he states that from "our present primitive propositions" he cannot derive "Dedekindian relations and well-ordered relations" and observes that if there is a new axiom to replace the axiom of reducibility "it remains to be discovered".[16] Theory of simple types In the 1920s, Leon Chwistek[17] and Frank P. Ramsey[18] noticed that, if one is willing to give up the vicious circle principle, the hierarchy of levels of types in the "ramified theory of types" can be collapsed. The resulting restricted logic is called the theory of simple types[19] or, perhaps more commonly, simple type theory.[20] Detailed formulations of simple type theory were published in the late 1920s and early 1930s by R. Carnap, F. Ramsey, W.V.O. Quine, and A. Tarski. In 1940 Alonzo Church (re)formulated it as simply typed lambda calculus.[21] and examined by Gödel in 1944. A survey of these developments is found in Collins (2012).[22] 1940s–present Gödel 1944 Kurt Gödel in his 1944 Russell's mathematical logic gave the following definition of the "theory of simple types" in a footnote: By the theory of simple types I mean the doctrine which says that the objects of thought (or, in another interpretation, the symbolic expressions) are divided into types, namely: individuals, properties of individuals, relations between individuals, properties of such relations, etc. (with a similar hierarchy for extensions), and that sentences of the form: " a has the property φ ", " b bears the relation R to c ", etc. are meaningless, if a, b, c, R, φ are not of types fitting together. Mixed types (such as classes containing individuals and classes as elements) and therefore also transfinite types (such as the class of all classes of finite types) are excluded. That the theory of simple types suffices for avoiding also the epistemological paradoxes is shown by a closer analysis of these. (Cf. Ramsey 1926 and Tarski 1935, p. 399).".[23] He concluded the (1) theory of simple types and (2) axiomatic set theory, "permit the derivation of modern mathematics and at the same time avoid all known paradoxes" (Gödel 1944:126); furthermore, the theory of simple types "is the system of the first Principia [Principia Mathematica] in an appropriate interpretation. . . . [M]any symptoms show only too clearly, however, that the primitive concepts need further elucidation" (Gödel 1944:126). Curry–Howard correspondence, 1934–1969 The Curry–Howard correspondence is the interpretation of proofs-as-programs and formulae-as-types. The idea starting in 1934 with Haskell Curry and finalized in 1969 with William Alvin Howard. It connected the "computational component" of many type theories to the derivations in logics. Howard showed that the typed lambda calculus corresponded to intuitionistic natural deduction (that is, natural deduction without the Law of excluded middle). The connection between types and logic lead to a lot of subsequent research to find new type theories for existing logics and new logics for existing type theories. de Bruijn's AUTOMATH, 1967–2003 Nicolaas Govert de Bruijn created the type theory Automath as a mathematical foundation for the Automath system, which could verify the correctness of proofs. The system developed and added features over time as type theory developed. Martin-Löf's Intuitionistic type theory, 1971–1984 Per Martin-Löf found a type theory that corresponded to predicate logic by introducing dependent types, which became known as intuitionistic type theory or Martin-Löf type theory. Martin-Löf's theory uses inductive types to represent unbounded data structures, such as natural numbers. Martin-Löf's presentation of his theory using rules of inference and judgments becomes the standard for presenting future theories. Coquand and Huet's Calculus of Constructions, 1986 Thierry Coquand and Gérard Huet created the Calculus of Constructions,[24] a dependent type theory for functions. With inductive types, it would be called "the Calculus of Inductive Constructions" and become the basis for Coq and Lean. Barendregt's lambda cube, 1991 The lambda cube was not a new type theory but a categorization of existing type theories. The eight corners of the cube included some existing theories with simply typed lambda calculus at the lowest corner and the calculus of constructions at the highest. Identity Proofs are Not Unique, 1994 Prior to 1994, many type theorists thought all terms of the same identity type were the same. That is, that everything was reflexivity. But Martin Hofmann and Thomas Streicher showed that that was not required by the rules of the identity type. In their paper, "The Groupoid Model Refutes Uniqueness of Identity Proofs",[25] they showed that equality terms could be modeled as a group where the zero element was "reflexitivity", addition was "transitivity" and negation was "symmetry". This opened up a new area of research, homotopy type theory, where category theory was applied to the identity type. https://en.wikipedia.org/wiki/History_of_type_theory	タイプ理論（型理論）の歴史型理論は当初、様々な形式論理や書き換えシステムにおけるパラドックスを回避するために作られた。その後、型理論とは、すべての数学の基礎となる素朴な集合論の代わりとなるような、一群の形式的体系を指すようになった。プリンキピア・マテマティカ以来、今日の証明支援に至るまで、形式数学と結びついている。 1900-1927 ラッセルの型理論の起源 1902年、バートランド・ラッセルはゴットローブ・フレーゲに宛てた手紙の中で、フレーゲのベグリフシュリフトにおけるパラドックスの発見を発表した [1]。フレーゲの言葉を引用しよう：ところで、「述語はそれ自身を述語とする」という表現は正確ではないようだ。述語は原則として第一レベルの関数であり、この関数は引数として対象を必要とし、それ自体を引数（主語）として持つことはできない。したがって、私は「概念はそれ自身の拡張を述語とする」と言った方がいいと思う[2]。彼はこれがどのように機能するかを示そうとしているが、そこから後退しているように見える。ラッセルのパラドックスとして知られるようになったことの結果として、フレーゲとラッセルの両者は、印刷所で持っていた著作をすぐに修正しなければならなかった。ラッセルが『数学原理』（1903年）に付け加えた付録Bには、彼の「暫定的な」型の理論がある。この問題はラッセルを5年ほど悩ませた[3]。ウィラード・クワイン[4]は、型の理論と「ramified」型の理論の起源に関する歴史的な概略を提示している：型の理論の放棄を検討した後（1905年）、ラッセルは順番に3つの理論を提案した：ジグザグ理論大きさの制限の理論無階級理論（1905-1906年）である、型理論の再採用(1908ff) クワインは、ラッセルが「見かけの変数」という概念を導入した結果、次のようなことが起こったと述べている： all」と「any」の区別である： all」は普遍量化の束縛された（「見かけの」）変数によって表現され、それは型の範囲に及ぶものであり、「any」は自由な（「現実の」）変数によって表現される。クワインはこの「束縛された変数」という概念を「型の理論のある側面を除けば無意味なもの」として退けている[5]。 1908年の「ramified」型理論クワインはramified理論について次のように説明している：関数の型がその引数の型と、その関数に含まれる（またはその式に含まれる）見かけ上の変数の型の両方に依存し、それらが引数の型を超える場合、関数の型はその引数の型に依存するため、このように呼ばれるようになった」[5] Stephen Kleeneは1952年の『メタ数学入門』の中で、ramified theory of typesをこのように説明している：一次的な対象や個体（すなわち、論理的分析の対象とならない与えられたもの）は一つの型（例えば0型）に、個体の性質は1型に、個体の性質の性質は2型に、といった具合に割り当てられ、これらの論理的型のいずれにも当てはまらない性質は認められない（例えば、これによって「予測可能」と「予測不可能」という性質は...論理学の埒外に置かれることになる）。より詳細な説明では、関係やクラスなど、他の対象について認められる型を記述することになる。そして、型内の述語的定義を除外するために、型0以上の型はさらに順序に分けられる。従って、タイプ1では、全体性に言及せずに定義された性質はオーダー0に属し、与えられたオーダーの性質の全体性を用いて定義された性質は、次の上位のオーダーに属する。... しかし、このように次数に分離されると、上で見たような非可述的な定義を含むおなじみの分析を構成することが不可能になる。もし定義可能な性質だけが存在すると考えるなら、この公理は、与えられた型内のすべての非述語的定義に等価な述語的定義が存在することを意味する（Kleene 1952:44-45）。還元性の公理と「行列」の概念ラッセルは1908年の『型の理論に基づく数学論理学』[6]で還元性の公理を提案している。1910年までにホワイトヘッドとラッセルは『プリンキピア・マテマティカ』の中で、この公理を行列の概念（関数の完全な拡張的仕様）でさらに補強することになる。すなわち、（i）行列から関数への（見かけの変数を使った）一般化と、（ii）見かけの変数に対する引数の代入による型の減少という逆のプロセスである。この方法によって impredicativityを回避することができる[7]。真理値表 1921年、エミール・ポストは「真理関数」とその真理値表の理論を開発する。彼の「序論」（1921年）より：「ホワイトヘッドとラッセル(1910, 1912, 1913)の）完全な理論が、命題の発音のために、個体と異なる種類の命題関数の両方を表す実変数と見かけの変数を必要とし、その結果、面倒な型の理論を必要とするのに対して、この副次的な理論は実変数のみを使用し、これらの実変数は、著者たちが素命題と呼ぶことにした1種類の実体を表す」[8]。ほぼ同時期に、ルートヴィヒ・ウィトゲンシュタインが1922年の著作『論理哲学綱要』の中で同様の考えを展開している： 3.331 この観察から、ラッセルの「類型論」に対するさらなる見解が得られる。ラッセルの誤りは、記号規則を作成する際に、記号の意味を語らなければならないという事実によって示される。 3.332 命題はそれ自身について何も語ることができない。なぜなら、命題記号はそれ自身に含まれることができないからである（これが「型の理論」全体である）。 3.333 関数はそれ自身の論証にはなりえない。なぜなら、機能記号はそれ自身の論証の原型をすでに含んでおり、それ自身を含むことはできないからである...。ウィトゲンシュタインは真理値表法も提案した。彼の4.3から5.101において、ウィトゲンシュタインは彼の基本的な論理的実体として束縛のないシェファー・ストロークを採用し、そして2変数の16の関数をすべて列挙している（5.101）。真理値表としての行列の概念は、1940-1950年代のタルスキーの研究において、例えば1946年の索引 "Matrix, see：真理値表"[9]などである。ラッセルの疑念ラッセルは1920年の『数理哲学入門』の中で、「無限の公理と論理的型」に章全体を割いており、そこで自分の懸念を述べている：「この理論の多くはまだ未熟で、混乱しており、不明瞭である。しかし、ある種の型の教義の必要性は、その教義がとるべき正確な形よりも、それほど疑わしくはない。そして、無限の公理との関連において、そのような教義の必要性を見ることはとりわけ容易である」[10]。ラッセルは還元可能性の公理を放棄する：プリンキピア数学』の第2版（1927年）において、彼はウィトゲンシュタインの議論を認めている[11]。序論の冒頭で、彼は「実変数と見かけの変数の区別が必要ないことは......疑う余地がない」と宣言している[12]。さらに、彼は「行列」の新しい（省略され、一般化された）概念、すなわち「論理行列......」を導入している。定数を含まないものである。したがって、p\|qは論理行列である」[14]。このようにラッセルは事実上、還元可能性の公理を放棄した[15]が、最後の段落で彼は「現在の原始命題」から「デデキンディアン関係と整序関係」を導くことはできないと述べ、還元可能性の公理に代わる新しい公理があるとすれば「それは発見されるままである」と述べている[16]。単純型の理論 1920年代、Leon Chwistek[17]とFrank P. Ramsey[18]は、悪循環の原理を放棄することを厭わなければ、「ラム化された型の理論」における型のレベルの階層を崩すことができることに気づいた。単純型理論の詳細な定式化は1920年代後半から1930年代前半にかけてR.カーナップ、F.ラムゼイ、W.V.O.クワイン、A.タルスキーによって発表された。1940年にはアロンゾ・チャーチが単純型付きラムダ計算として（再）定式化し[21]、1944年にはゲーデルによって検討された。これらの発展に関するサーベイがCollins (2012) にある[22]。 1940年代-現在ゲーデル1944年クルト・ゲーデルは1944年の『ラッセルの数理論理学』において、脚注の中で「単純型の理論」について次のように定義している：単純型の理論とは、思考の対象（別の解釈では記号表現）は、個体、個体の性質、個体間の関係、そのような関係の性質などの型に分けられ（拡張についても同様の階層がある）、次のような形式の文があるという教義を意味する：「aはφという性質を持つ」、「bはcに対してRという関係を持つ」などという形の文は、a、b、c、R、φが互いに適合する型でなければ意味がない。混合型（個体とクラスを要素として含むクラスなど）、したがって超限定型（有限型のすべてのクラスのクラスなど）は除外される。単純型の理論が認識論的パラドックスも回避するのに十分であることは、これらをより詳細に分析することによって示される。(Ramsey 1926およびTarski 1935, p. 399参照）」[23]。彼は、(1)単純型の理論と(2)公理的集合論は「現代数学の導出を可能にし、同時にすべての既知のパラドックスを回避する」(Gödel 1944:126)、さらに単純型の理論は「適切な解釈における最初のプリンキピア[Principia Mathematica]の体系である。. . . [しかし、どのような症状も、原初的な概念にはさらなる解明が必要であることをはっきりと示している」(Gödel 1944:126)。カリー-ハワード書簡、1934年-1969年カリー-ハワード対応とは、証明-プログラム、式-型という解釈である。1934年にハスケル・カリーが提唱し、1969年にウィリアム・アルヴィン・ハワードが提唱した。これは多くの型理論の「計算要素」を論理学の導出と結びつけるものである。ハワードは型付きラムダ計算が直観主義的自然演繹（つまり排中律のない自然演繹）に対応することを示した。型と論理の結びつきは、既存の論理のための新しい型理論や、既存の型理論のための新しい論理を見つけるという、その後の多くの研究につながった。 de BruijnのAUTOMATH, 1967-2003 Nicolaas Govert de Bruijnは、証明の正しさを検証するAutomathシステムの数学的基礎として、型理論Automathを作成した。このシステムは、型理論の発展とともに発展し、機能を追加していった。マーティン=レフの直観主義型理論（1971年-1984年 Per Martin-Löfは、従属型を導入することで述語論理に対応する型理論を発見し、直観主義型理論またはMartin-Löf型理論として知られるようになった。 Martin-Löfの理論は、自然数などの非束縛データ構造を表現するために帰納的型を用いる。 Martin-Löfは、推論と判断のルールを用いて理論を提示し、これが後の理論提示の標準となった。 CoquandとHuetのCalculus of Constructions（1986年ティエリー・コカン（Thierry Coquand）とジェラール・ユエ（Gérard Huet）は、関数のための従属型理論である「Calculus of Constructions」[24]を作った。帰納的型を持つこの理論は「帰納的構成論」と呼ばれ、CoqとLeanの基礎となった。バレンドレヒトのラムダキューブ、1991年ラムダキューブは新しい型理論ではなく、既存の型理論を分類したものである。キューブの8つの角には、既存の理論がいくつか含まれており、最も低い角には単純型ラムダ計算が、最も高い角にはコンストラクション計算があった。同一性証明は唯一無二ではない 1994年 1994年以前、多くの型理論家は、同じID型の項はすべて同じだと考えていた。つまり、すべてが再帰性だと考えていたのだ。しかし、Martin HofmannとThomas Streicherは、それが同一性の型の規則では要求されないことを示した。彼らの論文「The Groupoid Model Refutes Uniqueness of Identity Proofs」[25]では、等式項が、ゼロ要素が「再帰性」、加算が「推移性」、否定が「対称性」である群としてモデル化できることを示した。これにより、ホモトピー型理論という新しい研究分野が開かれ、カテゴリー理論が恒等式に適用された。

リンク

︎▶︎▶︎︎▶︎▶︎︎▶︎▶︎︎▶︎▶︎︎▶︎▶︎

文献

+++++

その他の情報

Copyleft, CC, Mitzub'ixi Quq Chi'j, 1996-2099

☆☆

In mathematics and theoretical computer science, a type theory is the formal presentation of a specific type system.[a] Type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a foundation of mathematics. Two influential type theories that have been proposed as foundations are: Typed λ-calculus of Alonzo Church Intuitionistic type theory of Per Martin-Löf Most computerized proof-writing systems use a type theory for their foundation. A common one is Thierry Coquand's Calculus of Inductive Constructions.	数学および理論計算機科学において、タイプ理論（型理論）とは特定の型システムの形式的な提示である。いくつかの型理論は、数学の基礎としての集合論に代わるものである。基礎として提案された2つの影響力のある型理論がある：アロンゾ・チャーチの型付きλ微積分 Per Martin-Löfの直観主義型理論コンピュータによる証明書作成システムの多くは、その基礎に型理論を用いている。一般的なものとしては、ティエリー・コカンの帰納的構成論がある。
History Main article: History of type theory Type theory was created to avoid a paradox in a mathematical equation based on naive set theory and formal logic. Russell's paradox (first described in Gottlob Frege's The Foundations of Arithmetic) is that, without proper axioms, it is possible to define the set of all sets that are not members of themselves; this set both contains itself and does not contain itself. Between 1902 and 1908, Bertrand Russell proposed various solutions to this problem. By 1908, Russell arrived at a ramified theory of types together with an axiom of reducibility, both of which appeared in Whitehead and Russell's Principia Mathematica published in 1910, 1912, and 1913. This system avoided contradictions suggested in Russell's paradox by creating a hierarchy of types and then assigning each concrete mathematical entity to a specific type. Entities of a given type were built exclusively of subtypes of that type,[b] thus preventing an entity from being defined using itself. This resolution of Russell's paradox is similar to approaches taken in other formal systems, such as Zermelo-Fraenkel set theory.[3] Type theory is particularly popular in conjunction with Alonzo Church's lambda calculus. One notable early example of type theory is Church's simply typed lambda calculus. Church's theory of types[4] helped the formal system avoid the Kleene–Rosser paradox that afflicted the original untyped lambda calculus. Church demonstrated[c] that it could serve as a foundation of mathematics and it was referred to as a higher-order logic. In the modern literature, "type theory" refers to a typed system based around lambda calculus. One influential system is Per Martin-Löf's intuitionistic type theory, which was proposed as a foundation for constructive mathematics. Another is Thierry Coquand's calculus of constructions, which is used as the foundation by Coq, Lean, and other computer proof assistants. Type theory is an active area of research, one direction being the development of homotopy type theory.	沿革主な記事型理論の歴史型理論は、素朴な集合論と形式論理に基づく数学方程式におけるパラドックスを回避するために作られた。ラッセルのパラドックス（ゴットロープ・フレーゲの『算術の基礎』で初めて説明された）とは、適切な公理がなければ、自分自身のメンバーではないすべての集合の集合を定義することが可能であるというものである。1902年から1908年にかけて、バートランド・ラッセルはこの問題に対する様々な解決策を提案した。 1908年までにラッセルは、還元可能性の公理とともに、両者とも1910年、1912年、1913年に出版されたホワイトヘッドとラッセルの『プリンキピア・マテマティカ』に登場する、両者とも「反復された型の理論」に到達した。この体系では、型の階層を作り、具体的な数学的実体をそれぞれ特定の型に割り当てることで、ラッセルのパラドックスが示唆する矛盾を回避している。与えられた型の実体はその型の部分型だけで構成され[b]、実体がそれ自身を用いて定義されることを防いだ。このラッセルのパラドックスの解決は、ツェルメロ＝フレンケル集合論など、他の形式システムで取られたアプローチと類似している[3]。型理論は、特にアロンゾ・チャーチのラムダ計算と関連して人気がある。型理論の初期の顕著な例として、チャーチの単純型付きラムダ計算がある。チャーチの型理論[4]は、型付けされていないオリジナルのラムダ計算を苦しめていたKleene-Rosserのパラドックスを回避するのに役立った。チャーチはそれが数学の基礎として機能することを示し[c]、高次論理学と呼ばれるようになった。現代の文献では、「型理論」はラムダ計算を中心とした型付きシステムを指す。構成的数学の基礎として提唱されたペール・マルティン＝レフの直観主義的型理論もその一つである。もうひとつはティエリー・コカンの構成論であり、Coq、Lean、その他のコンピュータ証明支援システムで基礎として使われている。型理論は活発な研究分野であり、その一つの方向性はホモトピー型理論の発展である。
History of Type Theory The type theory was initially created to avoid paradoxes in a variety of formal logics and rewrite systems. Later, type theory referred to a class of formal systems, some of which can serve as alternatives to naive set theory as a foundation for all mathematics. It has been tied to formal mathematics since Principia Mathematica to today's proof assistants. 1900–1927 Origin of Russell's theory of types In a letter to Gottlob Frege (1902), Bertrand Russell announced his discovery of the paradox in Frege's Begriffsschrift.[1] Frege promptly responded, acknowledging the problem and proposing a solution in a technical discussion of "levels". To quote Frege: Incidentally, it seems to me that the expression "a predicate is predicated of itself" is not exact. A predicate is as a rule a first-level function, and this function requires an object as argument and cannot have itself as argument (subject). Therefore I would prefer to say "a concept is predicated of its own extension".[2] He goes about showing how this might work but seems to pull back from it. As a consequence of what has become known as Russell's paradox both Frege and Russell had to quickly amend works that they had at the printers. In an Appendix B that Russell tacked onto his The Principles of Mathematics (1903) one finds his "tentative" theory of types. The matter plagued Russell for about five years.[3] Willard Quine[4] presents a historical synopsis of the origin of the theory of types and the "ramified" theory of types: after considering abandoning the theory of types (1905), Russell proposed in turn three theories: the zigzag theory theory of limitation of size, the no-class theory (1905–1906) and then, readopting the theory of types (1908ff) Quine observes that Russell's introduction of the notion of "apparent variable" had the following result: the distinction between 'all' and 'any': 'all' is expressed by the bound ('apparent') variable of universal quantification, which ranges over a type, and 'any' is expressed by the free ('real') variable which refers schematically to any unspecified thing irrespective of type. Quine dismisses this notion of "bound variable" as "pointless apart from a certain aspect of the theory of types".[5] The 1908 "ramified" theory of types Quine explains the ramified theory as follows: "It has been so called because the type of a function depends both on the types of its arguments and on the types of the apparent variables contained in it (or in its expression), in case these exceed the types of the arguments".[5] Stephen Kleene in his 1952 Introduction to Metamathematics describes the ramified theory of types this way: The primary objects or individuals (i.e. the given things not being subjected to logical analysis) are assigned to one type (say type 0), the properties of individuals to type 1, properties of properties of individuals to type 2, etc.; and no properties are admitted which do not fall into one of these logical types (e.g. this puts the properties 'predicable' and 'impredicable' ... outside the pale of logic). A more detailed account would describe the admitted types for other objects as relations and classes. Then to exclude impredicative definitions within a type, the types above type 0 are further separated into orders. Thus for type 1, properties defined without mentioning any totality belong to order 0, and properties defined using the totality of properties of a given order belong to the next higher order. ... But this separation into orders makes it impossible to construct the familiar analysis, which we saw above contains impredicative definitions. To escape this outcome, Russell postulated his axiom of reducibility, which asserts that to any property belonging to an order above the lowest, there is a coextensive property (i.e. one possessed by exactly the same objects) of order 0. If only definable properties are considered to exist, then the axiom means that to every impredicative definition within a given type there is an equivalent predicative one (Kleene 1952:44–45). The axiom of reducibility and the notion of "matrix" But because the stipulations of the ramified theory would prove (to quote Quine) "onerous", Russell in his 1908 Mathematical logic as based on the theory of types[6] also would propose his axiom of reducibility. By 1910 Whitehead and Russell in their Principia Mathematica would further augment this axiom with the notion of a matrix — a fully extensional specification of a function. From its matrix a function could be derived by the process of "generalization" and vice versa, i.e. the two processes are reversible — (i) generalization from a matrix to a function (by using apparent variables) and (ii) the reverse process of reduction of type by courses-of-values substitution of arguments for the apparent variable. By this method impredicativity could be avoided.[7] Truth tables In 1921, Emil Post would develop a theory of "truth functions" and their truth tables, which replace the notion of apparent versus real variables. From his "Introduction" (1921): "Whereas the complete theory [of Whitehead and Russell (1910, 1912, 1913)] requires for the enunciation of its propositions real and apparent variables, which represent both individuals and propositional functions of different kinds, and as a result necessitates the cumbersome theory of types, this subtheory uses only real variables, and these real variables represent but one kind of entity, which the authors have chosen to call elementary propositions".[8] At about the same time Ludwig Wittgenstein developed similar ideas in his 1922 work Tractatus Logico-Philosophicus: 3.331 From this observation we get a further view – into Russell's Theory of Types. Russell's error is shown by the fact that in drawing up his symbolic rules he has to speak of the meanings of his signs. 3.332 No proposition can say anything about itself, because the propositional sign cannot be contained in itself (that is the whole "theory of types"). 3.333 A function cannot be its own argument, because the functional sign already contains the prototype of its own argument and it cannot contain itself... Wittgenstein proposed the truth-table method as well. In his 4.3 through 5.101, Wittgenstein adopts an unbounded Sheffer stroke as his fundamental logical entity and then lists all 16 functions of two variables (5.101). The notion of matrix-as-truth-table appears as late as the 1940–1950s in the work of Tarski, e.g. his 1946 indexes "Matrix, see: Truth table"[9] Russell's doubts Russell in his 1920 Introduction to Mathematical Philosophy devotes an entire chapter to "The axiom of Infinity and logical types" wherein he states his concerns: "Now the theory of types emphatically does not belong to the finished and certain part of our subject: much of this theory is still inchoate, confused, and obscure. But the need of some doctrine of types is less doubtful than the precise form the doctrine should take; and in connection with the axiom of infinity it is particularly easy to see the necessity of some such doctrine".[10] Russell abandons the axiom of reducibility: In the second edition of Principia Mathematica (1927) he acknowledges Wittgenstein's argument.[11] At the outset of his Introduction he declares "there can be no doubt ... that there is no need of the distinction between real and apparent variables...".[12] Now he fully embraces the matrix notion and declares "A function can only appear in a matrix through its values" (but demurs in a footnote: "It takes the place (not quite adequately) of the axiom of reducibility"[13]). Furthermore, he introduces a new (abbreviated, generalized) notion of "matrix", that of a "logical matrix . . . one that contains no constants. Thus p\|q is a logical matrix".[14] Thus Russell has virtually abandoned the axiom of reducibility,[15] but in his last paragraphs he states that from "our present primitive propositions" he cannot derive "Dedekindian relations and well-ordered relations" and observes that if there is a new axiom to replace the axiom of reducibility "it remains to be discovered".[16] Theory of simple types In the 1920s, Leon Chwistek[17] and Frank P. Ramsey[18] noticed that, if one is willing to give up the vicious circle principle, the hierarchy of levels of types in the "ramified theory of types" can be collapsed. The resulting restricted logic is called the theory of simple types[19] or, perhaps more commonly, simple type theory.[20] Detailed formulations of simple type theory were published in the late 1920s and early 1930s by R. Carnap, F. Ramsey, W.V.O. Quine, and A. Tarski. In 1940 Alonzo Church (re)formulated it as simply typed lambda calculus.[21] and examined by Gödel in 1944. A survey of these developments is found in Collins (2012).[22] 1940s–present Gödel 1944 Kurt Gödel in his 1944 Russell's mathematical logic gave the following definition of the "theory of simple types" in a footnote: By the theory of simple types I mean the doctrine which says that the objects of thought (or, in another interpretation, the symbolic expressions) are divided into types, namely: individuals, properties of individuals, relations between individuals, properties of such relations, etc. (with a similar hierarchy for extensions), and that sentences of the form: " a has the property φ ", " b bears the relation R to c ", etc. are meaningless, if a, b, c, R, φ are not of types fitting together. Mixed types (such as classes containing individuals and classes as elements) and therefore also transfinite types (such as the class of all classes of finite types) are excluded. That the theory of simple types suffices for avoiding also the epistemological paradoxes is shown by a closer analysis of these. (Cf. Ramsey 1926 and Tarski 1935, p. 399).".[23] He concluded the (1) theory of simple types and (2) axiomatic set theory, "permit the derivation of modern mathematics and at the same time avoid all known paradoxes" (Gödel 1944:126); furthermore, the theory of simple types "is the system of the first Principia [Principia Mathematica] in an appropriate interpretation. . . . [M]any symptoms show only too clearly, however, that the primitive concepts need further elucidation" (Gödel 1944:126). Curry–Howard correspondence, 1934–1969 The Curry–Howard correspondence is the interpretation of proofs-as-programs and formulae-as-types. The idea starting in 1934 with Haskell Curry and finalized in 1969 with William Alvin Howard. It connected the "computational component" of many type theories to the derivations in logics. Howard showed that the typed lambda calculus corresponded to intuitionistic natural deduction (that is, natural deduction without the Law of excluded middle). The connection between types and logic lead to a lot of subsequent research to find new type theories for existing logics and new logics for existing type theories. de Bruijn's AUTOMATH, 1967–2003 Nicolaas Govert de Bruijn created the type theory Automath as a mathematical foundation for the Automath system, which could verify the correctness of proofs. The system developed and added features over time as type theory developed. Martin-Löf's Intuitionistic type theory, 1971–1984 Per Martin-Löf found a type theory that corresponded to predicate logic by introducing dependent types, which became known as intuitionistic type theory or Martin-Löf type theory. Martin-Löf's theory uses inductive types to represent unbounded data structures, such as natural numbers. Martin-Löf's presentation of his theory using rules of inference and judgments becomes the standard for presenting future theories. Coquand and Huet's Calculus of Constructions, 1986 Thierry Coquand and Gérard Huet created the Calculus of Constructions,[24] a dependent type theory for functions. With inductive types, it would be called "the Calculus of Inductive Constructions" and become the basis for Coq and Lean. Barendregt's lambda cube, 1991 The lambda cube was not a new type theory but a categorization of existing type theories. The eight corners of the cube included some existing theories with simply typed lambda calculus at the lowest corner and the calculus of constructions at the highest. Identity Proofs are Not Unique, 1994 Prior to 1994, many type theorists thought all terms of the same identity type were the same. That is, that everything was reflexivity. But Martin Hofmann and Thomas Streicher showed that that was not required by the rules of the identity type. In their paper, "The Groupoid Model Refutes Uniqueness of Identity Proofs",[25] they showed that equality terms could be modeled as a group where the zero element was "reflexitivity", addition was "transitivity" and negation was "symmetry". This opened up a new area of research, homotopy type theory, where category theory was applied to the identity type. https://en.wikipedia.org/wiki/History_of_type_theory	タイプ理論（型理論）の歴史型理論は当初、様々な形式論理や書き換えシステムにおけるパラドックスを回避するために作られた。その後、型理論とは、すべての数学の基礎となる素朴な集合論の代わりとなるような、一群の形式的体系を指すようになった。プリンキピア・マテマティカ以来、今日の証明支援に至るまで、形式数学と結びついている。 1900-1927 ラッセルの型理論の起源 1902年、バートランド・ラッセルはゴットローブ・フレーゲに宛てた手紙の中で、フレーゲのベグリフシュリフトにおけるパラドックスの発見を発表した [1]。フレーゲの言葉を引用しよう：ところで、「述語はそれ自身を述語とする」という表現は正確ではないようだ。述語は原則として第一レベルの関数であり、この関数は引数として対象を必要とし、それ自体を引数（主語）として持つことはできない。したがって、私は「概念はそれ自身の拡張を述語とする」と言った方がいいと思う[2]。彼はこれがどのように機能するかを示そうとしているが、そこから後退しているように見える。ラッセルのパラドックスとして知られるようになったことの結果として、フレーゲとラッセルの両者は、印刷所で持っていた著作をすぐに修正しなければならなかった。ラッセルが『数学原理』（1903年）に付け加えた付録Bには、彼の「暫定的な」型の理論がある。この問題はラッセルを5年ほど悩ませた[3]。ウィラード・クワイン[4]は、型の理論と「ramified」型の理論の起源に関する歴史的な概略を提示している：型の理論の放棄を検討した後（1905年）、ラッセルは順番に3つの理論を提案した：ジグザグ理論大きさの制限の理論無階級理論（1905-1906年）である、型理論の再採用(1908ff) クワインは、ラッセルが「見かけの変数」という概念を導入した結果、次のようなことが起こったと述べている： all」と「any」の区別である： all」は普遍量化の束縛された（「見かけの」）変数によって表現され、それは型の範囲に及ぶものであり、「any」は自由な（「現実の」）変数によって表現される。クワインはこの「束縛された変数」という概念を「型の理論のある側面を除けば無意味なもの」として退けている[5]。 1908年の「ramified」型理論クワインはramified理論について次のように説明している：関数の型がその引数の型と、その関数に含まれる（またはその式に含まれる）見かけ上の変数の型の両方に依存し、それらが引数の型を超える場合、関数の型はその引数の型に依存するため、このように呼ばれるようになった」[5] Stephen Kleeneは1952年の『メタ数学入門』の中で、ramified theory of typesをこのように説明している：一次的な対象や個体（すなわち、論理的分析の対象とならない与えられたもの）は一つの型（例えば0型）に、個体の性質は1型に、個体の性質の性質は2型に、といった具合に割り当てられ、これらの論理的型のいずれにも当てはまらない性質は認められない（例えば、これによって「予測可能」と「予測不可能」という性質は...論理学の埒外に置かれることになる）。より詳細な説明では、関係やクラスなど、他の対象について認められる型を記述することになる。そして、型内の述語的定義を除外するために、型0以上の型はさらに順序に分けられる。従って、タイプ1では、全体性に言及せずに定義された性質はオーダー0に属し、与えられたオーダーの性質の全体性を用いて定義された性質は、次の上位のオーダーに属する。... しかし、このように次数に分離されると、上で見たような非可述的な定義を含むおなじみの分析を構成することが不可能になる。もし定義可能な性質だけが存在すると考えるなら、この公理は、与えられた型内のすべての非述語的定義に等価な述語的定義が存在することを意味する（Kleene 1952:44-45）。還元性の公理と「行列」の概念ラッセルは1908年の『型の理論に基づく数学論理学』[6]で還元性の公理を提案している。1910年までにホワイトヘッドとラッセルは『プリンキピア・マテマティカ』の中で、この公理を行列の概念（関数の完全な拡張的仕様）でさらに補強することになる。すなわち、（i）行列から関数への（見かけの変数を使った）一般化と、（ii）見かけの変数に対する引数の代入による型の減少という逆のプロセスである。この方法によって impredicativityを回避することができる[7]。真理値表 1921年、エミール・ポストは「真理関数」とその真理値表の理論を開発する。彼の「序論」（1921年）より：「ホワイトヘッドとラッセル(1910, 1912, 1913)の）完全な理論が、命題の発音のために、個体と異なる種類の命題関数の両方を表す実変数と見かけの変数を必要とし、その結果、面倒な型の理論を必要とするのに対して、この副次的な理論は実変数のみを使用し、これらの実変数は、著者たちが素命題と呼ぶことにした1種類の実体を表す」[8]。ほぼ同時期に、ルートヴィヒ・ウィトゲンシュタインが1922年の著作『論理哲学綱要』の中で同様の考えを展開している： 3.331 この観察から、ラッセルの「類型論」に対するさらなる見解が得られる。ラッセルの誤りは、記号規則を作成する際に、記号の意味を語らなければならないという事実によって示される。 3.332 命題はそれ自身について何も語ることができない。なぜなら、命題記号はそれ自身に含まれることができないからである（これが「型の理論」全体である）。 3.333 関数はそれ自身の論証にはなりえない。なぜなら、機能記号はそれ自身の論証の原型をすでに含んでおり、それ自身を含むことはできないからである...。ウィトゲンシュタインは真理値表法も提案した。彼の4.3から5.101において、ウィトゲンシュタインは彼の基本的な論理的実体として束縛のないシェファー・ストロークを採用し、そして2変数の16の関数をすべて列挙している（5.101）。真理値表としての行列の概念は、1940-1950年代のタルスキーの研究において、例えば1946年の索引 "Matrix, see：真理値表"[9]などである。ラッセルの疑念ラッセルは1920年の『数理哲学入門』の中で、「無限の公理と論理的型」に章全体を割いており、そこで自分の懸念を述べている：「この理論の多くはまだ未熟で、混乱しており、不明瞭である。しかし、ある種の型の教義の必要性は、その教義がとるべき正確な形よりも、それほど疑わしくはない。そして、無限の公理との関連において、そのような教義の必要性を見ることはとりわけ容易である」[10]。ラッセルは還元可能性の公理を放棄する：プリンキピア数学』の第2版（1927年）において、彼はウィトゲンシュタインの議論を認めている[11]。序論の冒頭で、彼は「実変数と見かけの変数の区別が必要ないことは......疑う余地がない」と宣言している[12]。さらに、彼は「行列」の新しい（省略され、一般化された）概念、すなわち「論理行列......」を導入している。定数を含まないものである。したがって、p\|qは論理行列である」[14]。このようにラッセルは事実上、還元可能性の公理を放棄した[15]が、最後の段落で彼は「現在の原始命題」から「デデキンディアン関係と整序関係」を導くことはできないと述べ、還元可能性の公理に代わる新しい公理があるとすれば「それは発見されるままである」と述べている[16]。単純型の理論 1920年代、Leon Chwistek[17]とFrank P. Ramsey[18]は、悪循環の原理を放棄することを厭わなければ、「ラム化された型の理論」における型のレベルの階層を崩すことができることに気づいた。単純型理論の詳細な定式化は1920年代後半から1930年代前半にかけてR.カーナップ、F.ラムゼイ、W.V.O.クワイン、A.タルスキーによって発表された。1940年にはアロンゾ・チャーチが単純型付きラムダ計算として（再）定式化し[21]、1944年にはゲーデルによって検討された。これらの発展に関するサーベイがCollins (2012) にある[22]。 1940年代-現在ゲーデル1944年クルト・ゲーデルは1944年の『ラッセルの数理論理学』において、脚注の中で「単純型の理論」について次のように定義している：単純型の理論とは、思考の対象（別の解釈では記号表現）は、個体、個体の性質、個体間の関係、そのような関係の性質などの型に分けられ（拡張についても同様の階層がある）、次のような形式の文があるという教義を意味する：「aはφという性質を持つ」、「bはcに対してRという関係を持つ」などという形の文は、a、b、c、R、φが互いに適合する型でなければ意味がない。混合型（個体とクラスを要素として含むクラスなど）、したがって超限定型（有限型のすべてのクラスのクラスなど）は除外される。単純型の理論が認識論的パラドックスも回避するのに十分であることは、これらをより詳細に分析することによって示される。(Ramsey 1926およびTarski 1935, p. 399参照）」[23]。彼は、(1)単純型の理論と(2)公理的集合論は「現代数学の導出を可能にし、同時にすべての既知のパラドックスを回避する」(Gödel 1944:126)、さらに単純型の理論は「適切な解釈における最初のプリンキピア[Principia Mathematica]の体系である。. . . [しかし、どのような症状も、原初的な概念にはさらなる解明が必要であることをはっきりと示している」(Gödel 1944:126)。カリー-ハワード書簡、1934年-1969年カリー-ハワード対応とは、証明-プログラム、式-型という解釈である。1934年にハスケル・カリーが提唱し、1969年にウィリアム・アルヴィン・ハワードが提唱した。これは多くの型理論の「計算要素」を論理学の導出と結びつけるものである。ハワードは型付きラムダ計算が直観主義的自然演繹（つまり排中律のない自然演繹）に対応することを示した。型と論理の結びつきは、既存の論理のための新しい型理論や、既存の型理論のための新しい論理を見つけるという、その後の多くの研究につながった。 de BruijnのAUTOMATH, 1967-2003 Nicolaas Govert de Bruijnは、証明の正しさを検証するAutomathシステムの数学的基礎として、型理論Automathを作成した。このシステムは、型理論の発展とともに発展し、機能を追加していった。マーティン=レフの直観主義型理論（1971年-1984年 Per Martin-Löfは、従属型を導入することで述語論理に対応する型理論を発見し、直観主義型理論またはMartin-Löf型理論として知られるようになった。 Martin-Löfの理論は、自然数などの非束縛データ構造を表現するために帰納的型を用いる。 Martin-Löfは、推論と判断のルールを用いて理論を提示し、これが後の理論提示の標準となった。 CoquandとHuetのCalculus of Constructions（1986年ティエリー・コカン（Thierry Coquand）とジェラール・ユエ（Gérard Huet）は、関数のための従属型理論である「Calculus of Constructions」[24]を作った。帰納的型を持つこの理論は「帰納的構成論」と呼ばれ、CoqとLeanの基礎となった。バレンドレヒトのラムダキューブ、1991年ラムダキューブは新しい型理論ではなく、既存の型理論を分類したものである。キューブの8つの角には、既存の理論がいくつか含まれており、最も低い角には単純型ラムダ計算が、最も高い角にはコンストラクション計算があった。同一性証明は唯一無二ではない 1994年 1994年以前、多くの型理論家は、同じID型の項はすべて同じだと考えていた。つまり、すべてが再帰性だと考えていたのだ。しかし、Martin HofmannとThomas Streicherは、それが同一性の型の規則では要求されないことを示した。彼らの論文「The Groupoid Model Refutes Uniqueness of Identity Proofs」[25]では、等式項が、ゼロ要素が「再帰性」、加算が「推移性」、否定が「対称性」である群としてモデル化できることを示した。これにより、ホモトピー型理論という新しい研究分野が開かれ、カテゴリー理論が恒等式に適用された。