This is a seminar series on Provability, Interpretability, Intuitionism and Arithmetic, organized jointly by the universities of Amsterdam, Nijmegen and Utrecht. Each session will consist of informal technical talks, followed by elaborate discussion. The meetings will take place about once a month, either in Amsterdam or Utrecht.


15:00 – 17:00, May 20, 2015 Room G2.13, Amsterdam Science Park 904

Rutger Kuyper: Intuitionistic logic, computability, and the Medvedev and Muchnik lattices

In an attempt to characterise intuitionistic logic, Kolmogorov gave an informal semantics for intuitionistic logic as a `calculus of problems’. This was later formalised by Medvedev using concepts from computability theory, which yields a structure called the Medvedev lattice. This Medvedev lattice is a Brouwer algebra (the order-dual of a Heyting algebra) and can therefore be used to give semantics for intermediate propositional logics. It turns out that the logic characterised by the Medvedev lattice is not intuitionistic propositional logic IPC, but is exactly Jankov’s logic consisting of the deductive closure of IPC plus the weak law of the excluded middle `(not)p or (not)(not)p’.

A very nice result of Skvortsova says, however, that there is a principal factor of the Medvedev lattice which yields IPC. In this talk we will discuss some of the results about the theories of principal factors of the Medvedev lattice. Furthermore, we will also discuss similar results for the Muchnik lattice, a variation on the Medvedev lattice. Finally, we will sketch an extension of these ideas to first-order logic.

Jeroen Goudsmit: Finite frames fail, or How Infinity Works its Way into the Semantics of Admissibility

How does one recognize the non-theorems of a logic? In many intermediate logics, it suffices to inspect all finite models of a certain size, bounded in some way by the formula under consideration. This desirable result is utterly unattainable in many an intermediate logic, when generalizing from theorems to rules.

February 27, 2015 Academy Hall, Domplein 29, Utrecht

Arend Heyting Day

Friday, 5th of December 2014, 16:00 ILLC seminar Room F1.15, Science Park 107

Volodya Shavrukov: Astrology of Nerode semirings

Nerode semirings are models of the true forall-exists 1st order arithmetic that are finitely generated with respect to total recursive functions. They are aged at around half a century. They can also be seen as ultrapowers of N restricted to total recursive functions, with the suitable ultrafilter being one on the algebra of recursive sets.

We relate the structure of Nerode semirings to combinatorial amd complexity properties of recursive ultrafilters, and to how these ultrafilters are positioned w.r.t. various r.e. sets. We address issues such as ordering of skies in a Nerode semiring, existential completeness, and substructure lattices. We also discuss a couple of generalizations such as r.e. ultra- and prime powers.

This is joint work with James Schmerl.

Wednesday, 22nd of October 2014, 15.00 – 16.00 Utrecht, Janskerkhof 13, Stijlkamer 0.06

Fan Yang: Propositional dependence logic

Wednesday, 28th of May 2014, 15.00 – 16.00 Amsterdam, Science Park 107, ILLC Room F1.15

Paula Henk: Adding the Supremum to Interpretability Logic

Wednesday, 30 April 2014, 15:00 – 17:00 Amsterdam, Science Park 107, ILLC Room F1.15

Fatemeh Seifan: Uniform Interpolation for Coalgebraic Fixpoint Logic

In this talk we will use the connection between automata and logic to prove that a wide class of coalgebraic fixpoint logics enjoy the uniform interpolation. To this aim, first we generalize one of the central results in coalgebraic automata theory, namely closure under projection, which is known to hold for weak-pullback preserving functors, to a more general class of functors, i.e.; functors with quasi-functorial lax extensions. Then we will show that closure under projection implies definability of the bisimulation quantifier in the language of coalgebraic fixpoint logic, and finally we prove the uniform interpolation theorem.

Jeroen Goudsmit: Using Admissible Rules to Characterise Logics

The admissible rules of a logic are those rules under which the set of its theorems are closed. A most straightforward example is the rule A ∨ B / {A,B}, which is admissible precisely if the logic enjoys the disjunction property. Iemhoff (2001) showed that IPC can be characterised in terms of its admissible rules, by showing that it is the sole intermediate logic which admits a certain set of rules.

We will present a similar characterisation for the Gabbay-de Jongh logics, also known as the logics of bounded branching. Our reasoning is based on the characterisation of IPC by Skura (1989), who presented a refutation system for IPC. In particular we show how one can inductively define the set of formulae that are non-derivable in the Gabbay-de Jongh logics. This talk is based on the work described in "Admissibility and Refutation: Some Characterisations of Intermediate Logics".

Wednesday, 26th of February, 15.00 – 17:00 Amsterdam, Science Park 904, A1.08

Albert Visser: The Interpretability of Inconsistency

Wednesday, 29th of January, 15:00 – 17:00 Amsterdam, SP D1.114

Nick Bezhanishvili: Canonical formulas and stable intermediate logics

Dick de Jongh: NNIL and ONNILLI

Monday, 9th of September, 16:00 – 18:00 Utrecht, Janskerkhof 13, room: Stijlkamer 0.06

Ivano Ciardelli: Inquisitive semantics and intermediate logics

Traditionally, the meaning of a sentence is identified with its truth-conditions or, in a dynamic view, with the potential the sentence has to provide new information. However, in communication information is both provided and requested, in a dynamic process of raising and resolving issues. Based on this idea, Inquisitive semantics proposes a more comprehensive notion of meaning, that encompasses not only informative content, but also inquisitive content, the potential a sentence has to raise new issues.

The propositional logic InqL arising from the standard system of inquisitive semantics is a non-substitution closed intermediate logic, whose atoms are "classical" in the sense that they satisfy the double negation law. We will see that this logic can be characterized as the disjunctive-negative fragment of intuitionistic logic, i.e., the fragment consisting of those formulas which are (equivalent to) disjunctions of negations. A range of sound and complete axiomatizations for InqL will be established, and the schematic fragment of the logic will be seen to coincide with Medvedev's logic of finite problems.

In the final part of the talk, I will consider in more generality the effect that assuming classical atoms (i.e., adding atomic double negation) has on some well known intermediate logics, discussing in particular when this gives rise to new schematic validities.

24 June 2013 16:00 – 18:00 Drift 23, room 106

Albert Visser: Inconsistency Statements

Do (in)consistency statements still have meaning when they occur in the context of weak and / or unsound theories? Or rather, what does it mean that a formula is a(n) (in)consistency statement in such cases? I will explain why I think such questions are misdirected.

Sometimes wrong-headed philosophy leads to nice mathematics. One idea to address the meaning question is to say that to be a provability predicate is to fulfill a certain role in reasoning. This role is codified as the satisfaction of certain global modal principles: the Hilbert-Bernays and / or the Löb Conditions. I will briefly criticise this idea (mainly by giving examples). However, as I will illustrate, the idea leads to an interesting technical result.

Let U be a base theory, like Peano Arithmetic. (We will explain the conditions on base theories in the talk.) Let's say that A is an inconsistency statement for U if A is the inconsistency statement of some predicate that satisfies both the Löb and the Hilbert-Bernays conditions for U. We say that a sentence B is interpretable *over* U if U interprets U+A. One variant of the Second Incompleteness Theorem, due to Solomon Feferman, says that all inconsistency statements for U are interpretable over U. We will show the converse: all sentences interpretable over U are inconsistency statements of U.

Thus, it turns out that there is a connection between interpretability and inconsistency (in the sense of the role conception). We will further explore this connection. We can use our result to *define* interpretability in terms of inconsistency statements. Can we reprove known results about interpretability only using insights about proof predicates? Yes, we can. I will illustrate this idea by discussing the connection with the interpretability logic ILM.

20 March 2013 15:00 – 17:00 Drift 7, Utrecht, Room 0.07
  • 15:00 – 15:40, Rosalie Iemhoff: Uniform Interpolation
  • 16:00 – 16:45, Jeroen Goudsmit: Admissible Rules in Gabbay-de Jongh Logics
  • 17:00 – 18:00: Discussion
  • 18:00 – undetermined: Dinner
23 January 2013 13:00 – 15:00 Science Park 904, Amsterdam, A1.06

Paula Henk: On the possibility of finding a relational semantics for the interpretability logic ILMS – a negative result.

In this talk, we show that ILMS, a system of modal logic with two binary operators, cannot have the kind of relational semantics we would have liked it to have.

The modal logic ILMS is a member of the family of interpretability logics. This family consists of modal logics in which the modal operators are interpreted as metamathematical notions such as provability or interpretability in some sufficiently strong theory, for example Peano Arithmetic (PA). Examples of interpretability logics are the normal modal logic GL (also known as provability logic), and ILM - an extension of GL with a binary modality whose intended meaning is interpretability between finite extensions of PA. Both GL and ILM are sound and complete with respect to the intended arithmetical interpretation of their modal operators. The logic ILMS is obtained by adding to ILM a further binary modality whose intended meaning is the supremum operator in the lattice of interpretability (of finite extensions of PA).

Although the study of interpretability logics is ultimately motivated by the arithmetical meaning of the modalities, this talk focuses on the properties of interpretability logics as modal logics, in particular on their modal semantics.

The logic GL is sound and complete with respect to the class of Kripke frames where the accessibility relation is transitive and conversely well-founded. Also the logic ILM has a relational semantics: it is sound and complete with respect to a natural class of so-called Veltman frames. The latter extend Kripke frames by having - apart from the usual accessibility relation - a relation S_x for every node x in the domain.

Thus, just as ILM is an extension of GL, the relational semantics for ILM is an extension of the relational semantics for GL. Since ILMS in turn is an extension of ILM, it is natural to ask whether it has a relational semantics that is an extension of the semantics for ILM. In this talk, we will show that the answer to this question is negative: there is no way of extending the usual semantics for ILM to obtain a relational semantics for ILMS. We will sketch the proof of this result by way of a counterexample, pointing out which features of the ILM-frames are responsible for the impossibility of incorporating a supremum operator.

21 November 2012 13:00 – 15:00 Science Park 904, Amsterdam, D1.113


The following people participate in the seminar. If you wish to be on the list below, please contact Jeroen.


If you wish to provide some background material for your talk, mail references to Jeroen.