Heyting Day 2015

The Heyting Day 2015 will take place in the «Belle van Zuylenzaal»  of Utrecht University Academy Hall, Domplein 29, Utrecht. The day is dedicated to the celebration of the 75th birthdays of Dick de Jongh and Anne Troelstra.

Programme

On the topological interpretations of provability logic

Lev Beklemishev

Provability logic concerns the study of modality box as provability in formal systems such as Peano arithmetic. Natural, albeit quite surprising, topological interpretation of provability logic has been found in the 1970's by Harold Simmons and Leo Esakia. They have observed that the dual diamond modality, corresponding to consistency in the context of formal arithmetic, has all the basic properties of the topological derivative operator acting on a scattered space. The topic has become a long-term project for the Georgian school of logic with occasional contributions from elsewhere. More recently, a new impetus came from the study of polymodal provability logic GLP that was known to be Kripke incomplete and, in general, to have a more complicated behavior than its unimodal counterpart. Topological semantics provided a better alternative to Kripke models in the sense that GLP was shown to be topologically complete. At the same time, new fascinating connections with set theory and large cardinals have emerged. We give a survey of these recent developments while trying to trace the analogy between certain proof-theoretic and topological notions. [slides]

On Proof Interpretations and Linear Logic

Paulo Oliva

Proof interpretations of intuitionistic logic (e.g. realizability and Dialectica) are amongst the main tools in constructive mathematics. Similar to the Curry–Howard correspondence for minimal logic, these interpretations allow us to view mathematical proofs as effective constructions. The interpretations differ mainly on the set of «interpreted principles», i.e. logical principles that go beyond intuitionistic logic, but that nevertheless have a computational interpretation. Some examples of these are: Markov principle, Church-Turing thesis, fan principle and continuity axioms. This talk describes recent work on trying to understand the structure and relationship between various interpretation. Our proposal is to use intuitionistic linear logic (ILL) as a refinement of intuitionistic logic (IL), and study how the different interpretations operate on ILL. Making use of standard translations ILL → IL and IL → ILL we can recover interpretations of IL from those of ILL. We observe two curious outcomes:

1. The contraction axiom is responsible for most of the differences between various interpretations, i.e. most interpretations coincide when restricted to the pure fragment of ILL.
2. The different ways of translating IL into ILL are responsible for the existence of “variants” such as realizability with truth and q-realizability. [slides]

Intuitionism, Generalized Computability and Effective Operations

Jaap van Oosten

The talk discusses some aspects of recent work with Eric Faber on «freely adding effective operations» to models of generalized computation. This work touches both on Intuitionism and the theory of Recursive Functions.

I learnt Intuitionism from Anne, who was a student of Heyting, who was a student of Brouwer, who invented Intuitionism; and I learnt Recursion Theory from Dick, who was a student of Kleene, who invented Recursive Function Theory. [slides]

On Jankov-de Jongh formulas

Nick Bezhanishvili

In the 1960s Jankov and independently de Jongh introduced the method of frame formulas that became an important tool for axiomatizing intermediate logics. The key ingredient of de Jongh formulas was a dual charaterization of Heyting homomorphisms between Heyting algebras corresponding to Kripke frames, which was developed by de Jongh and Troelstra (1966). In this talk, I will overview the method of Jankov-de Jongh formulas and will discuss its various generalizations. [slides]

136 years and still going strong(?): Cantor's continuum problem

Michael Rathjen

Cantor's continuum hypothesis, CH, asserts that an infinite set of reals is either countable or of the same size as the entire continuum (so nothing exists in between). The quest for its status became enshrined in Hilbert's famous 1900 list, earning it a first place.

Hilbert announced a proof of CH in his 1925 talk «On the Infinite» which arguably inspired Gödel to find a model of set theory that validates CH. With the work of Cohen in the 1960s, many people were convinced that CH was now a settled problem as all essential facts about it were deeply understood. This situation, however, did not convince everybody (e.g. Gödel). The last 20 years or so saw a surprising resurgence of the problem in modern set theory. In the first part of the talk, I plan to survey some important known facts about CH. This will be followed by relating some of the modern attempts at finding new axioms to settle CH. Their justifications are partly based on technical results but also tend to be highly speculative and often come enmeshed with essentially philosophical arguments.

Finally I shall consider a specific proposal by Solomon Feferman to clarify the nature of CH. He has advocated an account of the set-theoretic universe which allows him to distinguish between definite and indefinite mathematical problems. His way of formally regimenting this informal distinction is by employing Heyting's logic for domains for which one is a potentialist and reserving classical logic for domains for which one is an actualist. This framework allowed him to state a precise conjecture about CH, which has now been proved. I plan to indicate a rough sketch of the proof which features realizability and forcing. [slides]