Dept. of Philosophy
University of Alberta
2-40 Assiniboia Hall
Edmonton, AB, T6G 2E7
∞ (None, really.)
Association for Symbolic
Society for Exact
Friends of the Stanford
PhD (philosophy and
Diploma with highest
Latest update on:
March 3rd, 2014
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 four-valued 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
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 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 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 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
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
In the 2014/15 academic year I will not teach, because I will be on
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
Phil 120: Symbolic Logic
In the fall term of the 2013/14 academic year I taught Phil
220: Symbolic Logic
- 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 (24 pages, to appear).
- 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.]
- 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.]
- 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),
- 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
- 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,
- 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,