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, 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. (shrink)

The method of morphisms is a well-known application of Dialectica categories to set theory. In a previous work, Valeria de Paiva and the author have asked how much of the Axiom of Choice is needed in order to carry out the referred applications of such method. In this paper, we show that, when considered in their full generality, those applications of Dialectica categories give rise to equivalents of either the Axiom of Choice or Partition Principle —which is a consequence of (...) $\textbf{AC}$ whose precise status of its relationship with$\textbf{AC}$ itself is an open problem for more than a hundred years. (shrink)

When Gödel developed his functional interpretation, also known as the Dialectica interpretation, his aim was to prove consistency of first order arithmetic by reducing it to a quantifier-free theory with finite types. Like other functional interpretations Gödel’s Dialectica interpretation gives rise to category theoretic constructions that serve both as new models for logic and semantics and as tools for analysing and understanding various aspects of the Dialectica interpretation itself. Gödel’s Dialectica interpretation gives rise to the Dialectica categories , in: Contemp. (...) Math., vol. 92, Amer. Math. Soc., Providence, RI, 1989, pp. 47–62] and J.M.E. Hyland in [J.M.E. Hyland, Proof theory in the abstract, Ann. Pure Appl. Logic 114 43–78, Commemorative Symposium Dedicated to Anne S. Troelstra ]). These categories are symmetric monoidal closed and have finite products and weak coproducts, but they are not Cartesian closed in general. We give an analysis of how to obtain weakly Cartesian closed and Cartesian closed Dialectica categories, and we also reflect on what the analysis might tell us about the Dialectica interpretation. (shrink)