Mailing address: Dept. of Philosophy
Email address:
Erdös number: Three
Gödel number: ∞ (None, really.)
Memberships: Association for Symbolic
Academic degrees: PhD (philosophy and
Latest update on: March 3rd, 2014 
Professor
Katalin Bimbó
Research My main research area is logic. I am especially interested in nonclassical logics, including relevance and substructural logics, modal logics, combinatory logics and λcalculi. Nonclassical logics were first introduced as a solution to philosophical problems such as the problem of implication and entailment. Later on, new logics emerged in many disciplines from mathematics and computer science to linguistics. Some of my research interests — beyond logic and the philosophy of logic — are connected to those areas. I have a keen interest in the philosophy of mathematics, in particular, in the foundations of mathematics. I also actively follow developments in the philosophy of computer science and informatics, especially, concerning questions related to theoretical computer science — such as algorithmics, programming language design, information theory, complexity theory and cyber security. Earlier, I worked on some questions in the semantics of natural languages, primarily, using modal (tense) logics and discourse representation theory. Some of my research results concern semantics for various nonclassical logics (e.g., calculi for combinatory logic). J. Michael Dunn and I wrote a book on the relational semantics of nonclassical logical calculi. These kinds of semantics generalize Kripke's possible worlds semantics for normal modal logics, and have been the preferred sort of semantics for decades. A few years ago, we worked out representations for Kleene logic and action logic, which are closely related to dynamic logic. We also collaborated on defining a fourvalued semantics for the minimal substructural logic. A more precise characterization of classes of structures for various nonclassical logics leads straightforwardly to topological frames. I proved topological duality theorems for ortho and De Morgan lattices and for the algebra of the logic of entailment. These duality theorems provide plenty of insights into the logics themselves, because interpretations are maps in a category. Combinatory logics and λcalculi are connected to other nonclassical logics in various ways, one of which is the CurryHoward correspondence. Certain combinatory terms are equivalent to proofs in various nonclassical logics; therefore, the question of decidability turns into the question of inhabitation. Combinatory logic in itself is an elegant and powerful formalism that can represent computable functions — just as Turing machines and Markov algorithms can. A book on combinatory logic that I wrote appeared not long ago. The proof theory of nonclassical logics sometimes gets tricky. The original classical sequent calculus is a seemingly simple proof system, but in reality, the proofs are tightly controlled — as evidenced by the cut theorem. Some wellknown relevance logics cannot be formalized as extensions of the associative Lambek calculus, which causes various “technical complications.” I succeeded in defining sequent calculi for some of these relevance logics together with proving the cut theorem for them. The purely inductive proofs that I used to prove the cut theorem for the single cut rule yield a purely inductive cut proof for LK, Gentzen's original sequent calculus for classical logic — without a detour through mix. A major research project that I and J. Michael Dunn worked on within my SSHRC SRG, was the problem of the decidability of the implicational fragment of ticket entailment. We solved the decidability problem of the logic of implicational ticket entailment, which was open for more than 50 years. The two papers where we present and explain these results appeared in the NDJFL and in the JSL. We are working on expanding the Curry–Howard correspondence to various implicational logics (beyond intuitionistic logic) to match combinators and classes of sequent calculus proofs. Our first paper on inhabitant extraction is soon to appear in the Logica Universalis. I have been working on a book manuscript on proof theory in the last couple of years; the product of this project — a new book — is scheduled to appear this year. Obviously, I believe that logic — together with its many connections and offsprings — is an exciting and thriving field of research. I received a Faculty of Arts Research Excellence Award in 2012.
Teaching In the 2014/15 academic year I will not teach, because I will be on sabbatical. In the winter term of the 2013/14 academic year I teach Phil 422: Topics in Advanced Symbolic Logic together with Phil 522: Topics in Logic and Phil 120: Symbolic Logic 1. In the fall term of the 2013/14 academic year I taught Phil 220: Symbolic Logic 2.
Selected publications
