Abstract

We discuss Lorenzen’s consistency proof for ramified type theory without reducibility, published in 1951, in its historical context and highlight Lorenzen’s contribution to the development of modern proof theory, notably by the introduction of the ω\documentclass[12pt]{minimal} \usepackage{amsmath} \usepackage{wasysym} \usepackage{amsfonts} \usepackage{amssymb} \usepackage{amsbsy} \usepackage{mathrsfs} \usepackage{upgreek} \setlength{\oddsidemargin}{-69pt} \begin{document}$$\omega $$\end{document}-rule.