Münchenwiler Meeting Autumn 2018

Ingo Blechschmidt — "New reduction techniques in commutative algebra driven by logical methods"

We present a new reduction technique which proposes the following trade-off: If we agree to restrict to constructive reasoning, then we may assume without loss of generality that a given reduced ring is Noetherian and in fact a field, thereby reducing to one of the easiest situations in commutative algebra.

This technique is implemented by constructing a suitable sheaf model and cannot be mimicked by classical reduction techniques. It has applications both in constructive algebra, for mining classical proofs for constructive content, and in classical algebra, where it has been used to substantially simplify the 50-year-old proof of Grothendieck's generic freeness lemma.

Almudena Colacito — "An Open Problem in the Theory of Ordered Groups"

In 2004, Sikora’s paper Topology on the spaces of orderings of groups [3] pioneered a new perspective on the study of the interplay between topology and ordered groups, that has led to applications to both orderable groups and algebraic topol- ogy (see, e.g., [2]). The basic construction in Sikora’s paper is the definition of a topology on the set of orders on a given orderable group.

It is known that free groups are orderable, and hence, it is possible to consider the topological space of orders on a free group. Nonetheless, for free groups of finite rank n ≥ 2, the so-called ‘homeomorphism type’ of the corresponding topo- logical space is still unknown. In this talk, we are going to focus on the following related open problem:

 Question 1. Does the space of orders on a free group of rank n ≥ 2 have isolated points?

This question was first raised (in an equivalent form) by McCleary [1] in 1985, and negatively answered by Sikora in the Abelian case. After sketching Sikora’s original proof for the Abelian case, I am going to present an alternative approach to the problem, based on a correspondence between the space of orders on the free Abelian group and a topological space naturally associated with the free Abelian lattice-ordered group (called its spectral space). As we show in an ongoing work with Vincenzo Marra, such a correspondence is not limited to the Abelian set- ting, and can be seen as an instance of a much more general result involving all the varieties of lattice-ordered groups. I am thereby going to conclude by illustrat- ing how this alternative approach could be exploited to eventually open up new paths towards solving Question 1 — and maybe other open problems in the theory of ordered groups.

  [1] A. K. Arora. and S. H. McCleary. Centralizers in free lattice-ordered groups. Houston Journal of Mathematics, 12(4):455–482 (1986).
  [2] A. Clay and D. Rolfsen. Ordered Groups and Topology. Vol. 176. American Mathematical Society (2016).
  [3] A. Sikora. Topology on the spaces of orderings of groups. Bulletin of the London Mathematical Society, 36(4):519-526 (2004).

Kentaro Sato — "Interpretation Sextet: Renovations of Proof Theoretic Reducibility"

Reductive proof theory aims (in part) at proving relative consistency of formal systems which formalise (reasonably large fragments of) mathematics, whereas proof theory, in Hilbert's original idea, aimed at proving absolute consistency. In this talk, renovations of relative consistency results (or more generally proof theoretic reducibility) based on interpretation will be explained. The emphasis will be on the historical and philosophical motivations for this enterprise, rather than technical results. We will see relative consistency results by one interpretation, those by two interpreations, then those by three, by four --- finally those by six.

Peter Michael Schuster — "The Jacobson Ideal and Glivenko's Theorem"

Joint work with Giulio Fellin and Daniel Wessel (both University of Verona)

Alongside the analogy between maximal ideals and complete theories, the Jacobson radical carries over from ideals of commutative rings to theories of propositional calculi. This prompts a variant of Lindenbaum's Lemma that relates classical validity and intuitionistic provability, and the syntactical counterpart of which is Glivenko's Theorem. Apart from shedding some more light on intermediate logics, this eventually prompts a non-trivial interpretation in logic of Rinaldi, Schuster and Wessel's conservation criterion for Scott-style entailment relations (BSL 2017 & Indag. Math. 2018).

Franziskus Wiesnet — "Applications of the Functional Interpretation with States"

In his paper "A functional interpretation with state" Thomas Powell considers an extension of Gödel's functional interpretation. This new interpretation is not given by a static term, but it depends dynamically on a state, which codes the underlying mathematical environment. In this talk we show how we can use the functional interpretation with states for several applications, and how we have dealt with some of the ensuing difficulties. In particular, we consider learning-based realizability, i.e. a realiser of the law of excluded middle, and how one can use the functional interpretation with states to improve the efficiency of realisers.