The Role of the Higher Infinite in Mathematics and Other Disciplines
Monday 14th December 2015 to Friday 18th December 2015
09:30 to 09:50  Registration  
09:50 to 10:00  Welcome from Christie Marr (INI Deputy Director)  
10:00 to 11:00  Ramsey theory in topological dynamics  INI 1  
11:00 to 11:30  Morning Coffee  
11:30 to 12:00 
Strong Chang's Conjecture, SemiStationary Reflection, Strong Tree Property and Two Cardinal Square Principles We prove that the SemiStationary Reflection Principle, together with the negation of the Continuum Hypothesis, implies that $\omega_2$ has the Strong Tree Property. Also, we show that SSR implies the negation of $\Box(\lambda, \omega)$ for all regular cardinals $\lambda\geq\omega_2$. This is a joint work with Liuzhen Wu. 
INI 1  
12:00 to 13:30  Lunch Break  
13:30 to 14:30  Approximate Ramsey properties of Matrices  INI 1  
14:30 to 15:00  Afternoon Tea  
15:00 to 15:30 
The unreasonable effectiveness of Nonstandard Analysis The aim of my talk is to highlight a hitherto unknown computational aspect of Nonstandard Analysis. In particular, we provide an algorithm which takes as input the proof of a mathematical theorem from ‘pure’ Nonstandard Analysis, i.e. formulated solely with the nonstandard definitions (of continuity, integration, dif ferentiability, convergence, compactness, et cetera), and outputs a proof of the as sociated effective version of the theorem. Intuitively speaking, the effective version of a mathematical theorem is obtained by replacing all its existential quantifiers by functionals computing (in a specific technical sense) the objects claimed to exist. Our algorithm often produces theorems of Bishop’s Constructive Analysis ([2]). The framework for our algorithm is Nelson’s syntactic approach to Nonstandard Analysis, called internal set theory ([4]), and its fragments based on Goedel’s T as introduced in [1]. Finally, we establish that a theorem of Nonstandard Analysis has the same computational content as its ‘highly constructive’ Herbrandisation. Thus, we establish an ‘algorithmic twoway street’ between socalled hard and soft analysis, i.e. between the worlds of numerical and qualitative results.
References: [1] Benno van den Berg, Eyvind Briseid, and Pavol Safarik, A functional interpretation for non standard arithmetic, Ann. Pure Appl. Logic 163 (2012), no. 12, 1962–1994. [2] Errett Bishop and Douglas S. Bridges, Constructive analysis, Grundlehren der Mathematis chen Wissenschaften, vol. 279, SpringerVerlag, Berlin, 1985. [3] Fernando Ferreira and Jaime Gaspar, Nonstandardness and the bounded functional interpre tation, Ann. Pure Appl. Logic 166 (2015), no. 6, 701–712. [4] Edward Nelson, Internal set theory: a new approach to nonstandard analysis, Bull. Amer. Math. Soc. 83 (1977), no. 6, 1165–1198. [5] Stephen G. Simpson, Subsystems of second order arithmetic, 2nd ed., Perspectives in Logic, CUP, 2009. 
INI 1  
15:30 to 16:00  Break  
16:00 to 17:00  A revision theory for typefree probability  INI 1  
17:00 to 18:00  Welcome Wine Reception 
10:00 to 11:00 
On relating strong type theories and set theories
There exists a fairly tight fit between type theories à la MartinLöf and constructive set theories such as CZF and its extension, and there are connections to classical KripkePlatek set theory and extensions thereof, too. The technology for determining the (exact) prooftheoretic strength of such theories was developed in the late 20th century. The situation is rather different when it comes to type theories (with universes) having the impredicative type of propositions Prop from the Calculus of Constructions that features in some powerful proof assistants. Aczel's setsastypes interpretation into these type theories gives rise to rather unusual settheoretic axioms: negative power set and negative separation. But it is not known how to determine the consistency strength of intuitionistic set theories with such axioms via familiar classical set theories (though it is not difficult to see that ZFC plus infinitely many inaccessibles provides an upper bound). The first part of the talk will be a survey of known results from this area. The second part will be concerned with the rather special computational and prooftheoretic behavior of such theories.

INI 1  
11:00 to 11:30  Morning Coffee  
11:30 to 12:30 
Inaccessible cardinals and accessible categories
There is a growing list of important questions in category theory, abstract homotopy theory or model theory where answers depend on large cardinals. These questions concern various properties of accessible categories which can be imagined as categories of models of infinitary first order theories. The answers depend on Vopenka's principle or its consequences, mostly on the existence of a proper class of suitable large cardinals. We will give examples of such questions, explain their characteristic features and mention open problems.

INI 1  
12:30 to 13:30  Lunch Break  
13:30 to 14:30  The Pinning Down Number and Cardinal Arithmetic  INI 1  
14:30 to 14:45  Afternoon Tea  
14:45 to 15:45 
Partition Relation Perspectives We will look at partition relations from various perspectives, and discuss recent results and open problems. 
INI 1  
15:45 to 16:00  Afternoon Tea  
16:00 to 17:00 
M Magidor (Hebrew University of Jerusalem) TBA 
INI 1  
18:00 to 19:00  Cambridge University Press Wine Reception CUP Book Shop, 1 Trinity Street 
10:00 to 11:00 
Wellquasiorderings for progam analysis and computational complextiy
Coauthor: Sylvain Schmitz (ENS Cachan)
The talk will survey some of the applications of wellquasiorderings in computer science.
Wellquasiorderings are an important tool in some areas like program verification, or computeraided deduction and theoremproving. Most importantly, they provide easy proofs for the decidability of logical or combinatorial problems. Recent work by the authors aim at extracting computational complexity bounds from decidability proofs that rely on wellquasiorderings.

INI 1  
11:00 to 11:30  Morning coffee  
11:30 to 12:00 
Infinite Matroids and Pushdown Automata on Infinite Words
The aim of this talk is to propose a topic of study that connects infinite matroids with pushdown automata on words indexed by arbitrary linear orders. The motivation for this study is the key open conjecture concerning infinite matroids, the Intersection Conjecture of NashWilliams, as well as a result from my paper "Infinite Matroidal Version of Hall's Matching Theorem, J. London Math. Soc., (2) 71 (2005), 563–578." The main result of this paper can be described using pushdown automata as follows. Let P=(M,W) be a pair of matroids on the same groundset E. We assign to P a language L_P consisting of transfinite words (indexed by ordinals) on the alphabet A={1,0,1}. The language L_P is obtained by taking all injective transfinite sequences of the elements of E and translating each such sequence f into a word of L_P. The translation involves replacing an element of f by 1, 0 or 1 depending on whether it is spanned by its predecessors in both, one or none of the matroids M and W.
Theorem There exists a pushdown automaton T on transfinite sequences in the alphabet A such that the language L_T consisting of words accepted by T has the following property: For every pair P of matroids satisfying property (*), the language L_P is a subset of L_T if and only if the pair P has a packing (the ground set E can be partitioned into sets E_M and E_N that are spanning in M and N, respectively). The property (*) is that M is either finitary or a countable union of finite corank matroids and W is finitary. 
INI 1  
12:00 to 12:30  Weihrauch degrees of determinacy  INI 1  
12:30 to 13:30  Lunch Break  
13:30 to 14:30 
Computing beyond Constructibility: The Recognizability Strength of Ordinal Time Machines
Coauthor: Philipp Schlicht (Universität Bonn)
Transfinite machine models of computation provide an approach to an `effective mathematics of the uncountable'. However, their settheoretical interest seems to be limited by the fact that even the strongest such model, Koepke's Ordinal Turing Machines with parameters (pOTMs), can only compute constructible sets.
Recognizability is a more liberal notion than computability in that it only requires the machine to be able to identify a certain object when it is given to it as an input, not to produce that object.
By invoking notions from algorithmic randomness and considering recognizability rather than computability, we connect transfinite computability to large cardinals and forcing axioms incompatible with the axiom of constructibility on the one hand and inner models for large cardinals on the other. In particular, under appropriate large cardinal assumptions, a real number is heriditarily recognizable by a pOTM if and only if it is an element of the mouse for one Woodin cardinal.
This is joint work with Philipp Schlicht.

INI 1  
14:30 to 15:00  Afternoon Tea  
15:00 to 16:00  Long and short recursive constructionscardinal invariants and parametrized diamonds  INI 1 
10:00 to 11:00 
Set Theory and Automata Theory
We review some recent results on links between (descriptive) set theory and automata theory. In particular, we consider the topological complexity of languages of infinite words accepted by various kinds of automata, the infinite games specified by automata, and independence results in automata theory.

INI 1  
11:00 to 11:30  Morning Coffee  
11:30 to 12:30 
ContextDependent Deterministic Parallel Feedback Turing Computability
The limit of this kind of computability is the least ordinal which is \Pi_1 gapreflecting on admissibles. If you would like to know what any of this means, come to the talk!

INI 1  
12:30 to 13:30  Lunch Break  
13:30 to 14:30 
An Introduction to infinite matroids
For various questions in Infinite Graph Theory, matroids have turned out to be the right tool to tackle them. This introduction to infinite matroids will be selfcontained; in particular I will explain what a matroid is.

INI 1  
14:30 to 14:45  Afternoon Tea  
14:45 to 15:45  Determinacy in Infinite Matroids  INI 1  
15:45 to 16:00  Afternoon Tea  
16:00 to 17:00 
Pairwise Sums in the Reals
Coauthors: Neil Hindman (Howard University), Dona Strauss (University of Leeds)
We show (assuming CH) that there is a finite colouring of the reals such that no infinite set X has X+X (meaning the pairwise sums from X, allowing repetition) monochromatic. And we give positive results for ‘nice’ colourings.

INI 1  
19:00 to 22:00  Conference Dinner at Corpus Christi College 
10:00 to 11:00  Another proof of the JayneRogers theorem  INI 1  
11:00 to 11:30  Morning Coffee  
11:30 to 12:30 
Borel Matchings and equidecompositions
We discuss several results related to the question of when a Borel graph has a Borel matching. Here, the analogue of Hall's matching theorem fails, but there are positive results giving Borel matchings in several contexts if we are willing to discard null or meager sets. We also discuss some applications to geometrical paradoxes. This is
joint work with Spencer Unger.

INI 1  
12:30 to 13:30  Lunch Break  
13:30 to 14:30 
Set theory and algebraic topology
In this talk I plan to discuss some joint work with Sheila Miller related to knots. Quandles are algebraic structures that can be associated to (tame) knots, and they in fact constitute one of the few complete invariants we have for knots. However, there is some dissatisfaction with quandles as invariants, as it heuristically seems difficult to determine whether two quandles are isomorphic. Our result supports this impression: we show that the isomorphism relation of quandles is as complex as it possibly could be in Borel reducibility terms, being Borel complete. On the other hand, equivalence of tame knots is trivial from a Borel reducibility perspective, raising the prospect that more manageable complete invariants might exist.

INI 1  
14:30 to 17:00  INI EndoftheYear Party 