Prof. Katalin Bimbo
Teaching Research Contact and other info

Fall 2016
PHIL 220: Symbolic Logic 2
PHIL 365: Risk, Choice and Rationality

Winter 2017
PHIL 367: Philosophy of Computing
PHIL 420/522: Metalogic/Topics in Logic

Other courses

I taught the following philosophy courses (some of them more than once) in the last several years. (These are all “PHIL” courses, listed by number, in decreasing order.)

  • 422/522 Topic: Proof theory of classical and substructural logics
  • 422/522 Topic: Computability and Gödel's incompleteness theorems
  • 422/522 Topic: Gaggle theory applied to modal, relevance and other non-classical logics
  • 421/522 Modal Logic/Topics in Logic
  • 420/522 Metalogic/Topics in Logic
  • 367 Introduction to the Philosophy of Mathematics
  • 365 Philosophy of Computing
  • 325 Risk, Choice and Rationality
  • 220 Symbolic Logic 2
  • 120 Symbolic Logic 1

My main research area is logic.  I am especially interested in nonclassical logics, including relevance and substructural logics, modal logics, combinatory logic 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 other disciplines — from mathematics and computer science to linguistics.  Some of my research interests — beyond logic and the philosophy of logic — are connected to the latter areas.  I have a keen interest in the philosophy of mathematics, in particular, in the foundations of mathematics.  I also try to follow the latest developments in the philosophy of computer science and informatics, especially, those that concern 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 (specifically, temporal/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 minimal substructural logic.  We continue to work — within a SSHRC IG — on problems related to the semantics of non-classical logics, primarily, on questions connected to the three-termed relational semantics. The Third Workshop (poster), which is thematically connected to this project, will take place on May 16–17, 2016, at the University of Alberta.

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 viewed as maps in a category.

Combinatory logic and λ-calculi are connected to other nonclassical logics in various ways, one of which is the Curry–Howard correspondence (CHC).  J. Michael Dunn and I wrote a paper not long ago about extracting combinatory inhabitants from proofs in a sequent calculus for implicational ticket entailment.  This is first step to extend CHC into new directions.  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 or register 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 really 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.  A major research project that I and J. Michael Dunn worked on (as a SSHRC SRG), was the problem of the decidability of the implicational fragment of ticket entailment, which remained open for over 50 years.  Our proof was made possible by our new conceptualization of a sequent calculus for implicational R.  I have been writing a book on proof theory in the last years, which has appeared not long ago.  In the summer of 2014, I closed another long-open problem: I proved that MELL, the multiplicative–exponential fragment of linear logic is decidable.

I am certain 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.

Mailing address:

University of Alberta
Department of Philosophy
2-40 Assiniboia Hall
Edmonton, AB T6G 2E7, Canada

Email address:

bimbo at ualberta dot ca

Page updated on:

April 4th, 2016

My Erdös number:

Three (i.e., 3)


Association for Symbolic Logic (ASL)

American Mathematical Society (AMS)

Society for Exact Philosophy (SEP)

American Philosophical Association (APA)

Friends of the Stanford Encyclopedia
   of Philosophy

Some U of A links:

University of Alberta

Department of Philosophy

Publications selected from the 21st century
cover image of the book on proof theory authored by K. Bimbó cover image of the book on combinatory logic authored by K. Bimbó cover image of the book authored by K. Bimbó and J. M. Dunn
  • K. Bimbó (ed.), J. Michael Dunn on Information Based Logics, Outstanding Contributions to Logic, vol. 8, Springer International Publishing AG, Switzerland, 2016.  [The book @ Springer's web site, @ Springer Link. Table of contents (PDF).]
  • K. Bimbó, “The decidability of the intensional fragment of classical linear logic,” Theoretical Computer Science 597 (2015), pp. 1–17.
  • K. Bimbó, Proof Theory: Sequent Calculi and Related Formalisms, CRC Press, Boca Raton, FL, 2015.   [The book @ the CRC web site.]  
    (A growing collection of solutions to selected exercises from the book.)
  • K. Bimbó and J. M. Dunn, “Extracting BB'IW inhabitants of simple types from proofs in the sequent calculus LTt for implicational ticket entailment,” Logica Universalis 8(2) (2014), pp. 141–164.
  • K. Bimbó and J. M. Dunn, “On the decidability of implicational ticket entailment,” Journal of Symbolic Logic 78(1) (2013), pp. 214–236.   [JSL @ CUP.]
  • 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.]
  • 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.   [RSL @ CUP.]
  • 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.]
  • 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 CUP.]
  • 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), p. 136. [BSL @ CUP.]
  • 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.