23/01/02 11:52:57.82 qZFMMNjk.net
>>301
>ハスケル・カリーすげぇ
> URLﾘﾝｸ(ja.wikipedia.org)
そっちは、迷走でしょう
まずは、下記のラッセルのパラドックスから、スタートでしょう
そして、下記ラッセルでは触れていないが、一階述語論理についても触れないと
(参考)
URLﾘﾝｸ(ja.wikipedia.org)
ラッセルのパラドックス
ラッセルが型理論（階型理論）を生み出した目的にはこの種のパラドックスを解消するということも含まれていた[5]。
概要
ラッセルのパラドックスとは、自分自身を要素として含まない集合全体の集合 R={x｜ x not∈ x} の存在から矛盾が導かれるという、素朴集合論におけるパラドックスである。いま R∈ R と仮定すると、R の定義より R not∈ R となるから、これは矛盾となる。したがって（仮定無しで） R not∈ R である。ところが R の定義より R∈ R となるから、やはり矛盾となる。
集合論が形式化されていないことは矛盾の原因ではない。このパラドックスは古典述語論理上の理論として形式化された無制限な内包公理を持つ素朴集合論においても生ずる。上記の証明では排中律並びにそれと同等な論理法則を用いていないから、直観主義論理上の素朴集合論においても矛盾は生ずる。したがって論理を古典論理から直観主義論理に変更しても、ラッセルのパラドックスは回避できない。パラドックスの回避については、様々な方法が提案されている。詳細は矛盾の解消を参照。
矛盾の解消
集合論の公理は通常の数学を集合論の上で展開するために十分なだけの集合の存在を保証しつつ、パラドックスを発生させる集合は構成できないように慎重に設定する必要がある。
1.公理的集合論による解消[6]
2.単純型理論による解消[7]
3.部分構造論理による解消[8]
URLﾘﾝｸ(ja.wikipedia.org)
一階述語論理
ZFC は一階述語論理を用いて形式化されており、数学の大部分はそのように形式化された ZFC の中で行うことができる。
(引用終り)
以上