October 19: Fedor Pakhomov: Transitive modal logics and second-order theories
16.00--17.00
For Kripke semantics,a modal language may express properties that can not be expressed by first-order formulas. It was shown by S.K. Thomason that there is a certain kind of effective reduction of second-order logic to modal logic (with semantical consequence relation). We show that there is an effective reduction of second-order logic to S4 with nominals.

For every Kripke complete logic L its Kuznetsov index is the least cardinal \kappa such that every refutable formula of this logic is already refutable in an L-frame of the cardinality less than \kappa. A.V. Kuznetsov had raised a question of characterization of all Kuznetsov indexes for superintuitonistic logics and for extensions of S4. M.Kracht had proved a theorem that says that a cardinal \kappa is a Kuznetsov index of a Kripke complete modal logic iff it is a (likewise defined) index of some \Pi^1_1-theory with countable signature. From our reduction result we conclude that the analogue of Kracht theorem for extensions of S4 with nominals holds.

February 9: Andrew Swan: Lifschitz Realizability as a Topological Construction
16:00-17:00
Lifschitz realizability is a form of realizability with the unusual property that the omniscience principle LLPO holds in the model alongside a form of Church's thesis: all functions N -> N are computable. Jaap van Oosten proved that there is a Lifschitz realizability topos and the remarkable result that the Lifschitz realizability topos can be viewed as a topos of sheaves over a Lawvere-Tierney topology in the effective topos. We are developing a new presentation of this result. Instead of topos theory we work in constructive set theory, and instead of Lawvere-Tierney topology and sheaves we use a topological model over formal topologies developed by Nicola Gambino. We show that the Lifschitz realizability model for IZF developed by Rathjen and Chen can be constructed by building a topological model inside the usual realizability model for set theory, V(K_1). Instead of working in V(K_1) directly, we identify the axioms needed to build the topological model: Markov's principle and a special case of independence of premises. This allows one to easily generalise the construction to several variants of Lifschitz realizability. Finally we use this to show several consistency and "existence property" results for IZF and CZF with LLPO or the weaker variants LLPO_n studied by Richman.
This is joint work with Michael Rathjen.

March 31: Lev Beklemishev: On the algebraic model for reflection calculus with conservativity modalities
11:00-12:00
The language of the Reflection Calculus RC consists of implications between formulas built up from propositional variables and the constant "true" using only conjunction and diamond modalities which are interpreted in Peano arithmetic as restricted uniform reflection principles.

We extend the language of RC by another series of modalities representing the operators associating with a given arithmetical theory T its fragment axiomatized by all theorems of T of arithmetical complexity \Pi _n, for all n > 0. We note that such operators, in a precise sense, cannot be represented in the full language of modal logic.

We formulate a formal system extending RC that is sound and, as we conjecture, complete under this interpretation. In this system one is able to express iterations of reflection principles up to any ordinal In this talk we introduce a universal algebraic model for this system that is built on top of the well-known universal Kripke frame due to Ignatiev. We give several equivalent definitions of this structure.

March 31: Martin Hyland: What is an interpretation of the Lambda Calculus?
11:00-12:00
For its first 40 years the pure Lambda Calculus was studied as a syntactic system. There was no study of semantics in the sense in which e.g. one studies the (evident) semantics of the predicate calculus or possible worlds semantics for modal logic. When the first models were developed around 1970 the community of logicians seems not to have concerned itself much about what was meant. Specialists had esoteric definitions of lambda model and lambda algebra but most were satisfied by Scott's explanation: restricting to continuous functions one can find spaces isomorphic to their space of endofunctions and that gives models. Since then the question of what is a model has been revisited many times: by Barendregt in his magnum opus (with a different account in the two editions), by Meyer and by Scott around 1980 and by Freyd and Selinger in the mid 1990s. Scott does not offer a definition so much as a category theoretic characterisation but in all the other approaches an interpretation of the lambda calculus is an algebraic structure with a cruciall operation of application.

In this talk I shall argue for a quite different view: an interpretation of the lambda calculus is a semi-closed algebraic theory. The link with the older views is given by what I think of as the Fundamental Theorem of the Lambda Calculus: there is a correspondence between such Lambda Theories and models of the initial such Theory. The new view enables direct approaches to Scott's characterisation, to the connection with the combinatory logic and to Lambda Monoids as studied in Koymans' neglected 1984 thesis.