[過去ﾛｸﾞ] Inter-universal geometry と ABC予想 (応援スレ) 45 (1002ﾚｽ)
上下前次1-新
抽出解除 ﾚｽ栞
このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索 歴削→次ｽﾚ 栞削→次ｽﾚ 過去ﾛｸﾞﾒﾆｭｰ
ﾘﾛｰﾄﾞ規制です｡10分ほどで解除するので､他のﾌﾞﾗｳｻﾞへ避難してください｡
608(1): 現代数学の系譜 雑談 ◆e.a0E5TtKE 2020/05/13(水)13:11 ID:uMe8boWM(6/22) AAS
>>607
つづき
型無しラムダ計算
20年ほど時代を下り，1930年代に話題を移そう．若き日の Alonzo Church は，自由変数を用いない*19形式論理学の記法あるいは計算体系として，ラムダ計算を提案する．
初出は1932年の A Set of Postulates for the Foundation of Logic であるようで，表題からも分かる通り，この頃の Church はラムダ計算を論理学の基礎として据えようと考えていたらしく，項として種々の論理定項を含んでいる．
しかし，このオリジナルの体系は証明力が強すぎたため，後に Stephen Kleene と John Barkley Rosser らにより矛盾を導くことが証明された*20．
単純型付ラムダ計算
省3
609: 現代数学の系譜 雑談 ◆e.a0E5TtKE 2020/05/13(水)13:12 ID:uMe8boWM(7/22) AAS
>>608
停止性問題・Godel の不完全性定理・対角線論法
Russell のパラドクスに始まり，[Math Processing Error] や [Math Processing Error] といった自己言及・自己適用を含んだ表現について見てきたが，計算機科学の素養がある読者なら，停止性問題の決定不能性の証明が，ある種の自己適用を用いたものだったことを思い出すかもしれない*27．
Godel の不完全性定理に登場する「この文は証明できない」といういわゆる Godel 文も自己言及を含んでいる．このように，ある種の自己言及を仮定すると矛盾を導く論法は対角線論法として知られている．
終わりに
これまで見てきたように，制限のない自己言及はしばしば矛盾を引き起こす．
これを防ぐために Russell は型の概念を発明し，論理学における式がどのような文脈で出現できるかに制限を加え，Church はこのアイディアを拝借し，ラムダ計算における式がどのような文脈で出現できるかに制限を加えた．
省5
上下前次1-新書関写板覧索設栞歴
ｽﾚ情報 赤ﾚｽ抽出 画像ﾚｽ抽出 歴の未読ｽﾚ AAｻﾑﾈｲﾙ
ぬこの手 ぬこTOP 0.035s