∑ 数学名人档案库
← 返回 王浩 简介档案 深度档案
数理逻辑计算机科学哲学

王浩（Hao Wang）

20 世纪少有的横跨数理逻辑、计算机科学与哲学的通才——他在 IBM 704 上用 9 分钟证明了《数学原理》中数百条定理，拉开了自动定理证明的时代大幕；他发明的「王浩铺砖」成为计算理论与复杂性理论的经典工具，其学生发现的非周期铺砖直接启发了彭罗斯铺砖与准晶；而他生命最后二十年与哥德尔的深度对话，使他成为哥德尔晚年思想无可替代的见证者与阐释者。

一、生平与时代背景

王浩 1921 年 5 月 20 日生于山东济南。他早年在中国受教育：1943 年获国立西南联合大学数学理学学士学位，1945 年获清华大学哲学硕士学位，在清华的老师包括哲学家冯友兰与金岳霖。1946 年他赴哈佛大学攻读逻辑与哲学，师从 W. V. O. 奎因（Willard Van Orman Quine），1948 年获博士学位，同年被聘为哈佛大学助理教授。

此后他的学术生涯在西方展开，但 1972 年后多次回到中国，并于 1985 年、1986 年分别成为北京大学与清华大学的名誉教授。1948—1951 年他任哈佛初级研究员（Junior Fellow of the Society of Fellows），其中 1950—1951 年在苏黎世与保罗·贝奈斯（Paul Bernays）合作。1956 年前他任哈佛哲学助理教授，1953—1955 年请假：1953—1954 年在 Burroughs 公司工作，1954—1955 年在国外，并于 1955 年春在牛津大学作约翰·洛克讲座（John Locke Lectures）。1956 年他任牛津大学数学哲学高级讲师（Reader）。1961 年回到哈佛，任 Gordon McKay 数理逻辑与应用数学教授。1967 年他任洛克菲勒大学教授，创立了一个逻辑研究组，使洛克菲勒成为活跃的逻辑研究中心（尤其是集合论）；1976 年该研究组被校方解散，只剩王浩一人，他一直留任到 1991 年退休，甚至退休后仍在那里工作。

1972 年，他加入由任之恭（Chih-Kung Jen）率领的首批美籍华裔科学家访华代表团。1983 年他获国际人工智能联合会议（IJCAI）颁发的首届自动定理证明里程碑奖（Milestone Prize for Automated Theorem Proving）。

1995 年 5 月 13 日，王浩在纽约医院（New York Hospital）因淋巴瘤去世，距其 74 岁生日仅一周。遗孀为 Hanne Tierney，另有一女二子。

二、学术生涯年表

年份 事件
1921 5 月 20 日生于山东济南
1943 获国立西南联合大学数学理学学士
1945 获清华大学哲学硕士（导师含冯友兰、金岳霖）
1946 赴哈佛大学，师从奎因学习逻辑与哲学
1948 获哈佛博士学位；同年任哈佛助理教授
1950 发表论文修正奎因 ML 集合论系统
1950—1951 在苏黎世与贝奈斯合作
1954 发表《数学的形式化》，提出直谓基础与自主迭代
1955 春在牛津作约翰·洛克讲座
1956 任牛津大学数学哲学高级讲师（Reader）
1959—1960 在 IBM 704 上实现《数学原理》定理的自动证明；发表《走向机械数学》
1961 回哈佛任 Gordon McKay 数理逻辑与应用数学教授
1962 与 Kahr、Moore 证明 AEA 情形判定问题不可解；引入王浩铺砖/多米诺问题
1966 任洛克菲勒大学教授，创立逻辑研究组
1967 与哥德尔首次通信，开启长期对话
1971 起与哥德尔频繁面谈
1972 参加首批美籍华裔科学家访华团
1974 出版《从数学到哲学》
1976 洛克菲勒逻辑组被校方解散，独留至退休
1983 获 IJCAI 首届自动定理证明里程碑奖
1985 出版《超越分析哲学》；任北大名誉教授
1986 任清华名誉教授
1987 出版《哥德尔的反思》
1991 从洛克菲勒退休
1995 5 月 13 日因淋巴瘤病逝于纽约，享年 73 岁
1996 遗著《逻辑之旅：从哥德尔到哲学》出版

三、核心成果（逐条技术解析）

1. 修正奎因的 ML 集合论系统（1950）

问题背景：奎因 1940 年《数理逻辑》（Mathematical Logic, ML）中的集合论系统，被 J. Barkley Rosser 证明是不一致的（库里悖论的一个变种）。奎因本人给出了一个他称之为「权宜之计」的修补。

关键思想：王浩更深入地分析了这一局面，在 1950 年的论文《形式逻辑系统》中给出了 ML 原本意图的正确表述：在奎因著名的 NF（New Foundations）系统所允许的集合之上，添加（可以是非直谓的）类（classes）。他给出了该系统相对于 NF 一致性的模型论证明。

结果：后来被称为 ML 的系统就是王浩的修正版，并被收入奎因著作 1951 年第二版。这是集合论基础研究的一项重要工作。

与前人关系：NF 由奎因 1937 年提出；王浩的贡献是修复并给出 ML 的正确、相对一致的版本。

2. 直谓主义数学基础与自主迭代（1954）

问题背景：直谓主义（predicativism）拒绝「循环定义」——不能用包含被定义对象本身的总体来定义它。外尔（Hermann Weyl）在 1918 年尝试用直谓方式重建分析，但未完成。

关键思想：王浩 1954 年在《数学的形式化》中构造了一个由序数加标的直谓分支系统（ramified systems）的超穷序列，与洛伦岑（Lorenzen）的同期工作一起，复兴了外尔开创的直谓分析路线。为回答「哪些序数可被允许用来加标序列」，他提出了一个富有启发性的自主迭代（autonomous iteration）原则：若一个序型为 $\beta$ 的序关系在系统 $\Sigma_\alpha$ 中可定义，则以 $\beta$ 加标的系统序列应当被接纳。

结果与局限：这一自主迭代思想在后来对直谓性的分析中发挥了重要作用。但正如 Parsons 所指出，王浩的具体原则并未达到他设想的效果：所有递归序数都是可接纳的，而递归 $\alpha$ 对应的 $\Sigma_\alpha$ 中可定义的序关系都是超算术的，由 Spector 定理可知它们不会产生新的序数。尽管如此，这一思路深刻影响了费弗曼（Feferman）等人后来对直谓性的精确刻画。

3. 计算机自动定理证明：《走向机械数学》（1960）

问题背景：能否让计算机自动证明数学定理？1950 年代人工智能先驱 Newell、Shaw、Simon 的「逻辑理论家」走启发式搜索路线，效率很低。

关键思想：王浩在 IBM 期间，运用 Herbrand 与 Gentzen 开创的逻辑分析方法（而非启发式搜索），直接处理一阶逻辑的证明搜索。1959 年他在 IBM 704 计算机上编写程序。

结果：1960 年发表于 IBM Journal of Research and Development 的《走向机械数学》（Toward Mechanical Mathematics）报告：程序在约 9 分钟内机械证明了怀特海与罗素《数学原理》（Principia Mathematica）中的全部命题逻辑定理，以及其中大多数谓词逻辑定理。这是自动推理史上的里程碑，远比之前的工作高效。

意义：王浩因此被视为自动定理证明的先驱，1983 年获 IJCAI 首届自动定理证明里程碑奖。他的方法（基于 Herbrand 定理与 Gentzen 式后承演算的搜索）奠定了后来经典逻辑自动证明器的基础。

4. AEA 情形的不可判定性（1962，与 Kahr、Moore）

问题背景：一阶逻辑的判定问题（Entscheidungsproblem）问：是否存在算法判定任一给定一阶逻辑公式是否可满足（或是否有效）？图灵、丘奇 1936 年证明一般情形不可判定。此后人们按量词前缀把前束公式分类，研究每个前缀类的可判定性，到 1960 年代初，唯一悬而未决的是 AEA 型（前缀形如 $\forall\exists\forall$、不含等词）的公式类。

结果：1962 年，王浩与 Andrew S. Kahr、Edward F. Moore 在美国《国家科学院院刊》（PNAS）发表论文，证明 AEA 情形不可判定（即该类公式的可满足性问题不可解），从而完成了量词前缀分类的最后一块拼图。

5. 王浩铺砖（多米诺问题）与计算复杂性

问题背景：在研究定理证明与判定问题的过程中，王浩引入了一种组合模型——王浩铺砖（Wang tiles，又称多米诺问题）。

精确定义：给定一个有限的单位正方形砖集合，每块砖的四条边各着色；要求用这些砖的副本铺满平面（第一象限），使相邻砖的公共边颜色匹配，且砖不得旋转或反射（可加额外约束）。

关键思想：王浩在 1961 年证明了铺砖问题与 AEA 判定问题的等价性：一类「对角约束」铺砖问题的可解性等价于 AEA 公式的可满足性，由此（结合上面的不可判定性）证明铺砖问题不可判定。

王浩猜想与其推翻：王浩曾猜想「任何能铺满平面的砖集都存在一个周期铺法」——若成立，则铺砖问题可判定。这个猜想被他的学生 Robert Berger 在 1966 年的博士论文中推翻：Berger 构造出第一个非周期（aperiodic）王浩砖集，从而严格证明铺砖问题不可判定。

深远影响： - 非周期铺砖直接启发了 1970 年代的彭罗斯铺砖（Penrose tiling）与 1980 年代准晶（quasicrystal）的发现； - 王浩铺砖与多米诺问题成为计算理论与计算复杂性理论的经典工具，影响了后来复杂性类的研究； - 王浩本人还证明了任意图灵机都可转化为一组王浩铺砖，使铺砖成为刻画计算能力的标准模型之一。

6. 数学哲学与哥德尔思想的权威阐释

事实主义：王浩在《从数学到哲学》（1974）中阐述了他的哲学立场「事实主义」（factualism）：数学知识是一个哲学家必须去理解的事实，哲学家的角色不是因为某部分数学达不到其哲学清晰标准就去否定它。这一立场类似自然主义，但不以自然科学（尤其是物理学）为模板。

哥德尔对话：1967 年，王浩因撰写斯科伦（Skolem）著作选集导论而向哥德尔请教，由此开始通信，并从 1971 年起与哥德尔进行了一系列非凡的面谈。这些对话深刻影响了他的哲学写作： - 《从数学到哲学》（1974）发表了哥德尔的两封信（强调其哲学信念在其重大逻辑发现中的作用）以及一段关于图灵可计算性分析的短文； - 《哥德尔的反思》（Reflections on Kurt Gödel, 1987）系统记述哥德尔思想； - 遗著《逻辑之旅：从哥德尔到哲学》（A Logical Journey: From Gödel to Philosophy, 1996，去世前几个月完成）大量引用哥德尔在对话中的言论，是研究哥德尔晚年哲学的首要一手来源。

Parsons 评价：没有人像王浩那样努力「完整地」理解哥德尔；王浩与哥德尔的对话是两位都具有统观抱负的思想家之间的交流。

四、代表著作与文献

五、师承、学派与同时代交往

六、争议、公案与历史评价

七、身后影响与学术谱系

八、延伸阅读与权威来源