21/10/25 00:09:10.20 wB/2IR+g.net
>>509
>>で、制限された内包公理で、Zermeloはパラドックスを避けることにしたわけです
>>結果、”in first-order logic”だったわけです
>Fregeの最初の理論には型がない
>一方型理論では無限に型がある つまり無限階論理ｗ
なんか変
おかしいね
”in first-order logic”＝一階述語論理
型理論でも、”基盤となる論理は一階述語論理”もあるし
型理論での、高位の型、超限数個の型があってもなんら不都合は生じない という記述と混同または誤解しているようだな
”高階述語論理の例として、アロンゾ・チャーチの Simple Theory of Types”とあるから、高階まで
「無限階論理」という用語は、存在しないのでは？
なお、「無限論理」と「∞カテゴリー」という用語は存在する
もう、無茶苦茶やね
書いていること
うろ覚えのデタラメじゃんｗ
URLﾘﾝｸ(ja.wikipedia.org)
型理論（かたりろん、英: Type theory）は、集合論を数学基礎論の観点から代替する目的で提唱された理論である。階型理論（かいけいりろん、英: Theory of Types）とも呼ばれる。20世紀初頭にバートランド・ラッセルが、いわゆるラッセルのパラドックスによってフレーゲの素朴集合論から矛盾が導き出されるという発見を説明するために提唱した、型の仮説群（theories of type）が型理論の始まりであり、後に簡約可能性公理（Axiom of reducibility）を随伴したその詳細は、ホワイトヘッドとラッセルの 『プリンキピア・マテマティカ』に収録されている。型理論は通常、計算機科学およびコンピュータプログラミングで用いられる型システムの学術研究として認知されている。
現在の型理論で有名なものは、アロンゾ・チャーチによる型付きラムダ計算と、マルティン・レーフによる直観主義型理論の二つである。
つづく