University of Alberta
Faculty of Arts
Department of Philosophy
Phil 522/422: Topics in Logic/Topics in Advanced Symbolic Logic
Winter term (2013/14)
This course surveys some of the best-known non-classical logics, for example, relevance logics, intuitionistic logic, Lambek calculi and modal logics.
Conceptually and historically, modern logic emerged as a formal calculus. For a long time, the dominant way to specify a formal system was to single out certain (perhaps, self-evident) formulas and to add a few rules, that is, to axiomatize a logic. For classical logic, a rigorous semantics followed half a century after the introduction of the first proof system.
The intent in this course is to focus on proof systems. In particular, we will primarily scrutinize sequent calculi (though we will not completely ignore the semantics of the logics). This type of proof system (for classical and intuitionistic logic) was invented by Gentzen in the mid 1930s, at the same time when he invented his natural deduction systems. Sequents capture inferences, and the rules in these calculi can be thought of as rules describing how sequences of premises or conclusions may be modified. A special rule called cut permits shorter proofs, but destroys the subformula property. However, the cut theorem, which establishes the admissibility of the cut rule, supplies a happy medium.
The sequent calculus approach to the formalization of logics has been very successful in the last 50–60 years. For instance, the Lambek calculi sparked new connections between logic and linguistics in the form of categorial grammars. Sequent calculi for the implicational fragments of R and E turned out to be a key component in decidability proofs. Structurally free logics fuse combinators and type-assignment systems.
Although sequent calculi are rarely included into introductory courses, they are very elegant proof systems. Sequent calculi, consecution calculi and display calculi have remarkably advanced our understanding of proofs, and they have produced many meta-theoretical results. —Among the latter is a result from the last couple of years by J. M. Dunn and K. Bimbó concerning the decidability of T→.
Time: M, W, F
14:00 pm–14:50 pm
Texts: Bimbó, K., and J. M. Dunn, Generalized Galois Logics: Relational Semantics of Nonclassical Calculi, CSLI Publications, Stanford, CA, 2008. (recommended),
and other publications (that will be announced later).
For further information, please contact the instructor at
The (official) course outline is available in the e-classroom during the course.
[Last updated on March 13th, 2013.]