自由格的代数与逻辑研究
逻辑
2023-09-22 v3
摘要
Lorenzen 的《自由格的代数与逻辑研究》（"Algebraische und logistische Untersuchungen über freie Verbände"）于 1951 年发表在《符号逻辑杂志》上。这些“研究”立即被公认为无穷证明论历史上的里程碑，但其方法和证明技术尚未被纳入证明论的主体之中。更确切地说，Lorenzen 通过对割公式和推导复杂度的双重归纳证明了割的容许性，而未使用任何序数赋值，这与大多数标准证明论教材中关于割消去的表述相反。本翻译旨在为其接受度注入新的动力。这些“研究”最为人所知的是为不含可归约性公理的分支类型论提供了构造性的一致性证明。它们通过表明该理论是一个平凡一致的“归纳演算”的一部分来实现这一点，该演算直接描述了我们对算术的知识。该证明仅依赖于公式和定理的归纳定义。此外，它们提出了半格、分配格、伪补半格以及可数完备布尔代数作为演绎演算的定义，并展示了如何呈现它们以在给定预序集上构造相应的自由对象。本翻译已获 Lorenzen 之女 Jutta Reinhardt 的许可出版。
引用
@article{arxiv.1710.08138,
title = {Algebraic and logistic investigations on free lattices},
author = {Paul Lorenzen},
journal= {arXiv preprint arXiv:1710.08138},
year = {2023}
}
备注
Translation of "Algebraische und logistische Untersuchungen \"uber freie Verb\"ande'', J. Symb. Log., 16(2), 81--106, 1951, http://www.jstor.org/stable/2266681