序列性质、选择器证明与一致性的可证性
逻辑
2024-03-20 v1
摘要
对于希尔伯特而言，一个形式理论 T 的一致性是一个关于陈述“D 无矛盾”的无穷序列，其中 D 为每个推导；而一个一致性证明则是 i) 一个操作，给定 D，产生一个 D 无矛盾的证明，以及 ii) 一个证明，表明 (i) 对所有输入 D 均有效。希尔伯特证明一致性的两阶段方法自然地推广为在给定理论中对一系列语句进行有限证明的概念。此类证明，我们称之为选择器证明，已在数学中被默示地使用。一致性的选择器证明，包括希尔伯特的 epsilon 替换方法，并不旨在推导出哥德尔式的一致性公式 Con(T)，因此并未被哥德尔第二不完备性定理所排除。我们给出了皮亚诺算术 PA 一致性的一个选择器证明，并在 PA 中形式化了该证明。
引用
@article{arxiv.2403.12272,
title = {Serial Properties, Selector Proofs, and the Provability of Consistency},
author = {Sergei Artemov},
journal= {arXiv preprint arXiv:2403.12272},
year = {2024}
}