<figure><img src="image_1.png" /></figure>

HAL
open science

# An introduction to Lorenzen's "Algebraic and logistic investigations on free lattices" (1951)

Thierry Coquand, Stefan Neuwirth

► To cite this version:

Thierry Coquand, Stefan Neuwirth. An introduction to Lorenzen's "Algebraic and logistic investigations on free lattices" (1951). 2023. hal-01629913v2

HAL Id: hal-01629913

https://hal.science/hal-01629913v2

Preprint submitted on 20 Sep 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.
# An introduction to Lorenzen's "Algebraic and logistic investigations on free lattices" (1951)

Thierry Coquand, Stefan Neuwirth, Henri Lombardi

<figure><img src="image_1.png" /></figure>

## To cite this version:

Thierry Coquand, Stefan Neuwirth, Henri Lombardi. An introduction to Lorenzen's "Algebraic and logistic investigations on free lattices" (1951). 2024. hal-01629913v3

HAL Id: hal-01629913

https://hal.science/hal-01629913v3

Preprint submitted on 23 Nov 2024

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_2.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# An introduction to Lorenzen's "Algebraic and
logistic investigations on free lattices" (1951)

Thierry Coquand

Stefan Neuwirth

## Contents

1 The beginnings. 3

2 The 1944 manuscript. 3

3 The 1945 manuscript. 3

3.1 Stripping away lattice theory. 3

3.2 Formula inductions and theorem inductions. 4

3.3 Bernays' judgement. 4

3.4 Independence of the axiom of reducibility. 5

4 The 1947 manuscript. 6

4.1 Restoring the lattice-theoretic part. 6

4.2 Semilattices. 6

4.3 Distributive lattices. 7

4.4 Lorenzen algebras. 7

4.5 Boolean algebras. 7

5 Toward publication. 8

5.1 Finitary vs. constructive logic. 8

5.2 Publication. 9

6 Reception. 9

6.1 Early accounts. 9

6.2 The difference with Fitch's proof. 10

6.3 Induction rules instead of transfinite inductions. 10

6.4 The logical status of the $\omega$-rule. 10

6.5 The $\omega$-rule combined with transfinite induction. 11

6.6 Semi-formal systems. 12
An introduction to Lorenzen's 'Algebraic and
logistic investigations on free lattices' (1951)

Thierry Coquand†, Henri Lombardi‡, and Stefan Neuwirth‡

†Computer science and engineering department, University of Gothenburg, Sweden

‡Université de Franche-Comté, CNRS, UMR 6623, LmB, 25000 Besançon, France, stefan.neuwirth@univ-fcomte.fr

1. **A foreword on Lorenzen and Gödel.** Lorenzen inscribes his 'Algebraic and logistic investigations on free lattices' into Hilbert's programme as updated after Gödel's impossibility theorems: they merely acknowledge a limitation inherent to the axiomatic method and Lorenzen considers them as a hint and not as an obstacle for a firm foundations of mathematics. *Metamathematik* (Lorenzen 1962) is written especially to show the irrelevance of Gödel's theorem for a methodical set-up of logic* (Lorenzen 1987, p. 55).

In 1947, Lorenzen becomes aware of Gödel's proof of consistency of the con-
tinuum hypothesis, but decides six months later to stop abruptly considering this
problem: 'The use of the word "continuum problem" I have stopped today' (see
*Neuwirth 2022*).

In 1955, Gödel writes a report on Lorenzen on the occasion of his invitation
to the Institute for Advanced Study on behalf of Hermann Weyl shortly before
his death. In this report, his 'Investigations' are considered to be his greatest
achievement in logic, whereas his operative mathematics are judged severely; this
is coherent with the way Gödel welcomes Lorenzen at his arrival in 1957, as told
by Edward Regis (1987, p. 58). However, he writes another report in 1958 at the
conclusion of Lorenzen's stay which is quite positive and insightful (see Coquand,
Lombardi, and Neuwirth 2025, § 4).

2. **Introduction.** 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. Their approach and method of proof have not been in-
corporated into the corpus of proof theory.<fnref n="1" /> We propose a translation and this
introduction with 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 formulas 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 calculi, and show how to present them for constructing conservatively the respective free object over a given preordered set. They illustrate that lattice theory is a bridge between algebra and logic for which the construction of an element corresponds to a step in a proof.

We shall describe the history of their reception, which focusses mainly on the
$\omega$-rule. The fruitfulness of this device is immediately recognised by Kurt Schütte.
It triggers the analysis by Ackermann (1951) of the infinitary inductive definition
of the accessibility predicate in Gentzen 1936 with the goal of proving transfinite
induction up to ordinal terms beyond $\epsilon_0$, which is also taken over by Schütte
(1952).

This article is an elaboration of the second half of Coquand and Neuwirth 2017, and it is a sequel to the elaboration Coquand and Neuwirth 2020 of its first half; we have tried to avoid repetitions and to keep this article self-contained; we invite the reader to look up our 2020 paper for more details about the genesis of Lorenzen's work.

**3. The beginnings.** Lorenzen will later recall a talk by Gerhard Gentzen on the consistency of elementary number theory in 1937 or 1938 as a trigger for his discovery that the reformulation of ideal theory in lattice-theoretic terms reveals that his ‘algebraic works [...] were concerned with a problem that had formally the same structure as the problem of consistency of the classical calculus of logic’ (letter to Carl Friedrich Gethmann, see Gethmann 1991, p. 76). This explains the title of Lorenzen’s article.

**4. The 1944 manuscript.** The preliminary manuscript ‘Ein halbordnungstheoretischer Widerspruchsfreiheitsbeweis’, published as *Lorenzen 2020* [1944], contains already the main ideas, the $\omega$-rule, the connection with free constructions in lattice theory, the admissibility of the cut rule, and applies them to a constructive proof of consistency for elementary number theory.

Note that Lorenzen expresses the concept of an admissible rule only in *Lorenzen 1948b* (see also his self-review *Lorenzen 1949*, both have been written after

<footnote n="1">1. 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.</footnote>
**1. The beginnings.** Lorenzen will later recall a talk by Gerhard Gentzen on the consistency of elementary number theory in 1937 or 1938 as a trigger for his discovery that the reformulation of ideal theory in lattice-theoretic terms reveals that his “algebraic works [...] were concerned with a problem that had formally the same structure as the problem of freedom from contradiction of the classical calculus of logic” (letter to Carl Friedrich Gethmann, see *Gethmann 1991*, page 76). This explains the title of Lorenzen’s article.

**2. The 1944 manuscript.** The preliminary manuscript “Ein halbordnungstheoretischer Widerspruchsfreiheitsbeweis”, published as *Lorenzen 2020* [1944], contains already the main ideas, the ω-rule, the connection with free constructions in lattice theory, the admissibility of the cut rule, and applies them to a constructive proof of consistency for elementary number theory.

Note that Lorenzen expresses the concept of an admissible rule only in *Lorenzen 1948b* (see also his self-review *Lorenzen 1949*, both have been written after *Lorenzen 1951*) and names it “erlaubt [permitted]” and then (in *Lorenzen 1950b*) “eliminierbar [eliminable]” before adopting today’s terminology “zulässig [admissible]” in *Lorenzen 1955*. Petr Sergeevich Novikov expresses this concept contemporaneously (see *Citkin 2016*).

**3. The 1945 manuscript.** In a letter dated 11 December 1945, Heinrich Scholz submits Lorenzen’s manuscript “Die Widerspruchsfreiheit der klassischen Logik mit verzweigter Typentheorie”<fnref n="2" /> to Paul Bernays (ETH-Bibliothek, Hochschularchiv, Hs. 975:4111) with a “request for judgement”.

**3.1. Stripping away lattice theory.** The manuscript begins as follows.

> The proof of consistency undertaken in the sequel originated as an application of a purely algebraic theorem of existence about “free” complete boolean lattices. In the present work, though, I limit myself exclusively to the logistic application and use no algebraic conceptions whatsoever.<fnref n="3" />

The choice of stripping away lattice theory may be motivated by targeting a public of logicians. In this way, the affinity with the strategy of Gentzen (1935, IV, § 3) becomes more visible: the deductive calculus of ramified type theory with the axioms of comprehension, extensionality and infinity, but without the axiom of reducibility, is compared to an inductive calculus that proceeds “without detour”;

<footnote n="2">2. “The consistency of classical logic with ramified type theory”. A copy of this manuscript can be found in Niedersächsische Staats- und Universitätsbibliothek Göttingen, Cod. Ms. G. Köthe M 10.</footnote>

<footnote n="3">3. “Der im folgenden durchgeführte Widerspruchsfreiheitsbeweis ist als eine Anwendung eines rein algebraischen Existenztheorems über ‘freie’ vollständige Boole’sche Verbände entstanden. In dieser Arbeit beschränke ich mich jedoch ausschließlich auf die logistische Anwendung und benutze keinerlei algebraische Begriffsbildungen.”</footnote>
Lorenzen 1951) and names it ‘erlaubt [permitted]’ and then (in Lorenzen 1950b) ‘eliminierbar [eliminable]’ before adopting today’s terminology ‘zulässig [admissible]’ in Lorenzen 1955. Petr Sergeevich Novikov expresses this concept contemporaneously (see Citkin 2016).

**5. The 1945 manuscript.** In a letter dated 11 December 1945 (ETH-Bibliothek, Hochschularchiv, Hs. 975:4111), Heinrich Scholz submits Lorenzen’s manuscript ‘Die Widerspruchsfreiheit der klassischen Logik mit verzweigter Typentheorie’² to Paul Bernays with a ‘request for judgement’.

**5.1. Stripping away lattice theory.** The manuscript begins as follows.

The proof of freedom from contradiction undertaken in the sequel originated as an application of a purely algebraic theorem of existence about ‘free’ complete boolean lattices. In the present work, though, I limit myself exclusively to the logistic application and use no algebraic conceptions whatsoever.³

The choice of stripping away lattice theory may be motivated by targeting a public of logicians. In this way, the affinity with the strategy of Gentzen (1935, IV, §3) becomes more visible: the deductive calculus of ramified type theory with the axioms of comprehension, extensionality and infinity, but without the axiom of reducibility, is compared to an inductive calculus that proceeds ‘without detour’; with respect to Gentzen’s calculus, it features an induction rule (compare rule [4] on p. 98) with infinitely many premisses, i.e. an $\omega$-rule in today’s terminology.

**5.2. Formula inductions and theorem inductions.** Lorenzen emphasises as follows.

This proof uses as auxiliary devices only formula inductions vs. theorem inductions, i.e. the fact that the concept of formula and the concept of theorem is defined inductively. The harmlessness of these auxiliary means seems to me to be even more transparent than the harmlessness of explicit transfinite inductions.⁴

These inductions establish that the deductive calculus is a part of the inductive calculus in section 7 of the article:

(1a) the ‘logical axiom’ $c \prec c$ is proved by formula induction;

2. ‘The freedom from contradiction of classical logic with ramified type theory’. A copy of this manuscript can be found in Niedersächsische Staats- und Universitätsbibliothek Göttingen, Cod. Ms. G. Köthe M 10.

3. ‘Der im folgenden durchgeführte Widerspruchsfreiheitsbeweis ist als eine Anwendung eines rein algebraischen Existenztheorems über “freie” vollständige Boole’sche Verbände entstanden. In dieser Arbeit beschränke ich mich jedoch ausschließlich auf die logistische Anwendung und benutze keinerlei algebraische Begriffsbildungen.’

4. ‘Dieser Beweis benutzt als Hilfsmittel nur Formelinduktionen bzw. Satzinduktionen, d. h. die Tatsache, daß der Formelbegriff und der Satzbegriff induktiv definiert ist. Die Unbedenklichkeit dieser Hilfsmittel scheint mir noch einleuchtender zu sein, als die Unbedenklichkeit expliziter transfiniter Induktionen.’
with respect to Gentzen's calculus, it features an induction rule (compare rule [4] on page 98) with infinitely many premisses, i.e. an $\omega$-rule in today's terminology.

## 3.2. *Formula inductions and theorem inductions.*
Lorenzen emphasises as follows.

This proof uses as auxiliary devices only formula inductions vs. theorem inductions, i.e. the fact that the concept of formula and the concept of theorem is defined inductively. The harmlessness of these auxiliary means seems to me to be even more transparent than the harmlessness of explicit transfinite inductions.<fnref n="4" />

These inductions establish that the deductive calculus is a part of the inductive calculus in section 7 of the article:

(1a) the "logical axiom" $c \prec c$ is proved by formula induction;

(1b) the axiom of comprehension follows from the construction of a $\lambda$-calculus and a rule of constants;

(1c) the axiom of extensionality results from a formula induction by the aid of two auxiliary rules proved by theorem induction;

(1d) the axiom of infinity follows from the properties of the order on numbers;

(2a) the admissibility of the cut rule is proved by a formula induction on the cut formula: if it is a numerical formula, a double theorem induction on the premisses is used; the only difficulties in the induction step result from the copresence of constants and free and bound variables in rules like [3d] on page 98; as usual, contraction plays an important rôle.

## 3.3. *Bernays' judgement.*
Bernays is able to appreciate its content on the spot and replies with detailed comments to Scholz on 24 April 1946 (carbon copy, Hs. 975:4112). On 17 April 1946, Lorenzen writes directly to Bernays (Hs. 975:2947); he gets an answer on 22 May 1946 with the following appreciation.

> It seems to me that your argumentation accomplishes in effect the desired and that thereby at the same time also a new, methodically more transparent proof of consistency for the number-theoretic formalism, as well as for Gentzen's subformula theorem<fnref n="5" /> is provided.

<footnote n="4">4. "Dieser Beweis benutzt als Hilfsmittel nur Formelinduktionen bzw. Satzinduktionen, d. h. die Tatsache, daß der Formelbegriff und der Satzbegriff induktiv definiert ist. Die Unbedenklichkeit dieser Hilfsmittel scheint mir noch einleuchtender zu sein, als die Unbedenklichkeit expliziter transfiniter Induktionen."</footnote>

<footnote n="5">5. In the letter of 24 April 1946, Bernays writes more precisely to Scholz "that one also gets a proof for the main theorem of Gentzen's 'Investigations into logical deduction' out of it, if on the one hand one omits the higher axioms [(1b, c, d) on page 95] in the deductive calculus, on the other hand one retains from the rules of the inductive calculus (for determining the concept of theorem) only [[2], [3a-d] on page 98], while one takes also the formula pairs $[c \prec c]$ as starting theorems for this calculus."⁶</footnote>

<footnote n="6">6. "dass man aus ihm auch einen Beweis für den Hauptsatz von Gentzen's 'Untersuchungen</footnote>
(1b) the axiom of comprehension follows from the construction of a λ-calculus and a rule of constants;

(1c) the axiom of extensionality results from a formula induction by the aid of two auxiliary rules proved by theorem induction;

(1d) the axiom of infinity follows from the properties of the order on numbers;

(2a) the admissibility of the cut rule is proved by a formula induction on the cut formula: if it is a numerical formula, a double theorem induction on the premisses is used; the only difficulties in the induction step result from the copresence of constants and free and bound variables in rules like [3d] on p. 98; as usual, contraction plays an important rôle.

**5.3. Bernays' judgement.** Bernays is able to appreciate its content on the spot and replies with detailed comments to Scholz on 24 April 1946 (carbon copy, Hs. 975:4112). On 17 April 1946, Lorenzen writes directly to Bernays (Hs. 975: 2947); he gets an answer on 22 May 1946 with the following appreciation.

It seems to me that your argumentation accomplishes in effect the desired and that thereby at the same time also a new, methodically more transparent proof of freedom from contradiction for the number-theoretic formalism, as well as for Gentzen's subformula theorem<sup>5</sup> is provided.

In the circumstance that all this is included in your result shows at the same time the methodical superiority of your method of proof with respect to a proof (that probably did not come to your knowledge) that F. B. Fitch [...] gave in 1938, and that also bears on the comparison of the deductive formalism with a system of formulas which is not delimited in a purely operative way; namely, this delimitation is carried out there according to a definition of truth in which the 'tertium non datur' (indeed only with respect to the species of natural numbers) is made use of.<sup>7</sup> By determining your system of comparison according to the idea of a generalisation of Gentzen's thought of 'deduction without detour', you gain the possibility of applying the constructive proof-theoretic view also in the case of your 'inductive calculus', i.e. of such an

5. In the letter of 24 April 1946, Bernays writes more precisely to Scholz 'that one also gets a proof for the main theorem of Gentzen's "Investigations into logical deduction" out of it, if on the one hand one omits the higher axioms [(1b, c, d) on p. 95] in the deductive calculus, on the other hand one retains from the rules of the inductive calculus (for determining the concept of theorem) only [[2], [3a-d] on p. 98], while one takes also the formula pairs [c ≪ c] as starting theorems for this calculus.'<sup>6</sup>

6. 'dass man aus ihm auch einen Beweis für den Hauptsatz von Gentzen’s “Untersuchungen über das logische Schliessen” erhält, indem man einerseits beim deduktiven Kalkul die höheren Axiome 1.) b), c), d) weglässt, andererseits von den Regeln des induktiven Kalkuls (zur Bestimmung des Satzbegriffes) nur 2) a)-d) beibehält, während man als Ausgangssätze auch für diesen Kalkul die Formelpaar e c ⊂ c nimmt.'

7. See *Fitch 1938* and its review *Bernays 1939*.
In the circumstance that all this is included in your result shows at
the same time the methodical superiority of your method of proof with
respect to a proof (that probably did not come to your knowledge) that
F. B. Fitch [...] gave in 1938, and that also bears on the comparison
of the deductive formalism with a system of formulas which is not de-
limited in a purely operative way; namely, this delimitation is carried
out there according to a definition of truth in which the "tertium non
datur" (indeed only with respect to the species of natural numbers)
is made use of.⁷ By determining your system of comparison accord-
ing to the idea of a generalisation of Gentzen's thought of "deduction
without detour", you gain the possibility of applying the constructive
proof-theoretic view also in the case of your "inductive calculus", i.e. of
such an inference system that does not comply with the recursiveness
conditions that the customary formalisms fulfil.⁸

### 3.4. Independence of the axiom of reducibility.
Lorenzen learns about Fitch's proof of consistency only by this letter. In his answer (dated 7 June 1946, Hs. 975:2949), he explains the lattice-theoretic background of his proof and encloses a manuscript, “Über das Reduzibilitätsaxiom”,⁹ which is a preliminary version of the last section of the published article, in which the axiom of reducibility is shown to be independent. However, Bernays seems to already have received this manuscript with Scholz's letter of 11 December 1945 (see his letter of 24 April 1946).

More precisely, he proves the consistency of the calculus obtained by adding
an axiom that expresses that all infinite sets are countable and then shows that

über das logische Schliessen' erhält, indem man einerseits beim deduktiven Kalkul die höheren Axiome 1.) b), c), d) weglässt, andererseits von den Regeln des induktiven Kalkuls (zur Bestimmung des Satzbegriffes) nur 2) a)-d) beibehält, während man als Ausgangssätze auch für diesen Kalkul die Formelpaare $c \subset c$ nimmt.”

7. See *Fitch 1938* and its review *Bernays 1939*.

8. “Es scheint mir, dass Ihre Beweisführung in der Tat das Gewünschte leistet und dass damit zugleich auch ein neuer, methodisch durchsichtigerer Wf.-Beweis für den zahlentheoretischen Formalismus wie auch ein solcher für Gentzen’s Teilformelsatz geliefert wird.

“In dem Umstande, dass alles dies in Ihrem Ergebnis eingeschlossen ist, zeigt sich zugleich die methodische Überlegenheit Ihres Beweisverfahrens gegenüber einem (Ihnen wohl nicht zur Kenntnis gelangten) Beweis, den F. B. Fitch 1938 für die Widerspruchsfreiheit der verzweigten Typentheorie gegeben hat (im Journal of symb. logic, vol. 3, S. 140-149), und der auch auf dem Vergleich des deduktiven Formalismus mit einem Formelsystem beruht, das auf eine nicht rein operative Art abgegrenzt ist; diese Abgrenzung erfolgt nämlich dort im Sinne einer Wahrheitsdefinition, wobei von dem ‘tertium non datur’ (allerdings nur demjenigen in Bezug auf die Gattung der natürlichen Zahlen) Gebrauch gemacht wird. Indem Sie Ihr Vergleichssystem gemäss der Idee einer Verallgemeinerung von Gentzen’s Gedanken der ‘umweglosen Herleitung’ bestimmen, gewinnen Sie die Möglichkeit, die konstruktive beweistheoretische Betrachtung auch im Falle Ihres ‘induktiven Kalküls’ anzuwenden, d. h. eines solchen Folgerungssystems, welches nicht den durch die üblichen Formalismen erfüllten Rekursivitätsbedingungen genügt.” (Hs. 975:2948.)

9. “On the axiom of reducibility”, Hs. 974:149. Another copy of this manuscript is in the Universitätsarchiv Bonn.
inference system that does not comply with the recursiveness conditions
that the customary formalisms fulfil.<fnref n="8" />

5.4. *Independence of the axiom of reducibility*. Lorenzen learns about Fitch's proof of consistency only by this letter. In his answer (dated 7 June 1946, Hs. 975:2949), he explains the lattice-theoretic background of his proof and encloses a manuscript, 'Über das Reduzibilitätsaxiom',<fnref n="9" /> which is a preliminary version of the last section of the published article, in which the axiom of reducibility is shown to be independent. However, Bernays seems to already have received this manuscript with Scholz's letter of 11 December 1945 (see his letter of 24 April 1946).

More precisely, he proves the consistency of the calculus obtained by adding an axiom that expresses that all infinite sets are countable and then shows that the axiom of reducibility is false in this calculus. In fact, as Lorenzen notes, Fitch (1939) proves this in his framework. These results answer questions raised by Whitehead and Russell (1925, pp. xiv, xlii–xxliii) in the introduction to the second edition of their *Principia mathematica* after Leon Chwistek (1925): without the axiom of reducibility, 'Cantor's proof that $2^n > n$ breaks down unless *n* is finite'.

# 6. The 1947 manuscript.

6.1. *Restoring the lattice-theoretic part.* By a letter dated 21 February 1947, Lorenzen writes to Bernays:

> After a revision of my proof of freedom from contradiction according to
> your precious remarks and after addition of an algebraic part, I would
> like to allow myself to ask you for your intercession for a publication
> in the Journal of Symbolic Logic.<fnref n="10" />

<footnote n="8">8. 'Es scheint mir, dass Ihre Beweisführung in der Tat das Gewünschte leistet und dass damit zugleich auch ein neuer, methodisch durchsichtigerer Wf.-Beweis für den zahlentheoretischen Formalismus wie auch ein solcher für Gentzen's Teilformelsatz geliefert wird.</footnote>

<footnote>In dem Umstande, dass alles dies in Ihrem Ergebnis eingeschlossen ist, zeigt sich zugleich die methodische Überlegenheit Ihres Beweisverfahrens gegenüber einem (Ihnen wohl nicht zur Kenntnis gelangten) Beweis, den F. B. Fitch 1938 für die Widerspruchsfreiheit der verzweigten Typentheorie gegeben hat (im Journal of symb. logic, vol. 3, S. 140-149), und der auch auf dem Vergleich des deduktiven Formalismus mit einem Formelsystem beruht, das auf eine nicht rein operative Art abgegrenzt ist; diese Abgrenzung erfolgt nämlich dort im Sinne einer Wahrheitsdefinition, wobei von dem "tertium non datur" (allerdings nur demjenigen in Bezug auf die Gattung der natürlichen Zahlen) Gebrauch gemacht wird. Indem Sie Ihr Vergleichssystem gemäss der Idee einer Verallgemeinerung von Gentzen's Gedanken der "umweglosen Herleitung" bestimmen, gewinnen Sie die Möglichkeit, die konstruktive beweistheoretische Betrachtung auch im Falle Ihres "induktiven Kalküls" anzuwenden, d. h. eines solchen Folgerungssystems, welches nicht den durch die üblichen Formalismen erfüllten Rekursivitätsbedingungen genügt' (Hs. 975:2948).</footnote>

<footnote n="9">9. 'On the axiom of reducibility', Hs. 974:149. Another copy of this manuscript is in the Universitätsarchiv Bonn.</footnote>

<footnote n="10">10. 'nach einer Überarbeitung meines Wf.beweises nach Ihren wertvollen Bemerkungen und nach Hinzufügung eines algebraischen Teiles möchte ich mir erlauben, Sie um Ihre Fürsprache zu bitten für eine Veröffentlichung im Journal of symbolic logic' (Hs. 975:2950).</footnote>
the axiom of reducibility is false in this calculus. In fact, as Lorenzen notes, Fitch (1939) proves this in his framework. These results answer questions raised by Whitehead and Russell (1925, pages xiv, xlii–xxliii) in the introduction to the second edition of their *Principia mathematica* after Leon Chwistek (1925): without the axiom of reducibility, “Cantor’s proof that $2^n > n$ breaks down unless $n$ is finite”.

# 4. The 1947 manuscript.

## 4.1. Restoring the lattice-theoretic part.
By a letter dated 21 February 1947, Lorenzen writes to Bernays:

> After a revision of my proof of consistency according to your previous remarks and after addition of an algebraic part, I would like to allow myself to ask you for your intercession for a publication in the Journal of Symbolic Logic.<fnref n="10" />

> This new draft is a kind of synthesis of “Ein halbordnungstheoretischer Widerspruchsfreiheitsbeweis” and “Die Widerspruchsfreiheit der klassischen Logik mit verzweigter Typentheorie”, or rather a juxtaposition of two parts: the seams remain apparent. However, the introduction now takes into account the added algebraic part. Its first paragraph emphasises that lattice theory is relevant for ideal theory with a reference to the reshaping of Krull’s Fundamentalsatz for integral domains in lattice-theoretic terms provided by his habilitation (Lorenzen 1950a, see Neuwirth 2021).

## 4.2. Semilattices.
In the new algebraic part, the construction of free semilattices and free distributive lattices stems in fact from ideal theory. Theorems 1–4 in section 2 of the article (page 84) introduce a semilattice as a “single statement entailment relation” and construct the free semilattice over a preordered set (a *preorder* or quasiorder is a reflexive and transitive relation on the set). This approach may be dated back to Skolem (1921, § 2), who constructs the free lattice over a preordered set in the course of studying the decision problem for lattices. It is paralleled in Lorenzen 1952 by the definition of a system of ideals for an arbitrary preordered set *M* on which a monoid *G* acts by order-preserving operators *x*: it is a relation satisfying items 1–4 of theorem 1 and furthermore

$$ \text{if } a_1, \dots, a_n \vdash b, \text{ then } xa_1, \dots, xa_n \vdash xb $$

(compare Coquand, Lombardi, and Neuwirth 2019, § 1C).

<footnote n="10">10. “nach einer Überarbeitung meines Wf.beweises nach Ihren wertvollen Bemerkungen und nach Hinzufügung eines algebraischen Teiles möchte ich mir erlauben, Sie um Ihre Fürsprache zu bitten für eine Veröffentlichung im Journal of symbolic logic.” (Hs. 975:2950.)</footnote>
This new draft is a kind of synthesis of ‘Ein halbordnungstheoretischer Widerspruchsfreiheitsbeweis’ and ‘Die Widerspruchsfreiheit der klassischen Logik mit verzweigter Typentheorie’, or rather a juxtaposition of two parts: the seams remain apparent. However, the introduction now takes into account the added algebraic part. Its first paragraph emphasises that lattice theory is relevant for ideal theory with a reference to the reshaping of Krull’s Fundamentalsatz for integral domains in lattice-theoretic terms provided by his habilitation (Lorenzen 1950a, see Neuwirth 2021).

### 6.2. Semilattices.
In the new algebraic part, the construction of free semilattices and free distributive lattices stems in fact from ideal theory. Theorems 1–4 in section 2 of the article (p. 84) introduce a semilattice as a ‘single statement entailment relation’ and construct the free semilattice over a preordered set (a *preorder* or quasiorder is a reflexive and transitive relation on the set). This approach may be dated back to Skolem (1921, § 2), who constructs the free lattice over a preordered set in the course of studying the decision problem for lattices. It is parallelled in Lorenzen 1952 by the definition of a system of ideals for an arbitrary preordered set *M* on which a monoid *G* acts by order-preserving operators *x*: it is a relation satisfying items 1–4 of theorem 1 and furthermore

$$ \text{if } a_1, \dots, a_n \vdash b, \text{ then } xa_1, \dots, xa_n \vdash xb $$

(compare Coquand, Lombardi, and Neuwirth 2019, § 1C).

### 6.3. Distributive lattices.
In the same way, theorems 5–8 provide the description of a distributive lattice as a deductive system that has been called since Scott (1971) an ‘entailment relation’. This description strikes Bernays as new to him (letter of 3 April 1947, Paul-Lorenzen-Nachlass, Philosophisches Archiv, Universität Konstanz, PL 1-1-118). His theorem 7 on p. 85 corresponds in fact to theorem 1 in Cederquist and Coquand 2000, obtained independently. This construction is used in Lorenzen 1953 for embedding a preordered group endowed with a system of ideals into a lattice-ordered group containing this system (compare Coquand, Lombardi, and Neuwirth 2019, § 2C).

### 6.4. Lorenzen algebras.
Section 3 of the article deals with (finitary) pseudocomplemented semilattices while his 1944 manuscript deals with countably complete ones. We propose to call them ‘Lorenzen algebras’:<fnref n="11" /> see definition 1 in our section 9, where we use them in a crucial way for our explanation of an impredicative system in terms of inductive definitions.

He constructs the free Lorenzen algebra generated by a preordered set as a cut-free sequent calculus (while his 1944 manuscript deals with the countably complete

<footnote n="11">11. The theory of Lorenzen algebras continues to develop: one can find an account of it by Grätzer (2011, pp. 99–101) and by Chajda, Halaš, and Kühr (2007, ch. 3).</footnote>
4.3. Distributive lattices. In the same way, theorems 5–8 provide the description of a distributive lattice as a deductive system that has been called since Scott (1971) an “entailment relation”. This description strikes Bernays as new to him (letter of 3 April 1947, Paul-Lorenzen-Nachlass, Philosophisches Archiv, Universität Konstanz, PL 1-1-118). His theorem 7 on page 85 corresponds in fact to theorem 1 in Cederquist and Coquand 2000, obtained independently. This construction is used in Lorenzen 1953 for embedding a preordered group endowed with a system of ideals into a lattice-ordered group containing this system (compare Coquand, Lombardi, and Neuwirth 2019, § 2C).

4.4. Lorenzen algebras. Section 3 of the article deals with (finitary) pseudocomplemented semilattices while his 1944 manuscript deals with countably complete ones. We propose to call them “Lorenzen algebras”:<fnref n="11" /> see definition 1 in our section 7, where we use them in a crucial way for our explanation of an impredicative system in terms of inductive definitions.

He constructs the free Lorenzen algebra generated by a preordered set as a cut-free sequent calculus (while his 1944 manuscript deals with the countably complete case).<fnref n="12" />

In section 4, he shows how to apply the construction of the free Lorenzen algebra to a simple intuitionistic logical calculus. He emphasises that the decision problem has a positive answer.

4.5. Boolean algebras. Lorenzen proceeds with describing the free countably complete boolean algebra<fnref n="13" /> generated by a preordered set as a cut-free infinitary sequent calculus with $\omega$-rules [3.9] and [3.10] on page 92. The main step in the construction is again to prove that the cut rule (which states on the same page that $a_1 \le c \lor b_1$ and $a_2 \land c \le b_2$ implies $a_1 \land a_2 \le b_1 \lor b_2$) is admissible.

He sketches this construction, which goes along the same lines as the construction of the free Lorenzen algebra, with one significant difference: in the latter case, he is able to prove contraction (see lemma (8) on page 88), whereas he has to put it into the definition in the former setting (he provides a counterexample on pages 92–93). Compare with his 1944 manuscript, where a contraction rule is present (see the comment in our 2020, end of § 2), and with the calculus defined

<footnote n="11">11. The theory of Lorenzen algebras continues to develop: one can find an account of it by Grätzer (2011, pages 99–101) and Chajda, Halaš, and Kühr (2007, chapter 3).</footnote>

<footnote n="12">12. The existence of the free Lorenzen algebra over a preordered set seems to be unknown in the literature, which considers only the case where the preorder is trivial; in the latter case, the decision problem was solved by Tamura (1974). Neuwirth 2015 proposes a streamlined presentation.</footnote>

<footnote n="13">13. In the second paragraph of the introduction, he addresses complete boolean algebras over a preordered set as studied by MacNeille (1937). The question about the existence of the free complete boolean algebra is usually attributed to Rieger (1951) and has led to the works of Gaifman (1964) and Hales (1964) that provide a negative answer; it may be seen as an anomaly of the set-theoretic approach to actual infinity, because such infinities cause that free complete boolean algebras would be too big. See also the proof of Solovay (1966) inspired by forcing.</footnote>
case).<fnref n="12" />

In section 4, he shows how to apply the construction of the free Lorenzen algebra to a simple intuitionistic logical calculus. He emphasises that the decision problem has a positive answer.

**6.5. Boolean algebras.** Lorenzen proceeds with describing the free countably complete boolean algebra<fnref n="13" /> generated by a preordered set as a cut-free infinitary sequent calculus with ω-rules [3.9] and [3.10] on p. 92. The main step in the construction is again to prove that the cut rule (which states on the same page that $a_1 \le c \lor b_1$ and $a_2 \land c \le b_2$ implies $a_1 \land a_2 \le b_1 \lor b_2$) is admissible.

He sketches this construction, which goes along the same lines as the construction of the free Lorenzen algebra, with one significant difference: in the latter case, he is able to prove contraction (see lemma (8) on p. 88), whereas he has to put it into the definition in the former setting (he provides a counterexample on pp. 92–93). Compare with his 1944 manuscript, where a contraction rule is present (see the comment in our *2020*, end of § 2), and with the calculus defined by Per Martin-Löf (*1970*, § 30) for Borel sets, where the problem of contraction is eluded by ‘identify[ing] sequents which are equal considered as finite sets’.

Let us comment on two aspects of this construction.

- Lorenzen works systematically with a preorder $\leq$ instead of an order and does not quotient with respect to the equivalence relation $a \equiv b$ defined by $a \leq b$ and $b \leq a$. If he did so, he would need to resort to the axiom of choice for defining meets.

- The universal property corresponding to freeness is proved by parallelling the construction of the free object with the construction of the sought-after morphism: see items (i)–(iii) on p. 89. *The Univalent Foundations Program (2013)* indicates a way to avoid the use of choice in a constructive setting precisely by defining inductively the free boolean algebra so that its objects and their equalities are defined simultaneously.

Compare our section 9 for the relevance of these two aspects.

Then Lorenzen shows how to deduce consistency for the logic of ramified type by an iterated construction of free countably complete boolean algebras, starting from a calculus without free variables, along the hierarchy of types.

<footnote n="12">12. The existence of the free Lorenzen algebra over a preordered set seems to be unknown in the literature, which considers only the case where the preorder is trivial; in the latter case, the decision problem has been solved by Tamura (*1974*). Neuwirth *2015* proposes a streamlined presentation.</footnote>

<footnote n="13">13. In the second paragraph of the introduction, he addresses complete boolean algebras over a preordered set as studied by MacNeille (*1937*). The question about the existence of the free complete boolean algebra is usually attributed to Rieger (*1951*) and has led to the works of Gaifman (*1964*) and Hales (*1964*) that provide a negative answer; it may be seen as an anomaly of the set-theoretic approach to actual infinity, because such infinities cause that free complete boolean algebras would be too big. See also the proof of Solovay (*1966*) inspired by forcing.</footnote>
by Per Martin-Löf (1970, § 30) for Borel sets, where the problem of contraction is eluded by “identify[ing] sequents which are equal considered as finite sets”.

Let us comment on two aspects of this construction.

— Lorenzen works systematically with a preorder $\leq$ instead of an order and does not quotient with respect to the equivalence relation $a \equiv b$ defined by $a \leq b$ and $b \leq a$. If he did so, he would need to resort to the axiom of choice for defining meets.

— The universal property corresponding to freeness is proved by parallelling the construction of the free object with the construction of the sought-after morphism: see items (i)–(iii) on page 89. The *Univalent Foundations Program (2013)* indicates a way to avoid the use of choice in a constructive setting precisely by defining inductively the free boolean algebra so that its objects and their equalities are defined simultaneously.

Compare our section 7 for the relevance of these two aspects.

Then Lorenzen shows how to deduce consistency for the logic of ramified type by an iterated construction of free countably complete boolean algebras, starting from a calculus without free variables, along the hierarchy of types.

**5. Toward publication.**

**5.1. Finitary vs. constructive logic.** At the end of his letter of 21 February 1947, Lorenzen asks:

> I beg once again to ask you for your advice—namely, it is not clear to me whether I rightly call the logic used here “finitary” logic.<fnref n="14" />

Bernays provides the following answer in his letter of 3 April 1947:

> When it comes to the methodical standpoint and to the terminology to be used in relation, then it seems advisable to me to keep with the mode chosen by Mister Gentzen, that one speaks of “finitary” reflections only in the narrower sense, i.e. relating to considerations that may be formalised in the framework of recursive number theory (possibly with extension of the domain of functions to arbitrary computable functions), that one uses in contrast the expression “constructive” for the appropriate extension of the standpoint of the intuitive self-evidence; by the way, this is employed also by many an American logician in the corresponding sense.

> Your proof of consistency cannot, I deem, be a finitary one in the narrower sense. Of course, this would conflict with the Gödel theorem. Actually, a nonfinitary element of your reflection lies in the induction

<footnote n="14">14. “Ich bitte noch einmal Sie um Ihren Rat fragen zu dürfen – es ist mir nämlich nicht klar, ob ich die hier benutzte Logik mit Recht ‘finite’ Logik nenne.” (Hs. 975:2950.)</footnote>
7. Toward publication.

7.1. *Finitary vs. constructive logic*. At the end of his letter of 21 February 1947, Lorenzen asks:

> I beg once again to ask you for your advice—namely, it is not clear to me whether I rightly call the logic used here ‘finitary’ logic.<fnref n="14" />

> Bernays provides the following answer in his letter of 3 April 1947:

> When it comes to the methodical standpoint and to the terminology to be used in relation, then it seems advisable to me to keep with the mode chosen by Mister Gentzen, that one speaks of ‘finitary’ reflections only in the narrower sense, i.e. relating to considerations that may be formalised in the framework of recursive number theory (possibly with extension of the domain of functions to arbitrary computable functions), that one uses in contrast the expression ‘constructive’ for the appropriate extension of the standpoint of the intuitive self-evidence; by the way, this is employed also by many an American logician in the corresponding sense.

> Your proof of freedom from contradiction cannot, I deem, be a fini-
> tary one in the narrower sense. Of course, this would conflict with the
> Gödel theorem. Actually, a nonfinitary element of your reflection lies
> in the induction rule of the inductive calculus, which contains indeed
> a premiss of a more general form.<fnref n="15" />

In other words, the ω-rule does not fit into a formal system, and this explains why Gödel’s theorem does not apply here. But Hilbert (1931, p. 491) describes the ω-rule as a ‘finitary deduction rule’ and this is probably why Lorenzen qualifies his deductions as ‘finitary’; note also the emphasis of Gentzen (1936, § 16.11) that accessibility is a finitary concept (see our section 8.7 below). Lorenzen answers as follows on 4 May 1947.

> Your proposal to call the means of proof not 'finitary' but 'constructive'
> acted on me as a sort of redemption. I was sticking so far to the word

<footnote n="14">14. 'Ich bitte noch einmal Sie um Ihren Rat fragen zu dürfen – es ist mir nämlich nicht klar, ob ich die hier benutzte Logik mit Recht "finite" Logik nenne' (Hs. 975:2950).</footnote>

<footnote n="15">15. 'Was den methodischen Standpunkt und die in Bezug darauf zu verwendende Terminologie betrifft, so erscheint es mir als empfehlenswert, den von Herrn Gentzen gewählten Modus beizubehalten, dass man von 'finiten' Betrachtungen nur im engeren Sinne spricht, d. h. mit Bezug auf Überlegungen, die sich im Rahmen der rekursiven Zahlentheorie (eventuell mit Erweiterung des Funktionenbereiches auf beliebige berechenbare Funktionen) formalisieren lassen, dass man dagegen für die sachgemäße Erweiterung des Standpunktes der anschaulichen Evidenz den Ausdruck 'konstruktiv' verwendet; dieser wird übrigens auch von manchen amerikanischen Logikern im entsprechenden Sinn gebraucht.</footnote>

<footnote>Ihr Wf-Beweis kann, so meine ich, kein finiter in dem genannten engeren Sinne sein. Das würde doch dem Gödelschen Theorem widerstreiten. Tatsächlich liegt, so viel ich sehe, ein nicht-finites Element Ihrer Betrachtung in der Induktionsregel des induktiven Kalkuls, welche ja eine Prämisse von allgemeinerer Form enthält' (PL 1-1-118).</footnote>
rule of the inductive calculus, which contains indeed a premiss of a
more general form.¹⁵

In other words, the ω-rule does not fit into a formal system, and this explains why Gödel’s theorem does not apply here. But Hilbert (1931, page 491) describes the ω-rule as a “finitary deduction rule” and this is probably why Lorenzen qualifies his deductions as “finitary”; note also the emphasis of Gentzen (1936, § 16.1.1) that accessibility is a finitary concept (see our section 6.7 below). Lorenzen answers as follows on 4 May 1947.

> Your proposal to call the means of proof not “finitary” but “constructive” acted on me as a sort of redemption. I was sticking so far to the word finitary only to emphasise that these are hilbertian ideas that I am trying to pursue.¹⁶

**5.2. Publication.** Lorenzen prepares another final draft that is very close to the published version.¹⁷ Bernays sends a first series of comments on 1 September 1947 (PL 1-1-112) and a second series (on a version including the final section on the axiom of reducibility) on 6 February 1949 (PL 1-1-107); the article is submitted to *The Journal of Symbolic Logic* soon afterwards¹⁸ and published as *Lorenzen 1951* with date of reception 17 March 1950. In fact, in 1947, Lorenzen already starts his project of layers of language which will lead to his operative logic (see *Neuwirth 2022* on the circumstances of this switch).

# 6. Reception.

**6.1. Early accounts.** For early accounts of the manuscripts, see *Lorenzen 1948a*, *Köthe 1948*, *Schmidt 1950*, § 11.

15. “Was den methodischen Standpunkt und die in Bezug darauf zu verwendende Terminologie betrifft, so erscheint es mir als empfehlenswert, den von Herrn Gentzen gewählten Modus beizu-behalten, dass man von ‘finiten’ Betrachtungen nur im engeren Sinne spricht, d. h. mit Bezug auf Überlegungen, die sich im Rahmen der rekursiven Zahlentheorie (eventuell mit Erweiterung des Funktionenbereiches auf beliebige berechenbare Funktionen) formalisieren lassen, dass man dagegen für die sachgemässe Erweiterung des Standpunktes der anschaulichen Evidenz den Aus-druck ‘konstruktiv’ verwendet; dieser wird übrigens auch von manchen amerikanischen Logikern im entsprechenden Sinn gebraucht.

“Ihr Wf-Beweis kann, so meine ich, kein finiter in dem genannten engeren Sinne sein. Das würde doch dem Gödelschen Theorem widerstreiten. Tatsächlich liegt, so viel ich sehe, ein nicht-finites Element Ihrer Betrachtung in der Induktionsregel des induktiven Kalkuls, welche ja eine Prämisse von allgemeinerer Form enthält.” (PL 1-1-118.)

16. “Ihr Vorschlag, die Beweismittel nicht ‘finit’, sondern ‘konstruktiv’ zu nennen, hat wie eine Art Erlösung auf mich gewirkt. Ich habe bisher an dem Wort finit nur festgehalten, um zu betonen, dass es Hilbertsche Ideen sind, die ich fortzuführen versuche.” (Hs. 975:2953.)

17. Two pages of this draft may be found in the file OB 5-3b-5; Cod. Ms. G. Köthe M 10 contains an excerpt of Part I.

18. See the letter of 27 April 1949 to Alonzo Church, in which Lorenzen thanks him for ac-knowledging receipt of the manuscript, writes a few words on its history, and proposes Bernays as a referee (Alonzo Church Papers, box 26 folder 4, Manuscripts division, Department of rare books and special collections, Princeton university library).
finitary only to emphasise that these are hilbertian ideas that I am trying to pursue.<fnref n="16" />

**7.2. Publication.** Lorenzen prepares another final draft that is very close to the published version.<fnref n="17" /> Bernays sends a first series of comments on 1 September 1947 (PL 1-1-112) and a second series (on a version including the final section on the axiom of reducibility) on 6 February 1949 (PL 1-1-107); the article is submitted to *The Journal of Symbolic Logic* soon afterwards<fnref n="18" /> and published as *Lorenzen 1951* with date of reception 17 March 1950. In fact, in 1947, Lorenzen already starts his project of language levels which will lead to his operative logic (see *Neuwirth 2022* on the circumstances of this switch).

## 8. Reception.

**8.1. Early accounts.** For early accounts of the manuscripts, see *Lorenzen 1948a*, *Köthe 1948*, *Schmidt 1950*, § 11.

Let us present the reactions to Lorenzen’s article by subject.

**8.2. The difference with Fitch's proof.** Hao Wang (1951) writes the review for *The Journal of Symbolic Logic* and tries to compare Lorenzen's approach with Fitch's; see *Coquand 2014* for a discussion of this review. Wang 1954 (p. 252) provides a more accurate comparison.

**8.3. Induction rules instead of transfinite inductions.** Gottfried Köthe and Lorenzen have worked together on lattice theory before World War II. In Spring 1947, they correspond on foundations of mathematics and physics. Köthe is preparing lectures on proofs of consistency up to Lorenzen's to be given in Fall 1947 at Mainz (see Cod. Ms. G. Köthe G 3).<fnref n="19" /> In an answer to a letter by Köthe dated 8 June 1947 (PL 1-1-114), Lorenzen writes on 17 June 1947 about his work:

> The formalisation of proofs of freedom from contradiction that I am striving for is not at all intent on staying inside a transfinite theory of numbers, but uses instead of 'transfinite inductions' induction rules like the 'formula induction' and 'theorem induction' of my proof of freedom from contradiction—these could also be formalised in a theory

<footnote n="16">16. 'Ihr Vorschlag, die Beweismittel nicht "finit", sondern "konstruktiv" zu nennen, hat wie eine Art Erlösung auf mich gewirkt. Ich habe bisher an dem Wort finit nur festgehalten, um zu betonen, dass es Hilbertsche Ideen sind, die ich fortzuführen versuche' (Hs. 975:2953).</footnote>

<footnote n="17">17. Two pages of this draft may be found in the file OB 5-3b-5; Cod. Ms. G. Köthe M 10 contains an excerpt of Part I.</footnote>

<footnote n="18">18. See the letter of 27 April 1949 to Alonzo Church, in which Lorenzen thanks him for acknowledging receipt of the manuscript, writes a few words on its history, and proposes Bernays as a referee (Alonzo Church Papers, box 26 folder 4, Manuscripts division, Department of rare books and special collections, Princeton university library).</footnote>

<footnote n="19">19. See Köthe's letter of 3 September 1947 (PL 1-1-113) and Cod. Ms. G. Köthe M 10.</footnote>
Let us present the reactions to Lorenzen’s article by subject.

6.2. *The difference with Fitch's proof.* Hao Wang (1951) writes the review for *The Journal of Symbolic Logic* and tries to compare Lorenzen's approach with Fitch's; see *Coquand 2014* for a discussion of this review. Wang 1954 (page 252) provides a more accurate comparison.

6.3. *Induction rules instead of transfinite inductions.* Gottfried Köthe and Lorenzen have worked together on lattice theory before World War II. In Spring 1947, they correspond on foundations of mathematics and physics. Köthe is preparing lectures on proofs of consistency up to Lorenzen's to be given in Fall 1947 at Mainz (see Cod. Ms. G. Köthe G 3).<sup>19</sup> In an answer to a letter by Köthe dated 8 June 1947 (PL 1-1-114), Lorenzen writes on 17 June 1947 about his work: "The formalisation of proofs of freedom from contradiction that I am striving for is not at all intent on staying inside a transfinite theory of numbers, but uses instead of 'transfinite inductions' induction rules like the 'formula induction' and 'theorem induction' of my proof of freedom from contradiction—these could also be formalised in a theory of numbers with sufficiently large constructible ordinal numbers, but nothing is gained from this".<sup>20</sup>

6.4. *The logical status of the ω-rule.* In his letter dated 9 June 1947, Ackermann would find appropriate that one "would describe somehow the constructive, contentful thinking" in Lorenzen's rule of induction. Four years later, Ackermann reflects upon the logical status of the ω-rule in the following terms.

> Indeed, the expression “derivation rule” does not seem entirely appropriate to us. For on the one hand it is a derivation rule with infinitely many premisses we are dealing with, so that no rigorous formalisation of thought is carried out, as the fact that a formal derivation can be given for each of the infinitely many premisses is the result of considerations in terms of content. [...] It matters to me here now to show that one can add certain basic formulas that have been obtained according to certain principles [...] without loosing freedom from contradiction. (*Ackermann 1952*, pages 368–369.)

This analysis is the same as that of Hilbert who writes the following about his
proof theory and formalisation twenty years earlier:

> Deducing in terms of content is superseded by an exterior acting
> according to rules, namely the use of the deduction scheme and sub-
> stitution. [...]

<footnote n="19">19. See Köthe's letter of 3 September 1947 (PL 1-1-113) and Cod. Ms. G. Köthe M 10.</footnote>

<footnote n="20">20. "Die Formalisierung der Wf beweise, die ich anstrebe, geht nun gar nicht darauf aus, innerhalb einer transfiniten Zahlentheorie zu bleiben, sondern benutzt statt der 'transfiniten Induktio nen' Induktionsregeln wie die 'Formelinduktion' und 'Satzinduktion' meines Wf beweises — diese ließen sich zwar auch in einer Zahlentheorie mit genügend großen konstruierbaren Ordinalzahlen formalisieren, dadurch wird aber nichts gewonnen." (Cod. Ms. G. Köthe M 10.)</footnote>
of numbers with sufficiently large constructible ordinal numbers, but
nothing is gained from this.<fnref n="20" />

8.4. *The logical status of the ω-rule.* In his letter dated 9 June 1947, Ackermann would find appropriate that one ‘would describe somehow the constructive, contentful thinking’ in Lorenzen’s rule of induction. Four years later, Ackermann (1952, pp. 368–369) reflects upon the logical status of the ω-rule in the following terms.

Indeed, the expression ‘derivation rule’ does not seem entirely appropriate to us. For on the one hand it is a derivation rule with infinitely many premisses we are dealing with, so that no rigorous formalisation of thought is carried out, as the fact that a formal derivation can be given for each of the infinitely many premisses is the result of considerations in terms of content. [...] It matters to me here now to show that one can add certain basic formulas that have been obtained according to certain principles [...] without losing freedom from contradiction.

This analysis is the same as that of Hilbert (1931). On p. 489, he writes the
following about his proof theory and formalisation twenty years earlier:

> Deducing in terms of content is superseded by an exterior acting accord-
> ing to rules, namely the use of the deduction scheme and substitution.
> [...].

To the proper thus formalised mathematics comes an in a way
new mathematics, a metamathematics, that is necessary to secure the
former, in which—contrary to the purely formal ways of deducing of
proper mathematics—deducing in terms of content is applied, but only
for verifying that the axioms are free from contradiction.

The axioms and provable assertions, i.e. the formulas that arise in
this interplay, are the images of the thoughts that have been making
up the habitual proceeding of mathematics up to now.

On p. 491, he writes:

> If it is verified that the formula

$\mathfrak{A}(\beta)$

becomes a correct numerical formula every time $\beta$ is a presented nu-
meral, then the formula

$(x)\mathfrak{A}(x)$

may be put on as starting formula.

<footnote n="20">20. ‘Die Formalisierung der Wf beweise, die ich anstrebe, geht nun gar nicht darauf aus, innerhalb einer transfiniten Zahlentheorie zu bleiben, sondern benutzt statt der “transfiniten Induktionen” Induktionsregeln wie die “Formelinduktion” und “Satzinduktion” meines Wf beweises – – diese ließen sich zwar auch in einer Zahlentheorie mit genügend großen konstruierbaren Ordinalzahlen formalisieren, dadurch wird aber nichts gewonnen’ (Cod. Ms. G. Köthe M 10).</footnote>
To the proper thus formalised mathematics comes an in a way
new mathematics, a metamathematics, that is necessary to secure the
former, in which—contrary to the purely formal ways of deducing of
proper mathematics—deducing in terms of content is applied, but only
for verifying that the axioms are free from contradiction.

The axioms and provable assertions, i.e. the formulas that arise in
this interplay, are the images of the thoughts that have been making
up the habitual proceeding of mathematics up to now.

If it is verified that the formula

$\mathfrak{A}(\mathfrak{z})$

becomes a correct numerical formula every time $\mathfrak{z}$ is a presented nu-
meral, then the formula

$(x)\mathfrak{A}(x)$

may be put on as starting formula. (Hilbert 1931, pages 489, 491.)

Thus the $\omega$-rule is considered as a rule of metamathematics applied in terms of content and it is ancillary in studying formal systems.

Ackermann discusses a version of Lorenzen's work, most probably the 1945
manuscript, in a letter to Lorenzen dated 31 April 1950 (sic, PL 1-1-95). *Acker-
mann 1953* provides a version of the consistency of ramified type theory in the
context of his type-free logic (see also *Schütte 1954a*).

6.5. *The $\omega$-rule combined with transfinite induction.* In an answer dated 4 November 1948 to a letter by Bernays that informs him about Lorenzen's work, Schütte states that Arnold Schmidt has acquainted him with it and writes: "As means of proof going beyond the narrower finitary standpoint, Mister Lorenzen uses inferences with infinitely many premisses, while I (as Gentzen) draw on beginning cases of the transfinite induction."<sup>21</sup>

In a letter to Bernays dated 26 August 1949, Schütte writes: “I believe that my investigations are not superfluous besides those of Lorenzen because with them the required metamathematical means of proof and the connections with the derivability of the formalised transfinite induction are uncovered.”<sup>22</sup>

<footnote n="21">21. "Als Beweismittel, die über den engeren finiten Standpunkt hinausgehen, benutzt Herr Lorenzen Schlüsse mit unendlich viel Prämissen, während ich (wie Gentzen) Anfangsfälle der transfiniten Induktion heranziehe." (Hs. 975:4228, note that Szabo translates "Anfangsfälle der" by the epithet "restricted".)</footnote>

<footnote n="22">22. “Ich glaube, daß meine Untersuchungen neben denen von Lorenzen deshalb nicht überflüssig sind, weil die benötigten metamathematischen Beweismittel und die Zusammenhänge mit der Herleitbarkeit der formalisierten transfiniten Induktion dabei aufgedeckt werden.” (Hs. 975:4230.)</footnote>
Thus the ω-rule is considered as a rule of metamathematics applied in terms of content and it is ancillary in studying formal systems.

Ackermann discusses a version of Lorenzen's work, most probably the 1945 manuscript, in a letter to Lorenzen dated 31 April 1950 (sic, PL 1-1-95). *Ackermann 1953* provides a version of the consistency of ramified type theory in the context of his type-free logic (see also *Schütte 1954a*).

**8.5. The ω-rule combined with transfinite induction.** In an answer dated 4 November 1948 to a letter by Bernays that informs him about Lorenzen's work, Schütte states that Arnold Schmidt has acquainted him with it and writes: 'As means of proof going beyond the narrower finitary standpoint, Mister Lorenzen uses inferences with infinitely many premisses, while I (as Gentzen) draw on beginning cases of the transfinite induction.'<sup>21</sup>

In a letter to Bernays dated 26 August 1949, Schütte writes: 'I believe that my investigations are not superfluous besides those of Lorenzen because with them the required metamathematical means of proof and the connections with the derivability of the formalised transfinite induction are uncovered.'<sup>22</sup>

Schütte writes to Lorenzen on 1 May 1950 in order to acknowledge the latter's priority in implementing the ω-rule into proofs of consistency.<sup>23</sup>

[...] I came to know that you had provided already before a proof of freedom from contradiction for a still more general domain, and had arrived at the following result: the cut-eliminability, that with Gentzen had been carried out only in pure logic, may also be transferred to mathematical formalisms, if instead of the inference of complete induction more general schemes of inference with infinitely many premisses are drawn on by extending the concept of derivation so that it may contain infinitely many formulas. This insight gained by you, that appears to me exceptionally important for fundamental research, I have now taken up.<sup>24</sup>

<footnote n="21">21. 'Als Beweismittel, die über den engeren finiten Standpunkt hinausgehen, benutzt Herr Lorenzen Schlüsse mit unendlich viel Prämissen, während ich (wie Gentzen) Anfangsfälle der transfiniten Induktion heranziehe' (Hs. 975:4228, note that Szabo translates 'Anfangsfälle der' by the epithet 'restricted').</footnote>

<footnote n="22">22. 'Ich glaube, daß meine Untersuchungen neben denen von Lorenzen deshalb nicht überflüssig sind, weil die benötigten metamathematischen Beweismittel und die Zusammenhänge mit der Herleitbarkeit der formalisierten transfiniten Induktion dabei aufgedeckt werden' (Hs. 975:4230).</footnote>

<footnote n="23">23. Both are not aware of the work of Novikov (1939, 1943) in this respect. See Mints 1991, § 1.2.</footnote>

<footnote n="24">24. '[...] erfuhr ich, daß Sie schon vorher einen Widerspruchsfreiheitsbeweis für einen noch allgemeineren Bereich erbracht hatten und dabei zu folgendem Ergebnis gekommen waren: Die Schnitt-Eliminierbarkeit, die bei Gentzen nur in der reinen Logik durchgeführt wurde, läßt sich auch auf mathematische Formalismen übertragen, wenn statt des Schlusses der vollständigen Induktion allgemeinere Schlußschemata mit unendlich vielen Prämissen herangezogen werden, indem der Begriff der Herleitung so erweitert wird, dass er unendlich viele Formeln enthalten darf. Diese von Ihnen gewonnene Erkenntnis, die mir außerordentlich wichtig für die Grundlagen</footnote>
Schütte writes to Lorenzen on 1 May 1950 in order to acknowledge the latter's priority in implementing the ω-rule into proofs of consistency.<fnref n="23" />

[...] I came to know that you had provided already before a proof of consistency for a still more general domain, and had arrived at the following result: the cut-eliminability, that in Gentzen had been carried out only in pure logic, may also be transferred to mathematical formalisms, if instead of the inference of complete induction more general schemes of inference with infinitely many premisses are drawn on by extending the concept of derivation so that it may contain infinitely many formulas. This insight gained by you, that appears to me exceptionally important for fundamental research, I have now taken up.<fnref n="24" />

**6.6. Semi-formal systems.** In fact, the reception of the logistic part of Lorenzen's article takes place mostly indirectly, through the articles *Schütte 1951, 1952* and the book *Schütte 1960*:<fnref n="25" /> see e.g. *Mendelson 1964*, Appendix, *Tait 1968*, *Girard 1987*, Chapter 6 and *Girard 2000*, § 2.1.

In his book, *Schütte (1960)* introduces the ω-rule as “rule UJ*”, where “UJ” stands for “infinite induction”, with a description of its meaning in terms of content by a reference to constructiveness: “For the application of rule UJ* requires a metalogical investigation. It will be requested that infinitely many formulas $F(z_1, \dots, z_n)$ have been proved to be derivable on the basis of general considerations before it is allowed to infer the derivability of the formula $F(a_1, \dots, a_n)$.” Here the $z_i$'s are numerals while the $a_i$'s are free variables. He writes further:

<footnote n="23">23. Both are not aware of the work of Novikov (1939, 1943) in this respect. See Mints 1991, § 1.2.</footnote>

<footnote n="24">24. “[...] erfuhr ich, daß Sie schon vorher einen Widerspruchsfreiheitsbeweis für einen noch allgemeineren Bereich erbracht hatten und dabei zu folgendem Ergebnis gekommen waren: Die Schnitt-Eliminierbarkeit, die bei Gentzen nur in der reinen Logik durchgeführt wurde, läßt sich auch auf mathematische Formalismen übertragen, wenn statt des Schlusses der vollständigen Induktion allgemeinere Schlußschemata mit unendlich vielen Prämissen herangezogen werden, indem der Begriff der Herleitung so erweitert wird, dass er unendlich viele Formeln enthalten darf. Diese von Ihnen gewonnene Erkenntnis, die mir außerordentlich wichtig für die Grundlagenforschung zu sein scheint, habe ich nun aufgegriffen.” (PL 1-1-95.)</footnote>

<footnote n="25">25. See § 18 and chapter IX. In a letter to Bernays dated 7 March 1957, Schütte tells the following foremost reason to write his book: “After Mister Lorenzen has published a book from his point of view [*Lorenzen 1955*], it seems necessary to me that the axiomatic direction also has its say. At any rate, I have the impression that the Americans and also the Münster school do not rightly take notice of the results of Mister Ackermann and myself.”²⁶ Note that *Schütte 1977* is not a mere translation of *Schütte 1960*, as the author abandons the treatment of ramified type theory in this second edition; in doing so, he conceals Lorenzen’s contributions to proof theory but for a spurious mention of *Lorenzen 1951* in the bibliography. Also the survey article *Schütte and Schwichtenberg 1990* records Lorenzen’s contribution to logic in an elusive way.</footnote>

<footnote n="26">26. “Nachdem Herr Lorenzen ein Buch von seinem Standpunkt aus herausgebracht hat, erscheint es mir nötig, daß auch die axiomatische Richtung zu Wort kommt. Ich habe jedenfalls den Eindruck, daß die Amerikaner und auch die Münstersche Schule die Ergebnisse von Herrn Ackermann und mir nicht recht beachten.” (Hs. 975:4234.)</footnote>
8.6. *Semi-formal systems*. In fact, the reception of the logistic part of Lorenzen’s article takes place mostly indirectly, through the articles *Schütte 1951, 1952* and the book *Schütte 1960*:<fnref n="25" /> see e.g. *Mendelson 1964*, Appendix, *Tait 1968*, *Girard 1987*, ch. 6, and *Girard 2000*, § 2.1.

In his book, *Schütte (1960)* introduces the $\omega$-rule as ‘rule UJ*’, where ‘UJ’ stands for ‘infinite induction’, with a description of its meaning in terms of content by a reference to constructiveness: ‘For the application of rule UJ* requires a metalogical investigation. It will be requested that infinitely many formulas $F(z_1, \dots, z_n)$ have been proved to be derivable on the basis of general considerations before it is allowed to infer the derivability of the formula $F(a_1, \dots, a_n)$.’ Here the $z_i$’s are numerals while the $a_i$’s are free variables. He writes further: ‘We request of a metalogical proof needed for the application of the infinite induction that it is led as all metalogical investigations in a constructive way. That is: the metalogical proof is to consist in the specification of a general procedure after which the requested derivations resp. derivation parts may be immediately exhibited’ (compare also *Schütte 1951*, p. 369). He coins the expression ‘semi-formal system’ for a formal system extended with the $\omega$-rule. In contrast, in the second edition of his book, *Schütte (1977)* keeps silent about the meaning of the $\omega$-rule and states only this: ‘We call the system DA* semi-formal since, as opposed to formal systems, it has basic inferences (S2.0*) with infinitely many premises’ (p. 174). This silence is in stark opposition to the introduction which insists in the same terms as the first edition on the ‘constructive character’ and the ‘constructive standpoint’ as the framework of metamathematics. Thus the way of dealing with infinitely many premisses is considered as a private business of the proof theorist: he should not need to express on the record the meaning of infinitary proof objects and might e.g. resort to set theory for these. The metalogical investigation is eluded.

*Schütte 1962*, written for a general audience, compares three methods for proving the consistency of arithmetic: Gentzen’s use of transfinite induction; Lorenzen’s ‘semi-formal’ use of the $\omega$-rule; Gödel’s use of computable functionals of finite

<footnote>genforschung zu sein scheint, habe ich nun aufgegriffen' (PL 1-1-95).</footnote>

<footnote n="25">25. See § 18 and ch. IX. In a letter to Bernays dated 7 March 1957, Schütte tells the following foremost reason to write his book: ‘After Mister Lorenzen has published a book from his point of view [*Lorenzen 1955*], it seems necessary to me that the axiomatic direction also has its say. At any rate, I have the impression that the Americans and also the Münster school do not rightly take notice of the results of Mister Ackermann and myself.’²⁶ Note that *Schütte 1977* is not a mere translation of *Schütte 1960*, as the author abandons the treatment of ramified type theory in this second edition; in doing so, he conceals Lorenzen’s contributions to proof theory but for a spurious mention of *Lorenzen 1951* in the bibliography. Also the survey article *Schütte and Schwichtenberg 1990* records Lorenzen’s contribution to logic in an elusive way.</footnote>

<footnote n="26">26. ‘Nachdem Herr Lorenzen ein Buch von seinem Standpunkt aus herausgebracht hat, erscheint es mir nötig, daß auch die axiomatische Richtung zu Wort kommt. Ich habe jedenfalls den Eindruck, daß die Amerikaner und auch die Münstersche Schule die Ergebnisse von Herrn Ackermann und mir nicht recht beachten’ (Hs. 975:4234).</footnote>
“We request of a metalogical proof needed for the application of the infinite in-
duction that it is led as all metalogical investigations in a constructive way. That
is: the metalogical proof is to consist in the specification of a general procedure
after which the requested derivations resp. derivation parts may be immediately
exhibited” (compare also *Schütte 1951*, page 369). He coins the expression “semi-
formal system” for a formal system extended with the ω-rule. In contrast, in the
second edition of his book, *Schütte (1977)* keeps silent about the meaning of the
ω-rule and states only this: “We call the system DA* semi-formal since, as opposed
to formal systems, it has basic inferences (S2.0*) with infinitely many premises”
(page 174). This silence is in stark opposition to the introduction which insists
in the same terms as the first edition on the “constructive character” and the
“constructive standpoint” as the framework of metamathematics. Thus the way
of dealing with infinitely many premisses is considered as a private business of the
proof theorist: he should not need to express on the record the meaning of infini-
tary proof objects and might e.g. resort to set theory for these. The metalogical
investigation is eluded.

*Schütte 1962*, written for a general audience, compares three methods for prov-
ing the consistency of arithmetic: Gentzen's use of transfinite induction; Loren-
zen's "semi-formal" use of the ω-rule; Gödel's use of computable functionals of
finite type. The last is the "most direct" as it possesses "a character of im-
mediate evidence" whereas "ordinal inductions appear as admissible only after
a corresponding foundation"; "semi-formal systems permit analyses of the logico-
mathematical deduction that suggest themselves and are particularly transparent";
"transfinite ordinals [...] give us the possibility to characterise the different in-
duction principles used metamathematically with respect to logical strength by
equivalent ordinal inductions" (pages 106–107).

The detour via Schütte’s reception may have contributed to proof theory con-
tinuing to focus on measuring logical strength by ordinal numbers, whereas the
fact that Lorenzen does not resort to ordinals in his proof of consistency should
be considered as a feature of his approach.

Tait (1968) provides a very clear presentation of Schütte’s approach with a
mention of Lorenzen; see also Feferman and Sieg 1981, § 3.2, for an account of
Tait 1968.

6.7. *The generalised inductive definition of accessibility.* Wilhelm Ackermann hears about Lorenzen’s proof of consistency in 1946 through Bernays (see his letter to Lorenzen dated 11 November 1946, PL 1-1-125). As he writes in a subsequent letter dated 21 May 1947, Ackermann is working at the time at setting up “mathematics out of a type-free logical system that is demonstrably free from contradiction”<fnref n="27" /> and for this he needs a “considerably higher ordinal number” than in the “trans-

<footnote n="27">27. “aus einem nachweislich widerspruchsfreien typenfreien logischen Axiomensystem die Mathematik aufzubauen” (PL 1-1-117).</footnote>
type. The last is the 'most direct' as it possesses 'a character of immediate evidence' whereas 'ordinal inductions appear as admissible only after a corresponding foundation'; 'semi-formal systems permit analyses of the logico-mathematical deduction that suggest themselves and are particularly transparent'; 'transfinite ordinals [...] give us the possibility to characterise the different induction principles used metamathematically with respect to logical strength by equivalent ordinal inductions' (pp. 106-107).

The detour via Schütte's reception may have contributed to proof theory continuing to focus on measuring logical strength by ordinal numbers, whereas the fact that Lorenzen does not resort to ordinals in his proof of consistency should be considered as a feature of his approach.

Tait (1968) provides a very clear presentation of Schütte's approach with a mention of Lorenzen; see also Feferman and Sieg 1981, § 3.2, for an account of Tait 1968.

**8.7. The generalised inductive definition of accessibility.** Wilhelm Ackermann hears about Lorenzen's proof of consistency in 1946 through Bernays (see his letter to Lorenzen dated 11 November 1946, PL 1-1-125). As he writes in a subsequent letter dated 21 May 1947, Ackermann is working at the time at setting up 'mathematics out of a type-free logical system that is demonstrably free from contradiction'<fnref n="27" /> and for this he needs a 'considerably higher ordinal number' than in the 'transfinite inductions up to the first ε-number' that 'Gentzen and [he] use in [their] proofs of freedom from contradiction of arithmetic'. He is therefore interested in 'constructively recordable numbers of the second number class' following Church (1938).<fnref n="28" />

In their correspondence, they are also interested in a set-up of ordinal numbers by Lorenzen: see Ackermann's letters of 21 May and of 9 June 1947. In the latter he writes: 'As far as I understand the train of thought of your set-up from your hints, your set-up of the ordinal numbers of the 2. number class appears to me as constructivistically usable'.<fnref n="29" />

Recall that Gentzen (1936, § 15.4) proves the finiteness of his reduction procedure by a transfinite induction described as the generalised inductive definition of the 'accessibility [Erreichbarkeit]' of the first ε-number. He discusses the constructiveness of this concept in § 16.1.1, which may be seen as the very heart of his proof of the consistency of elementary number theory: '[Accessibility] acquires

<footnote n="27">27. 'aus einem nachweislich widerspruchsfreien typenfreien logischen Axiomensystem die Matematik aufzubauen' (PL 1-1-117).</footnote>

<footnote n="28">28. 'So benutzen Gentzen und ich bei unseren Widerspruchsfreiheitsbeweisen für die Arithmetik transfinite Induktionen bis zur ersten ε-Zahl. Bei den Untersuchungen, an denen ich augenblicklich arbeite, gehe ich bis zu einer wesentlich höheren Ordinalzahl. Unter einer konstruktiv erfassbaren Zahl der II. Zahlenklasse verstehe ich dabei im Anschluss an A. Church [...]'</footnote>

<footnote n="29">29. 'Soweit ich den Gedankengang Ihres Aufbaus nach Ihren Andeutungen verstehe, erscheint mir Ihr Aufbau für die Ordinalzahlen der 2. Zahlenklasse als konstruktivistisch brauchbar' (PL 1-1-115).</footnote>
finite inductions up to the first ε-number” that “Gentzen and [he] use in [their]
proofs of freedom from contradiction of arithmetic”. He is therefore interested in
“constructively recordable numbers of the second number class” following Church
(1938).<fnref n="28" />

In their correspondence, they are also interested in a setup of ordinal numbers
by Lorenzen: see Ackermann's letters of 21 May and of 9 June 1947. In the latter
he writes: "As far as I understand the train of thought of your setup from your
hints, your setup of the ordinal numbers of the 2. number class appears to me as
constructively usable".<fnref n="29" />

Recall that Gentzen (1936, § 15.4) proves the finiteness of his reduction procedure by a transfinite induction described as the generalised inductive definition of the “accessibility [Erreichbarkeit]” of the first ε-number. He discusses the constructiveness of this concept in § 16.1.1, which may be seen as the very heart of his proof of the consistency of elementary number theory: “[Accessibility] acquires a sense merely by being predicated of a definite [ordinal] number for which its validity is simultaneously proved.”

Ackermann (1951) sets up the segment of ordinal numbers that he needs and gives a remarkably precise account of the constructiveness of accessibility, relying in particular on Lorenzen's ω-rule. He provides in fact a description for the generalised inductive definition of the concept of accessibility, and we guess that it has benefitted from his exchanges with Lorenzen. The “o-numbers” below are given as a certain recursively defined totally ordered system of symbols.

Now we have to show that the o-numbers are really ordinal num-
bers, or, in other words, that we are allowed to apply *deductions by
transfinite induction*.

In order to lay out the text of the following considerations with less
difficulty, it is advisable to introduce the following symbols, but with
which we only express concisely contentful states of affairs. These sym-
bols are: $\mathfrak{A}(\alpha)$, “the property $\mathfrak{A}$ applies to $\alpha$”; $\mathfrak{R}_x(\alpha, \mathfrak{A}(x))$, “the prop-
erty $\mathfrak{A}$ applies to all o-numbers which are less than $\alpha$”; $\mathfrak{V}_x(\alpha, \mathfrak{A}(x))$,
“with $\mathfrak{R}_x(\beta, \mathfrak{A}(x))$ also $\mathfrak{A}(\beta)$ has always to be the case, provided $\beta \leqslant \alpha$”.
It may now be that $\mathfrak{R}_x(\alpha + 1, \mathfrak{A}(x))$ is derivable from the assump-
tions $\mathfrak{A}(1)$ and $\mathfrak{V}_x(\alpha, \mathfrak{A}(x))$ by constructive deductions without assum-
ing anything else about $\mathfrak{A}$. We would then first say that the number $\alpha$
is accessible through $\mathfrak{A}$. Now, if an o-number is accessible through $\mathfrak{A}$,

<footnote n="28">28. “So benutzen Gentzen und ich bei unseren Widerspruchsfreiheitsbeweisen für die Arithmetik transfinite Induktionen bis zur ersten ε-Zahl. Bei den Untersuchungen, an denen ich augenblicklich arbeite, gehe ich bis zu einer wesentlich höheren Ordinalzahl. Unter einer konstruktiv erfassbaren Zahl der II. Zahlenklasse verstehe ich dabei im Anschluss an A. Church [...].”</footnote>

<footnote n="29">29. “Soweit ich den Gedankengang Ihres Aufbaus nach Ihren Andeutungen verstehe, erscheint mir Ihr Aufbau für die Ordinalzahlen der 2. Zahlenklasse als konstruktivistisch brauchbar.” (PL 1-1-115.)</footnote>
a sense merely by being predicated of a definite [ordinal] number for which its validity is simultaneously proved.'

Ackermann (1951) sets up the segment of ordinal numbers that he needs and gives a remarkably precise account of the constructiveness of accessibility, relying in particular on Lorenzen's ω-rule. He provides in fact a description for the generalised inductive definition of the concept of accessibility, and we guess that it has benefited from his exchanges with Lorenzen. The 'o-numbers' below are given as a certain recursively defined totally ordered system of symbols.

Now we have to show that the o-numbers are really ordinal numbers, or, in other words, that we are allowed to apply deductions by transfinite induction.

In order to lay out the text of the following considerations with less difficulty, it is advisable to introduce the following symbols, but with which we only express concisely contentful states of affairs. These symbols are: $\mathfrak{A}(\alpha)$, ‘the property $\mathfrak{A}$ applies to $\alpha$’; $\mathfrak{K}_x(\alpha, \mathfrak{A}(x))$, ‘the property $\mathfrak{A}$ applies to all o-numbers which are less than $\alpha$’; $\mathfrak{V}_x(\alpha, \mathfrak{A}(x))$, ‘with $\mathfrak{K}_x(\beta, \mathfrak{A}(x))$ also $\mathfrak{A}(\beta)$ has always to be the case, provided $\beta \leq \alpha$’. It may now be that $\mathfrak{K}_x(\alpha + 1, \mathfrak{A}(x))$ is derivable from the assumptions $\mathfrak{A}(1)$ and $\mathfrak{V}_x(\alpha, \mathfrak{A}(x))$ by constructive deductions without assuming anything else about $\mathfrak{A}$. We would then first say that the number $\alpha$ is accessible through $\mathfrak{A}$. Now, if an o-number is accessible through $\mathfrak{A}$, then it is also accessible through any other property $\mathfrak{B}$. For, as we had not assumed anything about $\mathfrak{A}$ in the derivation of $\mathfrak{K}_x(\alpha + 1, \mathfrak{A}(x))$ but that $\mathfrak{A}(1)$ and $\mathfrak{V}_x(\alpha, \mathfrak{A}(x))$ has to be the case, so we need only to replace everywhere $\mathfrak{A}$ by $\mathfrak{B}$ in the deductions that lead from $\mathfrak{A}(1)$ and $\mathfrak{V}_x(\alpha, \mathfrak{A}(x))$ to $\mathfrak{K}_x(\alpha + 1, \mathfrak{A}(x))$. We may therefore, instead of saying that $\alpha$ is accessible through $\mathfrak{A}$, simply say that $\alpha$ is accessible. It might now seem that accessibility is defined by a claim of generality over predicates. But this is not our conception. We want to conceive the accessibility of a number $\alpha$ as a certain intuitive fact, viz. precisely as the presence of a certain system of deductions that leads from $\mathfrak{A}(1)$ and $\mathfrak{V}_x(\alpha, \mathfrak{A}(x))$ to $\mathfrak{K}_x(\alpha + 1, \mathfrak{A}(x))$. All deductions of the so-called positive logic are to belong to these deductions, further also the number-theoretic induction and the corresponding operating with the universal sign for o-numbers as it would e.g. fit intuitionistic number theory. We do not want to specify here these deductions in detail because the following proof shows which are needed. We remark only that the following deduction is also needed: if a claim may be derived for each concrete o-number, then also the corresponding universal claim is to be derivable.² For the use of the universal sign we remark that the o-numbers represent a countable set that is precisely defined and set up constructively, so that the use of a universal sign for o-numbers
then it is also accessible through any other property $\mathfrak{B}$. For, as we had not assumed anything about $\mathfrak{A}$ in the derivation of $\mathfrak{R}_x(\alpha + 1, \mathfrak{A}(x))$ but that $\mathfrak{A}(1)$ and $\mathfrak{V}_x(\alpha, \mathfrak{A}(x))$ has to be the case, so we need only to replace everywhere $\mathfrak{A}$ by $\mathfrak{B}$ in the deductions that lead from $\mathfrak{A}(1)$ and $\mathfrak{V}_x(\alpha, \mathfrak{A}(x))$ to $\mathfrak{R}_x(\alpha + 1, \mathfrak{A}(x))$. We may therefore, instead of saying that $\alpha$ is accessible through $\mathfrak{A}$, simply say that $\alpha$ is accessible. It might now seem that accessibility is defined by a claim of generality over predicates. But this is not our conception. We want to conceive the accessibility of a number $\alpha$ as a certain intuitive fact, viz. precisely as the presence of a certain system of deductions that leads from $\mathfrak{A}(1)$ and $\mathfrak{V}_x(\alpha, \mathfrak{A}(x))$ to $\mathfrak{R}_x(\alpha + 1, \mathfrak{A}(x))$. All deductions of the so-called positive logic are to belong to these deductions, further also the number-theoretic induction and the corresponding operating with the universal sign for o-numbers as it would e.g. fit intuitionistic number theory. We do not want to specify here these deductions in detail because the following proof shows which are needed. We remark only that the following deduction is also needed: if a claim may be derived for each concrete o-number, then also the corresponding universal claim is to be derivable.<fnref n="2" /> For the use of the universal sign we remark that the o-numbers represent a countable set that is precisely defined and set up constructively, so that the use of a universal sign for o-numbers is legitimated in the same way as that of the universal sign for natural numbers.

In a letter to Ackermann dated 3 March 1951, Lorenzen writes:

> Thank you very much for your work "Constructive setup of a segment of the 2. number class"—your construction impresses me very much, I have tried earlier a similar one but not as far-reaching. I wholly share your views on the constructiveness of your definitions and proofs. (*Ackermann 1983*, page 197.)

Schütte (1954b, § 4) takes over the argument of Ackermann 1951 and extends its system of o-numbers into so-called "Klammersymbole" that generalise also the system of ordinal fixed points of Veblen (1908). This argument may also be found in Schütte 1960, § 11–12, that presents an intermediate system inspired by the coding as integers of Hilbert and Bernays 1939, § 5.3.c. In contrast, it is absent from Schütte 1977, as is any description of the nature of a constructive argument; as the beginning of § 24 introducing higher ordinals states, the reading, constructive or axiomatic, is up to the reader: "we use the notions *map* (*function*) and *set*

<footnote n="2">2. This deduction appears self-evident from the point of view of content. It has been applied first by P. Lorenzen inside a logistic system. Cf. P. Lorenzen, *The freedom from contradiction of the logic of ramified type* (Journal of Symbolic Logic, to appear shortly).</footnote>
is legitimated in the same way as that of the universal sign for natural numbers.

2. This deduction appears self-evident from the point of view of content. It has been applied first by P. Lorenzen inside a logistic system. Cf. P. Lorenzen, The freedom from contradiction of the logic of ramified type (Journal of Symbolic Logic, to appear shortly).

In a letter to Ackermann dated 3 March 1951 (see Ackermann 1983, p. 197), Lorenzen writes:

> Thank you very much for your work 'Constructive set-up of a segment of the 2. number class'—your construction impresses me very much, I have tried earlier a similar one but not as far-reaching. I wholly share your views on the constructiveness of your definitions and proofs.

Schütte (1954b, § 4) takes over the argument of Ackermann 1951 and extends its system of o-numbers into so-called 'Klammersymbole' that generalise also the system of ordinal fixed points of Veblen (1908). This argument may also be found in Schütte 1960, § 11–12, that presents an intermediate system inspired by the coding as integers of Hilbert and Bernays 1939, § 5.3.c. In contrast, it is absent from Schütte 1977, as is any description of the nature of a constructive argument; at the beginning of § 24 introducing higher ordinals on p. 221, the reading, constructive or axiomatic, is up to the reader: 'we use the notions *map (function)* and *set* in a naive way. But these may also be regarded as being determined axiomatically (in the context of a general axiom system for set theory)'.

> See also the account of accessibility by Gödel (1990 [1972], note c on p. 272).

**8.8. Are infinitary inductive definitions predicative?** A few years later, Schütte (1962, p. 110) dissociates himself from the analysis of Ackermann 1951 and qualifies the generalised inductive definition of accessibility as impredicative:

> Hereby one proceeds in an impredicative way by including the concept of accessibility itself, defined with reference to the totality of all properties of certain ordinals, into these properties.

Schütte (1965, p. 280) defines 'an ordering relation $<'$ of equivalence classes of natural numbers representing a sufficiently large segment of the second number class in a constructive way'. On p. 286, he writes: 'The relation $<'$ can be proved by impredicative methods to be a well-ordering using a proof similar to that for the related $\nleq$-relation in § 12 of Schütte 1960.'

In particular, Lorenzen's theorem induction would be impredicative if one followed Schütte's narrow acceptation.

**8.9. Further accounts. Lorenzen 1955** expands on the rôle of lattices in logic (§ 7) and mathematics (part III). Lorenzen 1958, 1987 provide a proof of Gentzen's
in a naive way. But these may also be regarded as being determined axiomatically
(in the context of a general axiom system for set theory)” (page 221).

See also the account of accessibility by Gödel (1990 [1972], note c on page 272).

6.8. Are infinitary inductive definitions predicative? In 1962, Schütte dissociates himself from the analysis of Ackermann 1951 and qualifies the generalised inductive definition of accessibility as impredicative:

Hereby one proceeds in an impredicative way by including the concept of accessibility itself, defined with reference to the totality of all properties of certain ordinals, into these properties. (Schütte 1962, page 110.)

In 1965, he defines “an ordering relation $\prec$ of equivalence classes of natural numbers representing a sufficiently large segment of the second number class in a constructive way” (page 280). He writes: “The relation $\prec$ can be proved by impredicative methods to be a well-ordering using a proof similar to that for the related $\prec$-relation in § 12 of Schütte 1960” (page 286).

In particular, Lorenzen's theorem induction would be impredicative if one followed Schütte's narrow acceptation.

6.9. Further accounts. Lorenzen 1955 expands on the rôle of lattices in logic (§ 7) and mathematics (part III). Lorenzen 1958, 1987 provide a proof of Gentzen's subformula theorem by the method of his article. Lorenzen 1962 (§ 7) returns to the subject of proofs of consistency.

Evert W. Beth (1959, page 253) gives a short and precise account of Lorenzen's article.

Haskell B. Curry (1963, Chapter 4, theorem B9) follows Lorenzen in characterising a distributive lattice as a lattice satisfying cut.

Manfred E. Szabo (1969, pages 12–13) comments on the relationship of Lorenzen's article with Gentzen's work.

Oskar Becker (1954) refers to Lorenzen's article in the last pages of his book Grundlagen der Mathematik in geschichtlicher Entwicklung.

Its philosophical significance is addressed by Matthias Wille (2013, 2016).

Coquand 2021 describes Lorenzen's standpoint in a broader context than given here.

7. Our reception: impredicative quantification and inductive definitions. Whitehead and Russell (1925, page 57) see the axiom of reducibility as a generalisation of Leibniz's identity of indiscernibles. For instance, the formula $\forall_X X(3) \rightarrow X(x)$, which seems impredicative since it contains a quantification over all predicates, is actually equivalent to the predicative formula $3 = x$. Using in a crucial way ideas from Lorenzen 2020 [1944], we extend this remark to a predicative interpretation of some formulae involving a seemingly impredicative universal quantification over all predicates.
subformula theorem by the method of his article. Lorenzen 1962 (§ 7) returns to
the subject of proofs of consistency.

Oskar Becker (1954) refers to Lorenzen’s article in the last pages of his book
*Grundlagen der Mathematik in geschichtlicher Entwicklung*.

Evert W. Beth (1959, p. 253) gives a short and precise account of Lorenzen’s
article.

Maurice Meigne (1959, p. 62–63) does so as well, but does not seem to under-
stand the content of the ω-rule.

Haskell B. Curry (1963, ch. 4, theorem B9) follows Lorenzen in characterising
a distributive lattice as a lattice satisfying cut.

Manfred E. Szabo (1969, p. 12–13) comments on the relationship of Lorenzen’s
article with Gentzen’s work.

Its philosophical significance is addressed by Matthias Wille (2013, 2016).

*Coquand 2021* describes Lorenzen’s standpoint in a broader context than given
here.

**9. Our reception: impredicative quantification and inductive definitions.** Whitehead and Russell (1925, p. 57) see the axiom of reducibility as a generalisation of Leibniz’s identity of indiscernibles. For instance, the formula $\forall_X X(3) \rightarrow X(x)$, which seems impredicative since it contains a quantification over all predicates, is actually equivalent to the predicative formula $3 = x$. Using in a crucial way ideas from Lorenzen 2020 [1944], we extend this remark to a predicative interpretation of some formulae involving a seemingly impredicative universal quantification over all predicates.

**9.1. Free Lorenzen algebras and countable choice.** Let us state the definition of a
countably complete Lorenzen algebra.

**Definition 1.** A *Lorenzen algebra* is a meet-semilattice with a *negation*, i.e. a
least element $0$ and an operation $\bar{a}$ such that $b \le \bar{a}$ if, and only if, $b \wedge a = 0$. (This
semilattice has then automatically a greatest element $1 = \bar{0}$.) Such an algebra
is *countably complete* if it is endowed with an infinitary meet operation over any
sequence of elements indexed by $\mathbb{N}$.

The main result of *Lorenzen 2020 [1944]* is to essentially build the free count-
ably complete Lorenzen algebra $K$ over a given preordered set $P$ and to show that
the canonical map $P \to K$ is an embedding. This is a purely semilattice-theoretic
reformulation of Gentzen’s 1936 consistency proof of arithmetic. We write ‘essen-
tially’ since the actual statement is a little more complex if one wants to avoid the
use of the axiom of countable choice. We provide such a statement below; note
that a possible constructive way to avoid the axiom of countable choice is provided
by the setting of *The Univalent Foundations Program* (2013).
7.1. *Free Lorenzen algebras and countable choice.* Let us state the definition of a countably complete Lorenzen algebra.

**Definition 1.** A Lorenzen algebra is a meet-semilattice with a *negation*, i.e. a least element 0 and an operation $\bar{a}$ such that $b \le \bar{a}$ if, and only if, $b \wedge a = 0$. (This semilattice has then automatically a greatest element $1 = \bar{0}$.) Such an algebra is *countably complete* if it is endowed with an infinitary meet operation over any sequence of elements indexed by $\mathbb{N}$.

The main result of Lorenzen 2020 [1944] is to essentially build the free countably complete Lorenzen algebra $K$ over a given preordered set $P$ and to show that the canonical map $P \to K$ is an embedding. This is a purely semilattice-theoretic reformulation of Gentzen's 1936 consistency proof of arithmetic. We write "essentially" since the actual statement is a little more complex if one wants to avoid the use of the axiom of countable choice. We provide such a statement below; note that a possible constructive way to avoid the axiom of countable choice is provided by the setting of the Univalent Foundations Program (2013).

7.2. *An impredicative formal system: syntax.* We consider the following language. The terms are of the form $S^k(0)$ and $S^k(x)$. A closed term $t$ represents such a natural number, that we will also write $t$. The atomic formulae are of the form $X(t)$ or $P(t_1, \dots, t_n)$, where $P$ represents some $n$-ary boolean-valued function.

We have formulae built from $\top$, $\neg\psi$, $\varphi \wedge \psi$, and $\forall_x\psi$ and $\forall_X\psi$.

A formula is arithmetical if it does not contain any quantification over predicates.

A formula is strictly $\Pi_1^1$ if it is of the form $\forall_X \mu$, where $\mu$ is arithmetical and uses only $X$ as a predicate variable.

We consider the fragment of the language in which we form only strictly $\Pi_1^1$ universal quantifications $\forall_X \mu$.

We also have terms for predicates $T, U, \dots$. They are of the form $T = \lambda_x \mu$. We define the substitution $\psi(T/X)$ for a closed predicate $T$ by induction on $\psi$:

$$ (X(t))(T/X) = \mu(t/x) \qquad (\neg\mu)(T/X) = \neg(\mu(T/X)) $$

$$ (Y(t))(T/X) = Y(t) \qquad (\mu_0 \wedge \mu_1)(T/X) = \mu_0(T/X) \wedge \mu_1(T/X) $$

$$ P(t_1, \dots, t_n)(T/X) = P(t_1, \dots, t_n) \qquad (\forall_x \mu)(T/X) = \forall_x \mu(T/X) $$

7.3. *A semilattice defined in a predicative metatheory.* We use Lorenzen 2020 [1944] to build, in a predicative metatheory, a special semilattice $L$.

We let $n, m, \dots$ range over natural numbers.

We start from an infinite set of symbols $X, Y, \dots$ representing predicate variables on numbers.

Then we build inductively the symbolic objects in $L$ by the rule

$$ a, b, \dots ::= X(n) \mid 0 \mid \neg a \mid a \wedge b \mid \bigwedge_n a_n $$
### 9.2. An impredicative formal system: syntax.
We consider the following language. The terms are of the form $S^k(0)$ and $S^k(x)$. A closed term $t$ represents such a natural number, that we will also write $t$. The atomic formulae are of the form $X(t)$ or $P(t_1, \dots, t_n)$, where $P$ represents some $n$-ary boolean-valued function.

We have formulae built from $\top$, $\neg\psi$, $\varphi \wedge \psi$, and $\forall_x\psi$ and $\forall_X\psi$.

A formula is arithmetical if it does not contain any quantification over predicates.

A formula is strictly $\Pi_1^1$ if it is of the form $\forall_X\mu$, where $\mu$ is arithmetical and uses only $X$ as a predicate variable.

We consider the fragment of the language in which we form only strictly $\Pi_1^1$ universal quantifications $\forall_X\mu$.

We also have terms for predicates $T, U, \dots$. They are of the form $T = \lambda_x\mu$. We define the substitution $\psi(T/X)$ for a closed predicate $T$ by induction on $\psi$:

$$ (X(t))(T/X) = \mu(t/x) \qquad (-\mu)(T/X) = -\mu(T/X) $$

$$ (Y(t))(T/X) = Y(t) \qquad (\mu_0 \wedge \mu_1)(T/X) = \mu_0(T/X) \wedge \mu_1(T/X) $$

$$ P(t_1, \dots, t_n)(T/X) = P(t_1, \dots, t_n) \qquad (\forall_x\mu)(T/X) = \forall_x(\mu(T/X)) $$

### 9.3. A semilattice defined in a predicative metatheory.
We use Lorenzen 2020 [1944] to build, in a predicative metatheory, a special semilattice $L$.

We let $n, m, \dots$ range over natural numbers.

We start from an infinite set of symbols $X, Y, \dots$ representing predicate variables on numbers.

Then we build inductively the symbolic objects in $L$ by the rule

$$ a, b, \dots ::= X(n) \mid 0 \mid \neg a \mid a \wedge b \mid \bigwedge_n a_n $$

with $|$ delimiting the alternatives of the rule.

One way to interpret Lorenzen 2020 [1944] is that he defines a *preorder* relation $a \le b$ on the set $L$ such that $a \le \neg b$ if, and only if, $a \wedge b \le 0$; $0 \le a$ for all $a$; $b \le \bigwedge_n a_n$ if, and only if, $b \le a_n$ for all $n$; $c \le a \wedge b$ if, and only if, $c \le a$ and $c \le b$.

If we wanted to build the free countably complete Lorenzen algebra over the atoms $X(n)$, we would have to quotient by the equivalence relation defined by $a \le b$ and $b \le a$, and countable choice would be needed to show that we get a countably complete Lorenzen algebra.

If $\Omega$ is a countably complete Lorenzen algebra and $\rho$ assigns to any predicate symbol $X$ occurring in $a$ a function $\rho(X): \mathbb{N} \to \Omega$, we can compute $a\rho$ in $\Omega$ by induction on $a$ by the following rules:

$$ X(n)\rho = \rho(X)(n) \quad 0\rho = 0 \quad (-a)\rho = \overline{a\rho} \quad (a\wedge b)\rho = a\rho\wedge b\rho \quad (\bigwedge_n a_n)\rho = \bigwedge_n (a_n\rho) $$

We have $a\rho \le b\rho$ in $\Omega$ whenever $a \le b$ in $L$.
with $|\cdot|$ delimiting the alternatives of the rule.

One way to interpret Lorenzen 2020 [1944] is that he defines a preorder relation $a \le b$ on the set $L$ such that $a \le \neg b$ if, and only if, $a \wedge b \le 0$; $0 \le a$ for all $a$; $b \le \bigwedge_n a_n$ if, and only if, $b \le a_n$ for all $n$; $c \le a \wedge b$ if, and only if, $c \le a$ and $c \le b$.

If we wanted to build the free countably complete Lorenzen algebra over the atoms $X(n)$, we would have to quotient by the equivalence relation defined by $a \le b$ and $b \le a$, and countable choice would be needed to show that we get a countably complete Lorenzen algebra.

If $\Omega$ is a countably complete Lorenzen algebra and $\rho$ assigns to any predicate symbol $X$ occurring in $a$ a function $\rho(X): \mathbb{N} \to \Omega$, we can compute $a\rho$ in $\Omega$ by induction on $a$ by the following rules:

$$X(n)\rho = \rho(X)(n) \quad 0\rho = 0 \quad \neg a\rho = \overline{a\rho} \quad (a \wedge b)\rho = a\rho \wedge b\rho \quad (\bigwedge_n a_n)\rho = \bigwedge_n (a_n\rho)$$

We have $a\rho \le b\rho$ in $\Omega$ whenever $a \le b$ in $L$.

We let $L_{\text{fin}}$ be the subset of symbolic objects in $L$ which depend on finitely many predicate symbols.

An ideal $A$ is a subset of $L_{\text{fin}}$ containing $0$ and such that $b \in A$ whenever $a \in A$ and $b \le a$. In particular any element $a$ in $L_{\text{fin}}$ defines the principal ideal $\downarrow a$ of all elements in $L_{\text{fin}}$ such that $b \le a$.

We let $\Omega$ be the set of all ideals. $\Omega$ has a structure of countably complete Lorenzen algebra, with meet as intersection and with least element $\{0\}$. The negation operation defines $\bar{A}$ as the ideal of elements $b$ in $L_{\text{fin}}$ such that $b \wedge a \le 0$ whenever $a$ is in $A$.

In particular, if $\rho$ assigns a function $\mathbb{N} \to \Omega$ to any predicate symbol $X$, we can compute $a\rho$ in $\Omega$ for $a$ in $L_{\text{fin}}$.

By induction on $a$, we can show the following result.

**Lemma 2.** If $a$ is in $L_{\text{fin}}$ and we have $\rho(X)(n) = \downarrow X(n)$ for the predicate symbols $X$ occurring in $a$, then $a\rho = \downarrow a$.

Let $c(X)$ be a symbolic object in $L_{\text{fin}}$ in which at most $X$ occurs as predicate symbol. We shall write $c(Y)$ for the object arising by substitution of $X$ by $Y$ in $c(X)$, and $c(X)(X = f)$ for the element $c(X)\rho$ computed in $\Omega$ with $\rho$ assigning the function $f: \mathbb{N} \to \Omega$ to $X$.

The key result which provides a predicative analysis of (strict) impredicative comprehension is the following.

**Theorem 3.** The family $c(X)(X = f)$, where $f$ ranges over the functions $\mathbb{N} \to \Omega$, has a g.l.b. $\bigwedge_f c(X)(X = f)$ in the semilattice $\Omega$.

*Proof.* Define $A$ to be the set of all elements $a$ such that $a \le c(X)$ for $X$ not occurring in $a$. Note that if neither $X$ nor $Y$ occur in $a$, then $a \le c(X)$ is equivalent
We let $L_{fin}$ be the subset of symbolic objects in $L$ which depend on *finitely many* predicate symbols.

An ideal $A$ is a subset of $L_{fin}$ containing $0$ and such that $b \in A$ whenever $a \in A$ and $b \le a$. In particular any element $a$ in $L_{fin}$ defines the principal ideal $\downarrow a$ of all elements in $L_{fin}$ such that $b \le a$.

We let $\Omega$ be the set of all ideals. $\Omega$ has a structure of countably complete Lorenzen algebra, with intersection as meet and with least element $\{0\}$. The negation operation defines $\bar{A}$ as the ideal of elements $b$ in $L_{fin}$ such that $b \wedge a \le 0$ whenever $a$ is in $A$.

In particular, if $\rho$ assigns a function $N \to \Omega$ to any predicate symbol $X$, we can compute $a\rho$ in $\Omega$ for $a$ in $L_{fin}$.

By induction on $a$, we can show the following result.

**Lemma 2.** If $a$ is in $L_{fin}$ and we have $\rho(X)(n) = \downarrow(X(n))$ for the predicate symbols $X$ occurring in $a$, then $a\rho = \downarrow a$.

Let $c(X)$ be a symbolic object in $L_{fin}$ in which at most $X$ occurs as predicate symbol. We shall write $c(Y)$ for the object arising by substitution of $X$ by $Y$ in $c(X)$, and $c(X)(X = f)$ for the element $c(X)\rho$ computed in $\Omega$ with $\rho$ assigning the function $f: N \to \Omega$ to $X$. The key result which provides a predicative analysis of (strict) impredicative comprehension is the following.

**Theorem 3.** *The family $c(X)(X = f)$, where $f$ ranges over the functions $N \to \Omega$, has a g.l.b. $\bigwedge_f c(X)(X = f)$ in the semilattice $\Omega$.*

*Proof.* Define $A$ to be the set of all elements $a$ such that $a \le c(X)$ if $X$ does not occur in $a$. Note that if neither $X$ nor $Y$ occur in $a$, then $a \le c(X)$ is equivalent to $a \le c(Y)$. It follows from this remark that $a$ is in $A$ if, and only if, $a \le c(X)$ for all $X$ not occurring in $a$ if, and only if, $a \le c(X)$ for some $X$ not occurring in $a$. If $a$ is in $A$ and $b \le a$, then $a \le c(X)$ for some $X$ not occurring in $a$; if we consider $Y$ occurring *neither* in $a$ nor in $b$, then $a \le c(Y)$ and hence $b \le c(Y)$, so that $b$ is in $A$. The set $A$ is thus an ideal, i.e. an element of $\Omega$.

We claim that $a$ is in $A$ if, and only if, it belongs to all $c(X)(X = f)$, which will show that $A$ is the g.l.b. of the family $c(X)(X = f)$.

If $a$ is in $A$ then $a \le c(X)$ for $X$ not occurring in $a$. Define $\rho(Z)(n) = \downarrow(Z(n))$ for $Z$ occurring in $a$ and $\rho(X) = f$. We then have $a\rho \le c(X)\rho$. But $a\rho = \downarrow a$ by lemma 2 and $c(X)\rho = c(X)(X = f)$. Hence $\downarrow a \le c(X)(X = f)$ and $a$ is in $c(X)(X = f)$.

If conversely $a$ contains no occurrence of $X$ and is in all $c(X)(X = f)$, where $f$ ranges over $N \to \Omega$, then in particular it is in $c(X)(X = g)$ for $g(n) = \downarrow(X(n))$. In this case $c(X)(X = g)$ is $\downarrow c(X)$ by lemma 2 and so $a \le c(X)$, i.e. $a$ is in $A$. $\square$
to $a \leqslant c(Y)$. It follows from this remark that $a$ is in $A$ if, and only if, $a \leqslant c(X)$ for all $X$ not occurring in $a$ if, and only if, $a \leqslant c(X)$ for some $X$ not occurring in $a$. If $a$ is in $A$ and $b \leqslant a$, then $a \leqslant c(X)$ for some $X$ not occurring in $a$; if we consider $Y$ occurring neither in $a$ nor in $b$, then $a \leqslant c(Y)$ and hence $b \leqslant c(Y)$, so that $b$ is in $A$. The set $A$ is thus an ideal, i.e. an element of $\Omega$.

We claim that $a$ is in $A$ if, and only if, it belongs to all $c(X)(X = f)$, which will show that $A$ is the g.l.b. of the family $c(X)(X = f)$.

If $a$ is in $A$ then $a \leqslant c(X)$ for $X$ not occurring in $a$. Define $\rho(Z)(n) = \downarrow Z(n)$ for $Z$ occurring in $a$ and $\rho(X) = f$. We then have $a\rho \leqslant c(X)\rho$. But $a\rho = \downarrow a$ by lemma 2 and $c(X)\rho = c(X)(X = f)$. Hence $\downarrow a \leqslant c(X)(X = f)$ and $a$ is in $c(X)(X = f)$.

If conversely $a$ contains no occurrence of $X$ and is in all $c(X)(X = f)$, where $f$ ranges over $\mathbb{N} \to \Omega$, then in particular it is in $c(X)(X = g)$ for $g(n) = \downarrow X(n)$. In this case $c(X)(X = g)$ is $\downarrow c(X)$ by lemma 2 and so $a \leqslant c(X)$, i.e. $a$ is in $A$. $\square$

### 7.4. Interpretation of strict $\Pi_1^1$-comprehension: semantics.
Any arithmetical formula $\nu$ defines an element $[\nu]$ in $L_{\text{fin}}$ by the rules

$$ 
\begin{array}{l@{\qquad}l@{\qquad}l}
[X(t)] = X(t) & [P(t_1, \dots, t_n)] = \delta_P(t_1, \dots, t_n) & \\
[\neg \mu] = \neg [\mu] & [\mu_0 \wedge \mu_1] = [\mu_0] \wedge [\mu_1] & [\forall_x \mu] = \bigwedge_n [\mu(n/x)]
\end{array}
$$

where $\delta_P$ is the $n$-ary 0, 1-valued function representing $P$.

If $\rho$ assigns a function $\rho(X): \mathbb{N} \to \Omega$ for $X$ free in $\psi$, we can define the semantics $[[\psi]]\rho$ as an element of $\Omega$.

We define it first for an arithmetical formula by the clauses

$$ 
\begin{array}{l@{\qquad}l@{\qquad}l}
[[X(t)]\rho = \rho(X)(t) & [[P(t_1, \dots, t_n)]\rho = \delta_P(t_1, \dots, t_n) & \\
[\neg \mu]\rho = \neg([\mu]\rho) & [\mu_0 \wedge \mu_1]\rho = [\mu_0]\rho \wedge [\mu_1]\rho & [\forall_x \mu]\rho = \bigcap_n [\mu(n/x)]\rho
\end{array}
$$

We can now define $[[T]]\rho$ for $T = \lambda_x \mu$ by $[[\lambda_x \mu]\rho(n) = [[\mu(n/x)]\rho]$.

If $\mu$ is an arithmetical formula with at most one free variable $X$, then $[[\mu]](X = f)$ is equal to $[\mu](X = f)$. By theorem 3, the family $[[\mu]](X = f)$ has a g.l.b. and we can define

$$ [[\forall X \mu]\rho = \bigwedge_f [[\mu]](\rho, X = f). $$

In particular, we get

$$ [[\forall X \mu]\rho \leq [[\mu]](\rho, X = [[T]]\rho) = [[\mu](T/X)]\rho $$

and our semantics, which we have built in a predictive metatheory, justifies comprehension for strictly $\Pi_1^1$ formulae.
9.4. Interpretation of strict Π₁¹-comprehension: semantics. Any arithmetical formula ν defines an element [ν] in Lfin by the rules

$$ 
\begin{gather*}
[X(t)] = X(t) \qquad [P(t_1, \dots, t_n)] = \delta_P(t_1, \dots, t_n) \\
[\neg \mu] = \neg [\mu] \qquad [\mu_0 \wedge \mu_1] = [\mu_0] \wedge [\mu_1] \qquad [\forall_x \mu] = \bigwedge_n [\mu(n/x)]
\end{gather*}
$$

where $\delta_P$ is the $n$-ary 0, 1-valued function representing $P$.

If $\rho$ assigns a function $\rho(X): \mathbb{N} \to \Omega$ for $X$ free in $\psi$, we can define the semantics $[[\psi]]\rho$ as an element of $\Omega$. We define it first for an arithmetical formula by the clauses

$$ 
\begin{gather*}
[[X(t)]\rho = \rho(X)(t) \qquad [P(t_1, \dots, t_n)]\rho = \delta_P(t_1, \dots, t_n) \\
[\neg \mu]\rho = \neg([\mu]\rho) \qquad [\mu_0 \wedge \mu_1]\rho = [\mu_0]\rho \wedge [\mu_1]\rho \qquad [\forall_x \mu]\rho = \bigcap_n [\mu(n/x)]\rho
\end{gather*}
$$

We can now define $[[T]]\rho$ for $T = \lambda_x \mu$ by $[[\lambda_x \mu]]\rho(n) = [[\mu(n/x)]\rho]$.

If $\mu$ is an arithmetical formula with at most one free variable $X$, then $[[\mu]](X = f)$ is equal to $[\mu](X = f)$. By theorem 3, the family $[[\mu]](X = f)$ has a g.l.b. and we can define

$$ [[\forall X \mu]]\rho = \bigwedge_f [[\mu]](\rho, X = f). $$

In particular, we get

$$ [[\forall X \mu]]\rho \leq [[\mu]](\rho, X = [[T]]\rho) = [[\mu(T/X)]\rho] $$

and our semantics, which we have built in a predicative metatheory, justifies comprehension for strictly $\Pi_1^1$ formulae.

## References

* Ackermann, H. R. 1983. 'Aus dem Briefwechsel Wilhelm Ackermanns'. *History and Philosophy of Logic*, **4**, 181–202. doi:10.1080/01445348308837054.

* Ackermann, W. 1951. 'Konstruktiver Aufbau eines Abschnitts der zweiten Cantorschen Zahlenklasse'. *Mathematische Zeitschrift*, **53**, 403–413. http://eudml.org/doc/169197.

* Ackermann, W. 1952. 'Widerspruchsfreier Aufbau einer typenfreien Logik. (Erweitertes System)'. *Mathematische Zeitschrift*, **55**, 364–384. http://eudml.org/doc/169263.

* Ackermann, W. 1953. 'Widerspruchsfreier Aufbau einer typenfreien Logik. II'. *Mathematische Zeitschrift*, **57**, 155–166. http://eudml.org/doc/169311.

* Becker, O. 1954. *Grundlagen der Mathematik in geschichtlicher Entwicklung*. Freiburg: Karl Alber.

* Bernays, P. 1939. 'Review of Fitch 1938'. *The Journal of Symbolic Logic*, **4**, 97–98. http://www.jstor.org/stable/2269079.

* Beth, E. W. 1959. *The Foundations of Mathematics: a Study in the Philosophy of Science*. (Studies in Logic and the Foundations of Mathematics), Amsterdam: North-Holland.
## References

Ackermann, H. R. 1983. 'Aus dem Briefwechsel Wilhelm Ackermanns'. *Hist. Philos. Logic*, 4(2), 181–202. doi:10.1080/01445348308837054.

Ackermann, W. 1951. 'Konstruktiver Aufbau eines Abschnitts der zweiten Cantorschen Zahlenklasse'. *Math. Z.*, 53, 403–413. http://eudml.org/doc/169197.

Ackermann, W. 1952. 'Widerspruchsfreier Aufbau einer typenfreien Logik. (Erweitertes System)'. *Math. Z.*, 55, 364–384. http://eudml.org/doc/169263.

Ackermann, W. 1953. 'Widerspruchsfreier Aufbau einer typenfreien Logik. II'. *Math. Z.*, 57, 155–166. http://eudml.org/doc/169311.

Becker, O. 1954. *Grundlagen der Mathematik in geschichtlicher Entwicklung*. Freiburg: Karl Alber.

Bernays, P. 1939. 'Review of Fitch 1938'. *J. Symb. Log.*, 4(2), 97–98. http://www.jstor.org/stable/2269079.

Beth, E. W. 1959. *The foundations of mathematics: a study in the philosophy of science*. Studies in Logic and the Foundations of Mathematics, North-Holland, Amsterdam.

Buchholz, W., Feferman, S., Pohlers, W., and Sieg, W. 1981. *Iterated inductive definitions and subsystems of analysis: recent proof-theoretical studies*. Lecture Notes in Mathematics, 897, Berlin: Springer-Verlag.

Cederquist, J. and Coquand, Th. 2000. 'Entailment relations and distributive lattices'. In S. R. Buss, P. Hájek, and P. Pudlák (eds.), *Logic Colloquium '98: proceedings of the annual European summer meeting of the Association for symbolic logic, held in Prague, Czech Republic, August 9–15, 1998*. Lecture Notes in Logic, 13, Association for Symbolic Logic, Urbana, 127–139.

Chajda, I., Halaš, R., and Kühr, J. 2007. *Semilattice structures*. Research and Exposition in Mathematics, 30, Heldermann Verlag, Lemgo.

Church, A. 1938. 'The constructive second number class'. *Bull. Amer. Math. Soc.*, 44(4), 224–232. doi:10.1090/S0002-9904-1938-06720-1.

Chwistek, L. 1925. 'The theory of constructive types. (Principles of logic and mathematics). II. Cardinal arithmetic'. *Ann. Soc. Polon. Math.*, 3, 92–141. http://name.umd1.umich.edu/AAS7985.0001.001.

Citkin, A. 2016. 'Multiple conclusion rules in logics with the disjunction property'. In S. Artemov and A. Nerode (eds.), *Logical foundations of computer science: international symposium, LFCS 2016: Deerfield Beach, FL, USA, January 4–7, 2016: proceedings*. Lecture Notes in Comput. Sci., 9537, Cham: Springer, 76–89. doi:10.1007/978-3-319-27683-0_6.

Coquand, Th. 2014. 'Recursive functions and constructive mathematics'. In J. Dubucs and M. Bourdeau (eds.), *Constructivity and computability in historical and philosophical perspective*. Logic, Epistemology, and the Unity of Science, 34, Springer, Dordrecht, 159–167.

Coquand, Th. 2021. 'Lorenzen and constructive mathematics'. In Heinzmann and Wolters 2021. 47–61.
Cederquist, J. and Coquand, Th. 2000. 'Entailment relations and distributive lattices'. In S. R. Buss, P. Hájek, and P. Pudlák (eds.), *Logic Colloquium '98: Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic, Held in Prague, Czech Republic, August 9-15, 1998.* (Lecture Notes in Logic, 13), Urbana: Association for Symbolic Logic, 127-139.

Chajda, I., Halaš, R., and Kühr, J. 2007. *Semilattice Structures*. (Research and Exposition in Mathematics, 30), Lemgo: Heldermann.

Church, A. 1938. 'The constructive second number class'. *Bulletin of the American Mathematical Society*, **44**, 224-232. doi:**10.1090/S0002-9904-1938-06720-1.**

Chwistek, L. 1925. 'The theory of constructive types. (Principles of logic and mathematics). II. Cardinal arithmetic'. *Annales de la Société Polonaise de Mathématique*, **3**, 92-141. http://name.umd1.umich.edu/AAS7985.0001.001.

Citkin, A. 2016. 'Multiple conclusion rules in logics with the disjunction property'. In S. Artemov and A. Nerode (eds.), *Logical Foundations of Computer Science: International Symposium, LFCS 2016: Deerfield Beach, FL, USA, January 4-7, 2016: Proceedings*. (Lecture Notes in Computer Science, 9537), Cham: Springer, 76-89. doi:**10.1007/978-3-319-27683-0_6**.

Coquand, Th. 2014. 'Recursive functions and constructive mathematics'. In J. Dubucs and M. Bourdeau (eds.), *Constructivity and Computability in Historical and Philosophical Perspective*. (Logic, Epistemology, and the Unity of Science, 34), Dordrecht: Springer, 159-167.

Coquand, Th. 2021. 'Lorenzen and constructive mathematics'. In *Heinzmann and Wolters 2021*. 47-61.

Coquand, Th., Lombardi, H., and Neuwirth, St. 2019. 'Lattice-ordered groups generated by an ordered group and regular systems of ideals'. *The Rocky Mountain Journal of Mathematics*, **49**, 1449-1489. doi:**10.1216/rmj-2019-49-5-1449.**

Coquand, Th., Lombardi, H., and Neuwirth, St. 2025. 'In 1955, Paul Lorenzen clears the sky in foundations of mathematics for Hermann Weyl'. In L. Crosilla, Ø. Linnebo, and M. Rathjen (eds.), *Weyl's Work on the Foundations and Philosophy of Mathematics*. (Logic and Computation in Philosophy), Oxford University Press.

Coquand, Th. and Neuwirth, St. 2017. 'An introduction to Lorenzen's "Algebraic and logistic investigations on free lattices" (1951)'. arXiv:**1711.06139v1**.

Coquand, Th. and Neuwirth, St. 2020. 'Lorenzen's proof of consistency for elementary number theory'. *History and Philosophy of Logic*, **41**, 281-290. doi:**10.1080/01445340.2020.1752034.**

Curry, H. Br. 1963. *Foundations of Mathematical Logic*. New York: McGraw-Hill.

Feferman, S. and Sieg, W. 1981. 'Iterated inductive definitions and subsystems of analysis'. In W. Buchholz *et al*. (eds.), *Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies*, ch. I. (Lecture Notes in Mathematics, 897), Berlin: Springer, 16-77.

Fitch, Fr. Br. 1938. 'The consistency of the ramified *Principia*. The Journal of Symbolic Logic*, **3**, 140-149. http://www.jstor.org/stable/2267777.
Coquand, Th., Lombardi, H., and Neuwirth, St. 2019. 'Lattice-ordered groups generated by an ordered group and regular systems of ideals'. *Rocky Mountain J. Math.*, 49, 1449–1489. doi:10.1216/rmj-2019-49-5-1449.

Coquand, Th. and Neuwirth, St. 2017. 'An introduction to Lorenzen's "Algebraic and logistic investigations on free lattices" (1951)'. arXiv:1711.06139v1.

Coquand, Th. and Neuwirth, St. 2020. 'Lorenzen's proof of consistency for elementary number theory'. *Hist. Philos. Logic*, 41(3), 281–290. doi:10.1080/01445340.2020.1752034.

Curry, H. B. 1963. *Foundations of mathematical logic*. McGraw-Hill, New York.

Feerman, S., Dawson, Jr., J. W., Kleene, S. C., Moore, G. H., Solovay, R. M., and van Heijenoort, J. (eds.). 1990. *Kurt Gödel: Collected works, II: Publications 1938–1974*. Oxford: Clarendon Press.

Feerman, S. and Sieg, W. 1981. 'Iterated inductive definitions and subsystems of analysis'. In *Buchholz, Feerman, Pohlers, and Sieg 1981*, chap. I. 16–77.

Fitch, F. B. 1938. 'The consistency of the ramified Principia'. *J. Symb. Log.*, 3(4), 140–149. http://www.jstor.org/stable/2267777.

Fitch, F. B. 1939. 'The hypothesis that infinite classes are similar'. *J. Symb. Log.*, 4(4), 159–162. http://www.jstor.org/stable/2268716.

Gaifman, H. 1964. 'Infinite Boolean polynomials. I'. *Fund. Math.*, 54, 229–250. http://eudml.org/doc/213758. Errata in *Fund. Math.*, 57, 117, 1965, http://eudml.org/doc/213847.

Gentzen, G. 1935. 'Untersuchungen über das logische Schließen. II'. *Math. Z.*, 39(1), 405–431. http://eudml.org/doc/168556. Translation by M. E. Szabo: Investigations into logical deduction, sections IV and V, in *Szabo 1969*, 103–131.

Gentzen, G. 1936. 'Die Widerspruchsfreiheit der reinen Zahlentheorie'. *Math. Ann.*, 112, 493–565. http://eudml.org/doc/159839. Translation by M. E. Szabo: The consistency of elementary number theory, in *Szabo 1969*, 132–201.

Gethmann, C. F. 1991. 'Phänomenologie, Lebensphilosophie und konstruktive Wissenschaftstheorie: eine historische Skizze zur Vorgeschichte der Erlanger Schule'. In C. F. Gethmann (ed.), *Lebenswelt und Wissenschaft: Studien zum Verhältnis von Phänomenologie und Wissenschaftstheorie*. Neuzeit und Gegenwart: philosophische Studien, 1, Bonn: Bouvier, 28–77.

Girard, J.-Y. 1987. *Proof theory and logical complexity*. Studies in Proof Theory, 1, Naples: Bibliopolis.

Girard, J.-Y. 2000. 'Du pourquoi au comment: la théorie de la démonstration de 1950 à nos jours'. In J.-P. Pier (ed.), *Development of mathematics 1950–2000*. Basel: Birkhäuser, 515–545.

Gödel, K. 1990 [1972]. 'On an extension of finitary mathematics which has not yet been used'. In *Feerman, Dawson, Kleene, Moore et al. 1990*. 271–280.

Grätzer, G. 2011. *Lattice theory: foundation*. Birkhäuser, Basel. doi:10.1007/978-3-0348-0018-1.

Hales, A. W. 1964. 'On the non-existence of free complete Boolean algebras'. *Fund. Math.*, 54, 45–66. http://eudml.org/doc/213773.
Fitch, Fr. Br. 1939. 'The hypothesis that infinite classes are similar'. *The Journal of Symbolic Logic*, 4, 159-162. http://www.jstor.org/stable/2268716.

Gaifman, H. 1964. 'Infinite Boolean polynomials. I'. *Fundamenta Mathematicae*, 54, 229-250. http://eudml.org/doc/213758. Errata in *Fundamenta Mathematicae*, 57, 117, 1965, http://eudml.org/doc/213847.

Gentzen, G. 1935. 'Untersuchungen über das logische Schließen. II'. *Mathematische Zeitschrift*, 39, 405-431. http://eudml.org/doc/168556. Translation by M. E. Szabo: 'Investigations into logical deduction', sections IV and V, in *Szabo 1969*, 103-131.

Gentzen, G. 1936. 'Die Widerspruchsfreiheit der reinen Zahlentheorie'. *Mathematische Annalen*, 112, 493-565. http://eudml.org/doc/159839. Translation by M. E. Szabo: 'The consistency of elementary number theory', in *Szabo 1969*, 132-201.

Gethmann, C. Fr. 1991. 'Phänomenologie, Lebensphilosophie und konstruktive Wissenschaftstheorie: eine historische Skizze zur Vorgeschichte der Erlanger Schule'. In C. Fr. Gethmann (ed.), *Lebenswelt und Wissenschaft: Studien zum Verhältnis von Phänomenologie und Wissenschaftstheorie*. (Neuzeit und Gegenwart: philosophische Studien, 1), Bonn: Bouvier, 28-77.

Girard, J.-Y. 1987. *Proof Theory and Logical Complexity*. (Studies in Proof Theory, 1), Naples: Bibliopolis.

Girard, J.-Y. 2000. 'Du pourquoi au comment: la théorie de la démonstration de 1950 à nos jours'. In J.-P. Pier (ed.), *Development of Mathematics 1950-2000*. Basel: Birkhäuser, 515-545.

Gödel, K. 1990 [1972]. 'On an extension of finitary mathematics which has not yet been used'. In S. Feferman *et al*. (eds.), *Kurt Gödel: Collected Works, II: Publications 1938-1974*. Oxford: Clarendon Press, 271-280.

Grätzer, G. 2011. *Lattice Theory: Foundation*. Basel: Birkhäuser. doi:10.1007/978-3-0348-0018-1.

Hales, A. W. 1964. 'On the non-existence of free complete Boolean algebras'. *Fundamenta Mathematicae*, 54, 45-66. http://eudml.org/doc/213773.

Heinzmann, G. and Wolters, G. (eds.). 2021. *Paul Lorenzen: Mathematician and Logician*. (Logic, Epistemology, and the Unity of Science, 51), Cham: Springer. doi:10.1007/978-3-030-65824-3.

Hilbert, D. 1931. 'Die Grundlegung der elementaren Zahlenlehre'. *Mathematische Annalen*, 104, 485-494. http://eudml.org/doc/159480.

Hilbert, D. and Bernays, P. 1939. *Grundlagen der Mathematik II*. (Die Grundlehren der mathematischen Wissenschaften in Einzeldarstellungen mit besonderer Berücksichtigung der Anwendungsgebiete, 50), Berlin: Springer.

Köthe, G. 1948. 'Verbände'. In *Süss 1948*. 81-95.

Lorenzen, P. 1948a. 'Grundlagen der Mathematik'. In *Süss 1948*. 11-22.

Lorenzen, P. 1948b. *Einführung in die Logik*. Bonn: Mathematisches Seminar der Universität.

Lorenzen, P. 1949. 'Einführung in die Logik'. *Archiv der Mathematik*, 2, 60-65. doi:10.1007/BF02036755.
Heinzmann, G. and Wolters, G. (eds.). 2021. *Paul Lorenzen—mathematician and logician*. Logic, Epistemology, and the Unity of Science, 51, Cham: Springer.
doi:10.1007/978-3-030-65824-3.

Hilbert, D. 1931. 'Die Grundlegung der elementaren Zahlenlehre'. *Math. Ann.*, 104(1), 485–494. http://eudml.org/doc/159480.

Hilbert, D. and Bernays, P. 1939. *Grundlagen der Mathematik. II*. Die Grundlehren der mathematischen Wissenschaften in Einzeldarstellungen mit besonderer Berücksichtigung der Anwendungsgebiete, 50, Berlin: Springer.

Kahle, R. and Rathjen, M. (eds.). 2020. *The legacy of Kurt Schütte*. Cham: Springer.
Köthe, G. 1948. 'Verbände'. In *Süss 1948*. 81–95.

Lorenzen, P. 1948a. 'Grundlagen der Mathematik'. In *Süss 1948*. 11–22.

Lorenzen, P. 1948b. *Einführung in die Logik*. Bonn: Mathematisches Seminar der Universität.

Lorenzen, P. 1949. 'Einführung in die Logik'. *Arch. Math. (Basel)*, 2, 60–65.
doi:10.1007/BF02036755.

Lorenzen, P. 1950a. 'Über halbgeordnete Gruppen'. *Math. Z.*, 52, 483–526.
http://eudml.org/doc/169131.

Lorenzen, P. 1950b. 'Konstruktive Begründung der Mathematik'. *Math. Z.*, 53, 162–202.
http://eudml.org/doc/169180.

Lorenzen, P. 1951. 'Algebraische und logistische Untersuchungen über freie Verbände'.
*J. Symb. Log.*, 16(2), 81–106. http://www.jstor.org/stable/2266681.

Lorenzen, P. 1952. 'Teilbarkeitstheorie in Bereichen'. *Math. Z.*, 55, 269–275.
http://eudml.org/doc/169251.

Lorenzen, P. 1953. 'Die Erweiterung halbgeordneter Gruppen zu Verbandsgruppen'.
*Math. Z.*, 58, 15–24. http://eudml.org/doc/169331.

Lorenzen, P. 1955. *Einführung in die operative Logik und Mathematik*. Die Grundlehren
der mathematischen Wissenschaften in Einzeldarstellungen mit besonderer Berücksichti-
gung der Anwendungsgebiete, 28, Springer, Berlin.

Lorenzen, P. 1958. *Formale Logik*. Sammlung Göschen, 1176-1176a, Berlin: Walter de
Gruyter. Translation by Fr. J. Crosson: *Formal logic*, D. Reidel, Dordrecht, 1965.

Lorenzen, P. 1962. *Metamathematik*. B-I-Hochschultaschenbücher, 25, Mannheim: Bi-
bliographisches Institut. Translation by J.-Bl. Grize: *Métamathématique*, Gauthier-
Villars, Paris, 1967. Translation by J. Muñoz: *Metamatemática*, Tecnos, Madrid, 1971.

Lorenzen, P. 1987. *Lehrbuch der konstruktiven Wissenschaftstheorie*. Bibliographisches Institut, Mannheim.

Lorenzen, P. 2020 [1944]. 'Ein halbordnungstheoretischer Widerspruchsfreiheitsbeweis'.
*Hist. Philos. Logic*, 41(3), 265–280. doi:10.1080/01445340.2020.1752040. Dual German-
English text, edited and translated by St. Neuwirth.

MacNeille, H. M. 1937. 'Partially ordered sets'. *Trans. Amer. Math. Soc.*, 42(3), 416–460.
doi:10.2307/1989739.

Martin-Löf, P. 1970. *Notes on constructive mathematics*. Almqvist & Wiksell, Stockholm.
Lorenzen, P. 1950a. ‘Über halbgeordnete Gruppen’. *Mathematische Zeitschrift*, **52**, 483–526. http://eudml.org/doc/169131.

Lorenzen, P. 1950b. ‘Konstruktive Begründung der Mathematik’. *Mathematische Zeitschrift*, **53**, 162–202. http://eudml.org/doc/169180.

Lorenzen, P. 1951. ‘Algebraische und logistische Untersuchungen über freie Verbände. *The Journal of Symbolic Logic*, **16**, 81–106. http://www.jstor.org/stable/2266681.

Lorenzen, P. 1952. ‘Teilbarkeitstheorie in Bereichen’. *Mathematische Zeitschrift*, **55**, 269–275. http://eudml.org/doc/169251.

Lorenzen, P. 1953. ‘Die Erweiterung halbgeordneter Gruppen zu Verbandsgruppen’. *Mathematische Zeitschrift*, **58**, 15–24. http://eudml.org/doc/169331.

Lorenzen, P. 1955. *Einführung in die operative Logik und Mathematik. (Die Grundlehren der mathematischen Wissenschaften in Einzeldarstellungen mit besonderer Berücksichtigung der Anwendungsgebiete)*, 78), Berlin: Springer.

Lorenzen, P. 1958. *Formale Logik. (Sammlung Göschen, 1176-1176a)*, Berlin: Walter de Gruyter. Translation by Fr. J. Crosson: *Formal Logic*, Dordrecht: D. Reidel, 1965.

Lorenzen, P. 1962. *Metamathematik. (B-I-Hochschultaschenbücher, 25)*, Mannheim: Bibliographisches Institut. Translation by J.-Bl. Grize: *Métamathématique*, Paris: Gauthier-Villars, 1967. Translation by J. Muñoz: *Metamatemática*, Madrid: Tecnos, 1971.

Lorenzen, P. 1987. *Lehrbuch der konstruktiven Wissenschaftstheorie*. Mannheim: Bibliographisches Institut.

Lorenzen, P. 2020 [1944]. ‘Ein halbordnungstheoretischer Widerspruchsfreiheitsbeweis’. *History and Philosophy of Logic*, **41**, 265–280. doi:10.1080/01445340.2020.1752040. Dual German-English text, edited and translated by St. Neuwirth.

MacNeille, H. M. 1937. ‘Partially ordered sets’. *Transactions of the American Mathematical Society*, **42**, 416–460. doi:10.2307/1989739.

Martin-Löf, P. 1970. *Notes on Constructive Mathematics*. Stockholm: Almqvist & Wiksell.

Meigne, M. 1959. *La consistance des théories formelles et le fondement des mathématiques. (Les Grandes Études)*, Paris: Le Cercle du livre. Ph.D. thesis, Université de Lille, 1957.

Mendelson, E. 1964. *Introduction to Mathematical Logic*. Princeton: D. Van Nostrand.

Mints, Gr. 1991. ‘Proof theory in the USSR 1925–1969’. *The Journal of Symbolic Logic*, **56**, 385–424. http://www.jstor.org/stable/2274689.

Neuwirth, St. 2015. ‘The free Lorenzen algebra generated by a preordered set’. http://neuwirth.perso.math.cnrs.fr/IMG/pdf/the_free.lorenzen_algebra_generated_by_a_preordered_set.pdf. Technical note.

Neuwirth, St. 2021. ‘Lorenzen’s reshaping of Krull’s Fundamentalsatz for integral domains (1938–1953)’. In *Heinzmann and Wolters 2021*. 141–180.

Neuwirth, St. 2022. “‘C’est comme œuf”: Paul Lorenzen et l’effondrement des preuves de non-contradiction’. In L. Dahan-Gaida (ed.), *Eurêka ! Récits savants de découverte et*
Mendelson, E. 1964. *Introduction to mathematical logic*. Princeton: D. Van Nostrand Co.

Mints, Gr. 1991. 'Proof theory in the USSR 1925–1969'. *J. Symb. Log.*, 56(2), 385–424.
http://www.jstor.org/stable/2274689.

Neuwirth, St. 2015. 'The free Lorenzen algebra generated by a preordered set'. http://neuwirth.perso.math.cnrs.fr/IMG/pdf/the_free.lorenzen_algebra_generated_by_Technical note.

Neuwirth, St. 2021. 'Lorenzen's reshaping of Krull's Fundamentalsatz for integral domains (1938–1953)'. In *Heinzmann and Wolters 2021*. 141–180.

Neuwirth, St. 2022. "'C'est comme œuf": Paul Lorenzen et l'effondrement des preuves de non-contradiction'. In L. Dahan-Gaida (ed.), *Eurêka! Récits savants de découverte et d'invention*. Cahiers d'histoire et de philosophie des sciences, Paris: Hermann, 241–258.
http://hal.archives-ouvertes.fr/hal-03104374.

Novikov, P. S. 1939. 'Sur quelques théorèmes d'existence'. *C. R. (Dokl.) Acad. Sci. URSS (N.S.)*, 23, 438–440.

Novikov, P. S. 1943. 'On the consistency of certain logical calculus'. *Mat. Sb. (N. S.)*, 12(54)(2), 231–261. http://mi.mathnet.ru/eng/msb6158. Announced in *Novikov 1939*.

Rieger, L. 1951. 'On free $\kappa_\xi$-complete Boolean algebras (with an application to logic)'. *Fund. Math.*, 38, 35–52. http://eudml.org/doc/213251. Review by Lorenzen: Zbl. 0044.26103.

Schmidt, A. 1950. 'Mathematische Grundlagenforschung'. In H. Hasse and E. Hecke (eds.), *Enzyklopädie der mathematischen Wissenschaften mit Einschluß ihrer Anwendungen, Band I: Algebra und Zahlentheorie, 1. Teil: A. Grundlagen B. Algebra*, chap. 2. Leipzig: B. G. Teubner, second ed..

Schütte, K. 1951. 'Beweistheoretische Erfassung der unendlichen Induktion in der Zahlentheorie'. *Math. Ann.*, 122, 369–389. http://eudml.org/doc/160227.

Schütte, K. 1952. 'Beweistheoretische Untersuchung der verzweigten Analysis'. *Math. Ann.*, 124, 123–147. http://eudml.org/doc/160263.

Schütte, K. 1954a. 'Ein widerspruchsloses System der Analysis auf typenfreier Grundlage'. *Math. Z.*, 61, 160–179. http://eudml.org/doc/169456.

Schütte, K. 1954b. 'Kennzeichnung von Ordnungszahlen durch rekursiv erklärte Funktionen'. *Math. Ann.*, 127, 15–32. http://eudml.org/doc/160361.

Schütte, K. 1960. *Beweistheorie*. Die Grundlehren der mathematischen Wissenschaften in Einzeldarstellungen mit besonderer Berücksichtigung der Anwendungsgebiete, 103, Springer, Berlin.

Schütte, K. 1962. 'Logische Abgrenzungen des Transfiniten'. In M. Käsbauer and F. v. Kutschera (eds.), *Logik und Logikkalkül*. Freiburg: K. Alber, 105–114.

Schütte, K. 1965. 'Predicative well-orderings'. In J. N. Crossley and M. Dummett (eds.), *Formal systems and recursive functions: proceedings of the eighth logic colloquium: Oxford, July 1963*. Studies in logic and the foundations of mathematics, 40, North-Holland, Amsterdam, 280–303.
d'invention. (Cahiers d'histoire et de philosophie des sciences), Paris: Hermann, 241–258.
http://hal.archives-ouvertes.fr/hal-03104374.

Novikov, P. S. 1939. 'Sur quelques théorèmes d'existence'. *Comptes Rendus (Doklady de l'Académie des Sciences de l'URSS, nouvelle série, 23*, 438–440.

Novikov, P. S. 1943. 'On the consistency of certain logical calculus'. *Recueil Mathématique (Matematicheskii Sbornik), nouvelle série, 12(54)*, 231–261. http://mi.mathnet.ru/eng/msb6158.

Regis, E. 1987. *Who Got Einstein's Office? Eccentricity and Genius at the Institute for Advanced Study*. Reading: Addison-Wesley.

Rieger, L. 1951. 'On free $\aleph_\xi$-complete Boolean algebras (with an application to logic)'. *Fundamenta Mathematicae, 38*, 35–52. http://eudml.org/doc/213251. Review by Lorenzen: Zbl. 0044.26103.

Schmidt, A. 1950. *Mathematische Grundlagenforschung. (Enzyklopädie der mathematischen Wissenschaften mit Einschluß ihrer Anwendungen*, Band I: Algebra und Zahlen-theorie, 1. Teil: A. Grundlagen B. Algebra, Heft 1, Teil II), Leipzig: B. G. Teubner.

Schütte, K. 1951. 'Beweistheoretische Erfassung der unendlichen Induktion in der Zahlentheorie'. *Mathematische Annalen, 122*, 369–389. http://eudml.org/doc/160227.

Schütte, K. 1952. 'Beweistheoretische Untersuchung der verzweigten Analysis'. *Mathematische Annalen, 124*, 123–147. http://eudml.org/doc/160263.

Schütte, K. 1954a. 'Ein widerspruchsloses System der Analysis auf typenfreier Grundlage'. *Mathematische Zeitschrift, 61*, 160–179. http://eudml.org/doc/169456.

Schütte, K. 1954b. 'Kennzeichnung von Ordnungszahlen durch rekursiv erklärte Funktionen'. *Mathematische Annalen, 127*, 15–32. http://eudml.org/doc/160361.

Schütte, K. 1960. *Beweistheorie. (Die Grundlehren der mathematischen Wissenschaften in Einzeldarstellungen mit besonderer Berücksichtigung der Anwendungsgebiete*, 103), Berlin: Springer.

Schütte, K. 1962. 'Logische Abgrenzungen des Transfiniten'. In M. Käsbauer and F. v. Kutschera (eds.), *Logik und Logikkalkül: Herrn Professor Dr. Wilhelm Britzelmayr zum siebzigsten Geburtstag von seinen Freunden und Schülern gewidmet*. Freiburg: Karl Alber, 105–114.

Schütte, K. 1965. 'Predicative well-orderings'. In J. N. Crossley and M. Dummett (eds.), *Formal Systems and Recursive Functions: Proceedings of the Eighth Logic Colloquium: Oxford, July 1963*. (Studies in Logic and the Foundations of Mathematics, 40), Amsterdam: North-Holland, 280–303.

Schütte, K. 1977. *Proof Theory. (Grundlehren der mathematischen Wissenschaften, 225)*, Berlin: Springer. Translation from the German by J. N. Crossley.

Schütte, K. and Schwichtenberg, H. 1990. 'Mathematische Logik'. In G. Fischer, F. Hirzebruch, W. Scharlau, and W. Törnig (eds.), *Ein Jahrhundert Mathematik: 1890-1990. (Dokumente zur Geschichte der Mathematik, 6)*, Braunschweig: Friedr. Vieweg, 717–740. Reprinted in R. Kahle and M. Rathjen (eds.), *The Legacy of Kurt Schütte*, Cham: Springer, 2020, 71–91.

Scott, D. 1971. 'On engendering an illusion of understanding'. *The Journal of Philosophy, 68*, 787–807. http://www.jstor.org/stable/2024952.
Schütte, K. 1977. *Proof theory*. Grundlehren der mathematischen Wissenschaften, 225, Springer, Berlin. Translation from the German by J. N. Crossley.

Schütte, K. and Schwichtenberg, H. 1990. 'Mathematische Logik'. In G. Fischer, F. Hirzebruch, W. Scharlau, and W. Törnig (eds.), *Ein Jahrhundert Mathematik: 1890-1990*. Dokumente zur Geschichte der Mathematik, 6, Braunschweig: Friedr. Vieweg, 717-740. Reprinted in *Kahle and Rathjen 2020*, 71-91.

Scott, D. 1971. 'On engendering an illusion of understanding'. *J. Philos.*, 68(21), 787-807.
http://www.jstor.org/stable/2024952.

Skolem, Th. 1921. 'Logisch-kombinatorische Untersuchungen über die Erfüllbarkeit oder Beweisbarkeit mathematischer Sätze nebst einem Theoreme über dichte Mengen'. *Skr. Videnskapsselskapet Kristiania 1920, I. Mat.-naturv. Kl.*, 1(4).
http://archive.org/details/skrifterutgitavv201chri.

Solovay, R. M. 1966. 'New proof of a theorem of Gaifman and Hales'. *Bull. Amer. Math. Soc.*, 72, 282-284. doi:10.1090/S0002-9904-1966-11493-3.

Süss, W. (ed.). 1948. *Naturforschung und Medizin in Deutschland 1939-1946, 1: Reine Mathematik, I*. Fiat Review of German Science, Dieterich'sche Verlagsbuchhandlung, Wiesbaden.

Szabo, M. E. (ed.). 1969. *The collected papers of Gerhard Gentzen*. Studies in Logic and the Foundations of Mathematics, Amsterdam: North-Holland.

Tait, W. W. 1968. 'Normal derivability in classical logic'. In J. Barwise (ed.), *The syntax and semantics of infinitary languages*. Lecture Notes in Mathematics, 72, Springer, Berlin, 204-236.

Tamura, S. 1974. 'A solution of the decision problem for free pseudo-complemented semilattices'. *J. Fac. Liberal Arts Yamaguchi Univ.*, 8, 235-238.

Univalent Foundations Program, T. 2013. *Homotopy type theory: univalent foundations of mathematics*. Institute for Advanced Study: https://homotopytypetheory.org/book.

Veblen, O. 1908. 'Continuous increasing functions of finite and transfinite ordinals'. *Trans. Amer. Math. Soc.*, 9(3), 280-292. doi:10.2307/1988605.

Wang, H. 1951. 'Review of *Lorenzen 1951*'. *J. Symb. Log.*, 16(4), 269-272.
http://www.jstor.org/stable/2267912.

Wang, H. 1954. 'The formalization of mathematics'. *J. Symb. Log.*, 19(4), 241-266.
http://www.jstor.org/stable/2267732. Reprinted in *A survey of mathematical logic*, North-Holland, Amsterdam, 1963, 559-584.

Whitehead, A. N. and Russell, B. 1925. *Principia mathematica*, vol. I. Cambridge: University Press.

Wille, M. 2013. 'Zwischen Algebra und Erlanger Schule: Paul Lorenzens Beiträge zur Beweistheorie'. *Siegener Beiträge zur Geschichte und Philosophie der Mathematik*, 1, 79-108.
http://nbn-resolving.de/urn:nbn:de:hbz:467-8245.

Wille, M. 2016. 'Verzweigte Typentheorie, relative Konsistenz und Fitch-Beweis: wie Lorenzen (nach eigener Auskunft) Hilberts Forderungen für die Analysis erfüllte'. In *J. Mittelstraß (ed.), Paul Lorenzen und die konstruktive Philosophie*. Münster: mentis, 163-174.
Skolem, Th. 1921. 'Logisch-kombinatorische Untersuchungen über die Erfüllbarkeit oder Beweisbarkeit mathematischer Sätze nebst einem Theoreme über dichte Mengen'. *Skrifter utgit av Videnskapsselskapet i Kristiania 1920, I. Matematisk-naturvidenskabelig Klasse*, 1(4). http://archive.org/details/skrifterutgitavv201chri.

Solovay, R. M. 1966. 'New proof of a theorem of Gaifman and Hales'. *Bulletin of the American Mathematical Society*, **72**, 282–284. doi:10.1090/S0002-9904-1966-11493-3.

Süss, W. (ed.). 1948. *Naturforschung und Medizin in Deutschland 1939–1946, 1: Reine Mathematik, I. (Fiat Review of German Science)*, Wiesbaden: Dieterich'sche Verlags-buchhandlung.

Szabo, M. E. (ed.). 1969. *The Collected Papers of Gerhard Gentzen. (Studies in Logic and the Foundations of Mathematics)*, Amsterdam: North-Holland.

Tait, W. W. 1968. 'Normal derivability in classical logic'. In J. Barwise (ed.), *The Syn-tax and Semantics of Infinitary Languages*. (Lecture Notes in Mathematics, 72), Berlin: Springer, 204–236.

Tamura, S. 1974. 'A solution of the decision problem for free pseudo-complemented semilattices'. *Journal of the Faculty of Liberal Arts, Yamaguchi University*, **8**, 235–238.

The Univalent Foundations Program. 2013. *Homotopy Type Theory: Univalent Foun-dations of Mathematics*. Institute for Advanced Study: https://homotopytypetheory.org/book.

Veblen, O. 1908. 'Continuous increasing functions of finite and transfinite ordinals'. *Transactions of the American Mathematical Society*, **9**, 280–292. doi:10.2307/1988605.

Wang, H. 1951. 'Review of *Lorenzen 1951*'. *The Journal of Symbolic Logic*, **16**, 269–272. http://www.jstor.org/stable/2267912.

Wang, H. 1954. 'The formalization of mathematics'. *The Journal of Symbolic Logic*, **19**, 241–266. http://www.jstor.org/stable/2267732. Reprinted in *A Survey of Mathemat-ical Logic*, Amsterdam: North-Holland, 1963, 559–584.

Whitehead, A. N. and Russell, B. 1925. *Principia Mathematica*, vol. I. Cambridge: University Press.

Wille, M. 2013. 'Zwischen Algebra und Erlanger Schule: Paul Lorenzens Beiträge zur Beweistheorie'. *Siegener Beiträge zur Geschichte und Philosophie der Mathematik*, **1**, 79–108. http://nbn-resolving.de/urn:nbn:de:hbz:467-8245.

Wille, M. 2016. 'Verzweigte Typentheorie, relative Konsistenz und Fitch-Beweis: wie Lorenzen (nach eigener Auskunft) Hilberts Forderungen für die Analysis erfüllte'. In J. Mittelstraß (ed.), *Paul Lorenzen und die konstruktive Philosophie*. Münster: mentis, 163–174.