PROALG · Proof-theoretic methods in algebra

Proof-theoretic methods in algebra

Executive Summary: The overall goal of the project was to develop and exploit proof-theoretic methods for ordered algebraic structures. Traditionally, algebra and proof theory represent two distinct approaches within logic: the former concerned with semantic meaning and structures, the latter with syntactic and algorithmic aspects. In many intriguing cases, however, methods from one field have been essential to obtaining proofs in the other. In particular, proof-theoretic techniques have been used to establish important results for classes of algebras in the framework of residuated lattices. This includes both algebras for a wide range of non-classical logics investigated across mathematics, computer science, philosophy, and linguistics, and also important examples from algebra such as lattice-ordered groups. The work on the project was conducted by myself together with Leonardo Cabrer, a postdoc from Argentina (now a Marie Curie Fellow in Florence), my doctoral students Christoph Röthlisberger and Jonas Rogger (supported by a Swiss National Science Foundation project), and co-workers from Austria, France, Italy, Spain, the Netherlands, the USA, Argentina, and Colombia. Regarding the scientific objectives of the project, many of these have been met and have led inevitably to interesting new research questions. One significant part of the project was concerned with exploiting the relationship between proof theory and algebra to investigate fuzzy modal logics suitable for modelling reasoning about modalities such as necessity and uncertainty in the presence of vagueness. In a journal paper with Nicola Olivetti and a recent conference paper with my doctoral student Jonas Rogger, Xavier Caicedo, and Ricardo Rodriguez, I have defined both new calculi and new semantics, leading to decidability and complexity results and answering also an open problem for the decidability of the one-variable fragment of first-order Goedel logic. Moreover, in related ongoing work with Nikolaos Galatos, I have defined new proof systems for lattice-ordered groups and used these systems to obtain syntactic proofs of fundamental theorems for this class of algebras, as well as a first complexity result for the class. A second core topic of the project has been interpolation and amalgamation, a key example of the fruitful interaction of algebra and logic. A seventy page journal paper with Franco Montagna and Constantine Tsinakis on this topic in the context of ordered algebras has just been accepted, and I also have a journal paper published with Enrico Marchioni which describes the limits of Craig interpolation in logics based on semilinear residuated lattices and gives a complete description of the situation for extensions of the logic R-mingle. The relationship between proof theory and algebra has also played in a crucial role in joint work with my doctoral student Christoph Röthlisberger on admissibility in finite algebras (equivalently, finite-valued logics). We have two journal papers and a conference paper published on this topic, and I also have a published journal paper with Petr Cintula on admissibility in fragments of intermediate logics and a submitted paper with Leonardo Cabrer on relationships between admissibility and duality. Finally, I have contributed a chapter on proof theory to the handbook of mathematical fuzzy logic.

Data: CORDIS, © European Union