Invited talks
-
Gaps in Hardy fields. Matthias Aschenbrenner, University of Vienna
Hardy fields are an algebraic setting for a tame part of asymptotic analysis. In this talk, after an introduction into this area, I will explain what we know and don’t know about gaps in Hardy fields, with particular focus on analytic Hardy fields, which are those that mainly arise in practice. (Joint work with L. van den Dries and J. van der Hoeven.)
-
Forcing axioms, (*), and the Continuum Problem. David Aspero, University of East Anglia, United Kingdom
In this talk I will survey old and new results concerning the role that forcing axioms, and other principles in their region, play in the ongoing search for natural axioms supplementing ZFC.
-
Logic and property testing on graphs of bounded degree. Isolde Adler, University of Bamberg, Germany
Property testing (for a property P) asks for a given graph, whether it has property P, or is “structurally far” from having that property. A “testing algorithm” is a probabilistic algorithm that answers this question with high probability correctly, by only looking at small parts of the input. Testing algorithms are thought of as “extremely efficient”, making them relevant in the context of large data sets.
In this talk I will introduce property testing and present recent positive and negative results about testability of properties definable in first-order logic and monadic second-order logic on classes of bounded-degree graphs.
This is joint work with Polly Fahey, Frederik Harwath, Noleen Köhler and Pan Peng.
-
Synthetic Computability Theory without Choice. Yannick Forster, Inria Paris, France
Mathematical practice in most areas of mathematics is based on the assumption that proofs could be made fully formal in a chosen foundation in principle. This assumption is backed by decades of formalising various areas of mathematics in various proof assistants and various foundations. An area that has been largely neglected for computer-assisted and machine-checked proofs is computability theory. This is due to the fact that making computability theory (and its sibling complexity theory) formal is several orders of magnitude more involved than formalising other areas of mathematics, due to the – citing Emil Post – ``forbidding, diverse and alien formalisms in which this […] work of Gödel, Church, Turing, Kleene, Rosser […] is embodied.’’. For instance, there have been various approaches of formalising Turing machines, all to the ultimate dissatisfaction of the respective authors, and none going further than constructing a universal machine and proving the halting problem undecidable. Professional computability theorist and teachers of computability theory thus rely on the informal Church Turing thesis to carry out their work and only argue the computability of described algorithms informally.
A way out was proposed in the 1980s by Fred Richman and developed during the last decade by Andrej Bauer: Synthetic computability theory, where one assumes axioms in a constructive foundation which essentially identify all (constructively definable) functions with computable functions. A drawback of the approach is that assuming such an axiom on top of the axiom of countable choice - which is routinely assumed in this branch of constructive mathematics and computable analysis - is that the law of excluded middle, i.e. classical logic, becomes invalid. Computability theory is however dedicatedly classical: Almost all basic results are presented by appeal to classical axioms and even the full axiom of choice.
We observe that a slight foundational shift rectifies the situation: By basing synthetic computability theory in the Calculus of Inductive Constructions, the type theory underlying amongst others the Coq proof assistant, where countable choice is independent and thus not provable, axioms for synthetic computability are compatible with the law of excluded middle.
I will give an overview over a line of research investigating a synthetic approach to computability theory in constructive type theory, discussing, if time allows, suitable axioms, a Coq library of undecidability proofs, results in the theory of reducibility degrees, a synthetic definition of Kolmogorov complexity, constructive reverse analysis of theorems, and synthetic oracle computability.
Parts of results are in collaboration with Dominik Kirst, Gert Smolka, Felix Jahn, Fabian Kunze, Nils Lauermann, Niklas Mück, Haoyi Zeng, and the contributors of the Coq Library of Undecidability Proofs.
-
Broad Infinity and Generation Principles. Paul Blain Levy, University of Birmingham, United Kingdom.
We introduce Broad Infinity, a new set-theoretic axiom scheme that may be considered plausible. It states that three-dimensional trees whose growth is controlled by a specified class function form a set. Such trees are called “broad numbers”.
Assuming the axiom of choice, or at least the weak version known as WISC, we see that Broad Infinity is equivalent to Mahlo’s principle, which states that the class of all regular limits is stationary. Broad Infinity also yields a convenient principle for generating a subset of a class using a “rubric” (family of rules). This directly gives the existence of Grothendieck universes, without requiring a detour via ordinals.
In the absence of choice, Broad Infinity implies that the derivations of elements from a rubric form a set. This yields the existence of Tarski-style universes.
Additionally, we reveal a pattern of resemblance between “Wide” principles, that are provable in ZFC, and “Broad” principles, that go beyond ZFC.
-
Incompleteness Theorems for Observables in General Relativity. Aristotelis Panagiotopoulos, Kurt Gödel Research Center for Mathematical Logic, University of Vienna, Austria
One of the biggest open problems in mathematical physics has been the problem of formulating a complete and consistent theory of quantum gravity. Some of the core technical and epistemological difficulties come from the fact that General Relativity (GR) is, fundamentally, a geometric theory and, as such, it oughts to be ‘generally covariant,’ i.e. invariant under change of coordinates by the arbitrary diffeomorphism of the ambient manifold. The Problem of Observables is a famous instance of the difficulties that general covariance brings into quantization: no non-trivial diffeomorphism-invariant quantity has ever been reported on the collection of all spacetimes. It turns out that there is a good reason for this. In this talk, I will present my recent joint work with Marios Christodoulou and George Sparling, where we employ methods from Descriptive Set Theory (DST) in order to show that, even in the space of all vacuum solutions, no complete observables for full GR can be Borel definable. That is, the problem of observables is to ‘analysis’ what the Delian problem is to ‘straightedge and compass.’
-
Christina Vassilakopoulou, National Technical University of Athens, Greececancelled
Tutorials
-
Degrees of Unsolvability: A Realizability-theoretic perspetive. Takayuki Kihara, Nagoya University, Japan
The theories of degrees of unsolvability and realizability interpretation both have long histories, having both been born in the 1940s. S. C. Kleene was a key figure who led the development of both theories. Despite having been developed by the same person, there seems to have been little deep mixing of these theories until recently. In this tutorial, we will reconstruct the theory of degrees of unsolvability from the perspective of realizability theory.
-
Formalising mathematics with proof assistants. Angeliki Koutsoukou-Argyraki, Royal Holloway University of London, United Kingdom
Part I
The first part of this tutorial will involve a general introduction to the area of formalisation of mathematics using proof assistants (interactive theorem provers). I will discuss the state of the art and potential of the area.
Part II
During the second part, I will give some practical information for beginners on getting started with the proof assistant Isabelle/HOL, and as an example I will present a formalisation of Aristotle’s Assertoric Syllogistic in Isabelle/HOL.
Special Sessions
Philosophy
-
Classicism, Free Classicism, and Necessitism. Cian Dorr, New York University, United States of America
A very natural higher order logic, ‘Classicism’, can be axiomatized by adding the rule of substitution of logical equivalents to a basic higher order logic (comprising standard classical rules for connectives, quantifiers, and identity, together with lambda conversion rules). Perhaps its most controversial theorem is ’Broad Necessitism’, according to which for every thing (in a given type), the proposition that there is something identical to that thing is identical to a tautology. For those who want to avoid this result, it is natural to retreat to ‘Free Classicism’, the variant of Classicism in which the quantifier rules are weakened to those of free logic. Within Free Classicism, we develop a general theory of what it is for a property of properties of things of some given type to be a (universal, perhaps-restricted) quantifier, as well as a notion of absolute unrestrictedness for quantifiers, which is uniquely instantiated (in a type) if instantiated at all. Using these tools we introduce a central question facing Free Classicists: are there any absolutely unrestricted quantifiers, and if not, is being an absolutely unrestricted quantifier even possible (in the sense of not being identical to a contradictory property)? We present an argument for the claim that there are absolutely unrestricted quantifiers, and a further argument, based on metasemantic considerations, that if there are such quantifiers, Classicism is true.
-
Upper Logicism. Bruno Jacinto, University of Lisbon, Portugal
Russell strived to defend the view that arithmetic is nothing but logic by conceiving of the natural numbers as the finite cardinalities. The received view is that Russell’s logicist project has failed. His reduction of arithmetic to logic presupposed the axiom of infinity’s logicality. But the axiom of infinity doesn’t appear to be a logical truth, as Russell himself acknowledged.
In this talk I present and partially defend Upper Logicism - a neoRussellian form of logicism based on higher-order modal logic. As I’ll show, among its virtues is the fact that the Upper logicist reduction of arithmetic to logic does not rely on the axiom of infinity’s truth or logicality. I’ll conclude by comparing Upper Logicism with other, seemingly related, philosophies of arithmetic, and sketching how to extend it to a logicist reduction of set theory.
-
Diagonalization and Paradox. Gabriel Uzquiano, University of Southern California, United States of America
We aim to clarify the role of diagonalization in the derivation of important limitative results in higher-order logic. A familiar diagonal argument is generally involved in common derivations of the inconsistency of Frege’s Axiom V and the Russell-Myhill theorem. These observations are often given a cardinality gloss, which presuppose a measure of impredicativity. We will look at further limitative results underwritten by the diagonal argument even in the presence of predicative strictures. These observations will place additional constraints on consistent implementations of structured views of propositions, even though they have nothing to do with cardinality.
In memoriam: Thanases Pheidas
-
Decidability results of subtheories of polynomial rings and formal power series. Dimitra Chompitaki, University of Crete, Greece
Hilbert’s tenth problem (the tenth of the famous list of problems Hilbert proposed in 1900) was:
H10(ℤ): Find a procedure (in modern terminology: an algorithm) which determines (in a finite number of steps) whether an arbitrary polynomial (for any degree and any number of variables), with integer coefficients, has or does not have integer zeroes.When Hilbert proposed this problem in 1900, the notion of an algorithm was not yet formalized. The theory of recursive functions was developed about 30 years later. Hilbert’s tenth problem was answered negatively by Y. Matiyasevich in 1970, after work by M. Davis, H. Putnam and J. Robinson. In modern terminology, the positive existential theory of the ring ℤ of the rational integers is undecidable.
Since then a number of similar problems have been solved over other domains of mathematical interest. However, some others remain open. For example, although the theory of a ring of power series F[[z]] in a variable z over a field F with a decidable theory is decidable if the characteristic of F is zero, the similar problem for F of positive characteristic p is open problem.
Thus, it is interesting at least to produce results which produce algorithms for deciding certain sub-theories of the full ring theory of F[[z]], for F of positive characteristic. In this talk, we will survey decidability and undecidability results of the structures and substructures of polynomial rings and rings of formal power series.
Then we will focus on the structure of addition and localized divisibility in polynomial rings and the corresponding rings of formal power series and inter relations. In particular, we will show that a ring of polynomials over a prime field is an elementary substructure of the corresponding ring of formal power series in the language of addition, localized divisibility, equality and the constants 0 and 1.
Finally, the theories of these structures admit elimination of quantifiers. In addition, we will present some theorems that relate the positive and the zero characteristic cases
-
Reflections on the work of T. Pheidas. Konstantinos Kartas, Sorbonne University, France
Hilbert’s tenth problem is to devise an algorithm which decides whether a given polynomial equation in many variables has a solution in the integers. The celebrated DPRM theorem (after Davis, Putnam, J. Robinson and Matiyasevich) shows that in fact no such algorithm exists. It is also natural to consider variants of Hilbert’s tenth problem, where one seeks for solutions in domains other than the integers. We will survey some of the most important results in that direction, which were obtained by Pheidas.
-
The Mathematics of Thanasis Pheidas: Explained for an audience that includes non-mathematicians. Lefteris Kirousis, University of Athens, Greece
Anticipating that a sizable portion of the audience will be non-mathematicians, I will give a presentation not of the novel technical results by Thanasis but of the wider area where these results belong and their significance aiming on the one hand to be comprehensible to the non-technically trained listeners and on the other to hold the interest of fellow logicians, especially the younger ones and students, working in other areas.
-
The journey of Thanases Pheidas in the realm of analytic functions. Xavier Vidaux, University of Concepción, Chile
Though Thanases has worked in all the major open problems in the area of Hilbert’s Tenth Problem, I believe that analytic functions had a special place in his heart. I will tell some things that I know about his contributions there, and how his 1995 failure to solving the problem for entire functions led him to a series of beautiful ideas.