** British Logic Colloquium (BLC) 2013, University of Leeds, 5-7 September 2013
**

**
Titles and Abstracts
**

**Invited Talks**(for contributed talks see below)

- Ulrich Berger (Swansea),
*How Constructive is Abstract Mathematics?*

This talk will discuss the question to which extent classical abstract mathematics is compatible with constructive views of mathematics. We will make the case that if one interprets "constructive" in the weak sense of "being able to extract computational information", large parts of abstract mathematics are constructive "as is". In particular, there is no need to "constructivize" mathematical objects and notions. We will illustrate and support this thesis by examples from mathematics about real numbers, explain its theoretical foundation and hint at possible applications in computer science.

- Olaf Beyersdorff (Leeds),
*Parameterized Proof Complexity.*

- Laurent Bienvenu (CNRS, Moscow),
*Probabilistic algorithms in computability theory.*Can we compute with randomness something we cannot without? While complexity theorists still struggle with the fascinating question BPP =? P, the analogue problem in computability theory has seemingly been solved a long time ago: in 1954, de Leeuw, Moore, Shannon, and Shapiro proved that if a function can be computed by a probabilistic algorithm (= Turing machine), then it can be deterministically computed. However, the situation changes if one wishes to probabilistically generate {some} function in a class. For example, Martin showed that there exists a probabilistic algorithm which, with positive probability, computes some function which is not dominated by any computable one (obviously there is no way to computably and deterministically compute such a function). In fact, Martin's proof was quite abstract, but the best way to understand it is via an explicit probabilistic algorithm. I will present the proof of this result and several others classical theorems of the same type. I will then present some more recent work connecting the idea of probabilistic algorithm to reverse mathematics.

- Vasco Brattka (Munich/Cape Town),
*The Unreasonable Effectiveness of Choice or Metamathematics in the Weihrauch Lattice.*

- Kentaro Fujimoto (Bristol),
*Some miscellaneous topics from the problem of implicit commitment in set theory.*When we accept a formal system S, we thereby implicitly commit ourselves to certain desirable properties of S depending on one's criterion or purpose of "acceptance". For example, in one's initial acceptance of S, she may presuppose or commit herself to the consistency of S, reflection principles for S ("soundness"), quantification over definable sets in S ("predicativism"), and the truth of S. However, as is well known, these properties are not derivable or expressible within S itself. Then, we could argue that, when we accept a formal system S, we implicitly commit ourselves to and thereby accept stronger or richer systems than S in general. Or we might be able to further argue that, when we are justified to accept a formal system on a certain fundamental ground, we can justifiably accept certain stronger or richer systems on the same fundamental ground. The question is: How much more should be or can be accepted on the same fundamental ground by one's initial acceptance of a system? This problem is well-investigated concerning formal systems of arithmetic by the works of Turing, Kreisel, Feferman, Schmerl, Friedman, Beklemishev, and Strahm (maybe some more others). However, it seems to me that not so much attention (from the "proof-theoretic" point of view) has been paid on the same problem concerning formal systems of set theory. I will present some miscellaneous topics on this problem particularly in set theory ZFC.

- Nicola Gambino (Palermo/Leeds),
*Cartesian closed bicategories.*It is well known that cartesian closed categories provide models for the simply-typed lambda calculus in which the beta and eta rules are valid as strict equalities. Moving from standard, 1-dimensional, category theory to 2-dimensional category theory, it is possible to formulate the notion of a cartesian closed bicategory, which gives us models where the beta and eta rules are interpreted as isomorphisms. The aim of this talk is to describe in elementary terms what cartesian closed bicategories are and present some examples which arise in the theory of operads. This is based on joint work with Andre' Joyal.

- Charlotte Kestner (Central Lancashire),
*Stability theory and weak one-basedness.*We give an introduction to independence relations and stability theory, mentioning some known results. We then introduce the notion of weak one-basedness, and show various equivalences in context such as thorn-rank 1 theories. This is joint work with Gareth Boxall, David Bradley-Williams, Alexandra Omar-Aziz, and Davide Penazzi.

- Jochen Königsmann (Oxford),
*Undecidability in Number Theory.*In this talk we will highlight some classical and some recent decidability and undecidability results and conjectures on various rings and fields of number theoretic interest, trying to explain some of the beautiful methods developed for tackling these questions.

- Todor Tsankov (Universite Paris Diderot),
*Weakly almost periodic functions, model-theoretic stability, and minimality of topological groups.*It is a well known fact that there is a narrow correspondence between properties of omega-categorical structures and those of their automorphism groups. We investigate properties on the group side that correspond to stability and it turns out that an omega-categorical structure is stable iff every continuous function on the group that is both left and right uniformly continuous is weakly almost periodic. As an application, we show that every such group is minimal, i.e., every continuous surjective homomorphism to another topological group is open, generalizing previous results for particular groups of Stoyanov, Uspenski, Glasner, and others. Our methods can be applied in the setting of both classical and continuous logic. This is joint work with Itai: Ben Yaacov.

- Jon Williamson (Kent),
*Inductive Logic for Automated Decision Making.*According to Bayesian decision theory, one's acts should maximise expected utility. To calculate expected utility one needs not only the utility of each act in each possible scenario but also the probabilities of the various scenarios. It is the job of an inductive logic to determine these probabilities, given the evidence to hand. The most natural inductive logic, classical inductive logic, attributable to Wittgenstein, was dismissed by Carnap due to its apparent inability to capture the phenomenon of learning from experience. I argue that Carnap was too hasty to dismiss this logic: classical inductive logic can be rehabilitated, and the problem of learning from experience overcome, by appealing to the principles of objective Bayesianism. I then discuss the practical question of how to calculate the required probabilities and show that the machinery of probabilistic networks can be fruitfully applied here. This culminates in an objective Bayesian decision theory that has a realistic prospect of automation.

**Contributed Talks**

- William Anscombe (Oxford/Leeds),
*Existentially and universally definable valuation rings.*We survey recent results (from a paper of Cluckers-Derakhshan-Leenknegt-Macintyre, and from joint work of the speaker with Fehm and Koenigsmann) about the definability of valuation rings in valued fields by existential formulas and by universal formulas, using few parameters. We mainly work in power series fields and use parameters from the embedded residue field.

- Arno Pauly (Cambridge),
*The logic of Weihrauch degrees.*On one hand, Weihrauch reducibility has been used successfully as a framework for a metamathematical classification of mathematical theorems with a similar agenda to reverse mathematics. As theorems can be combined by logical operators, we do expect Weihrauch degrees to retain this to some extent. On the other hand, the Weihrauch degrees have been equipped with a rich algebraic structure. As such, the question is immediate whether the degrees with (a subset of) the algebraic operations form a model of some logic, e.g. a Heyting algebra. A few variations of this question will be answered.

- Silvia Steila (Torino),
*Ramsey Theorem for pairs as a classical principle in Intuitionistic Arithmetic.* - Gregory Woods (Swansea),
*A Case Study on Imperative Program Extraction: In-place Quicksort.*The process of program extraction is primarily being associated with functional programs with little research into imperative program extraction. In this paper we present a case study where we extract a program for a typical imperative algorithm, in-place quicksort, from a constructive proof that every array of natural numbers can be sorted. The formal proof and the program extraction process, which is based on realizability, have been carried out in the interactive proof assistant Minlog. Using monads we are able to exhibit the inherent imperative nature of the extracted programs.