26/08/01 11:03:25.71 sQaREFls.net
>>719
>そもそも素朴集合論が矛盾を抱えた欠陥品だったからこそZF集合論が開発されたのに、あとから「結局正しい」とされる訳が無い。
>自分の持論こそ正しいと信じて疑わないど素人さんにも困ったものだ。
そう近視眼的な見方は、よろしくないね
・一つは、歴史的な順を理解することだね
つまり、カントール集合論があってこそ、公理的集合論が生まれたことと
カントールが得ていた集合論の結論（定理）は、矛盾なく公理的集合論で再現されたこと
・ZF集合論などが常用する記号による主に一階述語論理は
出来上がった定理証明や 理論展開用には 優れている面はあるが
まだ 海のものとも山のものともつかぬ対象を考えていくのには向かない
（つまり、これから新しい数学理論を作っていくときは、自然言語がベースになる）
実際、ZFないしZFC公理系のロジックだけで 自然言語は殆ど使わないというような、
数学テキストは 現在は存在しないだろう
一方で、コンピューター言語は 主は記号論理のみで 自然言語はコメントのみ
Rocq（旧Coq）や Lean >>720 は、こちら
(参考)>>720 より追加
URLﾘﾝｸ(en.wikipedia.org)
Type_theory
(google訳)
型理論
歴史
メイン記事：型理論の歴史
型理論は、素朴集合論や形式論理におけるパラドックス、例えばラッセルのパラドックスなどを回避するために考案されました。ラッセルのパラドックスとは、適切な公理がない場合、自分自身の要素ではないすべての集合の集合を定義することが可能であり、この集合は自分自身を含みつつ、自分自身を含まないという矛盾を抱えていることを示すものです。1902年から1908年にかけて、バートランド・ラッセルはこの問題に対する様々な解決策を提案しました。
1908年までに、ラッセルは型に関する分岐理論と還元可能性の公理に到達し、これらはどちらも1910年、1912年、1913年に出版されたホワイトヘッドとラッセルの『プリンキピア・マテマティカ』に登場した。この体系は、型の階層構造を作成し、各具体的な数学的実体を特定の型に割り当てることで、ラッセルのパラドックスで示唆された矛盾を回避した。ある型の実体は、その型のサブタイプのみから構成されるため、実体がそれ自身を用いて定義されることはなかった。このラッセルのパラドックスの解決は、ツェルメロ＝フレンケル集合論などの他の形式体系で採用されているアプローチと類似している。[ 4 ]