U of A

Mailing address:

Dept. of Philosophy
University of Alberta
2-40 Assiniboia Hall
Edmonton, AB, T6G 2E7

Email address:

bimbo at ualberta dot ca

Erdös number:


Gödel number:

∞ (None, really.)


Association for Symbolic
   Logic (ASL)

American Mathematical
   Society (AMS)

Society for Exact
   Philosophy (SEP)

American Philosophical
   Association (APA)

Friends of the Stanford
   Encyclopedia of

Academic degrees:

PhD    (philosophy and
   cognitive science)
Doctorate    (logic)
CoHAS    (philosophy)
Diploma with highest
   distinction (philosophy)

Latest update on:

July 13th, 2014

Professor Katalin Bimbó


My main research area is logic.  I am especially interested in nonclassical logics, including relevance and substructural logics, modal logics, combinatory logics and λ-calculiNonclassical 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-world semantics for normal modal logics, and have been the preferred sort of semantics for decades.  Some 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 four-valued semantics for the minimal substructural logic.  We continue to work on questions related to the semantics of non-classical logics, especially, concerning the three-termed relational semantics within a SSHRC IG.

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 Curry–Howard 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 a couple of years 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 well-known 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 has appeared in the Logica Universalis this year.  I have been writing a book on proof theory in the last two years or so, which will be published soon.

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.


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 taught 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

  • K. Bimbó, Proof Theory: Sequent Calculi and Related Formalisms, CRC Press, Boca Raton, FL, 2014 (to appear).   [The book @ the CRC web site.]  
    A growing collection of solutions to selected exercises in the book.

    cover image of the book on 
proof theory authored by K. Bimbó

  • K. Bimbó and J. M. Dunn, “Extracting BB'IW inhabitants of simple types from proofs in the sequent calculus Tt for implicational ticket entailment,” Logica Universalis 8(2) (2014), pp. 141-236.
  • K. Bimbó and J. M. Dunn, “On the decidability of implicational ticket entailment,” Journal of Symbolic Logic 78(1) (2013), pp. 214-236.   [JSL @ JSTOR.]
  • K. Bimbó and J. M. Dunn, “New consecution calculi for Rt,” Notre Dame Journal of Formal Logic 53(4) (2012), pp. 491-509.   [NDJFL @ Project Euclid.]
  • K. Bimbó, Combinatory Logic: Pure, Applied and Typed, CRC Press, Boca Raton, FL, 2012.   [The book @ the CRC Press web site.]

    cover image of the book on 
combinatory logic authored by K. Bimbó

  • K. Bimbó and J. M. Dunn, “Calculi for symmetric generalized Galois logics,” In: A Festschrift for Joachim Lambek, J. van Benthem and M. Moortgat (eds.), Linguistic Analysis, 36 (2010), pp. 307-343.
  • K. Bimbó, “Schönfinkel-type operators for classical logic,” Studia Logica 95 (2010), pp. 355-378.
  • K. Bimbó and J. M. Dunn, “Symmetric generalized Galois logics,” Logica Universalis 3 (2009), pp. 125-152.
  • K. Bimbó, J. M. Dunn and R. D. Maddux, “Relevance logics and relation algebras,” Review of Symbolic Logic 2 (2009), pp. 102-131.
  • K. Bimbó, Combinatory logic,” Stanford Encyclopedia of Philosophy.   [SEP @ Stanford University.]
  • K. Bimbó, “Dual gaggle semantics for entailment,” Notre Dame Journal of Formal Logic 50 (2009), pp. 23-41.   [NDJFL @ Project Euclid.]
  • K. Bimbó and J. M. Dunn, Generalized Galois Logics. Relational Semantics of Nonclassical Logical Calculi, CSLI Lecture Notes, v. 188, CSLI, Stanford, CA, 2008.   [The book @ CSLI Publications and @ the University of Chicago Press.]

    cover image of the book 
authored by K. Bimbó and J. M. Dunn

  • K. Bimbó, “Functorial duality for ortholattices and De Morgan lattices,” Logica Universalis 1 (2007), pp. 311-333.
  • K. Bimbó, LEt, LR°ˆ˜, LK and cut free proofs,” Journal of Philosophical Logic 36 (2007), pp. 557-570.
  • K. Bimbó, “Relevance logics,” In: Philosophy of Logic, D. Jacquette (ed.), (volume 5 of Handbook of the Philosophy of Science, D. Gabbay, P. Thagard, J. Woods (eds.)), Elsevier (North-Holland), 2006, pp. 723-789.   [The Handbook of the Philosophy of Science project and the book @ at Elsevier.]
  • K. Bimbó, “Admissibility of cut in LC with fixed point combinator,” Studia Logica 81 (2005), pp. 399-423.
  • K. Bimbó, “The Church-Rosser property in symmetric combinatory logic,” Journal of Symbolic Logic 70 (2005), pp. 536-556.   [JSL at JSTOR.]
  • K. Bimbó and J. M. Dunn, “Relational semantics for Kleene logic and action logic,” Notre Dame Journal of Formal Logic 46 (2005), pp. 461-490.   [NDJFL @ Project Euclid.]
  • K. Bimbó, “Types of I-free hereditary right maximal terms,” Journal of Philosophical Logic 34 (2005), pp. 607-620.
  • K. Bimbó, “Semantics for dual and symmetric combinatory calculi,” Journal of Philosophical Logic, 33 (2004), pp. 125-153.
  • K. Bimbó, “A set theoretical semantics for full propositional linear logic,” (abstract), Bulletin of Symbolic Logic 10 (2004), pp. 136.
  • K. Bimbó, “The Church-Rosser property in dual combinatory logic,” Journal of Symbolic Logic 68 (2003), pp. 132-152.   [JSL @ JSTOR.]
  • K. Bimbó and J. M. Dunn, “Four-valued logic,” Notre Dame Journal of Formal Logic 42 (2002), pp. 171-192.   [NDJFL @ Project Euclid.]
  • K. Bimbó, “Semantics for the structurally free logic LC+,” Logic Journal of IGPL, 9 (2001), pp. 525-539.
  • K. Bimbó, “Kripke semantics for structurally free logics without distributivity,” (abstract), Bulletin of Symbolic Logic, 6 (2000), pp. 248-249.
  • K. Bimbó and J. M. Dunn, “Two extensions of the structurally free logic LC,” Logic Journal of IGPL 6 (1998), pp. 403-424.
  • K. Bimbó, “Specificity and definiteness of temporality in Hungarian,” In: J. Bernard and K. Neumer (eds.), Zeichen, Sprache, Bewuβtsein. Österreichisch-Ungarische Dokumente zur Semiotik und Philosophie 2, ÖGS-ISSS, Wien-Budapest, 1994, pp. 7-25.
  • K. Bimbó, “Are the ‘and’ and ‘.’ the same sentence connectives?,” In: J. Darski and Z. Vetulani (eds.), Akten des 26. linguistischen Kolloquiums, v.2, Max Niemeyer, Tübingen, 1993, pp. 485-490.
  • K. Bimbó, (ed.), Proceedings of the 4th Symposium on Logic and Language, Áron Publishers, Budapest, 1993. (with a co-editor)
  • K. Bimbó, “On the problem of conditional statements,” In: V. A. Smirnov, P. I. Bystrov and A. S. Karpenko (eds.), Filosofskie osnovaniya neklassicheskikh logik, Institut Filosofii AN SSSR, Moscow, 1990, pp. 12-25.
  • K. Bimbó, “Translation of three-valued logics into sequent calculi,” In: Yu. V. Ivlev (ed.), Sovremennaya logika i metodologiya nauki, Izdatel'stvo MGU, Moscow, 1987, pp. 108-119.