关于自由格的代数与逻辑研究
Algebraic and logistic investigations on free lattices
AI总结：
本文翻译了洛伦岑1951年的经典论文，该论文通过双重归纳证明切割可容许性，并给出分支类型论的构造性相容性证明及多种格结构的演绎演算定义，旨在推动其方法在证明论中的重新接受。
摘要：
洛伦岑的《关于自由格的代数与逻辑研究》于1951年发表在《符号逻辑杂志》上。这些“研究”立即被公认为无穷证明论历史上的一个里程碑，但其方法和证明途径尚未被纳入证明论的主体体系。更准确地说，洛伦岑通过对切割公式和推导复杂度的双重归纳来证明切割的可容许性，而不使用任何序数指派，这与大多数证明论标准教材中对切割消去的呈现方式相反。本翻译旨在为其接受提供新的推动力。这些“研究”最著名的贡献是为不带可归约性公理的分支类型论提供了一个构造性的相容性证明。其做法是表明该理论是一个平凡相容的“归纳演算”的一部分，该演算无迂回地描述了我们对算术的知识。该证明仅依赖于公式和定理的归纳定义。此外，他们还提出了半格、分配格、伪补半格以及可数完全布尔代数作为演绎演算的定义，并展示了如何呈现它们以在给定的预序集上构造相应的自由对象。本翻译经洛伦岑之女尤塔·莱因哈特惠允出版。
英文摘要：
Lorenzen's ``Algebraische und logistische Untersuchungen über freie Verbände'' appeared in 1951 in The journal of symbolic logic. These ``Investigations'' have immediately been recognised as a landmark in the history of infinitary proof theory, but their approach and method of proof have not been incorporated into the corpus of proof theory. More precisely, Lorenzen proves the admissibility of cut by double induction, on the cut formula and on the complexity of the derivations, without using any ordinal assignment, contrary to the presentation of cut elimination in most standard texts on proof theory. This translation has the intent of giving a new impetus to their reception. The ``Investigations'' are best known for providing a constructive proof of consistency for ramified type theory without axiom of reducibility. They do so by showing that it is a part of a trivially consistent ``inductive calculus'' that describes our knowledge of arithmetic without detour. The proof resorts only to the inductive definition of formulae and theorems. They propose furthermore a definition of a semilattice, of a distributive lattice, of a pseudocomplemented semilattice, and of a countably complete boolean algebra as deductive calculuses, and show how to present them for constructing the respective free object over a given preordered set. This translation is published with the kind permission of Lorenzen's daughter, Jutta Reinhardt.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
