Lorenzen’s operative justification of intuitionistic logic
With his Introduction to Operative Logic and Mathematics1, 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.
KeywordsIntuitionistic Logic Natural Deduction Logical Constant Elimination Rule Introduction Rule
Unable to display preview. Download preview PDF.