Ludwig-Maximilians-Universität München	Mathematisches Institut
Impressum	Datenschutz
Constructive convex analysis	Josef Berger                 Gregor Svindland

---

second CORE meeting

27 january 2017     Department of Mathematics, Theresienstraße 39, second floor, room B252

programme

9:45–10:00	J. Berger / G. Svindland	opening
10:00–10:45	Klaus Mainzer	Bridging Logic, Mathematics, Computer Science, and Philosophy
10:45–11:30	Vasco Brattka	The Computational Content of the Brouwer Fixed Point Theorem Revisited
11:30–12:15	Douglas S. Bridges	Boundaries and separation
13:45–14:30	Peter M. Schuster	Lindenbaum's Lemma, Syntactically?
14:30–15:15	Helmut Schwichtenberg	Logic for exact real arithmetic
15:30–16:15	Hajime Ishihara	A constructive proof of the minimax theorem
16:15–16:45	Takako Nemoto	Weak König's Lemma for convex trees
17:00–17:30	Tatsuji Kawai	The space of located subsets
17:30–18:00	Sam Sanders	The crazy Reverse Mathematics of Nonstandard Analysis and Computability Theory

Dinner (for the speakers)

19:00   Tafel & Schwafel, Augustenstr. 80

Abstracts

• Vasco BrattkaThe Computational Content of the Brouwer Fixed Point Theorem Revisited
  We discuss the uniform computational content of the Brouwer Fixed Point Theorem in the fine grained Weihrauch lattice. While the classification of this theorem from dimension three onwards can be achieved with a neat geometric argument, the classification in dimension two turns out to be more intriguing and can be obtained with an inverse limit construction. The analysis of the corresponding proofs hints at a computational difference of path wise connectedness in dimension two versus higher dimensions. Finally, we also discuss the question in which way Lipschitz continuity simplifies finding fixed points and we point out that there is a trichotomy depending on the whether the Lipschitz constant is less or larger than one or exactly one. In the last mentioned case the Brouwer Fixed Point Theorem is related to convexity by recent results of Neumann.
  This talk is based on joint work with Stéphane Le Roux, Arno Pauly and Joseph S. Miller.
• Tatsuji Kawai The space of located subsets
  We introduce the notion of located subset for continuous lattices in setting of a constructive and predicative point-free topology. Examples include detachable subsets of any set, spreads on the binary tree, the located upper cuts (i.e. extended reals), semi-located subsets of Bishop locally compact metric spaces (i.e. located subsets including the empty subset). We define a geometric theory over a continuous lattice whose models are the class of located subsets of the given continuous lattice. The formal topology (i.e. frame) presented by this theory is called the space of located subsets of the continuous lattice. The construction of this point-free space from a continuous lattice extends to a functor that is left adjoint to the forgetful functor from the category KReg of compact regular formal topologies to that of continuous lattices and perfect maps. Thus, the space of located subsets exhibits the Lawson topology on the continuous lattice. As expected, the monad on KReg induced by this functor is isomorphic to the Vietoris moand.
• Klaus MainzerBridging Logic, Mathematics, Computer Science, and Philosophy
  In a period of increasing specialization, the scientific communities of logic, mathematics, computer science, and philosophy seem to diverge in different directions. Foundational investigations in logic and mathematics are sometimes considered as merely philosophical issues without any practical meaning for mathematical research. But, actually, our practical mathematical applications (e.g., in scientific computing, numerical mathematics, functional analysis, financial mathematics) need constructive foundations, in order to become more safe, controllable, and reliable. Recent foundational research in proof mining, program extraction, and reverse mathematics is following this line. They stand in elder philosophical traditions of constructive and intuitionistic mathematics. Constructive Operations Research (CORE) means bridging logic, mathematics, computer science, and philosophy. In an age of increasing digitalization, people must get a deeper awareness of our information and algorithmic world.
• Sam SandersThe crazy Reverse Mathematics of Nonstandard Analysis and Computability Theory
  Reverse Mathematics is a program in the foundations of mathematics founded by Friedman. The goal is to find the minimal axioms required to prove a theorem of ordinary, i.e. non-set theoretic mathematics. Most such theorems fall into only five categories, called the Big Five, which are also linearly ordered. We show that the counterparts of the Big Five (and other systems) in Nonstandard Analysis behave very differently. These results are obtained via (and often reformulations of) results in higher-order computability theory. As an example, the nonstandard counterpart of WKL behaves like Kohlenbach’s generalisation of WKL, but with nonstandard continuity instead of the epsilon-delta variety.
  Joint work with Dag Norman.
• Peter Schuster Lindenbaum's Lemma, Syntactically?
  Our Universal Krull-Lindenbaum theorem has brought us to a an even more universal syntactical conservation criterion, for Scott's multi-conclusion entailment relations over Tarski-style single-conclusion ones. The criterion is satisfied, and therefore yields a proper conservation theorem, for many of the entailment relations by which one can describe an algebraic context (Cederquist-Coquand 2000). We thus have achieved in a uniform way syntactical counterparts of quite some forms of the Axiom of Choice, including cases already known before (Coste-Lombardi-Roy 2001, Negri-Coquand-von Plato 2004, etc.). Now we eventually dare to ask: what does this mean in logic, i.e. for Lindenbaum's Lemma proper? Perhaps we should rather ask: what is Gödel's completeness theorem good for?
  Joint work with Davide Rinaldi, Verona, and Daniel Wessel, Trento.
• Helmut Schwichtenberg Logic for exact real arithmetic
  Real numbers in the exact (as opposed to floating-point) sense can be given in different formats, for instance as Cauchy sequences (of rationals, with Cauchy modulus), or else as infinite sequences (streams) of (i) signed digits -1, 0, 1 or (ii) -1, 1, bot containing at most one copy of bot (meaning undefinedness), so-called Gray code (di Gianantonio 1999, Tsuiki 2002). We are interested in formally verified algorithms on real numbers given as streams. To this end we consider formal (constructive) existence proofs M and apply a proof theoretic method (realizability) to extract their computational content. We switch between different representations of reals by labelling universal quantifiers on reals x as non-computational and then relativising x to a predicate CoI coinductively defined in such a way that the computational content of x in CoI is a stream representing x. The desired algorithm is obtained as the extracted term of the existence proof M, and the required verification is provided by a formal soundness proof of the realizability interpretation. As an example we consider multiplication of reals.