---
title: 希尔伯特计划 (Hilbert's Program)
created: 2025-04-15
updated: 2026-05-01
type: concept
tags: []
sources: []
---

# 希尔伯特计划 (Hilbert's Program)

- **领域**: 数学基础、元数学
- **提出者**: 大卫·希尔伯特 (David Hilbert), 1920年代
- **来源**: [[godel-incompleteness-tutorial|哥德尔不完备定理教程]]

## 定义

希尔伯特计划是 20 世纪初提出的旨在为整个数学奠定坚实基础的宏伟研究纲领。其核心目标为：

1. **形式化**：将全体数学表达为公理化的[[formal-systems|形式系统]] F
2. **一致性证明**：使用有穷主义方法（finitary methods）证明 F 是一致的
3. **完备性证明**：证明 F 是完备的——所有可表达的真命题都可在 F 内证明

## 历史背景

计划诞生于[[russells-paradox|第三次数学危机]]之后。面对集合论悖论对数学基础的动摇，希尔伯特试图通过严格的[[metamathematics|元数学]]方法一劳永逸地解决所有基础问题。他于 1930 年在哥尼斯堡科学会议上发表著名演讲，以「我们必须知道，我们必将知道」结尾——这句话后来成为其墓志铭。

## 哥德尔的终结

[[godel-incompleteness-theorems|哥德尔不完备定理]]直接否定了希尔伯特计划的后两个核心目标：
- 第一不完备定理 ⇒ 完备性不可实现
- 第二不完备定理 ⇒ 一致性无法在系统内部自证

然而希尔伯特计划的遗产并未消亡——它催生的证明论和模型论至今是数理逻辑的重要分支。

## 影响与遗产

- 催生了证明论（Proof Theory）和模型论（Model Theory）
- 引导数学家接受[[mathematical-pluralism|数学多元主义]]
- 形式化方法在计算机科学中重生（[[formal-verification|形式验证]]、[[automated-theorem-proving|自动定理证明]]）

## 相关概念

[[peano-arithmetic]] · [[consistency-logic]] · [[completeness-logic]] · [[russells-paradox]]