Skip to content

ndrwnaguib/principia

使用 Lean 重写 Bertrand Russell 教授的《数学原理》（Principia Mathematica）

ndrwnaguib.com/principia/

使用 Lean4 形式化 Bertrand Russell 的《数学原理》（Principia Mathematica）

./images/principia-mathematica-book-cover.png

这个 项目 旨在利用 Lean 定理证明器来形式化 Bertrand Russell 教授的《数学原理》（Principia Mathematica）的第一卷。目标是确保形式化与书中相应的定理清晰对齐，以避免混淆（参见 [Metaprogramming =Syll=](https://github.com/ndrwnaguib/</ndrwnaguib/principia/blob/main/*Metaprogramming =Syll=>)）。

符号

Principia Mathematica 的符号（Peano-Russell 符号）以其复杂性而闻名，以至于 在斯坦福哲学百科全书 (SEP) 上有一个单独的条目。此外，Landon Elkind 教授的 Squaring the Circles: a Genealogy of Principia’s Dot Notation 巧妙地解释了这种符号。

我认为没有必要阅读它们，我希望在阅读一些公式如何被形式化的例子，并将其与 Russell 教授的符号进行对比之后，一切都应该变得清晰。

在整个形式化过程中，我试图严格遵循 Russell 教授的证明，没有或几乎没有添加我这边的陈述，这些陈述仅在形式化中是必要的，而不是逻辑论证所必需的。如果您发现任何不准确之处（即使它不一定会伪造证明），请告诉我，因为我想以与 Russell 教授相同的严谨精神进行下去。

在开始这个项目之前，我已经找到了 Elkind 教授使用 Coq 对《数学原理》进行形式化的工作，这是一个比这个项目成熟得多的工作。但是，我仍然认为使用 Lean4 来做这件事会很有趣（参见 [Remarks](https://github.com/ndrwnaguib/</ndrwnaguib/principia/blob/main/*Remarks>））。

编辑

我为每个定理包含了一个 $\LaTeX$ 片段，它代表了 Russell 教授的证明。如果您使用 Emacs，我建议在 Lean 缓冲区中启用 org-preview-latex。如果您使用的是 VSCode，可以通过安装 Better Comments 扩展来实现类似的体验。这是我的样子：

./images/editing-experience.png

关于形式化的说明

$∗ 1 ⋅ 11$

Russell 教授反复使用 *1.11 来表示从另一个命题推断出一个命题，例如 $[(3).(8).∗ 1⋅ 11]$ 是通过链接命题 (8) 和 (3) 推导出的命题。在 Lean 中，这可以类似于几个 tactics 或 atoms，例如，<|、simp 等。

Metaprogramming Syll

我计划在阅读形式化时的体验是在同一文件中包含《数学原理》中的相应文本，只是将 Russell 教授的证明替换为它们的 Lean 形式化。例如，这是 *2.16 以及形式化中的一个独特部分，即 metaprogramming 一个新的 tactic，以遵循 Russell 教授对 Syll 的表示法：

./images/syll.png

open Lean Meta Elab Tactic Term
structure ImpProof where
 (ant cons : Expr)
 (proof : Expr)
 deriving Inhabited
theorem compose {p q r : Prop} (a : p → q) (b : q → r) : p → r :=
 b ∘ a
/-- Compose two implication proofs using the `compose` theorem. -/
def ImpProof.compose (a : ImpProof) (b : ImpProof) : MetaM ImpProof := do
 unless ← isDefEq a.cons b.ant do
  throwError "\
   Consequent{indentD a.cons}\n\
   is not definitionally equal to antecedent{indentD b.ant}"
 let proof := mkApp5 (.const ``compose []) a.ant a.cons b.cons a.proof b.proof
 return { ant := a.ant, cons := b.cons, proof := proof }
/-- Create the proof of `p -> p` using the `id` function. -/
def ImpProof.rfl (p : Expr) : ImpProof :=
 { ant := p, cons := p, proof := .app (.const ``id [.zero]) p}
syntax "Syll" (ppSpace "[" term,* "]")? : tactic
elab_rules : tactic
 | `(tactic| Syll $[[$[$terms?],*]]?) => withMainContext do
  -- Elaborate all the supplied hypotheses, or use the entire local context if not provided.
  let hyps ←
   match terms? with
   | none => getLocalHyps
   | some terms => terms.mapM fun term => Tactic.elabTerm term none
  liftMetaTactic1 fun goal => do
   let goalType ← goal.getType
   -- A list of implications extracted from `hyps`.
   let mut chain : Array ImpProof := #[]
   let getImplication? (e : Expr) : MetaM (Option (Expr × Expr)) := do
    -- There may be metadata and metavariables, so do some unfolding if necessary:
    let ty ← instantiateMVars (← whnfR e)
    -- Check if it is a non-dependent forall:
    if ty.isArrow then
     return (ty.bindingDomain!, ty.bindingBody!)
    else
     return none
   for hyp in hyps do
    match ← getImplication? (← inferType hyp) with
    | some (p, q) => chain := chain.push {ant := p, cons := q, proof := hyp}
    | none => logInfo m!"Expression {hyp} is not of the form `p → q`"
   let some (p, q) ← getImplication? goalType
    | throwError "Goal type is not of the form `p → q`"
   if chain.isEmpty then
    throwError "Local context has no implications"
   unless ← isExprDefEq chain[0]!.ant p do
    throwError "The first hypothesis does not match the goal's antecedent"
   unless ← isExprDefEq chain[chain.size - 1]!.cons q do
    throwError "The last hypothesis does not match the goal's consequent"
   let comp ← chain.foldlM (init := ImpProof.rfl p) (fun pf1 pf2 => pf1.compose pf2)
   -- It's good to do one last check that the proof has the correct type before assignment.
   unless ← isDefEq (← inferType comp.proof) goalType do
    throwError "Invalid proof of goal"
   goal.assign comp.proof
   return none

因此，我可以写出以下内容：

./images/syll-example.png

这仅仅是我贪婪地编写一个 tactic 来处理更一般的假言推理形式的结果；我相信在《数学原理》的案例中，我可以接受只接受两个假设的 tactic。

备注

除了学习从头开始构建数学的思考过程外，我看不到这个项目的特殊用途。正如 Freeman Dyson 教授所说，尽管《数学原理》被认为是“一个巨大的失败”，但对我来说，阅读和形式化它都是一种丰富的体验——尤其是在观察到后者，更复杂的结果，是如何使用我亲自形式化的更简单的结果获得的之后。

./images/building-from-constituents.png

./images/logic-semantics-and-metamathematics-book-cover.png

也许接下来的一个项目将是形式化 Alfred Tarski 的《逻辑、语义学和元数学》。