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.]