Fall 2018
Phil 220: Symbolic Logic 2
Phil 120: Symbolic Logic 1
Winter 2019
Phil 421/Phil 522: Modal Logic
Phil 365: Philosophy of computing
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: 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
nonclassical 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 λ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 other disciplines too — from mathematics to
computer science 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 the philosophy of computer science and informatics,
especially, those that concern questions related to theoretical computer
science — like 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 and 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 logics. These kinds of semantics generalize
Kripke's possibleworld 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 “fourvalued”
semantics for minimal substructural logic. We continue to work —
within a SSHRC IG — on problems related to the semantics of
nonclassical logics, primarily, on questions connected to the threetermed
relational semantics.
(More info on the project.) A paper I wrote about
the semantics of implicational relevance logics appeared in the proceedings
of the IsraLog 2014 workshop. The (first) Third Workshop, which is thematically connected
to the SSHRC IG project, took place on May 16–17, 2016, at the
University of Alberta. (Here is the
poster of the workshop.)
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 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 about extracting combinatory inhabitants from proofs in a sequent
calculus for implicational ticket entailment. This is a first step to
extend CHC into a new direction. 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 sequent calculi LK and LJ are
seemingly simple proof systems, 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.
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, which
extends a sequent calculus for implicational T by two rules that
add exactly what the difference between these logics is.
I wrote a book on proof theory with a
focus on sequent calculi (including some tableaux and resolution
systems), which was published in 2014. Then, I proved the
decidability of MELL (the
multiplicative–exponential fragment of linear logic).
J. Michael Dunn and I proved the decidability of several modal relevance
logics. Last year, I proved another group of modal logics
(“semilattice based modal logics”) 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
240 Assiniboia Hall
Edmonton, AB T6G 2E7, Canada
Email address:
Page updated on:
March 7th, 2018
My Erdös number:
Three (i.e., 3)
Memberships:
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
Alter
ego page

 K. Bimbó, “On the decidability of certain semilattice 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, v. 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 settheoretical
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, @
Springer Link. Table of contents (PDF).]
 K. Bimbó, “Some relevance logics from the point of view of relational
semantics,” in Israeli Workshop on Nonclassical 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.
 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ó, “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.
 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.
 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 R^{t}_{→},” 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önfinkeltype 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ó, “LE^{t}_{→},
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 (NorthHolland), 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 ChurchRosser 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 Ifree 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 ChurchRosser property in dual combinatory
logic,” Journal of
Symbolic Logic 68 (2003), pp. 132–152. [JSL
@ JSTOR.]
 K. Bimbó and J. M. Dunn, “Fourvalued
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.
