Fall 2024:
Phil 220: Symbolic Logic 2
Phil 365: Philosophy of computing

Winter 2025:
Phil 325: Risk, choice and rationality
Phil 422/522: Topics in Advanced Symbolic Logic/Topics in Logic: Applied Logic

Other courses

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

• 422/522 Topic: Relevance and substructural logics
• 422/522 Topic: Computability and Gödel's incompleteness theorems
• 422/522 Topic: Gödel's incompleteness theorems
• 422/522 Topic: Gaggle theory applied to modal, relevance and other non-classical logics
• 422/522 Topic: Proof theory of classical and substructural 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 λ-calculuses.  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 other disciplines too — from mathematics to informatics and 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 informatics, especially, those that concern questions related to the theory of computing — like algorithmics, information theory, complexity theory, programming language design and cyber security.  Earlier, I worked on some questions in the semantics of natural languages, primarily, using modal (specifically, temporal and tense) logics and discourse representation theory.

Some of my research results concern semantics for various nonclassical logics (e.g., calculuses for combinatory logic).  J. Michael Dunn and I wrote a book on the relational semantics of nonclassical logics.  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.  Within a SSHRC IG project, we worked on the history of the three-termed relational semantics and problems of its applicability to relevance logics with thin sets of connectives.  The (first) Third Workshop, which took place on May 16–17, 2016, at the University of Alberta [workshop poster], was thematically connected to the same SSHRC IG.  I continue to work on questions related to various relational semantics for substructural logics — especially, from the perspective of Dunn's gaggle theory (i.e., generalized Galois logics) as part of my SSHRC IG. The 2nd Third Workshop will take place on May 13–14, 2024, at the University of Alberta.

A more precise characterization of classes of structures for various nonclassical logics leads straightforwardly to topological frames.  I proved full 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 of formulas can be viewed as maps in a category.

Combinatory logic and λ-calculuses 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 about extracting combinatory inhabitants from proofs in a sequent calculus for implicational ticket entailment, and I further applied the approach to implicational intuitionistic logic.  The use of sequent calculuses — instead of a natural deduction system — leads to other combinator sets and other combinatory inhabitants than usual.  This approach shows a way to extend CHC without switching to λ-terms or introducing a substitution operation.  Typable combinatory terms encode proofs in an axiomatic formulation of a logic; 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, for instance, abacus machines can.  These are some of the motivations why I wrote a book on combinatory logic.

The proof theory of nonclassical logics sometimes gets really tricky.  The original sequent calculuses LK and LJ are seemingly simple proof systems, 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 calculuses for some of these relevance logics — including E^t₊ — 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 decidability proof was made possible by a new sequent calculus for implicational R^t (R^t_→), which extends a sequent calculus for implicational T^t by two rules that add the exact difference between these logics to the latter to obtain the former.  I wrote a book on proof theory with a focus on sequent calculuses (including some tableaux and resolution systems). 

J. Michael Dunn and I proved the decidability of several modal relevance logics — including propositional linear logic.  I proved some related results such as the decidability of MELL and that of NLL (in a group of certain semi-lattice based modal logics).  Problems with the reception of our results, which stem from a lack of understanding of sequent calculuses, led to the introduction of a new research area called reverse computation, in 2019.  One of the first results in reverse computation is that abacus machines cannot reverse compute primitive recursive functions.

I am certain that logic — together with its many connections and offsprings — is an exciting and thriving field of research, which is of utmost importance for the protection and enhancement of rationality.

• K. Bimbó, “On the origins of gaggle theory,” in Logica Yearbook 2022, I. Sedlár (ed.), College Publications, London, UK, 2023, pp. 19–36.
• K. Bimbó and J. M. Dunn, “Modalities in lattice-R,” in Relevance Logics and other Tools for Reasoning. Essays in Honor of J. Michael Dunn, K. Bimbó (ed.), Tributes, vol. 46, College Publications, London, UK, 2022, pp. 89–127.
• K. Bimbó (ed.), Relevance Logics and other Tools for Reasoning. Essays in Honor of J. Michael Dunn, Tributes, vol. 46, College Publications, London, UK, 2022.   (The book @ College Publications. Table of contents (PDF).)
• K. Bimbó and J. M. Dunn, “St. Alasdair on lattices everywhere,” in Alasdair Urquhart on Nonclassical and Algebraic Logic, and Complexity of Proofs, I. Düntsch and E. Mares (eds.), Outstanding Contributions to Logic, vol. 22, Springer Nature, Switzerland, 2022, pp. 323–346.   (The paper @ Springer Link.)
• K. Bimbó, “Interpretations of weak positive modal logics,” in Arnon Avron on Semantics and Proof Theory for Non-classical Logics, O. Arieli and A. Zamansky (eds.), Outstanding Contributions to Logic, vol. 21, Springer Nature, Switzerland, 2021, pp. 13–38.   (The paper @ Springer Link.)
• K. Bimbó, “The development of decidability proofs based on sequent calculi,” in Contemporary Logic and Computing, A. Rezuş (ed.), Landscapes in Logic, vol. 1, College Publications, London (UK), 2020, pp. 5–37. (The volume @ College Publications.)
• K. Bimbó, “On the algebraization of relevance logics. (A preamble to J. Michael Dunn's PhD dissertation),” in Logic PhDs, vol. 2: J. Michael Dunn, The Algebra of Intensional Logics, College Publications, London (UK), 2019, pp. 1–22. (The volume @ College Publications.)
• K. Bimbó, “Default rules in the logic of first-degree entailments,” in New Essays on Belnap–Dunn Logic, H. Omori and H. Wansing (eds.), Synthese Library, vol. 418, Springer Nature, Switzerland, 2019, pp. 113–131.   (The paper @ Springer Link.)
• K. Bimbó, “Inhabitants of intuitionistic implicational theorems,” in Logic, Language, Information and Computation. Proceedings of the 25th International Workshop, WoLLIC 2018, Bogota, Colombia, July 24–27, 2018., L. S. Moss, R. de Queiroz and M. Martinez (eds.), Lecture Notes in Coputer Science, vol. 10944, Springer, 2018, pp. 1–24.   (The paper @ Springer Link.)
• K. Bimbó, J. M. Dunn and N. Ferenz, “Two manuscripts, one by Routley, one by Meyer: The origins of the Routley–Meyer semantics for relevance logics,” Australasian Journal of Logic 15 (2018), pp. 171–209.   (The paper @ Victoria University of Wellington.)
• K. Bimbó and J. M. Dunn, “Larisa Maksimova’s early contributions to relevance logic,” in Larisa Maksimova on Implication, Interpolation and Definability, S. Odintsov (ed.), Outstanding Contributions to Logic, vol. 15, Springer Nature, Switzerland, 2018, pp. 33–60.   (The paper @ Springer Link.)
• K. Bimbó, “On the decidability of certain semi-lattice based modal logics,” in Automated Reasoning with Analytic Tableaux and Related Methods. Proceedings of the 26th International Conference, TABLEAUX 2017, Brasilia, Brazil, September 25–28, 2017, R.A. Schmidt and C. Nalon (eds.), Lecture Notes in Artificial Intelligence, vol. 10501, Springer, 2017, pp. 44–61.   (The paper @ Springer Link.)
• K. Bimbó and J. M. Dunn (eds.), Proceedings of the Third Workshop, May 16–17, 2016, Edmonton, Canada, special issue of the IFCoLog Journal of Logics and their Applications 4(3) (2017).
• K. Bimbó and J. M. Dunn, “The emergence of set-theoretical semantics for relevance logics around 1970,” in Proceedings of the Third Workshop, May 16–17, 2016, Edmonton, Canada, K. Bimbó and J. M. Dunn (eds.), special issue of the IFCoLog Journal of Logics and their Applications 4 (2017), pp. 557–589.
• 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; the book@ Springer Link. Table of contents (PDF).)
• K. Bimbó, “Some relevance logics from the point of view of relational semantics,” in Israeli Workshop on Non-classical Logics and their Applications (IsraLog 2014), O. Arieli and A. Zamansky (eds.), special issue of the Logic Journal of the IGPL 24 (2016), pp. 268–287.   (The paper @ Oxford University Press.)
• K. Bimbó, “The decidability of the intensional fragment of classical linear logic,” Theoretical Computer Science 597 (2015), pp. 1–17.   (The paper @ Elsevier.)
• 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 and an amendment to the book.)
• K. Bimbó, “Current trends in substructural logics,” in JPL40: The fortieth anniversary issue of the Journal of Philosophical Logic, J. Horty and F. Veltman, (eds.), special issue of the Journal of Philosophical Logic 44 (2015), pp. 609–624.   (The paper @ Springer Link.)
• K. Bimbó and J. M. Dunn, “Extracting BB'IW inhabitants of simple types from proofs in the sequent calculus LT^t_→ for implicational ticket entailment,” Logica Universalis 8(2) (2014), pp. 141–164.   (The paper @ Springer Link.)
• K. Bimbó and J. M. Dunn, “On the decidability of implicational ticket entailment,” Journal of Symbolic Logic 78(1) (2013), pp. 214–236.   (The paper @ Cambridge University Press.)
• K. Bimbó and J. M. Dunn, “New consecution calculi for R^t_→,” Notre Dame Journal of Formal Logic 53(4) (2012), pp. 491–509.   (The paper @ 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.   (The volume @ Linguistic Analysis.)
• K. Bimbó, “Schönfinkel-type operators for classical logic,” Studia Logica 95 (2010), pp. 355–378.   (The paper @ Springer Link.)
• K. Bimbó and J. M. Dunn, “Symmetric generalized Galois logics,” Logica Universalis 3 (2009), pp. 125–152.   (The paper @ Springer Link.)
• K. Bimbó, J. M. Dunn and R. D. Maddux, “Relevance logics and relation algebras,” Review of Symbolic Logic 2 (2009), pp. 102–131.   (The paper @ CUP.)
• K. Bimbó, “Combinatory logic,” Stanford Encyclopedia of Philosophy.  
• K. Bimbó, “Dual gaggle semantics for entailment,” Notre Dame Journal of Formal Logic 50 (2009), pp. 23–41.   (The paper @ 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 book @ the University of Chicago Press.)
• K. Bimbó, “Functorial duality for ortholattices and De Morgan lattices,” Logica Universalis 1 (2007), pp. 311–333.   (The paper @ Springer Link.)
• K. Bimbó, “LE^t_→, LR^°_ˆ˜, LK and cut free proofs,” Journal of Philosophical Logic 36 (2007), pp. 557–570.   (The paper @ Springer Link.)
• 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.   (The paper @ Springer Link.)
• K. Bimbó, “The Church-Rosser property in symmetric combinatory logic,” Journal of Symbolic Logic 70 (2005), pp. 536–556.   (The paper 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.   (The paper @ Project Euclid.)
• K. Bimbó, “Types of I-free hereditary right maximal terms,” Journal of Philosophical Logic 34 (2005), pp. 607–620.   (The paper @ Springer Link.)
• K. Bimbó, “Semantics for dual and symmetric combinatory calculi,” Journal of Philosophical Logic, 33 (2004), pp. 125–153.   (The paper @ Springer Link.)
• K. Bimbó, “The Church-Rosser property in dual combinatory logic,” Journal of Symbolic Logic 68 (2003), pp. 132–152.   (The paper at CUP.)
• K. Bimbó and J. M. Dunn, “Four-valued logic,” Notre Dame Journal of Formal Logic 42 (2002), pp. 171–192.   (The paper @ Project Euclid.)
• K. Bimbó, “Semantics for the structurally free logic LC+,” Logic Journal of IGPL, 9 (2001), pp. 525–539.   (The paper at OUP.)