Scott Aaronson 用图灵机讲清 Rosser 定理，无需算术化
jessi_cata · x · 2026-10-17
Scott Aaronson 在博客《Rosser's Theorem via Turing machines》中给出了一条用可计算性理论直接证明哥德尔第一不完备定理（Rosser 加强版）的路径，适合计算机背景的读者跳过传统算术化技巧。
要点：
- 哥德尔原定理说的是「不存在既可靠又完备的形式系统」，但哥德尔原始证明和计算机科学常用的备选证明，其实只直接给出较弱的「完备与一致不可兼得」结论，这是 Aaronson 教本科生可计算性/复杂性课程时的长期痛点。
- 作者借此展示一个更宽的视角：不完备结果同时也说明数学很容易达到图灵完备——只要一个理论 T 的公理是可递归枚举的，T ⊢ φ 就蕴含 PA ⊢ (T ⊢ φ)，加法和乘法就足够了。
「研究」频道最新
- CoPE：给 GRPO 加一个动作预测损失，长程 Agent 样本效率最高翻倍 — Lianhuiq · 2026-10-17
- tszzl:神经网络生来可读,机械可解释性正迎来科学革命 — basedjensen · 2026-10-17
- Design Arena 数万网站分析：米色衬线风一年内从受捧变被嫌 — soleio · 2026-10-17
- 可解释性研究员：Mech Interp 可能净伤害世界，对齐远比想象难 — ArthurConmy · 2026-10-17
- 本地模型迎来新基准：测出你电脑上模型能干什么 — draginol · 2026-10-17
- MSR：测试时从真实语料挖掘类别模式提升生成多样性 — Kostas Triaridis · 2026-10-17