An Introduction to Lorenzen's ‘Algebraic and Logistic Investigations on Free Lattices’ (1951)

Bibliographic Data

ID21451273
AuthorsThierry Coquand (0000-0002-5429-5153, University of Gothenburg), Henri Lombardi (0000-0002-7920-9282, Université de franche-comté), Stefan Neuwirth (0000-0001-9139-4911, Université de franche-comté, corresponding author)
Year2025
Volume46
Issue4
Pages525-545
Publication date2025-10-02
Peer ReviewedYes
Open AccessNo
TypeARTICLE
VenueHistory and Philosophy of Logic (JOURNAL)
Journal identifiersISSN: 0144-5340 • E-ISSN: 1464-5149
PublisherInforma UK Limited (PUBLISHER • GB)
DOI10.1080/01445340.2024.2439683
OpenAlexW2770666422
LanguageEN
Citations received1
References cited55

Lorenzen's article has immediately been recognised as a landmark in the history of infinitary proof theory. We propose a translation and this introduction in order to publicise its approach and method of proof, without any ordinal assignment. It is best known for providing a constructive proof of consistency for ramified type theory without axiom of reducibility 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 formulas and theorems. It proposes a definition of semilattices, of distributive lattices, of pseudocomplemented semilattices, and of countably complete boolean algebras as deductive calculi, and constructs conservatively the respective free objects over a given preordered set. It illustrates that lattice theory is a bridge between algebra and logic: the construction of an element corresponds to a step in a proof. The fruitfulness of its use of the ω-rule is immediately recognised by Schütte. It triggers the analysis by Ackermann (1951) of the infinitary inductive definition of the accessibility predicate with the goal of proving transfinite induction up to ordinal terms beyond ε0

Algebra over a field · Axiom · Constructive · Constructive proof · Direct proof · Discrete mathematics · Distributive lattice · Distributive property · Distributivity · Mathematical proof · Programming language · Proof theory · Pure mathematics · Semilattice · Structural proof theory · Type (biology) · Type theory · Computer Science · Formal Methods in Verification · Logic, programming, and type systems · Logic, Reasoning, and Knowledge · Mathematics

Tools

Open DOIOpen Access