This collection of papers, celebrating the contributions of Swedish
logician Dag Prawitz to Proof Theory, has been assembled from those
presented at the Natural Deduction conference organized in Rio de
Janeiro to honour his seminal research. Dag Prawitz's work forms the
basis of intuitionistic type theory and his inversion principle
constitutes the foundation of most modern accounts of proof-theoretic
semantics in Logic, Linguistics and Theoretical Computer Science.
The range of contributions includes material on the extension of natural
deduction with higher-order rules, as opposed to higher-order
connectives, and a paper discussing the application of natural deduction
rules to dealing with equality in predicate calculus. The volume
continues with a key chapter summarizing work on the extension of the
Curry-Howard isomorphism (itself a by-product of the work on natural
deduction), via methods of category theory that have been successfully
applied to linear logic, as well as many other contributions from highly
regarded authorities. With an illustrious group of contributors
addressing a wealth of topics and applications, this volume is a
valuable addition to the libraries of academics in the multiple
disciplines whose development has been given added scope by the
methodologies supplied by natural deduction. The volume is
representative of the rich and varied directions that Prawitz work has
inspired in the area of natural deduction.