Events

Location: MALL
Title: Peano arithmetic, games, and descent recursion

I will discuss a game semantics for classical (first-order) arithmetic due to Coquand. The real content of this semantics is a proof of cut elimination for infinitary propositional logic. As the title suggests, I will say something about descent recursive functions and how it all comes together.

Location: MALL

Location: MALL
Title: Natural Deduction Proof for Substructural, Constructive and Classical Logics

Since the 1990s, we have seen how to understand a very wide range of logical systems (classical logic, intuitionistic logic, dual intuitionistic logic, relevant logics, linear logic, the Lambek calculus, affine logic, orthologic and more) by way of the distinction between operational and structural rules. We can have one set of rules for a connective (say, conjunction, negation, or the conditional) in a sequent calculus, and get different logical behaviour depending on the shape of the sequents allowed and the structural rules governing those sequents.

In this talk, I will consider the relationship between the “big four” traditional substructural logics—intuitionistic, relevant, affine and linear—corresponding to the four options for including or excluding the structural rules of weakening and contraction, in the setting of Gentzen/Prawitz-style natural deduction proofs for implication and the simply typed λ calculus. Such a natural deduction setting—in which proofs have any number of premises and a single conclusion—has a natural bias toward constructive, or intuitionistic logic.

I will show how the choice of whether to “go classical”, expanding the structural context to allow for more than one formula in positive position is orthogonal to the choice of the other structural rules, so that even in the context of natural deduction proofs, the familiar pair of traditional implication introduction and elimination rules gives rise to eight different propositional logics, four of which are “classical” and four of which are “constructive”. Furthermore, the familiar double-negation translation of classical logic inside intuitionistic logic generalises to the other three classical/constructive pairings.

I will explain these results, and, if there is time, I will end the talk with some reflections on what this might mean for the relationship between classical and constructive reasoning.

Location: Roger Stevens LT 13 (10.13)
Title: Games, Comonads and Compositionality
NOTE location change: Roger Stevens LT 13 (10.13)

Recent work of Abramsky, Dawar and Wang, and subsequently Abramsky and Shah, provided a categorical abstraction of model comparison games such as the Ehrenfeucht-Fraïssé, pebble and bisimulation games, in the form of so-called game comonads. This work opened up new connections between disciplines associated with computational power and complexity such as finite model theory and combinatorics, and areas traditionally focussed upon the structural understanding of computation and logic, such as program semantics.

This talk will introduce the comonadic perspective upon model comparison games. I shall then describe more recent work, jointly with Tomáš Jakl and Nihil Shah, giving a categorical account of Feferman-Vaught-Mostowski type theorems with this categorical framework.

The talk will aim to be reasonably self-contained, assuming only a basic background in logic, and some understanding of the categorical notions of category, functor and natural transformation.