1. 概要
ジョン・バークリー・ロッサー・シニア(John Barkley Rosser Sr.ジョン・バークリー・ロッサー・シニア英語、1907年12月6日 - 1989年9月5日)は、アメリカの論理学者であり、数学者である。アロンゾ・チャーチの学生として学び、ラムダ計算におけるチャーチ＝ロッサーの定理の共同証明者として知られる。また、数論分野でロッサーの篩を開発し、素数に関するロッサーの定理を証明した。
彼の学術的キャリアは、コーネル大学数学科で長年にわたり、数回学科長を務めた後、ウィスコンシン大学マディソン校の陸軍数学研究所所長、そして国防分析研究所(IDA)の通信研究部門初代責任者として国防研究にも貢献した。ロッサーは、ゲーデルの不完全性定理を強化したロッサーのからくりや、クリーネ＝ロッサーのパラドックスの発見でも知られており、数多くの数学の教科書を執筆した。
2. 生涯
ジョン・バークリー・ロッサーは、アメリカ合衆国で生まれ、教育を受け、数理論理学と整数論の分野で重要な貢献をしました。彼の人生は、学術研究と国家の防衛研究に捧げられました。
2.1. 幼少期と教育
ロッサーは1907年12月6日にフロリダ州のジャクソンビルで生まれた。彼は著名な論理学者であるアロンゾ・チャーチの指導のもとで学んだ。
2.2. 学術的キャリア
ロッサーの学術的キャリアは、複数の著名な学術機関と国防関連の研究機関にわたって展開された。
2.2.1. コーネル大学時代
ロッサーは1936年から1963年までコーネル大学の数学科に在籍し、その期間中に数回、学科長を務めた。この時期に彼は数理論理学および整数論の分野で重要な研究を推進した。
2.2.2. ウィスコンシン大学および国防研究機関
コーネル大学を離れた後、ロッサーはウィスコンシン大学マディソン校に設置された陸軍数学研究所の所長を務めた。さらに、彼は国防分析研究所(IDA)の通信研究部門(Communications Research Divisionコミュニケーションズ・リサーチ・ディビジョン英語)の初代責任者としての役割も担い、国防研究の領域にも貢献した。
2.3. 私生活
ロッサーには、数学経済学者であった息子、ジョン・バークリー・ロッサー・ジュニア(John Barkley Rosser Jr.ジョン・バークリー・ロッサー・ジュニア英語)がいる。ジュニアはジェームズ・マディソン大学の教授を務めた。
2.4. 死去
ロッサーは1989年9月5日にウィスコンシン州マディソンの自宅で動脈瘤により死去した。
3. 主要な業績
ジョン・バークリー・ロッサーは、数理論理学と整数論の分野でいくつかの画期的な業績を残した。
3.1. チャーチ＝ロッサーの定理
ロッサーは、師であるアロンゾ・チャーチと共に、ラムダ計算におけるチャーチ＝ロッサーの定理を証明した。この定理は、ラムダ計算における式の評価が、評価の順序に依存せず、最終的な結果が一意に定まる(強い正規形を持つ)ことを保証するもので、ラムダ計算の基礎理論において極めて重要な位置を占めている。
3.2. ロッサーのからくりとゲーデルの不完全性定理
1936年、ロッサーはゲーデルの不完全性定理を強化する「ロッサーのからくり」を証明した。ゲーデルの元の定理では、無矛盾で十分に強力な形式的体系において、証明も反証もできない命題が存在するためには、その体系がω-無矛盾性(ω-consistencyオメガ無矛盾性英語)を満たす必要があるとされた。しかし、ロッサーのからくりでは、この条件を単なる無矛盾性に緩和し、より一般的な形式的体系に適用できることを示した。
ゲーデルの定理が「私は証明できない」という虚偽のパラドックスに相当する文を使用したのに対し、ロッサーは「私のあらゆる証明に対して、私の否定のより短い証明が存在する」という文を用いた。この巧妙な構成により、より弱い前提の下で不完全性を導き出すことが可能になった。
3.3. ロッサーの篩とロッサーの定理
数論の分野では、ロッサーは「ロッサーの篩」として知られる篩法の一種を開発した。これは、特定の条件下で素数を数える際の上界と下界を評価するために用いられる強力なツールである。また、彼は素数の分布に関する「ロッサーの定理」を証明した。これは、素数の分布をより正確に理解するための貢献であり、解析的整数論における重要な成果の一つとされている。
3.4. クリーネ＝ロッサーのパラドックス
ロッサーは、スティーヴン・クリーネと共に「クリーネ＝ロッサーのパラドックス」を発見した。このパラドックスは、元々のラムダ計算が矛盾を含んでいたことを示した。具体的には、ある特定の式が、あらゆる型を持つことを許してしまうという矛盾を指摘し、型理論を持たない純粋なラムダ計算が健全でないことを明らかにした。この発見は、後に型付きラムダ計算やより厳密な形式的体系の発展を促す契機となった。
4. 著作物
ジョン・バークリー・ロッサーは、数々の重要な数学の教科書や学術出版物を執筆し、数学および論理学の発展に貢献した。
- 『変数を持たない数理論理学』(A mathematical logic without variables英語) - 1934年、プリンストン大学の博士論文(p. 127-150, 328-355)。
- 『数学者のための論理学』(Logic for mathematicians英語) - 1953年にマグロウヒル社から出版。1978年にはチェルシー出版から第2版が出版された(578ページ、ISBN 0-8284-0294-9)。
- 『ラムダ計算の歴史のハイライト』(Highlights of the History of Lambda calculus英語) - 1984年、『アンナルズ・オブ・ザ・ヒストリー・オブ・コンピューティング』誌(第6巻第4号、p. 337-349)に掲載。
- 『簡略化された独立性証明：集合論のブール値モデル』(Simplified Independence Proofs: Boolean Valued Models of Set Theory英語) - 1969年、アカデミックプレス社から出版。
彼の著作物の完全なリストは、テキサス大学の記録管理のウェブサイトで確認できる[http://www.lib.utexas.edu/taro/utcah/00212/cah-00212.html ロッサーの論文集]。
5. 評価と影響
ジョン・バークリー・ロッサーの数学および論理学分野への貢献は、数理論理学の基礎、特に計算可能性理論と証明論において極めて重要である。チャーチ＝ロッサーの定理はラムダ計算の基本特性を確立し、その後の関数型プログラミング言語や計算理論の発展に不可欠な基盤を提供した。
彼のロッサーのからくりは、ゲーデルの不完全性定理の適用範囲を広げ、数学の基礎論における無矛盾性の概念の理解を深めた。これは、形式的体系の限界に関する洞察を提供する上で、画期的な業績と評価されている。また、ロッサーの篩やロッサーの定理といった数論への貢献は、素数の分布研究に新たな手法と知見をもたらした。
クリーネ＝ロッサーのパラドックスの発見は、ラムダ計算の初期の形式における矛盾を浮き彫りにし、型理論の必要性を認識させる上で重要な役割を果たした。これにより、より厳密で健全な形式的体系の構築へと研究がシフトする契機となった。
ロッサーの著作、特に『数学者のための論理学』は、多くの学生や研究者にとって標準的な教科書となり、論理学の教育に大きな影響を与えた。彼の業績は、現代の計算機科学、プログラミング言語理論、人工知能の基盤を築く上で、間接的ではあるが決定的な役割を果たした。
6. 外部リンク
- [https://web.archive.org/web/20020308033648/http://infoshare1.princeton.edu/libraries/firestone/rbsc/finding_aids/mathoral/pm02.htm プリンストン大学でのロッサーとスティーヴン・クリーネへのインタビュー]