British Logic Colloquium 2017

Programme

This is still a Preliminary Programme (subject to possible changes)

Thursday 7th of September  

2pm - 6pm: PhD Day
Details to be announced soon. If you are a PhD student and want to contribute, please get in touch with the organisers.

Friday 8th of September

9am Registration
Please regsiter at the begininng of the meeting, collect lunch vouchers and other info. You should have paid beforehand. An invoice will be sent after you registered.
10am Invited Talk: Oliver Kullmann (Swansea): Big proofs and SAT
TBA.
11am Tea/Coffee
11:30am Invited Talk: Joan Bragaria (Barcelona): Strong reflection principles and the hierarchy of large cardinals
Large cardinals provide a linear measuring system for the consistency strength of theories beyond ZFC. However, the existence of large cardinals, as well as the fact that they form a linear hierarchy, are still key questions in the foundations of set theory that need further clarification. In my talk I will present some results that characterise a variety of large cardinals in terms of a uniform strong reflection principle, called Structural Reflection, which yields some insight into the existence of large cardinals as natural axioms of set theory and explains their relative strength.
12:30pm Andrew Brooke-Taylor (Leeds):Products of CW complexes: the full story
CW complexes are the topological spaces of choice for much of algebraic topology, but the product of two CW complexes need not be a CW complex. Previous characterisations of when the product is a CW complex relied on making extra assumptions about the set-theoretic universe, such as CH. I will provide a complete characterisation of the circumstances under which the product of two CW complexes is a CW complex, valid without assuming any extra axioms; the characterisation involves the cardinal characteristic of the continuum b.
1pm - 2:30pm LUNCH
2:30pm Invited Talk: Hazel Bricknell (Bristol): Generalised Closed Unbounded and Stationary Sets

The notions of closed unbounded and stationary set are central to Set Theory, and provide a way to measure how "large" or "thick" a subset of an ordinal is. In this talk I will introduce a generalisation of these notions, based on the generalisation of stationarity defined in [1]. Surprisingly for a new concept is set theory, generalised closed unbounded and stationary sets are very simple to define and accessible. They are closely related to the phenomena of stationary reflection and indescribability and can be characterised in terms of derived topologies [2],[3]. These notions are being used to answer questions about provability logic (see [2]), and promise a range of further applications.

[1] Bagaria, J., Magidor, M., and Sakai, H. (2015) "Reflection and indescribability in the constructible universe." Israel Journal of Mathematics 208.1: 1-11.

[2] L. Beklemishev, D. Gabelaia, (2014) "Topological interpretations of provability logic," Leo Esakia on duality in modal and intuitionistic logics, Outstanding Contributions to Logic, 4, eds. G. Bezhanishvili, Springer, 257–290

[3] Bagaria, J. (2016). "Derived topologies on ordinals and stationary reflection." "https://www.newton.ac.uk/files/preprints/ni16031.pdf

3:30pm Sarah Lane Smith (Oxford): Apriority Across Worlds
The nesting problem exposes a fundamental tension between various ideas concerning how an apriori operator should function within formal systems (Forbes 2011, Chalmers and Rabern 2014). It suggests that there are conflicting desiderata on the notion of apriority more generally and, in particular, on its role within modal reasoning. It shows that three independently plausible principles concerning apriority cannot be jointly true on certain analyses. The principles are as follows: Firstly, that contingent apriori truths exist. Secondly, that if something is apriori, then it is necessarily apriori (Modal Stability). Thirdly, that, necessarily, if something is apriori, then it is true (Modal Factivity). Each of these principles can be viewed as independent desideratum for a proper semantics of apriority, yet one must be rejected.

Whilst traditional epistemic two-dimensionalism has provided a compelling way to think about the apriori and its relationship to metaphysical modality, it dictates a solution to the nesting problem that is extremely problematic- it rejects Modal Factivity. Recently, Chalmers and Rabern (2014) have amended the two-dimensional semantics in order to give a more satisfactory solution to the nesting problem. On the amended semantics of Chalmers and Rabern, an additional constraint on apriority is introduced- the liveness constraint. The motivation for introducing the liveness constraint is a revised conception of apriority on which ‘it is apriori that φ’ is understood in terms of there being some conclusive apriori warrant for φ. Chalmers and Rabern argue that there can only be a conclusive apriori warrant for φ at a world w if φ is entertainable at w, and that φ is only entertainable at w if it is live at w. The resulting ‘liveness’ semantics, unlike the traditional one, is able to validate all instances of Modal Factivity.

In this paper, I present a critique of Chalmers and Rabern’s amended liveness semantics for apriority. Whilst I agree that an adequate semantics for apriority must endorse Modal Factivity, I argue that the liveness semantics yields results that contravene certain important intuitions about apriority. Since the liveness semantics represents a strengthening of the traditional two-dimensional semantics, my critique of the former a fortiori applies to the latter. I challenge Chalmers and Rabern’s idea that an expression is entertainable in a world only if it is live in that world. I argue that this supposition is only plausible if the two-dimensionalist relativises the intensions that are entertainable in a world to the sentences or modes of presentation via which they may be entertained. Having attained a clearer idea of the how their semantics must work, I present a key problem case for the liveness account. In the the problem case, a sentence φ comes out as apriori at a world w on the liveness semantics, yet a disjunction of that sentence with another sentence ψ, (φ ∨ ψ), fails to come out as apriori at w. Since a disjunction is a logical consequence of either disjunct, I suggest that the liveness semantics contravenes the highly intuitive principle that, necessarily, the logical consequences of apriori truths are themselves apriori. I also argue that there also are many cases where, conversely, the liveness semantics predicts that a sentence is apriori when intuitively it is not. These kinds of cases are particularly illuminating in terms of diagnosing where the liveness account goes wrong. In my concluding remarks, I review the challenge that the nesting problem poses to any formal account of apriority and consider what my discussion of epistemic two-dimensionalism has shown about how we must begin solve it.

4pm Tea/Coffee
4:30pm Invited Talk: James Ladyman (Bristol) The Philosophical Logic of Homotopy Type Theory
Homotopy Type Theory (HoTT) is a research programme in mathematics that connects algebraic topology with logic, computer science, and category theory. Its name derives from the way it integrates homotopy theory (which concerns spaces, points and paths) and formal type theory (as pioneered by Russell, Church, and Goedel, and developed in computer science) by interpreting types as spaces and terms of them as points in those spaces. Much of the interest in HoTT is due to the fact that it may be regarded as a `programming language for mathematics', and it is formulated in a way that facilitates automated computer proof checking. HoTT is a `foundation for mathematics' in the sense of a framework or language for mathematical practice. Within the language of HoTT it is possible to characterise mathematical structures such as natural numbers, real numbers, and groups, and to formalise proofs in homotopy theory.

However, philosophers often mean something stronger by `foundation for mathematics'. They require a foundation to provide not just a language but also a conceptual and epistemological basis for mathematics, and moreover one that can be formulated without relying upon any other existing foundation. HoTT is interesting for philosophers because of its putative foundational status in this sense. However, there are many other philosophically rich aspects to HoTT. One is the way identity is treated in the theory, which is extremely different from traditional approaches and is what makes the theory in one sense 'intensional'. Another is that the Univalence Axiom in HoTT arguably (and according to Steve Awodey) expresses mathematical structuralism. Further matters of interest are that the theory is constructive and the way this interacts with its other features. Finally, type theory in general, and dependent types in particular provide a different formal approach to functions and quantification, and a different way of dealing with predication.

I will present the basic ideas of HoTT paying particular attention to its novel conceptual foundations, and discussing a selection of philosophical issues in lesser and greater depth.

In this talk I will present the basic ideas of HoTT paying particular attention to its novel conceptual foundations, and discussing a selection of philosophical issues in lesser and greater depth.

5:30pm BLC Annual General Meeting
7:30pm Conference Dinner in Brighton
More info soon.

Saturday 9th of September

9:30am Invited Talk: Tamara van Glehn (Cambridge): Games, traces and distributive laws
Game semantics studies various categories of two-player games with strategies as morphisms. For simple games, composition of strategies can be viewed as taking a trace in a compact closed category. In this talk we will investigate how this can be extended to more complex notions of game, by considering the interaction of monads and comonads and lifting traced monoidal structure to their Kleisli categories and coalgebras. This is joint work in progress with Martin Hyland.
10:30am Richard Whyman (Leeds): How do we Describe the Computational Capabilities of an Arbitrary Physical System?
Over the years various forms of physical computation whose method of computation is clearly distinct from that of the classic Turing machine model have been proposed and indeed utilised. Quantum computation being one of the most notable of these.

Various formalisms have already been proposed for describing in general how such physical systems compute . However, when it comes to describing what problems can be feasibly decided by these systems attention has typically focused on deriving complexity measures that only make sense in specific physical contexts. These measures are also typically incompatible with quantum computational complexity, which itself potentially falls short of providing reasonable complexity measures for physical systems that are even more computationally powerful than quantum computers, if such systems exist.

In this talk I shall present a new formalism for describing computation on an arbitrary physical system that avoids the time-dependent sequential algorithm and instead looks to the first-order theory of a given physical system for describing its decision capabilities. Computability-wise my new formalism suggests, as expected, that physical systems have the same decision capacity as Turing machines do. Complexity-wise this formalism gives the standard complexity classes for Turing machines and similar sequentially acting physical systems. However, the formalism also suggests that there are some physical systems which can, by going beyond the sequential algorithm, decide problems in $NP \cap co-NP$ rather than $P$, whilst utilising a polynomially bounded amount of resources.

Since factoring, the discrete logarithm and other problems that are feasibly computable by a quantum computer lie in $NP \cap co\text{-}NP$ our formalism potentially explains where the additional power of quantum computation is derived from.

11am Tea/Coffee
11:30am Invited Talk: Sam Staton (Oxford): Semantic models of higher-order probability theory
Bayesian statistics is full of interesting structure, particularly in its 'non-parametric' aspects. We have been working on semantic models for this structure from the perspective of probabilistic programming. For example, regression problems involve random functions, and we have built a new version of probability theory that allows probability measures over function spaces.

The talk will be based around recent papers in Proc. LICS and Proc. ESOP, partly in collaboration with Chris Heunen, Ohad Kammar, Frank Wood, Hongseok Yang and others.

12:30pm Uli Berger (Swansea): A concurrent computational interpretation of the law of excluded middle
We give a computational interpretation of the law of excluded middle as a scheme for the concurrent execution of processes. The interpretation, which takes place within the framework of realisability, involves two new logical operators: Set_n(A), allowing for n concurrent processes to realise the formula A, and A || B ('A restricted to B') which is realised by a computation that is guaranteed to terminate if A holds and, in case of termination, realises A.

We apply this interpretation to two examples of program extraction in computable analysis: Infinite Gray-code and matrix inversion via concurrent Gaussian elimination.

1pm - 2:30pm LUNCH
2:30pm John Longley (Edinburgh): Robust computability notions for types arising in classical analysis
A recurring question in computability theory has been whether one can identify a single `canonical' notion of computable operation on data of some given kind. If the data are natural numbers (or equivalently finite strings over a finite alphabet), then the existence of such a canonical notion is of course what is claimed by the classical Church-Turing thesis. If the data are themselves of a higher-order nature, then the situation is much more complex, but work of Normann (2000) and Longley (2007) has shown that even widely divergent concepts of higher-order computability will typically converge in the class of 'hereditarily total' functionals they give rise to.

I will outline some recent extensions of these results that imply the existence of similarly robust computability notions for many kinds of data arising in traditional mathematical practice, particularly complex analysis. To construct types such as the space of analytic functions on a given complex domain, one typically needs recourse not just to function spaces but also to subset and quotient types, and these constitute a non-trivial extension from the point of view of computability theory: the computable functions on a subset S of T are not immediately determined by those on T, as there may well be computable functions on S with no computable extension to T. Nevertheless, our new results show that one still obtains highly robust and `canonical' computability notions for a wide range of mathematical types arising in this way.

The talk will be high-level and aimed at a non-specialist audience. I will concentrate on the motivations for the work and on concrete mathematical examples, and will attempt a gentle introduction to the way in which the theorems in question are formulated, but will not go into their proofs.

A draft paper covering most of the material to be discussed is available at http://homepages.inf.ed.ac.uk/jrl/Research/ubiquity-reloaded3.pdf
3pm Paulo Oliva (Queen Mary London): Modular Searching with Higher-order Functions
In this talk I’ll describe how some searching algorithms (from simple exhaustive search to alpha-beta prunning) can be done in a modular way using the continuation monad.
3:30pm END of MEETING