\documentclass[dvips,german,french,english,twoside]{article}
\usepackage[a5paper,layoutwidth=148mm,layoutheight=7.77817in,
outer=10mm,inner=22bp,tmargin=10mm,bmargin=10mm,footskip=15bp,
]{geometry}
% \documentclass[11pt,german,french,english]{article}
% \usepackage[a4paper,margin=20.5mm]{geometry}
% \usepackage{changepage}

% \setcounter{tocdepth}{9}


\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage{fix-cm}
\usepackage{textcomp}
\usepackage{textgreek}
\newcommand\textb[1]{{\fontseries{b}\selectfont #1}}
\newcommand\sub[2]{\textsl{#2}}
\newcommand\add[1]{\textsl{#1}}
\usepackage{natbib}
\bibpunct (),.{},
\renewcommand{\bibfont}{\small}
\bibliographystyle{myauthordate}
\newcommand\urlprefix{}
\newcommand{\mockalph}[1]{}
\setlength{\bibhang}{\parindent}%
\setlength{\bibsep}{1.5pt plus 1pt}%
\let\bibfont=\small

\makeatletter
\DeclareFontEncoding{LS1}{}{}
\DeclareFontEncoding{LS2}{}{\noaccents@}
\DeclareSymbolFont{stix-letters}       {LS1}{stix}     {m}{it}
\DeclareSymbolFont{stix-arrows1}       {LS1}{stixsf}   {m} {n}
\DeclareSymbolFont{stix-operators}     {LS1}{stix}     {m} {n}
\DeclareSymbolFont{stix-largesymbols}  {LS2}{stixex}   {m} {n}
\DeclareSymbolFont{stix-bold-operators}{LS1}{stix}     {b} {n}
\DeclareFontSubstitution{LS1}{stix}{m}{n}
\DeclareFontSubstitution{LS2}{stix}{m}{n}
\SetSymbolFont{stix-letters}     {bold}{LS1}{stix}     {b}{it}
\SetSymbolFont{stix-arrows1}     {bold}{LS1}{stixsf}   {b} {n}
\SetSymbolFont{stix-operators}   {bold}{LS1}{stix}     {b} {n}
\SetSymbolFont{stix-largesymbols}{bold}{LS2}{stixex}   {b} {n}
% \DeclareSymbolFontAlphabet{\mathbf}  {stix-bold-operators}
% \DeclareSymbolFontAlphabet{\mathsf}  {stix-arrows1}

\def\stix@undefine#1{%
    \if\relax\noexpand#1\let#1=\@undefined\fi}
\def\stix@MathSymbol#1#2#3#4{%
    \stix@undefine#1%
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\stix@MathSymbol{\stixwedge}{\mathbin}  {stix-operators}{"E1} \let\land=\wedge
\stix@MathSymbol{\stixvee}  {\mathbin}  {stix-operators}{"E2} \let\lor=\vee
\def\bigwedgegras{\DOTSI\bigwedgeop\slimits@}
\def\bigveegras{\DOTSI\bigveeop\slimits@}
\stix@MathSymbol{\stixbigwedgeop}{\mathop}{stix-largesymbols}{"B4}
\stix@MathSymbol{\stixbigveeop}  {\mathop}{stix-largesymbols}{"B5}
\stix@MathSymbol{\stixrightarrow}               {\mathrel}{stix-arrows1}{"99}
\stix@MathSymbol{\stixrightleftarrows}          {\mathrel}{stix-arrows1}{"CB}
\makeatother

\renewcommand\land{\mathbin{\boldsymbol{\stixwedge}}}
\renewcommand\lor{\mathbin{\boldsymbol{\stixvee}}}
\newcommand\bigland{\mathop{\textstyle%\boldsymbol
{\stixbigwedgeop}}\nolimits}
\newcommand\biglor{\mathop{\textstyle%\boldsymbol
{\stixbigveeop}}\nolimits}

\newcommand\Srel{\mathrel{S}}

\usepackage{babel} \frenchbsetup{og=«,fg=»}
\newcommand\german[1]{\foreignlanguage{german}{#1}}
\usepackage[french]{varioref}
% \usepackage{siunitx}
% \usepackage{xspace}
\usepackage{enumerate}
\usepackage{graphicx}
\usepackage{pdfpages}
% \usepackage{pst-eucl,pst-poly,pst-plot}\usepackage[off]{auto-pst-pdf}
% \usepackage{tikz}

% \usepackage{wrapfig} \newlength{\wrapsep} \setlength{\wrapsep}{0pt} \RequirePackage{etoolbox} \makeatletter \patchcmd{\WF@putfigmaybe}{intextsep}{wrapsep}{}{} \patchcmd{\WF@putfigmaybe}{intextsep}{wrapsep}{}{} \patchcmd{\putfigmaybe}{intextsep}{wrapsep}{}{} \makeatother

\usepackage{xurl}
\usepackage[normalem]{ulem}

% \usepackage{csquotes}
% \usepackage[isbn=false,doi=false,backref=true,backend=biber,safeinputenc,citestyle=alphabetic,bibstyle=alphabetic]{biblatex}
% \usepackage{biblatex-anonymous}
% \addbibresource{references-href.bib}

\usepackage{refcount}
\usepackage{ebproof}
\usepackage{amsmath}
\usepackage{amsfonts}
\usepackage{amssymb}
\let\su\mathfrak
% \usepackage{upright} % math caps upright
\usepackage{mathtools} \mathtoolsset{mathic} % kerning of math surrounded by italic
\newcommand*\dng[1]{%
  \setbox0\hbox{$\mathaccent"0362{#1}^H$}%
  \setbox2\hbox{$\mathaccent"0362{\kern0pt#1}^H$}%
  \ifdim\ht0=\ht2 \overline{\overline{#1}}\else \bar{\bar#1}\fi
  }


% \usepackage{amsthm-nolist} % ams theorems that are not lists
% \theoremstyle{plain}
% \newtheorem{theorem}{Théorème}[section]
% \theoremstyle{definition}
% \newtheorem{exercise}[theorem]{Exercice}

\usepackage{indentfirst}
% \usepackage{raggsect} % raggedright sections
% \usepackage{quotation} % quotations that are not lists
\usepackage{framed}

\makeatletter
\newcommand{\leqnomode}{\tagsleft@true\let\veqno\@@leqno}
\newcommand{\reqnomode}{\tagsleft@false\let\veqno\@@eqno}
\makeatother

\newcommand\barre[2][]{#1}
\newcommand\bs{} % Bindestrich
\newcommand\nbsp{~}
\newcommand\bsp{\space}
\newcommand\Bs{-} % Bindestrich
\renewcommand\le\leqslant

% \PassOptionsToPackage{urlcolor=black,citecolor=black,anchorcolor=black,linkcolor=black,menucolor=black}{hyperref}%
\PassOptionsToPackage{urlcolor=magenta,citecolor=blue,anchorcolor=blue,linkcolor=blue,menucolor=cyan}{hyperref}%
\usepackage[pdftitle=,pdfauthor=Stefan\ Neuwirth,pdfdisplaydoctitle=true,pdflang=fr-FR,bookmarksopen=false,breaklinks=true,unicode=true,plainpages=false,hyperindex=true,pdfstartview=FitH,colorlinks=true,pdfpagelabels=true,bookmarksnumbered=true]{hyperref}
\ifx\texorpdfstring\undefined\newcommand\texorpdfstring[2]{#1}\fi
\ifx\pdfbookmark\undefined\newcommand\pdfbookmark[3]{}\fi

\usepackage{doi}
\begin{document}%\raggedright\pagestyle{empty}
\title{In 1955, Paul Lorenzen clears the sky in foundations of mathematics for Hermann Weyl}
% \title{Predicative mathematics: from Hermann Weyl to Paul Lorenzen}
\author{Thierry Coquand \and Henri Lombardi \and Stefan Neuwirth}
\date{}
\maketitle%\thispagestyle{empty}

% \tableofcontents

In 1955, Paul Lorenzen is a mathematician who devotes all his research to foundations of mathematics, on a par with Hans Hermes, but his academic background is algebra in the tradition of Helmut Hasse and Wolfgang Krull. This shift from algebra to logic goes along with his discovery that his ``algebraic works [\dots]\ have been concerned with a problem that has \emph{formally} the same structure as the problem of consistency of the classical calculus of logic'' (letter to \german{Carl Friedrich Gethmann} dated 14 January 1988, \citealp[see][page~76]{gethmann91}).

After having provided a proof of consistency for arithmetic in 1944 \citep[see][]{lorenzen20,coquandneuwirth19} and published it in 1951 \citep[see][]{lorenzen51wt,coquandneuwirth23}, Lorenzen inquires still further into the foundations of mathematics and arrives at the conviction that analysis can also be given a predicative foundation.

Wilhelm Ackermann as well as Paul Bernays have pointed out to him in 1947 that his views are very close to those proposed by Hermann Weyl in \emph{Das Kontinuum} (1918): sets are not postulated to exist beforehand; they are being generated in an ongoing process of comprehension.

This seems to be the reason for Lorenzen to get into contact with Weyl, who develops a genuine interest into Lorenzen's operative mathematics and welcomes with great enthusiasm his \emph{Einführung in die operative Logik und Mathematik} (1955), which he studies line by line. This book's aim is to grasp the objects of analysis by means of inductive definitions; the most famous achievement of this enterprise is a generalised inductive formulation of the Cantor-Bendixson theorem that makes it constructive.

This mathematical kinship is brutally interrupted by Weyl's death in 1955; a planned visit by Lorenzen at the Institute for Advanced Study in Princeton takes place only in 1957--1958.

As told by Kuno Lorenz, Lorenzen's first Ph.D. student, a discussion with Alfred Tarski during this visit provokes a turmoil in Lorenzen's operative research program that leads to his abandonment of language levels and to a great simplification of his presentation of analysis by distinguishing only between ``definite'' and ``indefinite'' quantifiers: the former govern domains for which a proof of consistency is available and secures the use of the law of excluded middle; the latter govern those for which there isn't, e.g.\ the real numbers. Lorenzen states in his foreword to \emph{Differential und Integral} (1965) that he is faithful to Weyl's approach of \emph{Das Kontinuum} in this simplification.

This history motivates a number of mathematical and philosophical issues about predicative mathematics: how does Weyl's interest into Lorenzen's operative mathematics fit with his turn to Brouwer's intuitionism as expressed in ``Über die neue Grundlagenkrise der Mathematik'' (\citeyear{weyl21})? Why does Lorenzen turn away from his language levels and how does this turn relate to Weyl's conception of predicative mathematics? What do Lorenzen's conceptions of mathematics reveal about Weyl's conceptions?
\[*\ *\ *\]

We propose a timeline for this history and describe briefly the issues related to it. Unless stated otherwise, the translations are ours. 

\section{1909--1918. \emph{Das Kontinuum}}
\label{sec:das-kontinuum}

The first three items of our timeline emphasise main themes of Weyl's monograph: real numbers and the problem of quantifying over them, the precedence of properties over sets.

\paragraph{1909. The rôle of Poincaré.}

According to Leon \citet[page~55]{chwistek35}, Poincaré's 1909 conferences in Göttingen \citep[see][]{poincare10} played a seminal rôle for Weyl's conception of real numbers in \emph{Das Kontinuum}.
\begin{quotation}
[Henri Poincaré] very positively asserted that real numbers do not form
a determined class and that it is meaningless to speak of all
real numbers. In the spring of 1909 I heard him deliver a
lecture at Göttingen, in which he expressed his point of view
very emphatically although in bad German. The youthful and
brilliant Hermann Weyl, an acknowledged disciple of Hilbert,
was present at this lecture. Undoubtedly it influenced his
conception of real numbers. \cite[pages~78-79.]{chwistek48}
\end{quotation}
% Selon Chwistek (référence?), c'est sous l'influence des conférences de Poincaré à Göttingen que Weyl a conçu le plan d'écrire \emph{Das Kontinuum}.

% \begin{quotation}
%   \selectlanguage{german}
%   \begin{minipage}{1.0\linewidth}\renewcommand\thempfootnote{\fnsymbol{mpfootnote}}\renewcommand*{\dotFFN}{)}
%     \makeatletter\def\@makefnmark{\mbox{\@textsuperscript{\normalfont\@thefnmark}) }}\makeatother
%     Eine Analysis „mit Stufenbildung" ist künstlich und unbrauchbar.
%     Sie verliert ihr eigentliches Erkenntnisobjekt, die Zahl, aus dem Auge
%     (vgl. die Anm. auf S. 21). E s ist klar, daß wir den andern Weg
%     einschlagen müssen — nämlich den Existenzbegriff nur hinsichtlich
%     der Grundkategorien (hier der natürlichen und rationalen Zahlen),
%     nicht aber mit Bezug auf das System der Eigenschaften und Rela-
%     tionen (oder der ihnen korrespondierenden Mengen, reellen Zahlen
%     u. dgl.) anzuwenden haben; mit andern Worten: es ergibt sich als
%     das einzig Natürliche, das engere Iterationsverfahren zu befolgen. Nur
%     dies Verfahren garantiert auch dafür — was mit Rücksicht auf die
%     Anwendungen von entscheidender Bedeutung ist — , daß alle Begriffe
%     und Tatsachen, Größen und Operationen einer solchen „Präzisions-
%     analysis" als Idealisierungen analoger Dinge in einer mit „Ungefähr-
%     Zahlen". operierenden Approximationsmathematik zu fassen sind.
%     Ein Satz wie der oben erwähnte, daß jede beschränkte Menge re-
%     eller Zahlen eine obere Grenze besitzt, muß dann freilich preis-
%     gegeben werden; wir lassen uns durch solche Opfer an dem Wege,
%     den wir eingeschlagen, nicht irre machen.\footnote{%
%       In der Wissenschaft gibt es nur „Gesetze", keine „Gebote". So soll
% denn auch hier nicht etwa „verboten" werden, den Terminus »es gibt« in Ver-
% bindung mit Gegenständen zu gebrauchen, die nicht zu den GrundKategorien
% gehören. Es ist natürlich durchaus möglich (und zulässig), das weitere Verfahren
% zu befolgen; tut man es, so tue man es aber in zirkelfreier Weise!}
%   \end{minipage}
% \end{quotation}

\paragraph{1918. Criticism of sets as basic objects of mathematics.} We cite from \citealt[Chapter~1]{weyl18}, in the translation by \citet{pollardbole87}.

\begin{quotation}
  No one can describe an infinite set other than by indicating
properties\label{pred} which are characteristic of the elements of the set.
And no one can establish a correspondence among infinitely
many things without indicating a rule, i.e., a relation, which
connects the corresponding objects with one another. The
notion that an infinite set is a ``gathering'' brought together by
infinitely many individual arbitrary acts of selection, assembled
and then surveyed as a whole by consciousness, is nonsensical. \citep[page~23.]{weyl87}.
\end{quotation}

\citet{pollard05} investigates how this criticism stems from Weyl's reading of Fichte.

\paragraph{1918. Artificiality of types in analysis.}

\begin{quotation}
[\dots] in the iteration of the mathematical
process \emph{the two principles of closure~\(5\) [``filling in''] and~\(6\) [``there is\dots''] are to be applied only to
blanks which are affiliated with a basic category}.\textsuperscript{24}

\dotfill\smallskip

A ``hierarchical'' version of analysis is artificial and useless.
It loses sight of its proper object, i.e., number (cf.\ note~24).
Clearly, we must take the other path---that is, we must restrict
the existence concept to the basic categories (here, the natural
and rational numbers) and must not apply it in connection with
the system of properties and relations (or the sets, real numbers,
and so on, corresponding to them). In other words, the only
natural strategy is \emph{to abide by the narrower iteration procedure}.
Further, only this procedure guarantees too that all concepts and
results, quantities and operations of such a ``precision analysis''
are to be grasped as idealizations of analogues in a mathematics
of approximation operating with ``round numbers.'' This is of
crucial significance with regard to \emph{applications}. So a proposition
such as the one mentioned above, that every bounded set of real
numbers has a least upper bound, must certainly be abandoned.
But such sacrifices should keep the path ahead clear of
confusion.\textsuperscript{29}

\dotfill\medskip

\noindent\hfil
  \textbf{Notes to Chapter~1}

\dotfill\smallskip

24. The primary significance of the narrower procedure is most clearly
conveyed by the following observation: The objects of the basic categories
remain uninterruptedly the genuine objects of our investigation only when
we comply with the narrower procedure; otherwise, the profusion of
derived properties and relations becomes just as much an object of our
thought as the realm of those primitive objects. In order to reach a decision
about ``finitary'' judgments, i.e., those which are formed under the
restrictions of the narrower procedure, we need only survey these basic
objects; ``transfinitary'' judgments require that one also survey all derived
properties and relations.

\dotfill\smallskip

29. In science there are no ``commandments'', just ``laws''. So here too,
using the term ``there is'' in connection with objects which do not belong
to the basic categories should certainly not be ``forbidden''. It is, of course,
entirely possible (and permissible) to adopt the broader procedure; but if
this is done, let it be done in a non-circular way. % [There is, in fact, no 
%shortage of constructivists who have successfully adopted the ``broader 
%procedure''. Cf. \citet[639-46]{wang70}.-Trans.]
\citep[pages~30, 32, 120; we have slightly amended the translation because we do not endorse the choice made in its note~37.]{weyl87}\end{quotation}
% Commenter/discuter la description de \emph{Das Kontinuum} par Solomon Feferman, en particulier en ce qui concerne le principe d'induction. Est-ce que LPO et Markov sont bien cernés? 


% \subsection{Discussion de Thierry avec PML en mars 2018}
% \label{sec:disc-thierry-avec}

% Dans son esprit, Lorenzen est reste très proche d’Hermann Weyl \emph{Das Kontinuum}
% (c’est le cas pour le livre de 1955??) et il n’a pas vraiment compris  Brouwer 
% (il m’a rappelé le conseil que Kolmogorov lui a donne quand il lui a dit qu’il était 
% intéressé par l’approche constructive: de lire Brouwer, ce que lui a fait, et ce que
% d'après lui, Lorenzen aurait dû faire). 
% Je pense que ce n’est pas vraiment correct, et que certains aspects du travail
% de Lorenzen montrent une compréhension profonde de l’approche constructive.
% En tout cas, la plupart des résultats intéressants de Lorenzen n’ont rien
% à voir avec \emph{Das Kontinuum}.

% \section{\emph{Sur la crise contemporaine des fondements des mathématiques}}
% \label{sec:sur-la-crise}

% Qu'est-ce que Weyl répudie en 1921 par rapport à 1918? Quelles conséquences le tournant vers Brouwer a-t-il?
% Regarder \citealt{weyl27,weyl49,weyl66}.

% \subsection{Réalisabilité de Kleene}
% \label{sec:real-de-kleene}

% La réalisabilité de Kleene correspond à la monnaie de Weyl (la promesse à tenir). C'est repris dans \citet{hilbertbernays34,hilbertbernays39}.

% \section{Hilbert-Bernays}
% \label{sec:hilbert-bernays}

Note that the reedition \citealt{weyl60} has been reviewed by \cite{lorenzen60}. \citet{lorenzen86b}, in one of his last articles, starts with Weyl's \emph{Continuum} for a historical and philosophical discussion of the possibility of theorising the continuum.

\section{1947--1951. Lorenzen discovers Weyl as a predecessor}

The next four items of our timeline describe how Lorenzen's operative mathematics take shape and register Weyl as predecessor.

\paragraph{1947. First mention of Weyl's \emph{Continuum} to Lorenzen by Wilhelm Ackermann.}

% \section{19470521-PL-1-1-117-Ackermann-Lorenzen}
% \label{sec:19470521-pl-1}

Let us cite from a letter by Wilhelm Ackermann to Lorenzen dated 21 May 1947 (\foreignlanguage{german}{Paul-Lorenzen-Nachlass}, \foreignlanguage{german}{Philosophisches Archiv} of \foreignlanguage{german}{Universität Konstanz}, PL 1-1-117), whose subject is Lorenzen's manuscript ``Zur Neubegründung der Mathematik [On the new grounding of mathematics]'' (Hs.~974:155; also, with an introduction, in the Gottfried-Köthe-Nachlass at \foreignlanguage{german}{Universitätsarchiv Göttingen}, Cod.\ Ms.\ G.~Köthe M~10), in which he introduces his idea of language levels (see page~\pageref{levels}) as a ``calculus of regions''; we translate ``Kalkül'' by (logical) ``calculus'', whereas \citet[page~3]{lorenzen55} proposes the translation ``formal system''. 

% \hfill Burgsteinfurt, 21.5.47

% \hfil Dear Mr.\ Lorenzen!\smallskip

\begin{quotation}
  [\dots] With regard first to the setup of your calculus of regions in general, which I can pretty much imagine according to your indications, I wish to encourage you to carry it out in detail as soon as possible. I also hold the view that a setup of mathematics free from contradiction (i.e.\ verifiably free from contradiction) must lie in the direction indicated by you or in a similar one, and the more so that I arrive at similar conceptions in my attempts to set up mathematics out of a type-free system of axioms that is verifiably free from contradiction. I do not believe any more that one may achieve a proof of freedom from contradiction for classical analysis.

  I am not as optimistic as you on the question whether the differences of such a setup with respect to classical analysis be merely irrelevant. It seems to me to the contrary that such a setup would not move that far away from that of Weyl (before he joined entirely the intuitionists). Consider first the theorem on the supremum of a bounded set of real numbers. It is clear to me that the theorem may be proved in the following form: every bounded set of real numbers over the \(n\)-th region admits a real number of the \(n+1\)-st region as supremum. But we are no longer talking about a real number per se and the set of real numbers seems to dissolve into sets of real numbers over the different regions. The same holds for the mean value theorem of continuous functions. You say at this point: the mean value theorem can be brought into the classical form if we form the union of all regions and define a real function as a definite sequence~\(f\), for which \(f_n\)~is a real function of the \(n\)-th~region such that \(f_{n+1}\)~is an extension of~\(f_n\). What do you mean here by the union of all regions? Do you mean the union of all finite regions? Then the defined real function belongs in my opinion to the region~\(\omega\). Or should one understand that you wish the regions to be extendable indefinitely upwards, and then form the union of all regions, i.e.\ with arbitrary ordinal? In this case you would not move inside the domain of a calculus verifiably free from contradiction. For the calculus of regions should be grounded in the freedom from contradiction of classical arithmetic. But there is no proof of freedom from contradiction of classical arithmetic per se. Namely, one may always state purely number-theoretic deductions that are not captured any more by a proof of freedom from contradiction at hand.\footnote{\selectlanguage{german}Was nun zunächst den Auf\bs
    bau Ihres Regionenkalküls im allgemeinen anbetrifft, von dem
    ich nach dem, was Sie schreiben, mir so ziemlich eine Vorstel\bs
    lung machen kann, so möchte ich Ihnen möglichst zureden, die\bs
    sen nun möglichst bald im einzelnen auszuführen. Ich bin auch der
    Ansicht, dass ein widerspruchsfreier (d.\ h.\ nachweislich wider\bs
    spruchsfreier) Aufbau der Mathematik in der von Ihnen angegebenen
    oder in ähnlicher Richtung liegen muss, und bin das um so mehr, 
    als ich bei meinen Versuchen, aus einem nachweislich wider\bs
    spruchsfreien typenfreien logischen Axiomensystem die Mathe\bs
    matik aufzubauen, auf ähnliche Begriffsbildungen komme. Dass
    sich ein Widerspruchsfreiheitsbeweis für die klassische Analysis 
    erzielen lässt, daran glaube ich nicht mehr.

    Nicht ganz so optimistisch wie Sie bin ich in der
    Frage, ob die Unterschiede eines derartigen Aufbaus gegen\bs
    über der klassischen Analysis nur unerheblich seien. Im Gegen\bs
    teil scheint es mir, dass ein derartiger Aufbau sich doch nicht
    so weit von dem von Weyl (bevor er sich ganz den Intuitionisten 
    anschloss) entfernt. Da wäre zunächst der Satz über die obere
    Grenze einer beschränkten Menge von reellen Zahlen. Es ist mir
    ohne weiteres klar, dass sich der Satz in der folgenden Form 
    beweisen lässt: Zu jeder beschränkten Menge von reellen Zahlen
    über der $n$-ten Region gibt es eine reelle Zahl der $n+1$-ten Region
    als obere Grenze. Aber von einer reellen Zahl schlechthin ist 
    dann doch keine Rede mehr, sondern die Menge von reellen Zah\bs
    len erscheint ein für allemal aufgelöst in Mengen von reellen
    Zahlen über den verschiedenen Regionen. Das gleiche gilt für
    den Zwischenwertsatz der stetigen Funktionen. Sie sagen an der
    Stelle: Der Zwischenwertsatz kann auch auf die klassische Form 
    gebracht werden, wenn wir die Vereinigung aller Regionen bilden
    und als reelle Funktion eine definite Folge~$f$ definieren, für
    die $f_n$~eine reelle Funktion der $n$-ten Region ist, sodass $f_{n+1}$ %[2]
    eine Fortsetzung von~$f_n$ ist. Was meinen Sie hierbei mit der 
    Vereinigung aller Regionen? Meinen Sie die Vereinigung aller 
    endlichen Regionen? Dann gehört meiner Ansicht nach die de\bs
    finierte reelle Funktion der Region~$\omega$ an. Oder ist das so
    zu verstehen, dass Sie die Regionen nach oben unbegrenzt er\bs
    weiterungsfähig lassen möchten, und nun die Vereinigung aller 
    Regionen, d.\ h.\ solcher mit beliebiger Ordnungszahl bilden wol\bs
    len. In diesem Falle würden Sie sich nicht mehr in dem Bereiche 
    eines nachweislich widerspruchsfreien Kalküls bewegen. Denn
    der Regionenkalkül soll sich ja auf die Widerspruchsfreiheit
    der klassischen Arithmetik gründen. Es gibt aber nun keinen
    Widerspruchsfreiheitsbeweis für die klassische Arithmetik 
    schlechthin\barre{, ebenso wenig wie es ein Axiomensystem für die
      klassische Arithmetik schlechthin gibt}. Es lassen sich näm\bs
    lich immer rein zahlentheoretische Schlüsse angeben, die durch
    einen vorliegenden Widerspruchsfreiheitsbeweis nicht mehr er\bs
    fasst werden.}
\end{quotation}

\paragraph{1947. Second mention of Weyl's \emph{Continuum} to Lorenzen by Paul Bernays.}

Let us cite from a letter by Paul Bernays to Lorenzen dated  1 September 1947 (PL 1-1-112; a carbon copy lies in ETH-Bibliothek, Hochschularchiv, Hs.~975:2955).

\begin{quotation}
  Concerning the narrower calculus of types, it certainly has something principled to itself. But for the actual mathematical usage, it is yet quite unwieldy; and one will generally try to get along without a calculus of types. A formalism roughly equivalent to the narrower (ramified) type calculus was put up by Hermann Weyl in his writing ``Das Kontinuum''. I would think that the method of your proof of freedom from contradiction might be carried over to a formalism of about this kind.\footnote{\selectlanguage{german}Was den engeren Stufenkalkul anbelangt, so hat dieser ge\bs
wiss manches Prinzipielle für sich. Für den faktischen mathemati\bs
schen Gebrauch ist er aber doch wohl recht schwerfällig; und man
wird wohl überhaupt versuchen, ohne einen Stufenkalkul auszukom\bs
men. Ein dem engeren (verzweigten) Stufenkalkul ungefähr äquiva\bs
lenter Formalismus ist ja von Hermann Weyl in seiner Schrift
``Das Kontinuum'' aufgestellt worden. Ich möchte denken, dass auf ei\bs
nen Formalismus etwa dieser Art die Methode Ihres Wf.-Beweises
sich übertragen lassen sollte.}
\end{quotation}

% \hfill%
% \begin{tabular}{@{}l@{}}%
% Zürich~2, 1.9.\ 1947.\\%
% Bodmerstrasse~11.%
% \end{tabular}

% \hfil Sehr geehrter Herr Dr.\ Lorenzen!\hfil

% \dotfill

% Ob es möglich ist, in der Beweistheorie ohne anschauliche
% Evidenz auszukommen, erscheint mir als sehr fraglich. Wenn man Kon\bs
% struktionen ausführt, so bedarf es doch immer noch gewisser Ein\bs
% sichten, um aus diesen ein Ergebnis von allgemeinem Charakter zu
% gewinnen, wie es doch insbesondere jede Feststellung von
% Widerspruchsfreiheit einer formalen Theorie ist.

% Was den engeren Stufenkalkul anbelangt, so hat dieser ge\bs
% wiss manches Prinzipielle für sich. Für den faktischen mathemati\bs
% schen Gebrauch ist er aber doch wohl recht schwerfällig; und man
% wird wohl überhaupt versuchen, ohne einen Stufenkalkul auszukom\bs
% men. Ein dem engeren (verzweigten) Stufenkalkul ungefähr äquiva\bs
% lenter Formalismus ist ja von Hermann Weyl in seiner Schrift
% "`Das Kontinuum"' aufgestellt worden. Ich möchte denken, dass auf ei\bs
% nen Formalismus etwa dieser Art die Methode Ihres Wf.-Beweises
% sich übertragen lassen sollte.

% \dotfill

% \hfil Ihr

% \hfill P. Bernays

\paragraph{1948. First inscription by Lorenzen of himself into the tradition of Weyl's \emph{Continuum}.}

% \section{19480815-2961-Lorenzen-Bernays}
% \label{sec:19480815-2961-lorenz}

In his letter to Bernays dated 15 August 1948 (Hs.~975:2961), Lorenzen writes about his enclosed manuscript ``Ein `trivialer' Widerspruchsfreiheitsbeweis für die Arithmetik [A `trivial' proof of freedom from contradiction for arithmetic]''  (Hs.~974:148) and concludes as follows.

\begin{quotation}
  % [Hs.975:2961]

  % Dr.\ Paul Lorenzen\hfill\vtop{\hbox{Bonn, den 15.8.48}%
  %   \hbox{Luisenstr.~3}}

  % Sehr verehrter Herr Professor,

  % Ganz unerwartet --~und wie zum Trost dafür, dass die
  % Reise nach Amsterdam an den politischen Unzulänglichkeiten
  % scheiterte~-- kam ein wunderschönes Paket von Ihnen hier an.
  % Meine Frau ist erfreulicherweise seit einiger Zeit wieder
  % auf, nachdem sie 4~Monate nach der Operation gelegen hatte.
  % Die herrlichen Dinge Ihres Paketes helfen uns jetzt sehr gut,
  % denn, obwohl jetzt einiges zu kaufen wäre, haben wir ja kein
  % Geld mehr dafür.

  % Es ist mir sehr schmerzlich, dass ich Sie nicht auf dem
  % Kongress sprechen konnte, ich hätte Ihnen gerne den beilie\bs
  % genden Wf-Beweis vorgelegt. Die Regeln, die ich in meiner
  % Einführung schrittweise als verträgliche Regeln hinzugenommen
  % hatte, nenne ich jetzt "`Postulate"', und die erlaubten Regeln
  % jetzt "`Axiome"'. Die Erlaubtheit der Axiome könnte selbstver\bs
  % ständlich in jedem Falle bewiesen werden durch Formel- oder
  % Satzinduktionen über das System von Postulaten, ähnlich wie
  % in meinem verbandstheoretischen Wf-Beweis. Für die hier ge\bs
  % brauchten Axiome scheint mir aber dieser Beweis kaum die Mühe
  % zu lohnen, da die Erlaubtheit, jedem, der mit Kalkülen um\bs
  % zugehen gewohnt ist, sofort vertraut ist. Auf diese Weise ent\bs
  % steht ein konstruktiver Aufbau einer intuitionistischen Logik,
  % der gegen die üblichen Einwände völlig immun ist, da die Be\bs
  % gründung ja keine "`inhaltliche Deutung"' im üblichen Sinne ist. [2]
  % Zur Erläuterung von Satz~4 des Beweises, möchte ich noch hin\bs
  % zufügen, dass hier mit "`beweisbar"' diejenigen Regeln ge\bs
  % meint sind, die sich aus den Postulaten und Axiomen formal
  % ableiten lassen mit Hilfe von\leqnomode
  % \begin{gather*}%
  %   \su c\Rightarrow\curlyvee\quad,\quad\su c\Rightarrow\su c\quad,\quad\curlywedge\Rightarrow\su c\\%
  %   \tag*{und}{\begin{prooftree}\hypo{\su a\Rightarrow\su b}\hypo{\su b\Rightarrow\su c}\infer2{\su a\Rightarrow\su c}\end{prooftree}}%
  % \end{gather*}%
  I hope that in this form the question of freedom from contradiction, that in my opinion has disquieted mathematics long enough, has found a satisfactory answer. Here one has now firm ground for building up a constructive analysis (e.g.\ in the sense of Weyl), and then one will be able to examine also the axiomatic analysis as of its usability.\footnote{\selectlanguage{german}Ich hoffe, dass in dieser Form die Frage der Wf., die
  m.\ E.\ lange genug die Mathematik beunruhigt hat, eine befrie\bs
  digende Lösung gefunden hat. Hier hat man jetzt festen Boden,
  um eine konstruktive Analysis (z.\ B.\ im Sinne von Weyl) auf\bs
  zubauen, und dann wird man in aller Ruhe auch die axiomatische
  Analysis auf ihre Brauchbarkeit untersuchen können.}

  % Mit den ergebensten Grüßen und sehr herzlichem Dank

  % \hfil Ihr

  % \hfil\hfil Paul Lorenzen.
\end{quotation}
% \section{Lorenzen 1950}
% \label{sec:lorenzen-1950}


\paragraph{1950. Lorenzen's relaunch of Weyl's approach.}

In his article ``Konstruktive Begründung der Mathematik'', \citet{lorenzen50} formulates his relaunch of Weyl's approach of 1918. We translate ``Begründung'' by ``justification'', but the word equally means ``foundation'', and ``establishment'' might be a good compromise; John Bacon uses the translation ``grounding'' in \citealt{MR0346097} (see the citation on page~\pageref{grounding}).

\begin{quotation}
  As most suggestive direction for further work results herefrom: first to develop in detail what has been summarised here under the name ``constructive set theory''. To the contrary of the intuitionistic attempts, one may use now throughout---after justifying logic unobjectionably---the excluded middle. The so uncomfortable restriction to ``decidable properties'', ``computable real numbers'', etc.\ is not necessary anymore. An approach in the direction intended here has been made by H. Weyl already in 1918---it had to fail because the justification of the excluded middle was still missing at that time.

  It is of course understood that the consolidation of a constructive analysis is of interest also independently of the goal of proving the usability of the traditional axiomatisations. New possibilities open up, e.g.\ for computing formally with infinite processes, independently of the concept of real number and convergence.

  The exploitation of such possibilities as the transfinite iteration for the process of set formation yields perhaps enough comfortable calculi to make the contemporary axiomatisations simply dispensable. (Pages~165--166.)
  % Obwohl es also gerechtfertigt wäre, axiomatische Mengenlehren,
  % für die kein konstruktives Modell vorhanden ist, einfach als mißglückte
  % Versuche in Zukunft beiseite zu lassen, besteht aber auch die andere
  % Möglichkeit, zu untersuchen, ob sich solche Axiomatisierungen -- nach\bs
  % dem sie einmal da sind und wir uns daran gewöhnt haben — nicht
  % doch auf irgend einem Umweg als kalkulatorisch zweckmäßige Fik\bs
  % tionen für die konstruktive Mathematik verwenden lassen. Mit der
  % bloßen Widerspruchsfreiheit der axiomatischen Mengenlehre wäre aller\bs
  % dings kaum etwas gewonnen, es Kommt darauf an, den Zusammenhang
  % mit der konstruktiven Mengenlehre herzustellen. Als naheliegendste.
  % Richtung zur Weiterarbeit ergibt sich hieraus: zunächst das, was hier
  % unter dem Namen „konstruktive Mengenlehre“ zusammengefaßt wurde,
  % ausführlich zu entwickeln. Im Gegensatz zu den intuitionistischen
  % Versuchen darf dabei jetzt — nach einwandfreier Begründung der
  % Logik — das tertium non datur stets benutzt werden. Die so unbe\bs
  % queme Beschränkung auf „entscheidbare Eigenschaften“, „berechen\bs
  % bare reelle Zahlen“ usw. ist nicht mehr erforderlich. Einen Ansatz in
  % der hier gemeinten Richtung hat H. Weyl schon 1918 gemacht —
  % dieser mußte allerdings scheitern, da die Begründung des tertium non
  % datur damals noch fehlte.

  % Der Ausbau einer konstruktiven Analysis ist hierbei selbstver\bs
  % ständlich auch unabhängig von dem Ziel, die Brauchbarkeit der tradi\bs
  % tionellen Axiomatisierungen zu beweisen, von Interesse. Es eröffnen
  % sich neue Möglichkeiten, etwa für das formale Rechnen mit unend\bs
  % lichen Prozessen, unabhängig vom Begriff der reellen Zahl und der
  % Konvergenz.

  % Durch die Ausnutzung solcher Möglichkeiten wie der transfiniten
  % Iteration für den Prozeß der Mengenbildung ergeben sich vielleicht
  % auch genügend bequeme Kalküle, daß die gegenwärtigen Axiomati\bs
  % sierungen einfach überflüssig werden.

  % Die vorliegende Arbeit beschränkt sich jedoch darauf, den Aufbau
  % der Mathematik nur bis zur Arithmetik lückenlos durchzuführen.
\end{quotation}

The very day he submits this article, 13 February 1950, he writes the following in a letter to Ackermann.
\begin{quotation}
  It seems thus more sensible to investigate the possibility of constructive set theories mindless of ``axioms''---instead of making random guesses among possible axioms with so-called plausibility considerations. The logic of ramified types (without reducibility) and Weyl's analysis are after all just the first attempts---if the distinction of types is dropped and only the ``ramification'' is retained (I call this then ``levels'')---then one obtains a further possibility which, as far as I see, leads to an analysis that practically does not differ from the non-formalised so-called naive analysis, as it is for instance common in lectures today. \citep[page~196.]{ackermann83}
\end{quotation}

In the follow-up article, submitted five months later, ``\german{Die Widerspruchsfreiheit der klassischen Analysis}'', Lorenzen emphasises as follows.

\begin{quotation}
  The problem of constructing real numbers has to my knowledge first been
  solved by H. Weyl (\emph{Das Kontinuum}, 1918). Admittedly, Weyl uses the arithmetic and logical rules without justification, in particular also the excluded middle. As a result of Brouwer's criticism, the intuitionistic analysis has then emerged, in which the fundamental theorems of classical analysis do not hold any more by the ban of the excluded middle and the restriction to a very narrow concept of function.

  Yet, after a constructive justification\textsuperscript{1} of arithmetic and logic (incl.\ excluded middle), a construction of real numbers may also be carried out, for which all fundamental theorems of classical analysis hold. The freedom from contradiction of classical analysis is contained therein. \citep[page~1.]{MR0043748}

  \vspace*{2.6pt}\noindent\hbox{\vbox{\footnoterule}}\vspace*{-5.6pt}

  \noindent{\footnotesize\rule{0pt}{\footnotesep}\textsuperscript{1} Cf. \citealt{lorenzen50}.}
% Die Aufgabe einer Konstruktion von reellen Zahlen ist m. W. erst\bs
% malig von H. Weyl (Das Kontinuum, 1918) gelöst worden. Wey be\bs
% nutzt allerdings die arithmetischen und logischen Regeln ohne Be\bs
% gründung, insbesondere auch das tertium non datur. Aufgrund der
% Brouwer’schen Kritik an dieser Regel ist dann die intuitionistische
% Analysis entstanden, in der durch das Verbot des tertium non datur
% und die Beschränkung auf einen sehr engen Funktionsbegriff die
% Fundamentalsätze der klassischen Analysis nicht mehr gelten.

% Nach einer konstruktiven Begründung!) von Arithmetik und Logik
% (einschl.\ tertium non datur) läßt sich jedoch auch eine Konstruktion
% von reellen Zahlen durchführen, für die alle Fundamentalsätze der
% klassischen Analysis gelten. Darin ist die Widerspruchsfreiheit
% der klassischen Analysis enthalten.
\end{quotation}
% \section{Lorenzen 1951}
% \label{sec:lorenzen-1951}

He proceeds by explaining the process of levels\label{levels} of language and concludes.
\begin{quotation}
  Yet one does not obtain the classical analysis with the language over the rational numbers, for---if one defines the real numbers by an equality relation between sets of rational numbers (cf.\ §~2)---then no sets and functions of real numbers (but only those of rational numbers) are defined. To this end the construction of a language must be repeated: first the language over the previous statements, sets, functions, and real numbers (individuals of the 1st~level), then again a language over the thus obtained individuals of the 2nd~level, etc. (These levels must not be mistaken for the types of the naive and axiomatic set theory.)

  We call the union of all levels of finite height the 0th hyperlevel. The construction of a language over this one yields further hyperlevels whose individuals we call hyperstatements, hypersets, hyperfunctions, and hyperreal numbers. However, if one restricts to levels, then the classical completeness principle:
\[\text%\parbox{\linewidth}%
  {``Each set of real numbers admits a real number as infimum''}
\]
becomes provable, although there are hypersets whose infimum is a hyperreal number. In §§~3--6 we obtain by an appropriate exclusion of hyperlevels all fundamental theorems of classical analysis (cf.\ for instance \german{Haupt--Aumann, \emph{Differential- und Integralrechnung~I}}). It\label{lines} is thus not the constructive analysis which is ``too narrow'' with regard to classical analysis: the closedness featured by classical analysis arises just by a restriction of the construction means. \citep[page~3.]{MR0043748}
  
% Mit der Sprache über die rationalen Zahlen erhält man jedoch noch
% nicht die klassische Analysis, denn -- definiert man die reellen Zahlen
% durch eine Gleichheitsrelation zwischen Mengen von rationalen Zahlen
% (vgl. §~2) -- so sind noch keine Mengen und Funktionen von reellen
% Zahlen (sondern nur solche von rationalen Zahlen) definiert. Dazu
% muß die Konstruktion einer Sprache wiederholt werden: zunächst die
% Sprache über die bisherigen Aussagen, Mengen, Funktionen und re\bs
% ellen Zahlen (Individuen der 1. Schicht), dann wieder eine Sprache
% über die so erhaltenen Individuen der 2. Schicht usw. (Diese Schichten
% sind nicht mit den Stufen der naiven und axiomatischen Mengenlehre
% zu verwechseln.)

% Die Vereinigung aller Schichten endlicher Höhe nennen wir die
% 0-te Hyperschicht. Die Konstruktion einer Sprache hierüber liefert
% weitere Hyperschichten, deren Individuen wir Hyperaussagen, Hyper\bs
% mengen, Hyperfunktionen und hyperreelle Zahlen nennen. Beschränkt
% man sich jedoch auf Schichten, so wird das klassische Vollständigkeits\bs 
% prinzip:
% \[\parbox{\linewidth}{%
%     „Zu jeder Menge von reellen Zahlen gibt es eine reelle Zahl
%     als untere Grenze“%
% }\]
% beweisbar, obwohl es Hypermengen gibt, deren untere Grenze eine
% hyperreelle Zahl ist. Durch geeignete Ausschließung der Hyperschichten
% erhalten wir in 88 3—6 alle Fundamentalsätze der klassischen Ana\bs
% lysis, wie sie in den modernen Lehrbüchern benutzt werden (vgl. etwa
% Haupt-Aumann, Differential- u. Integralrechnung I). Es ist demnach
% nicht die konstruktive Analysis, die gegenüber der klassischen Ana\bs
% lysis ``zu eng'' ist, sondern die Abgeschlossenheit, die die klassische
% Analysis besitzt, entsteht gerade durch eine Beschränkung der Kon\bs
% struktionsmittel.
\end{quotation}

\section{1955. Reception of Lorenzen's work by Weyl}

The next two items of our timeline tell how Weyl gets acquainted with Lorenzen.

In \citeyear{lorenzen55}, \citeauthor{lorenzen55} publishes his book \emph{Einführung in die operative Logik und Mathematik} that contains a comprehensive presentation of operational mathematics as a new foundation for mathematics. The term ``operational'' has been devised to indicate that the essential point is ``the operating according to rules'' \citep[page~4]{lorenzen55}; the alternative translation ``operative'' supersedes it only at a later point.

The reviews of the book are mostly positive or even enthusiastic (\citealp{kaminski55,robinson56,heinemann56,aubert56,becker57,frey57,skolem57,weizsaecker57}, \citealp[Chapter~III, §~7]{fraenkelbarhillel58}, \citealp{meigne70,heitsch71,demuth72,gardies72}); \citet{craig57} notes ``major though probably corrigible errors''; \citet{stegmueller58} wishes for ``a clear demarcation of the principles that are declared admissible for the reasonings in terms of content (the metatheoretical reasonings)'' and ``an elucidation of the strange, frequently encountered interlacing of object-linguistic and metalinguistic operations'';  the very detailed criticism and scepticism of \citet{mueller57} in the \emph{Zentralblatt} is puzzling because the preface of \citealt{lorenzen55} acknowledges his ``many good advices at the drafting of the manuscript and at the revisions'' (compare also \citealp{mueller57c}); four years later, this journal publishes another review by \citet{gericke61} that vindicates Lorenzen's book: ``an act of will is required not to measure the author's lines of thought by standards that are derived from other foundations. This difficulty can easily become the source of misconceptions''.


The theory proposed in \citealt{wang54} is ``essentially equivalent to the body of methods which Lorenzen
admits and applies'' \citep[page~78]{wang55}.

\paragraph{1955. ``Nachtrag Juni 1955'' to \citealt{weyl21}.}
\label{sec:nachtrag-}

In June 1955, \citeauthor{weyl56} writes an addendum to the inclusion of ``Über die neue Grundlagenkrise der Mathematik'' into his \emph{Selecta} (\citeyear{weyl56b}), in which he presents \citealt{lorenzen55} as ``most viable way out of the difficulties'' raised by the foundation of mathematics. 
% \begin{quotation}
%   Heute will mir scheinen,
%   dass die ``operative'' Einstellung von \textsc{Paul Lorenzen} den gangbarsten Weg
%   aus den Schwierigkeiten eröffnet; vgl.\ sein kürzlich erschienenes Buch \emph{Einführung in die operative Logik und Mathematik} (Springer-Verlag 1955). Die
%   Operationen des formalen Kalküls sind hier in fruchtbarer und zwangloser
%   Weise verflochten mit inhaltlichen Überlegungen über deren Produkte; die
%   \textsc{Gödel}sche Entdeckung verliert dadurch alles Beunruhigende.
% \end{quotation}
It is translated in \citealt[page~12]{heinzmann21}.

Weyl's lines have impressed in particular Ignacio Angelelli. He reminds them as follows in his reviews of translations of \emph{Das Kontinuum} and of an article about it.
\begin{quotation}
  Readers who are interested in the philosophy of mathematics should take into account Weyl's later remarks on Paul Lorenzen's work as representing the best furtherance of his program (gangbarster Weg) \citep{angelelli91}.

  One misses any reference [\dots] to Paul Lorenzen, whose work was celebrated by Weyl in the mid 1950's as ``the most feasible approach to his program'' \citep{angelelli97,angelelli98}.
\end{quotation}
Note that Angelelli, a student of Józef Bocheński, spent the year 1965-1966 at the university of Erlangen for a Humboldt postdoctoral fellowship under the direction of Lorenzen \citep[see][]{legris20}.

\paragraph{1955. Weyl's letter to Lorenzen.}\label{sec:la-lettre-de}

The whole known correspondence between Lorenzen and Weyl lies in the \foreignlanguage{german}{Paul-Lorenzen-Nachlass} (PL 1-1-2).

Transcriptions of Weyl's letter dated 23 September 1955 and translated below lie in the  Helmut-Hasse-Nachlass (Cod.\ Ms.\ H. Hasse 1:1529, Beil.~16), in the Gottfried-Köthe-Nachlass (Cod.\ Ms.\ G. Köthe A~358, Beil.), and in the Josef-König-Nachlass (Cod.\ Ms.\ J. König 186) at \foreignlanguage{german}{Universitätsarchiv Göttingen} and show that Lorenzen communicated about it to his teachers: Hasse was his Ph.D.\ advisor; Köthe introduced him to lattice theory and was ready to replace Wolfgang Krull as his habilitation advisor \citep[see][page~241, note~50]{neuwirth21c}; König was his teacher of philosophy in Göttingen.

This letter has been presented before in \citealt{thiel00} and subsequently (in excerpts) in \citealt{schlaudt14}.

% \includepdf[trim=0 300 0 0,pagecommand={}]{../../lorenzenprojekt/Briefwechsel/Lorenzen-Weyl/19550923-Cod-Ms-G-Koethe-A-358-Weyl-Lorenzen.pdf}

% L -> W 19480204
% W -> L 19480425
% L -> W 19480503
% L -> W 19480705
% W -> L 19510518
% W -> L 19550918
% W -> L 19550923
% W -> L 19550928

% PL 1-1-1 enthält masch. Abschriften dreier Briefe von Hermann Weyl, die in PL 1-1-2 im Original vorliegen sowie einen Originalumschlag mit Poststempel vom 23.9.1955. PF 1-1-2 enthält einen kurzen masch. Brief von Weyl vom 18.5.1951, einen masch. Brief vom 18.9.1955, einen hs. Brief vom 23.9.1955, einen hs. ergänzten masch. Brief vom 28.9.1955, einen masch. Brief vom 25.4.1948 und Durchschläge von masch. Briefen von Lorenzen an Weyl, vom 5.7.1948, vom 4.2.1948 und vom 3.5.1948. 

% Bei PL 1-1-50 handelt es sich um einen masch. Brief vom 31.7.1974 von Michael Weyl.

\begin{quotation}
  \noindent Hermann Weyl, Zürich\hfill 23 September 1955\nopagebreak%\medskip

  \noindent\hfil Dear Mr. Lorenzen,\nopagebreak\medskip

  Your letter dated 17.9.\ must have crossed mine dated 18.9. In the meantime I have concerned myself in depth with your book and \emph{am most profoundly impressed by it}. Your ``operative'' standpoint actually seems to combine in the most natural and fortunate way formal construction inside the calculus with considerations in terms of content that lead to the insight of derivability, admissibility, etc. It is actually very simple, but yet surprising, how the possibility of inversion thus turns up! And you are able to circumnavigate the cliff of the excluded middle by means of Kolmogorov's and Heyting's thought of reinterpreting \(p \lor q\) into \(\dng{p \lor q}\). I naturally cannot peruse a book as yours at one go. But whenever I was returning to the book after cogitating your treatment of my own, I was enchanted how carefully and precisely you formulate everything. When I think in what restricted form I have afforded the construction of relations in my little book of 1918 (by the principle of substitution and iteration), I cannot help being surprised by the free way in which you handle the inductive definition of relations~(\(\mathsf{I}_\varrho\)). I have not yet coped with this, but neither do I see what one could object against this broad-mindedness. I have noticed all the same that you yourself have found it good with regard your first account in 1951 to restrict the induction schemes through the requirement ``founded'' and ``separated'' (for the sake of definiteness). I do not remember today anymore precisely why I shied away from the iteration of the ``mathematical process'' in 1918, for you it is essential to iterate, even up to a limit ordinal.

  In spite of the so much further stretched frame, I naturally recognise the methodical kinship of your treatment for the justification of analysis with my much more limited approach of 1918---and am pleased by it! At the time, my belief into the truth of the excluded middle in terms of content was still unimpaired in the domain of the natural numbers. Brouwer had to come to free us from it, and in this respect you are also liable to Brouwer. Ultimately also to Hilbert: he emphasised the formalism of the calculus, his program of a proof of freedom from contradiction was perspicuous and promising in its first stages, one had first to experience the difficulties that show that this attack is as good as hopeless before one was ready to go other ways---\emph{your} way.

  I feel that I see at last again a clear sky after long years of resignation. I am happy that I have lived to see this. Please accept once again my warmest congratulations for the work done by you!---You hand this book over to me as present for my (soon due) 70th birthday. It has already arrived this morning. I believe that one could not have made me a finer present. I wholeheartedly thank you for this!\strut

  \hfil\hfil\begin{tabular}{c}
    With best greetings and wishes\\
    your\\
    Hermann Weyl\footnotemark
  \end{tabular}
\footnotetext{\selectlanguage{german}\noindent Hermann Weyl, Zürich\hfill 23.\ September 1955\nopagebreak%\medskip

    \noindent\hfil Lieber Herr Lorenzen,\nopagebreak\medskip

    Ihr Brief vom 17.9. muss sich mit dem meinigen vom 18.9.\ gekreuzt haben.
    In der Zwischenzeit habe ich mich eingehend mit Ihrem Buch beschäftigt und
    \emph{bin aufs tiefste davon beeindruckt}. Ihr ``operativer'' Standpunkt scheint wirk\bs
    lich auf die natürlichste und glücklichste Weise formale Konstruktion inner\bs
    halb des Kalküls mit inhaltlichen Überlegungen, die zur Einsicht in Ableit\bs
    barkeit, Zulässigkeit etc.\ führen zu kombinieren. Es ist ja wirklich sehr
    simpel, aber doch überraschend, wie sich so die Möglichkeit der Inversion
    herausstellt! Und die Klippe des tertium non datur können Sie mittels des
    Kolmogoroff-Heyting'schen Gedankens der Umdeutung von \(p \lor q\) in \(\dng{p \lor q}\) um\bs
    schiffen. Ich kann natürlich ein Buch wie das Ihre nicht auf einen Rutsch
    durchlesen. Aber immer, wenn ich nach eigenem Nachdenken über Ihr Verfahren
    zu dem Buch zurückkehrte, fand ich mich entzückt davon, wie sorgfältig und
    präzis Sie alles formulieren. Wenn ich daran denke, in wie eingeschränkter
    Form ich mir in meinem Büchlein von 1918 die Konstruktion von Relationen er\bs
    laubt hatte (durch das Substitutions- und Iterations-Prinzip), so kann ich
    nicht anders, als erstaunt sein über die freie Weise, in der Sie die induktive
    Definition von Relationen (\(\mathsf{I}_\varrho\)) handhaben. Das habe ich noch nicht ganz be\bs
    wältigt, aber ich sehe auch nicht, was man gegen diese Weitherzigkeit ein\bs
    wenden könnte! Immerhin bemerkte ich, dass Sie selbst es für gut fanden,
    gegenüber Ihrer ersten Darstellung 1951, die Induktionsschemata durch die For\bs
    derung ``fundiert'' und ``separiert'' einzuschränken (um der Definitheit willen).
    Ich erinnere mich heute nicht mehr genau, warum ich 1918 vor der Iteration
    des ``mathematischen Prozesses'' zurückschreckte, für Sie ist es wesentlich zu
    iterieren, sogar bis zu einer Limeszahl.

    Trotz des so viel weiter gespannten Rahmens erkenne ich natürlich die
    methodische Verwandtschaft Ihres Verfahrens zur Begründung der Analysis mit
    meinem viel limitierteren Ansatz von 1918 -- und bin erfreut darüber! Damals
    war bei mir noch der Glaube an die inhaltliche Wahrheit des tertium non datur
    im Gebiete der natürlichen Zahlen unerschüttert gewesen. Brouwer musste kom\bs
    men, uns davon zu befreien, und insofern sind Sie auch Brouwer verpflichtet.
    Schließlich auch Hilbert: er betonte den Formalismus des Kalküls, sein Pro\bs
    gramm eines Beweises der Widerspruchslosigkeit war einleuchtend und in den ersten
    Stadien versprechend, man musste erst die Erfahrung der Schwierigkeiten
    machen, die diesen Angriff so gut wie hoffnungslos erscheinen lassen, bevor
    man bereit war, andere Wege -- \emph{Ihren} Weg zu gehen.

    Mir geht es so, dass ich nach langen Jahren der Resignation endlich wie\bs
    der offenen Himmel sehe. Ich bin froh, dass ich das noch erlebt habe. Nehmen
    Sie noch einmal meine herzlichsten Glückwünsche entgegen für das von Ihnen
    vollbrachte Werk! -- Sie überreichen mir Ihr Buch als Geschenk zu meinem
    (bald fälligen) 70.~Geburtstag. Es ist heute morgen schon eingetroffen. Ich
    glaube, man hätte mir kein schöneres Geschenk machen können. Ich danke Ihnen
    von ganzem Herzen dafür!\strut

    \hfil\hfil\begin{tabular}{c}
      Mit den besten Grüßen und Wünschen\\
      Ihr\\
      Hermann Weyl
    \end{tabular}}
\end{quotation}
\section{1955-1958. Weyl's invitation of Lorenzen to the Institute for Advanced Study}\label{sec:linv-de-lorenz}

The next six items of our timeline document the missed opportunity of our two protagonists meeting and Gödel's irritation by Lorenzen's operative mathematics.

This invitation is documented in the file ``Lorenzen, Paul, 1955--1958'' of the School of Mathematics records, 00110, of the Institute for Advanced Study in the Shelby White and Leon Levy Archives Center.

% Lorenzen, Paul P. W. -M- 1957-58, Container: 88. Institute for Advanced Study (Princeton, N.J.). Director's Office. Member records, 00028. Shelby White and Leon Levy Archives Center.

% (DO = Director's Office, SM = School of Mathematics)

% \includepdf[pagecommand={},pages=8]{../photos_et_pdf_d_origine/Princeton/SM_Lorenzen.pdf}

\paragraph{1955. Letter from Weyl to Selberg.} This letter is not dated.

\begin{quotation}
  Dear Atle, I am writing to you to suggest as a candidate for
  the Institute, not for this, but maybe for the next academic year,
  Prof.\ \emph{Paul Lorenzen} from the University Bonn (address: Carl-Schurz\Bs
  Colleg, Kaiserstr.~57, Bonn). He is, of course, German, 40~years
  old, married and has one daughter, age~13. He is best known for
  his research in mathematical logic and foundations of mathematics.
  But he has also published a number of good papers in algebra.

  Quite recently a book of his ``Einführung in die operative
  Logik und Mathematik'' appeared in the Gelbe Sammlung (Sprin\-ger-Ver\bs
  lag). Of this book both van der Waerden and I think very highly.
  I am reading it at the moment with considerable enthusiasm. It seems
  to me that, after Brouwer's intuitionism and Hilbert's formalism
  and Gödel's debacle, this may actually show the right and best way
  out of the dilemma, and give us---if not the consistency proof of
  one of the formal axiomatic systems---at least all the essential
  theorems of analysis. On Lorenzen's ``operative'' standpoint Gödel's
  discovery loses completely its disquieting character.

  Whether my judgment is right or wrong: Lorenzen is certainly
  an investigator in his field of high originality and one whom it is
  worthwhile to bring over for a visit to the States. I do not know
  him personally, but most mathematicians here do, and they all tell
  me that he is a very lively and agreeable fellow.

  There is an additional reason why I could wish Lorenzen to
  have an opportunity to visit America: the younger Hirzebruch (and
  not he) got the vacant full professorship in Bonn, and H.\ will go
  there after his year at Princeton University. L.\ is merely what
  they call an apl.\ (meaning, I guess, ``außerplanmässiger'') professor
  in Bonn.

  \hfill H. Weyl
\end{quotation}
\paragraph{1955. School minutes of the School of Mathematics of the Institute for Advanced Study, 26 October.}
\label{sec:scho-minut-scho}

\begin{quotation}
  \begin{itemize}
  \item[3.] The case of \emph{Paul Lorenzen} of the University of Bonn was
    brought up by Professor Selberg. It is understood that Professor Gödel
    will examine Lorenzen's papers and report on them.
  \end{itemize}
\end{quotation}

\paragraph{1955. Gödel's first report on Lorenzen.}
The following draft by Gödel are taken from a file entitled ``Lorenzen, letter, drafts, and discussion notes: 1958 and undated'', Kurt Gödel Papers, Personal and Scientific Correspondence, Lorenzen, Paul, Box 2b, Folder 103, documents number 011467--011468, C0282, Manuscripts Division, Department of Special Collections, Princeton University Library. This draft is an elaboration of a sketch (011464, 011466, 011469). We have typeset our completion of Gödel's abbreviations in oblique type.

According to Jan von Plato, they contain ``perhaps the nastiest passages on scientific matters in the thousands of pages of the Kurt Gödel Papers''.

% \subparagraph{First draft of the report.}\leavevmode

% \begin{framed}%\parindent0pt\obeylines
%   [\texttt{011466 r, IMG\_7046.jpg}]
%   1. Algebr\sub.{a}\hfil not Weyl's reason for suggesting him.

% 2. refer to 3 subjects

% 1. extended Weyl's approach to analysis by higher orders
% of real nu\sub.{mbers} 
% He succ\sub.{eeds} to derive the theory of Leb\sub.{esgue}
% integral (main theorems) as far as
% they refer to meas\add{urable} sets \& meas\add{urable} funct\sub.{ions,}
% he proves the Urys\sub.{ohn} theorem of the emb\add{edding} of
% topol\sub.{ogical} spaces into metric ones\add.
% Papers are very good as far as they go but
% they do not cont\sub.{ain} any subst\sub.{antially} new ideas but
% routine procedures. And the value of this whole
% approach to analysis is rather questionable.
% Weyl\sub.{'s} quot\sub.{ation}

% 2. He developed a new method for consist\sub.{ency} proof\add{s}
% which is very important \& is the greatest prog\add{ress} in
% this field since Gentzen. However subst\sub.{antially} the same
% thing was done by Novik\sub.{off} 7 years earlier \&
% in an abstr\sub.{act} 10 years earlier\add, in English, reviewed
% \sub{Novik. }{}not quite alright\add, but still the main
% idea and also to a large ext\sub.{ent} the elab\sub.{oration is} due to
% Novik\add{off}. Moreover Schütte \add{is }simultaneous\add{ly}
% [\texttt{011466 v, IMG\_7047.jpg}]
% considerably better. \add{He }quotes Lorenzen but Lor\add{enzen} does not
% quote Schütte\add{; they are} indep\sub.{endent} from each other though not from
% Novikoff.

% 3. He developed some new approach to the found\sub.{ations} which is
% what he spec\sub.{ially} calls operationistic. \add{It is a }mixture of formalism
% \& intuitionism, simultaneous\add{ly} formal syst\sub.{ems} \& consid\sub.{erations}
% about them\add, where these consid\add{erations} are themselves
% formalised \& therefore again form part of the formal
% system. This work is in a rather un%
% finished state. Proofs \add{are }only ind\sub.{icated} but he claims the proofs, moreover it
% suffers from vagueness because \add{there are }formulas \&
% consid\add{erations} about formulas but it has potentialities
% of development. But if developed it would do exactly the opposite.

% [\texttt{011469 r, IMG\_7052.jpg}]

% 3. He shows here that he is a very gifted logician\add, that he has original
% ideas which if carried out properly
% probably might lead to something very
% interesting although certainly not to a proof but rather a \add{disproof of }his
% phil\sub.{osophical} view. But his phil\sub.{osophical} prej\sub.{udices} prevent
% him from carrying them out properly
% E.g.\ he has the prej\sub.{udice} that there are no axioms
% which must be used in metamath\sub.{ematics} \& this prevents
% him from analysing what he uses in
% his proofs which would be the most imp\sub.{ortant}
% thing to do. Se he simply
% stays muddy in his ideas.
% \end{framed}

%\subparagraph{Second draft of the report.}\leavevmode

\begin{quotation}%\parindent0pt\obeylines
%  [\texttt{011467 r, IMG\_7048.jpg}]
First: also purely algebraic papers which I have not read bec\sub.{ause} I
don't feel comp\sub.{etent} to judge about them\add.
His papers in the found\sub.{ations} refer to 3 different topics.

1. He has extended Weyl's constr\sub.{uctive} approach to analysis by intro\bs
ducing a hierarchy of order\add{s} of real nu\sub.{mbers}
\& he got as far as defining Leb\sub.{esgue} integral \& proving its
main properties. Also he proved Urysohn's theorem
about the introd\sub.{uction} of a metric in a topological space\add.
This work is very good as far as it goes. But the
res\sub.{ults} are not very prof\sub.{ound}. It is a well-known fact
that large parts of analysis do not use impred\sub.{icative} procedure\add s.
In many cases one only has to analyse the proofs in order to find it out.
Moreover this approach has its limits \& therefore it is entirely
unjustified to say (as Lorenzen does) that thereby the cons\sub.{istency}
of analysis has been proved.
In my op\sub.{inion} this whole appr\sub.{oach} goes in the wrong
direction.\footnote{In the sketch for this draft, Gödel is more explicit: he writes that ``the value of this whole
  approach to analysis is rather questionable'' and refers to three sentences of \citet[page~23]{weyl18}, copied in Gabelsberger short:

  ``1. An analysis with formation of types is artificial and useless.
  
  ``2. Every cell of this mighty organism is permeated by the poison of contradiction.

  ``3. We must restrict the existence concept to the basic categories.''\footnotemark}\footnotetext{%
  \begin{tabular}[t]{@{}l@{}}
    1. Eine Analysis mit Stufenbildung ist künstlich und unbrauchbar.\\
    2. Jede Zelle des gewaltigen Organ\add{ismus} der Analysis ist von diesem Gift durchsetzt.\\
    3. Der Existenzbegriff soll nur hinsichtlich der Grundkategorien angewendet werden.
  \end{tabular}}

2. The second topic of Lorenzen's work is a new method
for consistency proofs.\footnote{\label{lor1951}\citealt{lorenzen51wt}, see \citealt{coquandneuwirth23}.} This method constitutes a \uline{very}
import\sub.{ant} progress in this field. However this method is
really due to Novikoff who published it 7 years earlier
(1944) in English and a sketch of it even came out 10 years
earlier.\footnote{\citealt{novikoff39,novikoff43}.} Novikoff's proof is not quite satisfactorily
refereed
%  [\texttt{011467 v, IMG\_7049.jpg}]
but still I would say by far the greater part of the credit
has to go to Novik\add{off}. Moreover Lorenzen also does
not explicitly give the \uline{really interesting} result obtainable by
this method and it is not trivial to extricate it from his proof. It was
Schütte who did that.

3. The third topic of Lorenz\sub.{en's} work is a foundation of arithmetic
on the basis of his operational
viewpoint. It cons\sub.{ists} in a mixture of form\add{alism} \& intuitionism.
It is vague\add: it does not dist\sub.{inguish}
between formulas as marks on paper \& as expr\sub.{essions} having meaning.
The proofs are not carried out at all
but nevertheless he claims to have given a satisfactory
found\add{ation} of arithmetic. It is true that it contains ideas which probably
could be carried out
\& possibly might lead to something interesting
but then this found\add{ation} of arithm\add{etic} would
change its character \& would rather lead to
a disproof of the operational viewpoint namely
it would show that if
one wants to give a satisf\sub.{actory} found\add{ation} for number th\sub.{eory}
(including a cons\sub.{istency} proof) it is not possible to confine oneself to cons\sub.{istently}
referring to the handling of symbols but has to use cert\add{ain} abstr\sub.{act}
conc\sub.{epts} such as function, implic\add{ation}, etc.
%
% [\texttt{011468 r, IMG\_7050.jpg}]

I am definitely opposed to inviting Lorenzen\add.
My judgement is based on his work on the found\add{ations.} He wrote
some purely alg\sub.{ebraic} pap\sub.{ers}
about ord\add{ered} gr\sub.{oups} \& lattice gr\sub.{oups}
which I have not read but they
are not the reason why Weyl wants to invite him\add.
As to the foundations there is I.~his absurd phil\sub.{osophy} which
also reflects very unfavorably
on his math\sub.{ematical} work namely 1.~It induces him to
make openly false statements about his math\sub.{ematical} work
1.~that he has used no transf\sub.{inite} ind\add{uction} where he evidently has used
it\footnote{Compare the account of accessibility in \citealt[note~c on page~272,]{goedel90} and \citealt[§~6.3]{coquandneuwirth23}} or to say he has proved the cons\sub.{istency} of anal\sub.{ysis} where
there is nothing of the kind. One even gets the impr\sub.{ession} that
these ass\sub.{ertions} are consciously wrong\add. 2.~Moreover which is even more serious
his phil\add{osophical} prejudices prevent him from doing the math\add{ematical} work properly. He takes the pos\add{ition}
that there is
nothing like math\sub.{ematical} cogn\sub.{ition} or a math\add{ematical} intuition
or evident math\add{ematical} axioms
but that everything in math\add{ematics} is due to conv\sub.{ention} \& to expediency.
This prejudice prevents him from
analysing what he uses in his metamath\sub.{ematical} proofs which
is of preeminent[?]\ imp\sub.{ortance}
in this field. Moreover
this has the cons\sub.{equence} that he is imprecise in his metamath\sub.{ematical} reasoning\add.

II.~Considering his papers one by one the best no doubt is the one in \add{The Journal of Symbolic Logic.\footnotemark[\getrefnumber{lor1951}]}
\end{quotation}

Note that in a letter dated 20 March 1956, Gödel asks von Neumann what he thinks about Lorenzen's ``efforts to base analysis on ramified type theory [\dots] up to the theory of the Lebesgue measure'' \citep*[pages~376--377]{goedel03b}.

\paragraph{1955. Research intended by Lorenzen in Princeton.}%\leavevmode
\label{sec:rese-intend-lorenz}

\begin{quotation}
  \indent\indent Intended research.\bigskip

  I intend to continue the investigations I have started
  in my book. Above all I hope to achieve a progress in one
  of the following points:
  \begin{enumerate}[(1)]
  \item application of the operational method to functional
    analysis. In some lectures I have already developed
    an approach to additive set-functions and linear
    functionals.
  \item examination, as to how far the theorems of abstract
    topology may be reached ``operationally''.
  \item application of the operational method to metamathe\bs
    matics in the sense of Tarski and Robinson.
  \end{enumerate}

  \hfill
  \begin{tabular}{r}
    Paul Lorenzen\\
    Nov.~27, 55
  \end{tabular}
\end{quotation}
% \includepdf[pages={2}]{../photos_et_pdf_d_origine/Princeton/DO_Lorenzen.pdf}

% \includepdf[pages=1]{../photos_et_pdf_d_origine/Princeton/SM_Lorenzen.pdf}

\paragraph{1956. School minutes of the School of Mathematics of the Institute for Advanced Study, 11 April.}

\begin{quotation}
  \begin{itemize}
  \item[5.] It was voted to offer \emph{Paul Lorenzen} a grant of \$4,700 and membership for the academic year 1957--58. [Professor Selberg will write informally first.]
  \end{itemize}
\end{quotation}

\paragraph{1958. Gödel's second report on Lorenzen.}
\label{sec:godels-report-lorenz}

A draft of the report below is in the Kurt Gödel Papers (011463).\bigskip

{\parindent0em\noindent
  To be returned to the Committee at the conclusion of the scholar's stay at his host in\bs
  stitution.\smallskip

  \hfil\makebox[0pt][c]{REPORT TO THE COMMITTEE ON INTERNATIONAL EXCHANGE OF PERSONS}\smallskip

  \hfil Conference Board of Associated Research Councils

  \hfil 2101 Constitution Avenue, Washington 25, D. C.\rlap{\hspace{4em}1957-8}\smallskip

  \leavevmode\rlap{Name of Visiting Scholar: \textb{Paul LORENZEN}}\hphantom{Sponsoring Institution: \textb{Institute for Advanced Study}\qquad}Country \textb{Germany}\smallskip
  
  Sponsoring Institution: \textb{Institute for Advanced Study}\qquad Field \textb{Mathematics}\smallskip
  
  Member of faculty most familiar with his work: \textb{Professor Kurt Gödel}\smallskip

  \leavevmode\rlap{Arrival date at the institution:}\hphantom{Arrival date in U.S.\ (if known): }\textb{9/12/57}\enspace Departure date from institution: \textb{3/30/58}\smallskip
  
  Arrival date in U.S.\ (if known): \textb{9/12/57}\enspace Departure date from U.S.\ (if known): \textb{3/30/58}\smallskip
  
  Forwarding address if scholar is still in the United States:\smallskip

  Academic Status of Visitor: \textb{Member of the School of Mathematics}\smallskip

  Has the scholar been primarily engaged in research \hbox to 3em{\hfil\textb{Yes}\hfil}; in teaching \hbox to 3em{\hfil\textb{No}\hfil}?\smallskip

  If teaching, the following information would be helpful to the Committee:\smallskip

  {\leftskip 1em Approximate number of students taught:\qquad Number of teaching hours per week:\smallskip

  Did he teach primarily graduate or undergraduate students?\smallskip
  
  Did he teach courses regularly offered in the curriculum?\qquad (On reverse side,
  please list titles of courses taught)\smallskip

  }If he undertook research please comment briefly on the nature of his research, indicat\bs
  ing its value (a)~to your institution or (b) to his own professional development.\smallskip

  \textb{He obtained a considerable improvement and strengthening of one of the axioms of his
    ``operationistic'' mathematics and with its help, gave a proof of the Cantor-Bendixson
    Theorem which is constructivistic in a generalized sense. He also conceived interesting
    ideas of a game-theoretical interpretation of logic.}\smallskip

  Did the visitor have any difficulties with the language? \qquad. If so, was this a
serious handicap to him in pursuing his professional program? \qquad; in his social
contacts? \hspace*{2em}. (A reply to this question is requested if this is a report on a
visitor from Asia.)\smallskip

Additional remarks: (Please use reverse side if needed.)\bigskip

  \noindent
  \begin{tabular}[b]{l}
    Date: \textb{June 25, 1958}\\[\smallskipamount]
    \begin{tabular}[c]{@{}l}
      EPL:ej\\
      Oct.~56
    \end{tabular}\qquad August 14, 1958
  \end{tabular}
  \hfill
  \begin{tabular}[b]{l}
    Signature: /s/ Kurt Gödel\\[\smallskipamount]
    Signature: \textb{Kurt Gödel}\\[\smallskipamount]
    Title: \textb{Director}
  \end{tabular}

  }

\section{1958--1965. Transition of Lorenzen to a simple distinction of definite and indefinite}
\label{sec:trans-simple-dist}

The last four items of our timeline describe how Lorenzen shifts to dialogues and indefinite quantifiers.

\paragraph{1958. The transition to dialogical logic.}


% \section{Couches de langage}
% \label{sec:couches-de-langage}

% % Décrire l'entreprise des couches de langage dans \citealt{lorenzen55}. 
% Problème de définir ce qu'est une assertion: \emph{Dialogdefinitheit}. Quel est le problème pointé par Tarski? Est-il résolu par la logique dialogique?

% Quel est l'impact du passage d'une infinité à juste deux couches?

% \subsubsection{Échanges avec Kuno Lorenz en février 2022}
% \label{sec:echanges-avec-kuno}

% \paragraph{Stefan}

% Lieber Herr Lorenz,

% Zusammen mit Thierry Coquand und Henri Lombardi arbeite ich weiter über 
% Lorenzens Widerspruchsfreiheitsbeweis von 1951 und seine Entwicklung der 
% operativen und dialogischen Logik. Insbesondere möchten wir besser verstehen, 
% welchen Bezug dieser Beweis und diese Entwicklung haben.

% Dafür ist Ihr Beitrag zur Lorenzen-Konferenz in 2018 eine sehr wichtige 
% Informationsquelle.

% Wir wüssten gerne noch mehr von der Auseinandersetzung, die Lorenzen und Tarski 
% 1957/58 in Berkeley gehabt haben. Verstehen wir recht, dass Tarskis Kritik genau 
% darin besteht, dass es nicht möglich ist, behauptete Definitheiten und 
% Zulässigkeiten zu kontrollieren? Ist es genau deswegen, dass Sie schreiben, dass 
% die operative Logik nicht hinreichend fundiert ist? Könnten Sie uns genauer 
% erklären, inwiefern das ein Problem ist? Inwiedern ist die dialogische Logik, 
% sind die Dialogspiele eine Antwort auf diese Kritik?

% Besteht ein Zusammenhang zwischen diesem Fragenkreis und Lorenzens Abkehr von 
% Widerspruchsfreiheitsbeweisen?

% Wenn Sie es vorziehen, können wir diese Fragen auch telefonisch besprechen.

% \paragraph{Kuno Lorenz}

% Lieber Herr Neuwirth,
% es überrascht mich nicht, daß Sie gern mehr über den Inhalt der/des
% Gespräch[e/s] in Erfahrung bringen möchten. Leider kann ich über das hinaus,
% was Lorenzen mir über seine Begegnung mit Tarski gesagt hat und ich
% geschrieben habe, kein weiteres Detail beisteuern. Nur das ist klar: 
As Kuno \citet{lorenz21} tells, Lorenzen and Tarski met at the international symposium ``The axiomatic method with special reference to geometry and physics'' held at the university of
California at Berkeley from 26 December 1957 to 4 January 1958.
Lorenz witnesses that ``the further development of the operative to a \emph{dialogical} logic based on validity claims and their defense resp.\ rejection has not become a desideratum for Lorenzen before Tarski's doubts about the appropriateness of his usage of `definite'{}'' (private communication, 8 February 2022).
% erst
% durch Tarskis Zweifel an der Eignung von Lorenzens Gebrauch von `definit'
% ist für ihn die Fortentwicklung der operativen zu einer \emph{dialogischen}, auf
% Geltungsansprüchen und deren Verteidigung bzw. Zurückweisung fußenden Logik
% ein Desiderat geworden. Die spieltheoretische Fassung dieser Fortentwicklung
% mit ihrer für das Gelingen unerläßlichen Unterscheidung zwischen der Ebene
% konkreter Dialogführungen und der Ebene von Strategien der Dialogführung -
% erst auf dieser läßt sich der Wahrheitsbegriff ansiedeln, während
%  `dialogdefinit' auf die Ebene der konkreten Spielführungen gehört und sich
% deshalb dank des Prädikats  `nach geeignet zu wählenden Dialogregeln gewonnen
% oder verloren' zur Charakterisierung des Aussageseins eignet  -  ist dann
% der Inhalt meiner Dissertation geworden. 

% Salopp ausgedrückt ging es darum, ein entscheidbares Prädikat zu finden (und
% nicht etwa mit 0.1-Belegungen zu arbeiten wie bei informatischen
% Fragestellungen), das jenseits des grundsätzlich unentscheidbar bleibenden
% Wahr- oder Falschseins von Aussagen für Aussagen im Allgemeinen und nicht
% nur für mathematische bzw. kalkültheoretische als charakteristisch gelten
% darf wie eben das in einem geregelten Dialog Gewonnen- bzw. Verlorenhaben:
% die unentbehrliche pragmatische Grundlage jedweder Theoriebildung.
% Vielleicht ist es hilfreich, wenn Sie die erst seit wenigen Monaten
% verfügbare Sammlung meiner zur Logik im weitesten Sinne gehörenden Aufsätze
% zurate ziehen, insbes. den 12. (Die Entwicklung des dialogischen
% Prinzips\dots, in: K. L., \emph{Von der dialogischen Logik zum dialogischen
% Konstruktivismus}, Berlin 2021, de Gruyter, pp. 285-298); in diesem Band auch
% Näheres zu den Gründen für den Übergang von der operativen zur dialogischen
% Logik.

% Mit herzlichen Grüßen (auch den Combattanten)

% \paragraph{Stefan}

% vielen Dank für Ihre ausführliche und klare Antwort. Ich habe den Aufsatz, den 
% Sie mir empfohlen haben, im 2016 erschienenen Band \emph{Paul Lorenzen und die 
% konstruktive Philosophie} gefunden. Thierry Coquand hat mich seinerseits auf 
% Ihren Artikel „Basic objectives of dialogue logic in historical perspective“ 
% aufmerksam gemacht.

% Nun ist mir einerseits klar, dass es darum geht, den Begriff der Aussage zu 
% charakterisieren, und dass erst der Begriff der Dialogdefinitheit das 
% ermöglicht. Andererseits hat mich das Argument, dass in der operativen Logik dem 
% Begriff der Subjunktion der Begriff der Zulässigkeit zu Grunde liegt, dass 
% deshalb die Betrachtung von Formeln der Form \((A\implies B)\implies C\) zu einem Metakalkül 
% führt, in dem der Begriff der Ableitbarkeit unentscheidbar ist, sehr 
% interessiert.

% Jetzt können wir unsere Fragen genauer fassen: Welche Konsequenzen hat Lorenzens 
% Abkehr von den Sprachschichten und allgemeiner die Entwicklung der dialogischen 
% Logik auf seinen Bezug zur verzweigten Typentheorie? Ist diese weiterhin für ihn 
% die Grundlage der Mathematik geblieben? Diese Frage stellt sich uns insbesondere 
% in Bezug auf die reellen Zahlen, die bei Lorenzen doch arithmetischen Prädikaten 
% entsprechen, und die doch nur mit einer unendlichen Hierarchie von Typen erfasst 
% werden können.

% Wissen Sie übrigens, wie Lorenzen angesichts der Widerspruchsfreiheit der 
% Arithmetik über das ausgeschlossene Dritte in der Arithmetik gedacht hat, zum 
% Beispiel bezüglich der Goldbachschen Vermutung?

% Wissen Sie weiters, wie Lorenzen die Veröffentlichung von Errett Bishops Buch 
% \emph{Foundations of constructive analysis} (1967) empfangen hat? Hat es da eine 
% Zwischenwirkung mit \emph{Differential und Integral} gegeben, insbesondere in der 
% Rezeption von Lorenzens Buch?

% Angesichts der gegenwärtigen Bedeutung des Curry-Howard-\hspace{0pt}Isomorphismus (1969) 
% wüssten wir auch gerne, ob ihn diese Entwicklung noch interessiert hat.

% Endlich wären wir Ihnen sehr dankbar, wenn Sie uns die Bedeutung (die 
% Faszination!) von Lorenzens Vorlesung über die Differentialgeometrie darstellen 
% könnten.

% \paragraph{Stefan}

% Mir ist bewusst, dass ich Ihnen schon allzu viele Fragen stelle, aber in meinem 
% gestrigen Brief habe ich folgende Frage vergessen aufzuführen, obwohl sie uns 
% wichtig scheint. 

% Im Vorwort zu \emph{Differential und Integral} stellt Lorenzen eine Verbindung 
% zwischen der Vereinfachung der Begründung der Analysis einerseits und der 
% Vereinfachung der Logik von den Sprachschichten der \emph{Einführung in die operative 
% Logik und Mathematik} zur Dialogdefinitheit der \emph{Metamathematik} andererseits 
% her. Uns ist nicht klar, ob die Unterscheidung von definiten und indefiniten 
% Begriffen (die man ja auch als zwei Schichten betrachten könnte) auch in der 
% dialogischen Logik ihren Einschlag hat (oder zwischenwirkt), oder ob sie voll 
% und ganz in die Begründung der Analysis gehört.

% \paragraph{Traduction}

% «je ne suis pas surpris que vous aimeriez en savoir plus sur le[s] 
% conversation[s]. Je ne peux malheureusement pas rajouter de détail en plus de ce 
% que Lorenzen m'a dit sur sa rencontre avec Tarski et que j'ai écrit. Seul ceci 
% est clair: ce n'est que par le doute de Tarski sur l'adaptation de l'usage par 
% Lorenzen de “défini” que celui-ci a envisagé de développer la logique opérative 
% en une logique \emph{dialogique} basée sur des affirmations de validités et leur 
% défense resp.\ rejet. Puis la version théorie-des-jeux de ce développement avec 
% la distinction indispensable pour sa réussite entre le plan de dialogues menés 
% concrètement et le plan de stratégies pour mener des dialogues -- ce n'est que 
% sur celui-ci qu'on peut fixer le concept de vérité, alors que “d-défini [défini 
% au sens du dialogue]” appartient au plan des jeux menés concrètement et est donc 
% adapté à la caractérisation de ce que c'est qu'être une proposition grâce au 
% prédicat “gagné ou perdu selon des règles de dialogue à choisir de manière 
% adaptée” -- est devenue le contenu de ma thèse.

% «Il s'agissait en gros de trouver un prédicat décidable (et pas par exemple de 
% travailler avec des inscriptions de 0 et de 1 comme dans des problèmes 
% informatiques) qui puisse caractériser des propositions en général, et pas 
% seulement des propositions mathématiques et de théorie du calcul, au-delà de la 
% vérité et de la fausseté des propositions qui restent fondamentalement 
% indécidables, comme justement d'avoir gagné resp. perdu dans un dialogue selon 
% des règles: le fondement pragmatique indispensable de toute formation de 
% théorie.

% «Il peut être utile de consulter l'anthologie de mes articles qui appartiennent 
% à la logique au sens le plus large disponible depuis quelques mois seulement, en 
% particulier le douzième (Le développement du principe dialogique\dots, dans \emph{De la 
% logique dialogique au constructivisme dialogique}, Berlin 2021, de Gruyter, 
% p. 285-298). Ce volume précise aussi les raisons du passage de la logique 
% opérative à la logique dialogique.

% «Avec mes salutations cordiales (aussi aux combattants [c'est-à-dire vous 
% deux])»

% \paragraph{Épilogue}

\citet{lorenz01} describes the problematic of the meaning of implication (called subjunction) in operative logic. It is based on \emph{admissibility}, so that one has to move one level up in the following sense:  if the rule leading from~\(A\) to~\(B\) is admissible in a calculus, i.e.\ if it does not extend the class of derivable statements, then one states that \(A\implies B\) at a metalevel. However, admissibility is undecidable. Lorenz writes: ``Especially subjunctions in the 
operative interpretation could not any more be called ‘definite’ as it had been 
the explicit intention of the operative approach'' (page~257). He proceeds with pointing out the incapacity of operative logic to capture the meaning of what it is to be a proposition and the solution provided by the concept of ``dialogue-definiteness''.

\citeauthor{schroederheister08} (\citeyear{schroederheister08}, §~3.2, \citeyear{schroederheister08b}, §~3.1) describes Lorenzen's theory of implication in his comparison of operative mathematics with proof-theoretic semantics. 

% Dans l'article «Basic objectives of dialogue logic», Lorenz décrit en quoi la 
% manière de la logique opérative de donner un sens à l'implication est 
% problématique. En effet l'implication est définie sur la base de 
% l'admissibilité, et on se retrouve avec le problème de donner un sens à une 
% implication dont le premier terme est lui-même une implication, c'est-à-dire de 
% la forme \((A\implies B)\implies C\). Lorenzen propose pour cela de passer à un «métacalcul» 
% dans lequel une formule est dite dérivable si elle est admissible dans le calcul 
% dont on part: ainsi \(A\implies B\), définie comme une admissibilité dans le calcul dont 
% on part, devient une formule dérivable du métacalcul, et \((A\implies B)\implies C\) est 
% défini comme une admissibilité dans le métacalcul. Être une dérivation est un 
% prédicat décidable par rapport au calcul dont on part, et Lorenz objecte qu'être 
% admissible est indécidable. Ainsi Lorenz écrit: «Especially subjunctions in the 
% operative interpretation could not any more be called ‘definite’ as it had been 
% the explicit intention of the operative approach.»

% La suite de l'article traite plus fondamentalement du prédicat «être une 
% proposition» et indique que la logique opérative n'est pas capable de le capter 
% par les notions de définitude qu'elle développe. Lorenz décrit alors en détail 
% le concept de d-définitude, «être défini au sens du dialogue» qui supplée 
% ceci.

% J'ai lu l'article que Lorenz m'a conseillé (on a ici le livre dans lequel il est 
% paru à l'origine en 2016). C'est un article très philosophique et pour le moment 
% je ne saisis pas les véritables enjeux du texte. On y trouve cependant in 
% extenso ce que Lorenz m'a écrit dans son mail: le plan des dialogues concrets 
% et le plan des stratégies de dialogues; la d-définitude est la décidabilité 
% qu'un dialogue concret a mené à une victoire ou à une défaite.

\paragraph{1965. No language levels in Lorenzen's \emph{Differential und Integral}.}

The foreword to \citealt{MR0209410} underlines the simplification in abandoning the construction of language levels.

\begin{quotation}
    % \noindent\hfil\textsc{dedicated}
    
    % \noindent\hfil\textsc{to the memory of}
    
    % \noindent\hfil\textsc{Hermann Weyl}

    % \dotfill\bigskip

    % \noindent\hfil\textbf{PREFACE}\bigskip
    
  Since the appearance of my \emph{\german{Einführung in die operative Logik und
Mathematik}} (\citeyear{lorenzen55}), I have given a simplified account of the
grounding\label{grounding} of logic in \emph{Metamathematik} (\citeyear{lorenzen62}). I now put forth a
grounding of analysis which is likewise considerably simplified:
as was the case in H. Weyl's \emph{Das Kontinuum} (\citeyear{weyl18}), no construc\bs
tion of ``higher'' language levels is undertaken. For this reason
the book is dedicated to the memory of Hermann Weyl. \citep[page~\textsc{ix}.]{MR0346097}
\end{quotation}

% \citet{lorenzen86b} emphasises this.
% \begin{quotation}
%   The ``operative'' justification of analysis was---considered retrospectively---complicated in a deterrend way.
% \end{quotation}

\citet{feferman00} reports as follows on \citealt{MR0346097}: ``while significant portions of that are based on predicative grounds, it is not restricted to such''. Feferman does not justify his judgment; we presume that it targets the consideration of inductive definitions: as Laura \cite{crosilla22} points out, he is sticking to the ``classical approach'' of a ``predicativity given the natural numbers'' \citep{feferman05}.

% \subsection{Vorwort zur zweiten Auflage \citep{MR0241272}}

\paragraph{1965. Bernays reviews Lorenzen's \emph{Differential und Integral}.}

At the request of \german{Akademische Verlagsgesellschaft}, the publisher of \emph{Differential und Integral}, Bernays writes a review (Hs~975:5329) on 5 November 1965, and in particular the following.
\begin{quotation}
  The specifically remarkable about this book from the foundational point of view consists in avoiding consistently the ``impredicative'' methods. This methodical restriction, demanded first at the beginning of our century by several French mathematicians, and for which on the one hand  Russell und Whitehead with their ramified theory of types, on the other hand Hermann Weyl in his writing ``Das Kontinuum'' provided a formal framework, is carried out here in such a way that the explicit put-up of a formal framework is not required, that it is indeed enough to tighten the usual methods in the sense of a \emph{constructive version of the concept of existence for real numbers}, so that the variety of real numbers needn't be considered as a determined delimited one, but can rather be treated as an ``indefinite'' totality. The careful execution of this program confirms the view harboured by theorists of foundations that in doing so no essential perceptible restriction of the methods and results of analysis occurs.\footnote{\selectlanguage{german}
      % \hfill[Hs 975:5329]
% 
  % \hfill 5.~November 1965
% 
  % \begin{tabular}{@{}l@{}}%
  %   \quad An die\\%
  %   Akademische Verlagsgesellschaft\\%
  %   Cronstettenstrasse~6a\\%
  %   6 FRANKFURT AM MAIN%
  % \end{tabular}
% 
  % Sehr geehrter Herr Schmitt!
% 
  % Seit langem schulde ich der Akademischen Verlagsgesellschaft
  % meinen Dank für die freundliche Übersendung des Werkes "`Differential
  % und Integral"' von Prof.\ P. Lorenzen. Ihr Verlag wünschte auch von mir
  % eine Stellungnahme zu dem Buch und insbesondere eine Beurteilung im
  % Hinblick auf den Lehrbuchcharakter. Leider komme ich erst jetzt dazu,
  % Ihnen eine solche Äusserung über das Buch zugehen zu lassen. Ich hatte
  % im Sommer und Herbst die Zeit durch verschiedene Obliegenheiten sehr
  % ausgefüllt und kam nur hin und wieder dazu, mir das Lorenzen'sche Buch
  % vorzunehmen.
% 
  % Um zunächst über den Lehrbuchcharakter zu sprechen, so wendet
  % sich das Buch nicht an einen studentischen Anfänger, der überhaupt erst
  % die Differential- und Integralrechnung kennen lernen soll, wohl aber
  % wird es einem fortgeschrittenen Studierenden, der über die begrifflich
  % schwierigeren Punkte der Analysis Klarheit zu gewinnen sucht, sehr
  % willkommen sein. Desgleichen kann es für einen jeden der in dem Fache
  % der Infinitesimalrechnung zu unterrichten hat, von grossem Nutzen sein.
  % Alle die typischen Schwierigkeiten, an denen in elementare\barre{re}n Darstel\bs
  % lungen oft vorbeigegangen wird, werden hier zur Klärung gebracht
  Das spezifisch Bemerkenswerte des Buches vom grundlagentheoreti\bs
  schen Standpunkt besteht in der konsequenten Vermeidung der "`imprädika\bs
  tiven"' Methoden. Diese methodische Beschränkung, wie sie zuerst im
  Anfang unseres Jahrhunderts von mehreren der französischen Mathematiker
  gefordert wurde und für welche einerseits Russell und Whitehead mit %[2]
  ihrer verzweigten Stufen\-theorie, andrerseits Hermann Weyl in seiner
  Schrift "`das Continuum"' einen formalen Rahmen lieferten, wird hier in
  solcher Weise durchgeführt, dass es der expliciten Aufstellung eines
  formalen Rahmens für die Darstellung nicht bedarf, dass es vielmehr
  genügt, die üblichen Methoden im Sinne der \emph{konstruktiven Fassung des
    Existenzbegriffes für reelle Zahlen} zu verschärfen, sodass die Mannig\bs
  faltigkeit der reellen Zahlen nicht als eine bestimmt abgegrenzte in
  Anspruch genommen zu werden braucht, vielmehr als eine "`indefinite"'
  Gesamtheit behandelt werden kann. In der sorgfältigen Durchführung dieses
  Programmes bestätigt sich die schon von den Grund\-lagen\-theo\-re\-ti\-kern ge\bs
  hegte Ansicht, dass hierdurch die Methoden und Ergebnisse der Analysis
  keine wesentlich fühlbare Beschränkung erfahren.

  % Ungeachtet der gar nicht umfänglichen Gestaltung des Buches
  % bringt dieses dennoch eine eingehendere Behandlung der Funktionen von
  % mehreren Variablen und der differentialgeometrischen Begriffe. Der
  % Leser wird es insbesondere auch schätzen, dass auch die "`alternierende
  % Multiplikation und Differentiation"' (der calcul extérieur) zur Darstel\bs
  % lung gelangt.

  % Nun möchte ich noch nachträglich Ihrem Verlag für die Zueignung
  % des Exemplars von dem Buche meinen verbindlichen Dank aussprechen!\strut\medskip

  % \centerline{\begin{tabular}[t]{r}%
  %   Mit bestem Gruss\\%
  %   Prof.\ P\rlap{.\ B.}%
  % \end{tabular}}
  }
\end{quotation}

\paragraph{1969. Foreword to the second edition of Lorenzen' \emph{Einführung in die operative Logik und Mathematik}: indefinite quantifiers are more appropriate.}

In the foreword, \citet{MR0241272} apologises for keeping with an approach superseded by his later work.

\begin{quotation}
  Although I---understandably---hold the approaches of later works to be ``more appropriate'', e.g.\ a logic of dialogues instead of a logic of calculi, the usage of indefinite quantifiers instead of an explicit construction of language levels, this new edition contains the content of the 1st edition unchanged.

  The reader can thus carry out himself a comparison with my later works (cf.\ list of references).
  
  % Obwohl ich -- verständlicherweise -- jetzt die Ansätze der späteren
  % Arbeiten für ``sachgemäßer'' halte, z.\ B. eine Logik der Dialoge statt
  % einer Logik der Kalküle, die Verwendung indefiniter Quantoren statt
  % einer expliziten Konstruktion von Sprachschichten, enthält diese Neu\bs
  % auflage den Inhalt der \textsc{i}.~Auflage unverändert.

  % Der Leser kann also einen Vergleich mit meinen späteren Arbeiten
  % (vgl.\ Literaturverzeichnis) seIber durchführen.
\end{quotation}

The later works alluded to are \citealt{lorenzen62,MR0209410,MR0290929}.

\section{Focus on a few issues}
\label{sec:focus-few-points}

\paragraph{No presupposition of a totality in the constructive method.}

Let us cite \citealt{hilbertbernays34} in the translation of the \cite{bernaysproject03}: the axiomatic method involves a further assumption with respect to the constructive method, viz.\ the assumption of a fixed system of things. 
\begin{quotation}
  Another factor coming along in axiomatics in the narrowest sense is the \emph{existential form}. It serves to distinguish
  \emph{the axiomatic method} from the \emph{constructive} or \emph{genetic} method of founding
  a theory.\thinspace\textsuperscript{1} Whereas in the constructive method the objects of a theory
  are introduced merely as a \emph{family} of things,\thinspace\textsuperscript{2} in an axiomatic theory one
  is concerned with a fixed system of things (or several such systems) which
  constitutes a previously \emph{delimited domain of subjects} for all predicates from
  which the statement of the theory are constituted.
  
  Except in the trivial cases in which a theory has to do just with a finite,
  fixed totality of things, the presupposition of such a totality, of a ``domain
  of individuals'', involves an idealizing assumption joining the assumptions
  formulated in the axioms. \citep[pages~1--2.]{hilbertbernays34}

  \footnotesize\vspace*{2.6pt}\noindent\hbox{\vbox{\footnoterule}}\vspace*{-3pt}

  \noindent\rule{0pt}{\footnotesep}\textsuperscript{1} See for this comparison appendix~VI to Hilbert's Grundlagen der Geometrie: Über
    den Zahlbegriff, 1900.

    \noindent\textsuperscript{2} Brouwer and his school use the word ``species'' in this sense.
  % The identity relation
% \(x = y\) which is to be interpreted contentually appears in this formula along
% with the variable predicates. The acceptance of this predicate as contentually determinate is no violation of our methodological standpoint. For the
% contentual determination of identity---which is no relation at all in the true
% sense---does not depend on the particular range of imagination of the field
% being investigated axiomatically; rather it is only related to a question of
% distinguishing individuals which must be taken as already given when the
% domain of individuals is laid down. \citep[p.~8.]{hilbertbernays34}

% Moreover, the
% axioms are not in existential form. Euclid does not presuppose that points
% and lines constitute any fixed domain of individuals whatsoever. And that
% is why he does not formulate any existence-axioms but only construction-postulates.

% An example of such a postulate is: one can join two points with a straight
% line; furthermore, one can draw a circle around a given point with a prescribed radius.
   
% This methodological standpoint can only be carried out if the postulates
% are looked on as the expression of known facts or of immediate evidence.
% As is well known, the question of the range of validity of the geometrical
% axioms is a very awkward and controversial one; and it is indeed an essential
% advantage of formal axiomatics that it makes the foundation of geometry
% independent of deciding this question.

% In the domain of arithmetic we are free of these problems which are
% connected with the special character of geometrical knowledge; in fact we find
% in this domain, as well as in the disciplines of elementary number theory and
% algebra, the standpoint of direct contentual deliberation carried out without
% axiomatic assumptions in its purest form. The mark of such a standpoint
% is that the deliberation is carried out in the form of \emph{thought experiments}
% involving objects assumed to be\emph{ concretely given}. In number theory we are
% concerned with numbers assumed to be given, in algebra with expressions
% with letters with given number coefficients. \citep[p.~20.]{hilbertbernays34}
\end{quotation}
% \begin{quotation}
%   Bei der Axiomatik in der engsten Bedeutung kommt noch als weiteres Moment die
% existentiale Form hinzu. Durch diese unterscheidet sich die axiomatische
% Methode von der konstruktiven oder genetischen Methode der Begründung einer Theorie\footnote{Vgl. zu dieser Gegenüberstellung den Anhang VI von Hilberts Grundlagen
%   der Geometrie: Über den Zahlenbegriff, 1900.}. Während bei der konstruktiven Methode die
% Gegenstände der Theorie bloß als eine Gattung von Dingen eingeführt
% werden, hat man es in einer axiomatischen Theorie mit einem festen
% System von Dingen (bzw. mehreren solchen Systemen) zu tun, welches
% einen von vornherein abgegrenzten Bereich von Subjekten für alle Prädikate bildet, ans denen sich die Aussagen der Theorie zusammensetzen.
% In der Voraussetzung einer solchen Totalität des ``Individuen-Bereiches'' liegt —
% abgesehen von den trivialen Fällen, in denen eine
% Theorie es ohnehin nur mit einer endlichen, festbegrenzten Gesamtheit
% von Dingen zu tun hat
% — eine idealisierende Annahme, die zu den
% durch die Axiome formulierten Annahmen hinzutritt. (p.~1-2)

% In dieser Formel tritt neben den
% variablen Prädikaten noch die inhaltlich zu deutende Identitätsbeziehung
% \(x=y\) auf. Daß wir diese in inhaltlicher Bestimmtheit zulassen, ist nicht
% etwa ein Verstoß gegen unseren methodischen Standpunkt. Denn die
% Inhaltsbestimmung der Identität
% die im eigentlichen Sinne überhaupt
% gar keine Beziehung ist
% wird ja nicht dem besonderen Vorstellungskreis des axiomatisch zu untersuchenden Sachgebietes entnommen, sondern betrifft lediglich die Sonderung der Individuen, die mit der Zugrundelegung eines Individuenbereiches jedenfalls als gegeben angenommen werden muß. (p.~8)

% Ferner haben auch die Axiome nicht die existentiale Form.
% Euklid setzt nicht voraus, daß die Punkte sowie die Geraden je einen
% festen Individuenbereich bilden. Er stellt deshalb auch nicht Existenz-Axiome auf, sondern Konstruktions-Postulate.

% Ein solches Postulat ist z.\ B., daß man zwei Punkte durch eine Gerade
% verbinden kann ferner, daß man um einen gegebenen Punkt einen Kreis
% ;
% mit vorgeschriebenem Radius ziehen kann.
% Dieser methodische Standpunkt ist jedoch nur dann durchführbar,
% wenn die Postulate als der Ausdruck einer bekannten Tatsachlichkeit
% oder einer unmittelbaren Evidenz angesehen werden. Die hiermit sich
% erhebende Frage nach dem Geltungsbereich der geometrischen Axiome
% bekanntermaßen sehr heikel und strittig, und es besteht gerade ein
% wesentlicher Vorzug der formalen Axiomatik darin, daß sie die Begründung der Geometrie von der Entscheidung dieser Frage unabhängig
% ist
% macht.
% Von dieser Problematik, welche mit dem besonderen Charakter der
% geometrischen Erkenntnis zusammenhängt, sind wir frei im Gebiet der
% Arithmetik, und in der Tat ist auch hier, in den Disziplinen der elementaren Zahlenlehre und der Algebra, der Standpunkt der direkten inhaltlichen, ohne axiomatische Annahmen sich vollziehenden Überlegung
% am reinsten ausgebildet.
% Das Kennzeichnende für diesen methodischen
% Standpunkt ist, daß die Überlegung in der Form von Gedankenexperimenten
% an Gegenständen angestellt werden, die als konkret vorliegend angenommen werden.

% In der Zahlentheorie handelt es sich
% um Zahlen,
% die als vorliegend gedacht werden, in der Algebra um vorgelegte Buchstabenausdrücke mit gegebenen Zahl-Koeffizienten.

% (p.~20)
% \end{quotation}

Compare the last lines of the quotation from \citealt{MR0043748} translated on page~\pageref{lines}.

This ``genetic'' aspect of predicative mathematics is described as ``logical reflection'' in \citealt{MR0104569}.
\begin{quotation}
  But functions and relations are not the objects of arithmetic.
They are the concepts used in speaking about numbers as the proper objects.
Now the transition from arithmetic to analysis is achieved by taking as
the objects of a new theory just these concepts of the old theory. Psycholo\bs
gically expressed, the focus of attention has to pass from the old objects,
the numbers, to the functions and relations as new objects. Let me call this
transition a ``logical reflection'', because the reflection to be performed is
on the concepts occurring in the theorems of the old theory. Or more briefly,
the object of the reflection is the language used so far. In view of this one
may be justified in calling it a ``logical'' reflection. This logical reflection,
of course, does not simply mean that we become aware of the concepts
used so far; it also means that we ask ourselves the question: which concepts
could ``possibly'' be used. Put into words without safeguarding against
future difficulties, one might ask for ``the class of all possible arithmetical
functions and relations''. With this question, with this logical reflection,
the transition from arithmetic to analysis begins. It is the same process
which Hermann Weyl in his book \emph{Das Kontinuum} (Leipzig, 1918) simply
called ``the mathematical process'' because of its fundamental importance
to modern mathematics. Greek mathematics differs from modern mathe\bs
matics just by not having achieved this logical reflection. \citep[page~244.]{MR0104569}.
\end{quotation}

\citet[§~4]{kahleoitavem21} discuss the article \citealt{MR0043748} and judge that because of its account of the ``mathematical process'' by language levels, ``one can hardly call the system under consideration `classical analysis'{}'' and that ``it also marks a significant turn of Lorenzen away from Hilbert’s philosophical basis''. These judgments seem to consider that such a philosophical basis must aim at justifying Dedekind's impredicative introduction of real numbers.

%and limit the Hilbert program

\paragraph{Definiteness and %generalised
  inductive definitions.}
\label{sec:defin-induct-gener}

\citet{lorenzen55} introduces the concept of \emph{definite} proposition in order to ``specify the \emph{methods} with which the subject matter [of mathematics] may be investigated resp.\ recognised'' (page~4). In doing so, he leaves the notion of schematical operation undefined: ``To operate schematically with figures is familiar to everybody'' (page~9).
\begin{quotation}
  With a view of employing no unnecessary or arbitrary prohibition, the present essay leaves the methodical frame as large as possible. A limit that is insuperable for every part of mathematics that should  be considered as ``firm'', ``secure'' (or however one would like to name it), seems to me to lie in the propositions to be ``definite''.
  
  \dotfill\smallskip

  We give therefore the following inductive definition of ``definite'':
  \begin{enumerate}[(1)]
  \item Every proposition that is decidable by schematical operations is definite.
  \item If a definite concept of proof or of refutation is stipulated for a proposition, then the proposition itself is definite, more precisely proof-definite, resp.\ refutation definite.
  \end{enumerate}

  By the methodical demand of definiteness, the impredicative conceptions are of course excluded---as demanded already by Russell and Poin\-caré---, but quantifiers are not. If \(A(x)\) is definite, then let us stipulate as refutation for the proposition \(\bigland_xA(x)\) [for all~\(x\): \(A(x)\)]: a refutation of a proposition~\(A(x_0)\). For the proposition \(\biglor_xA(x)\) [for some~\(x\): \(A(x)\)], let us stipulate as proof: the proof of a proposition~\(A(x_0)\). \citep[pages~5--6.]{lorenzen55}
\end{quotation}

\citet[§~16]{lorenzen55} considers %generalised
inductive definitions as providing operative counterparts to impredicative conceptions. He works out the example of the concept of convergent subsequence \(r_{l_*}\) of a sequence~\(r_*\) of rational numbers between~\(0\) and~\(1\) with the following proof.
\begin{quotation}
  We let \(l_1=1\). We halve then the interval~\(I_1=[0,1]\). If both halves contain infinitely many terms of the sequence~\(r_*\), then let~\(I_2\) be the left half, else the half that contains infinitely many terms. Let~\(l_2\) be the minimal number such that \(l>l_1\) and \(r_l\in I_2\). Subsequently \(I_2\)~is halved, \(I_3\)~is defined as one of the halves, then \(l_3\)~is determined analogously, etc. \citep[page~166.]{lorenzen55}
\end{quotation}
He proposes to defines the concept of an interval~\([a,a+2^{1-n}]\) containing infinitely many terms of~\(r_*\) as a relation \(n\Srel a\) by the following %generalised
inductive rules:
\[%\left\{
  \begin{aligned}
    &\begin{prooftree}
      %\hypo{\vphantom{0}}
      \infer0{1\Srel 0}
    \end{prooftree}\\[3pt]
    &\begin{prooftree}
      \hypo{n\Srel a}\hypo{\bigland_{m_0}\biglor_{m>m_0}a\le r_m\le a+2^{-n}}\infer2{n+1\Srel a}
    \end{prooftree}\\[3pt]
    &\begin{prooftree}
      \hypo{n\Srel a}\hypo{\biglor_{m_0}\bigland_{m>m_0}(r_m<a\lor r_m> a+2^{-n})}\infer2{n+1\Srel a+2^{-n}}
    \end{prooftree}
  \end{aligned}%\right.
\]
As Lorenzen notes, these rules stipulate how a proposition~\(n\Srel a\) is to be proved, but it might well be that one does not obtain a proof of neither~\(2\Srel0\) nor~\(2\Srel2^{-1}\) (an instance of the law of excluded middle).

Then he defines the sequence of indices~\(l_*\) inductively by the following inductive rules.
\[%\left\{
  \begin{aligned}
    &\begin{prooftree}
      %\hypo{\vphantom{0}}
      \infer0{l_1=1}
    \end{prooftree}\\[3pt]
    &\begin{prooftree}\hypo{l_n=k}\hypo{n+1\Srel a}\hypo{m=\min\{\,l>k:a\le r_l\le a+2^{-n}\,\}}\infer3{l_{n+1}=m}
    \end{prooftree}    
  \end{aligned}%\right.
\]
Lorenzen concludes that the propositions \(l_n=k\) are definite, so that the concept of convergent subsequence is definite, regardless of its existence.

He introduces the following notation and terminology for the %generalised
inductive definition of the relation~\(l_n=k\) between~\(n\) and~\(k\):
\[\left.
  \begin{aligned}
    &\,\to\,{1,1}\in\varrho\\
    {n,k}\in\varrho\,\land\,{n+1\Srel a}\,\land\, {m=\min\{\,l>k:a\le r_l\le a+2^{-n}\,\}}&\,\to\, {{n+1,m}\in\varrho}
  \end{aligned}\right\}=\mathfrak A(\varrho)\]
is the corresponding \emph{induction scheme} and the sought-after relation is
\(\mathsf{I}_\varrho\mathfrak A(\varrho)\),
where  \(\mathsf{I}_\varrho\) is an \emph{induction operator}: this is the inductive counterpart to the notation~\(\iota_xA(x)\) for the~\(x\) such that~\(A(x)\).

On the other hand, although generalised inductive definitions are presented as ``the method of \citealt{lorenzen55}'' by \citet[page~48]{lorenzenmyhill59}, we have not been able to spot a discussion of these in this book. See \citet[§~2]{coquand21} for the generalised inductive definition of the perfect kernel of a closed set provided by \citet{MR0104569} as a constructive analysis of the Cantor--Bendixson theorem.
See also the discussion by \citet[§51, ``Predicativity and inductive definitions'']{parsons08}%, the most important issue at stake according to us
.

% Un sujet possible serait de discuter la notion de «prédicativé généralisée» en acceptant
% les définitions inductives générales (à la Lorenzen et Martin-Löf). On pourrait discuter d’exemples
% mathématiques où l’on a besoin de ID1 (Cantor-Bendixson) et peut-être d’autres exemples où l’on
% a besoin de ID1 (open induction et plus récemment Regular Element Property).

% \subsection{Questions au sujet de Schütte}
% \label{sec:questions-au-sujet}

% \subsubsection{Halbformale Systeme}
% \label{sec:halbformale-systeme}

% Ich würde gerne verstehen, wie Schütte selbst halbformale Systeme betrachtet hat und ob die Abwesenheit eines Hinweises auf eine notwendige metalogische Untersuchung etwa eine Entwicklung
% seines Standpunkts bedeutet. Wie sehen Sie die Entwicklung von 1960 bis 1977? Kurz gefasst: Was ist ein halbformales System? Wie hat sich der Begriff eventuell verwandelt? Reinhard Kahle schreibt dazu: „Es ist Schütte (aber eben nicht Lorenzen), der die oben von uns \emph{metakalkülisch} genannte Hilbert-Regel zu
% einer \emph{objektkalkülischen} \textomega-Regel umdeutet“; diese sei bei Schütte eine „rule on the object level“. Sehen Sie das auch so? Betrifft das schon die \emph{Beweistheorie} oder erst die \emph{Proof theory}? Wie würden Sie diese „Objekt-Ebene“ beschreiben? Jedenfalls habe ich den Eindruck, dass es Schütte darum geht, den
% Augenmerk von der metalogischen Untersuchung weg auf die logische Untersuchung zu zu wenden. Vielleicht genügt es ihm auch, in seiner Einleitung von 1960 und wortgleich in seiner Introduction von 1977 auf den „konstruktiven Charakter“ und den „konstruktiven Standpunkt“ der Methoden hinzuweisen.

% \paragraph{Prädikativität}
% \label{sec:pradikativitat}

% Es kann sein, dass sich der Augenmerk der Beweistheorie mehr und mehr der Prädikativität und der Imprädikativität zugewandt hat, weil in prädikativen Systemen die „double-negation translation“ allgemein eine Rückführung von Systemen mit Tertium non datur auf intuitionistische ermöglicht. So drückt sich Gödel in
% 1931 aus. Teilen Sie diese Sichtweise? Welche Rolle spielt sie Ihrer Meinung nach in der Beweistheorie?

\paragraph{The law of excluded middle.}
\label{sec:le-tiers-exclu}

Lorenzen considers that the proof of consistency of a calculus secures the use of the law of excluded middle in this calculus:
\begin{quotation}
  In this book we shall use the logical particles according to the
  rules of so-called \emph{classical logic}. [\dots]
  
  Our treatment can be called ``constructive'' even so, since
classical logic can itself be justified from the standpoint of a
\emph{constructive logic} by way of so-called consistency proofs (cf.\
\citealp{lorenzen62}). Furthermore, for indefinite quantifiers we shall
use only constructively valid inferences. \citep[page~15.]{MR0346097}
\end{quotation}
Another way of justifying the recourse to the law of excluded middle is that the proof of consistency provides a constructive understanding of classical truth within the calculus considered, i.e.\ of the definite quantifiers governed by classical logic. 
\begin{quotation}
  [\dots] recourse
to this law is ``innocuous'' in the following sense. By the use of
excluded middle one never gets statements contradictory to those
provable without excluded middle. % In particular, all statements
% built up out of decidable elementary statements without quantifi\bs
% ers that are provable by excluded middle are also provable with\bs
% out it. 
\citep[pages~33--34.]{MR0346097}
\end{quotation}

Lorenzen therefore uses freely the law of excluded middle for natural numbers but not for real numbers.
% {\ttfamily\raggedright
%
% Quelle est la signification du tiers exclu chez Weyl et chez Lorenzen? Voir \citealt{lorenzen50}. Voir la discussion dans \citealt*{fraenkelbarhillel58} (vérifier si le discours est le même dans \citealt*{fraenkelbarhillellevy73}).
%
% Qu'assurent les preuves de non-\hspace{0pt}contradiction? Dans quelle mesure peut-on encore parler de constructions lorsqu'on exploite la non-\hspace{0pt}contradiction? Juste la construction d'un calcul? 
%
% Quelle est l'attitude de Lorenzen au sujet de LPO? Qu'est-ce qui justifie l'emploi de LPO? Cf.\ Palmgren qui propose d'utiliser le tiers exclu pour les nombres mais pas pour les fonctions.
% }\cite{B67}\cite{B67}
%
This should be compared with the Limited Principle of Omniscience (LPO) of \citet{B67}.
An analysis of LPO together with dependent choice is made by \citet{coquandpalmgren00} and with more particulars by \citet{feferman12}, and then by \cite{rathjen19}.
% \paragraph{Tiers exclu et physique.}
% \label{sec:tiers-exclu-et}
% \begin{itemize}
% \item En mathématiques, on conçoit des modèles invraisemblables et on regarde ce que ça donne: on retient les manipulations formelles non contradictoires.
% \item En physique, on fait pareil selon Weyl: les constructions symboliques n'ont peut-être pas de référent dans la nature
% \end{itemize}

% PML critique cette approche «conventionnaliste» (?) de Weyl: la physique aussi nécessite des intuitions (elle aussi a une «âme»).

% Comment justifie-t-on la loi du levier ou le principe des travaux virtuels?

% Cependant, qu'est-ce qui assure que les mathématiques sont bien adaptées à la physique? Elles sont forgées par les humains et ne modélisent pas nécessairement quelque chose.

% Pour PML, la construction symbolique est du côté de la théorie, pas du modèle. Le tiers exclu est-il dans la construction symbolique? Est-ce un métathéorème? Sur quoi est-il une hypothèse? Pas sur le monde physique!

\paragraph{Physics.}
\label{sec:physique}

\citet[page~150]{lorenzen86b} emphasises that Weyl wants mathematics to be applicable in physics and that this is decisive in his enthusiasm for operative mathematics.

The journal issue \citet{schlaudt14b} deals with the common grounds of Dingler, Weyl, and Lorenzen in the foundation of physics. We limit ourselves to the following quotation of  \citealp{lorenzen64} in the translation of \citealt[page~235]{lorenzen87b}.
% \paragraph{Thierry.}
% \label{sec:thierry}

% J’ai trouve le livre\emph{ Constructive Philosophy} (traduction en anglais, mais je n’ai pas les dernières pages)
% dans lequel Lorenzen discute un peu de son approche de la physique, qui semble différente de celle suggérée 
% par Weyl.

% Par exemple, ce serait bien de comprendre le passage

\begin{quotation}
  Of course, we have accomplished nothing by merely asserting the a priori character of protophysics. Like Kant, we must ask what makes an a priori protophysics possible. Unfortunately, the Kantian investigations of this question are completely unsatisfactory in their details. Most physicists and mathematicians
  fail to see any problem here---or even dogmatically reject the possibility of the problem. Hugo Dingler and Hermann Weyl are recent exceptions.
\end{quotation}

% \paragraph{Stefan.}
% \label{sec:stefan}

% {\ttfamily\raggedright

% % Oui, je suis d'accord pour chercher à comprendre ce passage. Pour le moment, je peux juste exprimer
% Où j'en suis par rapport à cet aspect de Lorenzen:
% \begin{itemize}
% \item il met volontiers la géométrie du côté de la physique, contrairement à l'arithmétique, je crois au sens où la géométrie se confronte à l'espace physique alors que l'arithmétique est entièrement humaine;

% \item il distingue entre physique (science) et protophysique (expériences partagées qui permettent d'élaborer cette science) comme il distingue entre géométrie et protogéométrie;

% \item il soutient que la protogéométrie mène à la géométrie euclidienne (c'est-à-dire au postulat des parallèles) et que ce n'est que dans un deuxième lieu, celui de la science, que la géométrie non-euclidienne ou riemannienne se conçoivent;

% \item j'ai un vague souvenir que pareillement la protophysique mène à la physique galiléenne (et newtonienne?) et que ce n'est que dans un deuxième lieu que les théories d'Einstein se conçoivent.
% \end{itemize}
% Ce sont je crois dans ces deux derniers points que l'à priori kantien joue un rôle.
% }

% \paragraph{Hugo Dingler.}
% \label{sec:hugo-dingler}

% Quels sont les points communs entre mathématiques et physique? Quel impact le rôle donné à la physique a-t-il sur les mathématiques? D'où vient l'intérêt de Lorenzen pour Dingler? 

% \subparagraph{Thierry.}
% \label{sec:thierry-1}

%  La fin de l’article «Sur l’histoire et l’essence de l’expériment» donne une connection, il me semble, avec l’approche de Lorenzen.

% % \subparagraph{Stefan.}
% % \label{sec:stefan-1}

% Je sais que Lorenzen considère Dingler comme une de ses références (ce que 
% j'essaie de dire par là c'est qu'il découvre chez Dingler des chemins de pensée 
% qu'il a parcouru lui aussi et dans lesquels il se reconnaît. Il raconte qu'ils 
% ont pris contact dès 1948 en rapport avec sa protogéométrie et sa protophysique. 
% C'est le seul pour lequel Lorenzen a réalisé un travail d'édition (Hugo Dingler, 
% \emph{Aufbau der exakten Fundamentalwissenschaft}, Eidos-Verlag : Munich, 1964). Il 
% lui a consacré deux articles: «Formale Logik und Arithmetik in Dinglers 
% methodischer Philosophie» (1956) et «Neue Grundlagen der Geometrie» (1984).


% \subparagraph{Norbert Schappacher.}
% \label{sec:norbert-schappacher}

% Le texte «Paul Valéry et la potentialité des mathématiques» évoque Dingler et Lorenzen:
% \url{https://irma.math.unistra.fr/~schappa/NSch/Publications_files/2016d_Valery.pdf}

% \subparagraph{Thomas Barth, 8 mars 2019.}
% \label{sec:thomas-barth-8}

% Die Behauptungen rund um Dingler in \citealt{menzlertrott01} finde ich sehr gefährlich. Ich habe 1972
% zur Kenntnis genommen, dass Lorenzen ihn als wichtigen Beitrag erwähnte und
% dass er NS-kompromittiert war. Dinglers Ablehnung der Relativitätstheorie
% wurde auch Lorenzen angehängt. Die Physiker und Mathematiker, in Deutschland
% und auch in den USA, nutzten das, um Lorenzens Philosophie zu diffamieren.
% Der O-Ton dieser Diffamierung wird von Menzler-Trott wiedergegeben.

% Sie können Anita Ehlers auch zu diesem Thema befragen. 

% \paragraph{Théorie algébrique des nombres}
% \label{sec:theor-algebr-des}

% \subparagraph{Henri.}
% \label{sec:henri}

% Une autre chose intéressante serait de rendre compte du petit livre Algebraic number theory,
% qui suit Kronecker de très près, et le compare favorablement à Dedekind. À peu près au même moment, Chevalley publie aussi un livre (les deux chez Princeton je crois) dans une direction diamétralement opposée. C’est marrant parce que Chevalley est aussi un inventeur incroyable de choses extrêmement concrètes,
% comme ses séries infinies de groupes simples.

% \subparagraph{Stefan.}
% \label{sec:stefan-2}

% C'est peut-être \emph{Class Field Theory}, paru en 1954 aux éditions de l'université
% de Nagoya. On l'a à Besançon et j'ai trouvé un pdf:
% \url{http://neuwirth.perso.math.cnrs.fr/lorenzen/REFERENCES/weyl/chevalley-class_field_theory-1954.pdf}

% \subparagraph{Thierry.}
% \label{sec:thierry-2}

% Je me rappelle qu’Edwards disait que Weyl ne suivait pas vraiment Kronecker (à vérifier).

% En tout cas, Weyl parle de Chevalley à la fin de son livre.

% Voila ce qu’Edwards écrit sur le traitement de Weyl, mais après une lecture rapide de Weyl, je pense que ce n’est pas vraiment «fair» et que Weyl doit bien insister sur des points importants du traitement de Kronecker. En tout cas, la discussion Dedekind/Kronecker est vraiment liée à la discussion
% prédicatif/imprédicatif

% \begin{quotation}
%   Today most mathematicians who know about Kronecker's theory of divisors know about it from having read Hermann Weyl's lectures on algebraic number theory [We], and regard it, as Weyl did, as an alternative to Dedekind's theory of ideals. Weyl's axiomatization of what he calls ``Kronecker's'' theory
%   is built -- as Dedekind's theory was built -- around unique factorization. However, in presenting the theory in this way, Weyl overlooks one of Kronecker's most valuable ideas, namely, the idea that the objective of the theory is to define greatest common divisors, not to achieve factorization into primes.
% \end{quotation}

% \subparagraph{Henri.}
% \label{sec:henri-1}

% Autant que je me souvienne  Weyl, comme  Edwards,  note que la théorie des diviseurs
% de Kronecker est beaucoup plus générale que celle de Dedekind.

% Malheureusement, aussi bien Weyl qu’Edwards ne donnent aucun exemple qui ne soit pas
% de dimension 1.

% Aujourd’hui, on appelle la théorie de Kronecker  théorie des diviseurs d’André Weil.

% Ce qui est dû au fait que Weil n’a pas dit que sa théorie était une reformulation
% (soi-disant sans calcul) de celle de Kronecker.

% Il remplace les calculs par des idéaux premiers de hauteur 1 particuliers et tout
% est censé devenir clair sous ce nouvel éclairage-\hspace{0pt}obscurcissement.

% En tout cas, Weyl et Edwards manquent un brin de pédagogie
% car on est assez vite perdu dans leurs calculs.

% Cela concerne la théorie algébrique des nombres.


% \subparagraph{Claude.}
% \label{sec:claude}

% Un article historique de Steven Andrew Kieffer dans lequel il est
% question de (dans le désordre): Kronecker, Dedekind, Hilbert, Hensel,
% Artin, Hasse, Taussky, Zassenhaus, Lehmer, Weyl, Kummer: \url{http://www.cecm.sfu.ca/CAG/theses/kieffer.pdf}

% \section{Point d'accumulation d'une suite bornée de réels}
% \label{sec:point-dacc-dune}

% die im Anfang vom § 16 von \citet{lorenzen55} betrachtete induktive Definition dafür, dass 
% eine Folge reeller Zahlen in [0,1] eine Häufungspunkt hat.

% \section{Lorenzen 1965}
% \label{sec:lorenzen-1965}

% \subsection{Angelelli}
% \label{sec:angelelli}

\paragraph{Abstraction and its reception by Angelelli.}

Ignacio Angelelli proposes another emphasis of Lorenzen's reception of Weyl's work: abstract objects.

\begin{quotation}
  In the history of philosophy the word ``abstraction'' and cognate expressions (``abstract'',
etc.)\ have had a \emph{genuine} meaning, according to which abstraction involves an
operation by which something is \emph{retained} and something else is \emph{left out} [\dots]. In the special sense relevant for philosophy, the operation is intellectual, and the retaining and leaving out pertain to
our mental consideration of things. \cite[page~11.]{angelelli04}
\end{quotation}

He underlines the great relevance of the conception expounded in \citealt{lorenzen55}.
\begin{quotation}
  Thereby [that is according to what is customary since Frege and Russell] abstrac\bs
tion is to be reduced to the introduction of ``classes''. However, we will see below
that classes are nothing else but a special kind of abstract objects. \citep[Translation of {\citealt[page~101]{lorenzen55}}, in][page~26.]{angelelli04}
\end{quotation}

\citet{lorenzen55} introduces abstraction as follows: to define abstract objects as given concrete objects together with an equivalence relation that makes some of them equal; a statement about the abstract object is a statement about the concrete object that is invariant with respect to the equivalence relation. This should be compared to Bishop's conception of equality in constructive mathematics \citep[see][page~13]{B67}. In particular, classes (i.e.\ sets) of numbers are introduced as the abstraction of arithmetical predicates for the relation of logical equivalence, as does Weyl in our first citation of \emph{The continuum} on page~\pageref{pred}.

\citet[and in all his writings on abstraction cited there]{angelelli04} credits Lorenzen for having set up a modern theory of abstraction. He does so as well in several reviews.
\begin{quotation}
% Readers who are interested in the philosophy of mathematics should take into account Weyl's later remarks on Paul Lorenzen's work as representing the best furtherance of his program (gangbarster Weg [A. Weyl, Gesammelte Abhandlungen, Bände I, II, III, IV, Springer, Berlin, 1968; MR0230597]). Weyl (died 1955) referred to Lorenzen's Einführung in die operative Logik und Ma\-thematik [Springer, Berlin, 1955; MR0072065] without being able to know of Lorenzen's later work [Differential and integral, Univ. Texas Press, Austin, TX, 1970; MR0346097] (cf. also Lorenzen's brief remarks to the second edition of his Einführung [op. cit., second edition, 1968: MR0241272]).

% Readers who are logicians should not be discouraged by Weyl's very clumsy, if not defective, presentation of quantification theory. This is amazing, forty years after Frege's creation of predicate logic in 1879. Other shortcomings concerning logic are a hasty discussion of the autological-heterological paradox (rejected as ``nonsense'' without any explanation, pp. 6–7), and Weyl's not clearly presented view that two relational sentences like ``4<5'' and ``5>4'' ``express one and the same relation''. The logical aspects that deserve careful consideration are (a) the author's forceful, noncompromising awareness of the ``vicious circle'' that may arise from the quantification of predicate letters, (b) his rejection of the Cantorian notion of set as a ``gathering… surveyed as a whole by consciousness'' (p. 23) together with his negative view of Zermelo's axiomatization of set theory, more than implicit in Weyl's rejection of the prevailing view of axioms as stipulations as well as in his remarks on the ``hypothetico-deductive game'' as both ``worthless'' and ``logically untenable'' (end of §3). 
  Thus Weyl's view of sets is neither the naive Cantorian nor the axiomatic; Weyl wants his sets to emerge from properties. If the reader asks ``how?'' no clear answer will be found in this volume, except for hints at ``ideal elements'' and ``definitions by abstraction''. \citet[pp.~45–47]{weyl87} rightly points to Frege as his source in this respect but he is confused about abstraction; Frege did not really do abstraction %but proceeded according to a method this reviewer has labelled ``the looking-around method'' [cf., e.g., \citealp{angelelli84}]
  [\dots]. Here again the consideration of Lorenzen's work is recommended, at any rate for the understanding of what is still unclear or undeveloped in Weyl. (\citealp{angelelli91}.)\medskip
  
%   The second criticism has to do with abstraction. The author tries hard, in fact harder than most critics, but being unaware of modern abstraction (Peano-Weyl-Lorenzen), he falls short of a right understanding of this very entangled issue. Here is a sketch of the view which the reviewer considers correct. Cantor and most pre-Fregean philosophers of arithmetic insisted on defining number as the result of an abstraction on the set of objects to be counted. But traditional abstraction lacked the proper analysis of the abstractive process as relative to a previously specified equivalence relation (in this case bijection between sets) and consequently ``injected'' abstraction in the wrong place, namely in each individual unit, generating the nonsensical ``pure Ones'' so rightly criticized by Frege. On the other hand, Frege and Russell were no less wrong, in that they dismissed abstraction and ended up with what the reviewer has called the ``looking around'' method [cf. the reviewer, Studia Leibnitiana Sonderheft 8 (1979), 108–123; Philos. Natur. 21 (1984), no. 2, 453–471; Anuar. Filos. 14 (1981), no. 2, 9–21]. 
  The traditional and Cantorian insistence on number as an abstractum was basically right; it only needed a better theory of abstraction. This was done, apparently for the first time, by P. \citet[Section~13]{lorenzen55}. (\citealp{angelelli86}.)\medskip
  
% One misses any reference, in the editor's text, to Paul Lorenzen, whose work was celebrated by Weyl in the mid 1950's as ``the most feasible approach to his program'' (``den gangbarsten Weg'' [cf. H. Weyl, Gesammelte Abhandlungen. Bände I, II, III, IV, Springer, Berlin, 1968; MR0230597 (Band II, p. 180)]). \citep{angelelli97}

% {Reviewer's remarks: It is difficult to grasp what is exactly the author's definitive opinion concerning the basic question of his paper. Also, in an essay dealing with Das Kontinuum and Weyl's philosophico-foundational connections, one misses a reference to Paul Lorenzen, whose work was celebrated by Weyl in the mid 1950s as ``the most feasible approach to his foundational program (``den gangbarsten Weg'' [cf. H. Weyl, Gesammelte Abhandlungen. Bände I, II, III, IV, Springer, Berlin, 1968; MR0230597 (p. 180)])}
% \citep{angelelli98}

% Reviewer's remarks: The author makes a point of closely following Frege, and notifies the reader when he deviates from Fregean doctrines (as regarding quantitative domains). Since he does not say anything in the case of abstraction, the reader may be misled into assuming that abstraction was a concept cherished by Frege. The historical fact is, however, that Frege totally rejected abstraction as a method worthwhile to consider in the foundations of mathematics or in logic. Expressions such as ``Fregean abstraction principle'', or worse: ``Fregean abstraction'' (footnote~26) would shock Frege. On the other hand, however, Frege would quickly notice that the term ``abstraction'' does not appear to be used by the author in the sense of mentally disregarding something (``retaining something, leaving out something'' as Locke says), which is the sense that Frege assigned to the word, in agreement with the entire philosophical and logical tradition. Frege would discover that the author uses ``abstraction'' in order to refer to the first part of Frege's most cherished method, applied in his definition of number as well as in the introduction of sets.
  
% Frege's method has two stages. First stage: the author's ``Hume principle'', second stage: the author's ``explicit definition''. (Incidentally, Frege does not ``switch'' from the former to the latter, as claimed by the author, in the sense of replacing one method by another: the second is linked to the first which, obviously, complicates Hale's, and others', assertion that at a certain point in Grundlagen Frege proves Hume's principle from the explicit definition, cf. (1.4).) That and how Frege's method ended up, as in Hale's paper, being referred to as ``abstraction'' is one of the most complex and curious stories in the development of modern logic. 
The story begins with Peano who, contrary to Frege, was interested in abstraction and gave a place to it in logical theory under the label of ``definitions by abstraction''. % Peano's definitions by abstraction and Frege's method have important structural resemblances. At a certain point, there was a strange, unfortunate ``crossing'' of Peano's and Frege's methods. One result was that the phrase ``definition by abstraction'', or just ``abstraction'' began to be applied to Frege's method (in Hale's paper, as in other recent literature on Frege, there is a further move: ``abstraction'' is applied to just the first half of Frege's method, the so-called ``Hume principle''), although Frege was neither interested in abstraction nor did his method aim at performing any abstraction, i.e.\ at ``mentally disregarding'' anything. This became, and continues to be, as exemplified by Hale's paper, one of the prominent pseudo-uses of ``abstraction'' in the 20th century
[\dots] To be sure, Frege's (two-stage!) method can be ``overhauled'', or reconstructed as genuine abstraction. To this end, first, Frege's method should be dismantled and, secondly, rebuilt, according to the guidelines sketched by Peano, praised but only hinted at by Hermann Weyl, and systematically developed by Paul Lorenzen. In the latter's book [\citealp[§6]{MR0209410}], or in his earlier work [\citealp{lorenzen55}], real numbers are in fact introduced by abstraction---by genuine abstraction, that is, not by any pseudo-abstraction. %One misses in Hale's paper any reference to Lorenzen's work.
(\citealp{angelelli01}.)
\end{quotation}

Lorenzen, as \citet[page~15]{B67}, defines real numbers as Cauchy sequences together with the equivalence relation that their difference is a null sequence, instead of resorting to equivalence classes, i.e.\ quotients. The consideration of equivalence classes leads to the difficulty of choosing representatives and e.g.\ requires countable choice for keeping constructive the proof by \citet[page~25]{B67} that the real numbers are uncountable. Equality in the \citet{hottbook} proposes a way to define quotients that solves this issue.
\[*\ *\ *\]

Hermann Weyl and Paul Lorenzen share a profound interest into physics and especially into the continuum. They consider that mathematical analysis must be built up on the concept of number by a process called by the former ``the mathematical process'' and by the latter ``logical reflection'', leading to the concepts of function, relation, inductive definition. Both call for retrieving the corpus of classical analysis without resorting to impredicative concept formations like Dedekind cuts and do so by deepening the logical analysis of the objects involved, in particular by a better understanding of abstraction. As Poincaré asserted, the real numbers form an indefinite totality; \citet{weyl18} concludes that the least-upper-bound property ``must certainly be abandoned''; \citet{MR0043748,lorenzen55} retrieves it by introducing language levels; \citet{MR0209410} avoids them by considerations of definiteness. 

Weyl's enthusiasm for Lorenzen's operative mathematics witnesses how new logical insights can provide ``pillars of enduring strength'' for analysis and how logic, by specifying the way mathematical objects are given to us, is instrumental in this justification.

\paragraph{Acknowledgment.}

The authors thank Mark van Atten for providing them with the administrative documents relative to Lorenzen's visit to the Institute for Advanced Study.
They thank Jan von Plato for sharing his findings about Lorenzen in the Gödel papers. 
% \section{Lorenzen 1978}
% \label{sec:lorenzen-1978}


\bibliography{../Lorenzen.bib,lorenzen-weyl.bib,../lorenzen_s_algebraic_and_logistic_investigations_on_free_lattices/lorenzen-algebraic_and_logistic_investigations_on_free_lattices.bib}


\end{document}
