Lorenzen’s operative justification of intuitionistic logic

Abstract

With his Introduction to Operative Logic and Mathematics¹, which first appeared in 1955, Paul Lorenzen became an exponent of an approach to the foundations of logic and mathematics, which is both formalistic and intuitionistic in spirit. Formalistic because its basis is the purely syntactical handling of symbols—or ‘figures’, as Lorenzen preferred to say —, and intuitionistic because the insight into the validity of admissibility statements justifies the laws of logic. It is also intuitionistic with respect to its result, as Heyting’s formalism of intuitionistic logic is legitimatised this way. Along with taking formal calculi as its basis, the notion of an inductive definition becomes fundamental. Together with a theory of abstraction and the idea of transfinitely interating inductive definitions, Lorenzen devised a novel foundation for mathematics, many aspects of which still deserve attention. When he wrote his Operative Logic, neither a full-fledged theory of inductive definitions nor a proof-theoretic semantics for logical constants was available. A decade later, Lorenzen’s inversion principle was used and extended by Prawitz (Prawitz 1965) in his theory of natural deduction, and in the 1970s, the idea of inversion was used for a logical semantics in terms of proofs by Dummett, Martin-Löf, Prawitz and others. Prawitz and others. Another aspect which makes Lorenzen’ theory interesting from a modern point of view, is that in his protologic he anticipated certain views of rule-based reasoning and free equality which much later became central to the theory of resolution and logic programming.

Einführung in die operative Logik und Mathematik’ (Lorenzen 1955), henceforth OL. A major earlier paper propagating the operative approach is (Lorenzen 1950). For a biography of Lorenzen see (Thiel 1996), for a bibliography of his work see (Lorenzen 1996).