Past Alan Tayler Lecture

23 November 2015
Professor Philip Bond

 On November 25th 1915 Albert Einstein submitted his famous paper on the General Theory of Relativity. David Hilbert also derived the General Theory in November 1915 using quite different methods. In the same year Emmy Noether derived her remarkable ‘Noether’s Theorem’ which lies at the heart of much modern Physics. 1915 was a very good vintage indeed. We will take a brief walking tour of General Relativity using some of the ideas of Noether, Hilbert and Einstein to examine gravitational redshift, gravitational lensing, the impact of General Relativity on GPS systems and high precision atomic clocks, and Black holes all of which can be summarised by asking ‘how long is a piece of spacetime?’ 

4 March 2015
Martin Escardo

 Voevodsky asked what the topology of the universe is in a 
continuous interpretation of type theory, such as Johnstone's 
topological topos. We can actually give a model-independent answer: it 
is indiscrete. I will briefly introduce "intensional Martin-Loef type 
theory" (MLTT) and formulate and prove this in type theory (as opposed 
to as a meta-theorem about type theory). As an application or corollary, 
I will also deduce an analogue of Rice's Theorem for the universe: the 
universe (the large type of all small types) has no non-trivial 
extensional, decidable properties. Topologically this is the fact that 
it doesn't have any clopens other than the trivial ones.