Bridges between Financial and Constructive Mathematics
14.07.2015

Time

Tuesday 14.07.2015

Speakers

• Douglas S. Bridges University of Canterbury, New Zealand
• Helmut Schwichtenberg LMU
• Gregor Svindland LMU
• Josef Berger LMU
• Peter M. Schuster University of Verona
• Davide Rinaldi University of Leeds
• Basil Karadais University of Padova
• Iosif Petrakis LMU

Morning talks

Richard Wagner-Str. 10 Raum 101

• Douglas S. Bridges 9:00-9:45: "Preference and Utility - Constructive Developments"
• Helmut Schwichtenberg 10:00-10:45: "Remarks on constructive analysis"
• Gregor Svindland 10:45-11:30: "A separating hyperplane theorem, the fundamental theorem of asset pricing, and Markov's principle, part I"
• Josef Berger 11:45-12:30: "A separating hyperplane theorem, the fundamental theorem of asset pricing, and Markov's principle, part II"

Lunch

Afternoon talks

Mathematisches Institut, Raum B 349

• Peter M. Schuster 14:30-15:15: "Eliminating Disjunctions by Disjunction Elimination"
• Davide Rinaldi 15:15-16:00: "Formal Topology, Domains & Finite Density"
• Basil Karadais 16:30-17:15: "Normal forms and linearity over nonflat domains"
• Iosif Petrakis 17:15-18:00: "A constructive Stone-Weierstrass theorem for pseudo-compact Bishop spaces"

Dinner

Zwingereck, Rumfordstr. 35

19:00

Abstracts

• Gregor Svindland and Josef Berger: "A separating hyperplane theorem, the fundamental theorem of asset pricing, and Markov's principle"
  
  We prove constructively that every uniformly continuous convex function f: X \to \R⁺ has positive infimum, where X is the convex hull of finitely many vectors. Using this result, we prove that a separating hyperplane theorem, the fundamental theorem of asset pricing, and Markov's principle are constructively equivalent. This is the first time that important theorems are classified into Markov's principle within constructive reverse mathematics.
  
  We show that the Lemma on Alternatives,
  
  ALT For every m x n matrix A, either
  i) there exists q ∈ X_m such that q A ≤ 0 or
  ii) there exists p ∈ X_n such that A p ≥ 0
  
  is equivalent to LLPO. X_m is the set of elements of Rⁿ such that every component is nonnegative and the sum of the components is 1.
• Peter M. Schuster: "Eliminating Disjunctions by Disjunction Elimination" (joint work with Davide Rinaldi)
  
  If a Scott-style multi-conclusion entailment relation E extends a Tarskian single-conclusion consequence relation C, then E is conservative over C precisely when the appropriate rule of disjunction elimination can be proved for C. This readily follows from a sandwich criterion due to Scott, but can also be fleshed out into a proof-theoretical reduction. The principal application is to turn transfinite methods into admissible rules. For instance, contrapositive forms of Zorn's Lemma that are also known as completeness or spatiality are often applied in concrete contexts in which the corresponding conservation theorems would suffice. We now give a syntactical, uniform approach to many of those conservation theorems for definite Horn clauses, e.g. to the ones corresponding to the theorems by Krull-Lindenbaum, Artin-Schreier, Szpilrajn and Hahn-Banach. Related work can be found in locale theory (Mulvey--Pelletier 1991), dynamical algebra (Coste--Lombardi--Roy 2001, Lombardi 1997--8), formal topology (Cederquist--Coquand--Negri 1998) and proof theory (Coquand--Negri--von Plato 2004, Negri--von Plato 2011).
  
  This research is funded by the John Templeton Foundation project "Abstract Mathematics for Actual Computation: Hilbert's Program in the 21st Century". The speaker currently is an Alexander-von-Humboldt Foundation research fellow at the Munich Center for Mathematical Philosophy.
• Basil Karadais: "Normal forms and linearity over nonflat domains"
  
  Domain theory continues to be the prevalent norm in denotational semantics since the early works of Dana Scott and Gordon Plotkin in the seventies. In the traditionally preferred setting we interpret types as function spaces over f l a t rather than n o n f l a t domains for the base types. This is for good reasons: on the one hand, the flat model is already rich enough to address deep theoretical issues (like sequentiality and full abstraction), and on the other hand the nonflat model, though arguably mathematically more sound, may present daunting combinatorial complexity when one focuses on its details. Nevertheless, driven by necessity or curiosity, there have been several authors in the recent past who have taken up the challenge of looking into the nonflat model and its merits. This tendency can even be seen as a theoretical counterpart of the rise of increasingly practical nonstrict programming languages, like Haskell.
  In an attempt to tame the combinatorial complexity of the nonflat model, we study normal forms of finite approximations of objects. We then use our results to investigate the status of linearity (a concept which has strong ties to the notion of sequentiality, as Guo-Qiang Zhang has showed in the eighties): we show that we can work linearly in a systematic way within the nonlinear model, as well as restrict to a fully linear model whose ideals are in a bijective correspondence with the ones of the nonlinear.
• Iosif Petrakis: "A constructive Stone-Weierstrass theorem for pseudo-compact Bishop spaces"
  
  We introduce the notion of a base of a Bishop space and we describe its relation to the notion of a subbase in the case of a pseudo-compact Bishop space. We describe the base of a product of pseudo-compact Bishop spaces and we prove a Stone-Weierstrass theorem for pseudo-compact Bishop spaces. We work within Bishop's informal system of constructive mathematics BISH, inductive definitions included.
  

  Last modified

  07. Juli 2015