Mathematical Logic and Constructivity:

The Scope and Limits of Neutral Constructivism

Department of Mathematics, Stockholm University, August 20–23, 2019

With Errett Bishop’s seminal work Foundations of Constructive Analysis (1967), a neutral position in the foundations of constructive mathematics emerged. It avoided Brouwer’s assumptions about choice-sequences and continuity, and it did not assume that every total function on the natural numbers is computable. This made the position palatable also to the classical mathematician, and it is in the intersection of the three realms of foundations, commonly designated by the abbreviations INT, RUSS and CLASS. Successful full-fledged formal logical foundations for neutral constructivism exists, among the most well-known are Aczel-Myhill set theory and Martin-Löf type theory. Neutral constructive mathematics may also be studied for systems that make fewer ontological assumptions, which is important for reverse mathematics. To the surprise of many in constructive mathematics a new principle about sequences, the boundedness principle BD-N, was discovered, and found to be true in all the three realms without being true in neutral constructvism. Further principles of this kind are being investigated. In type theory new axioms have been discovered, such as the univalence axiom, whose constructive status was only later settled. Important questions are whether new axioms can be modelled indirectly using neutral constructive methods, or whether they can be directly justified.

This workshop aims to focus on the scope and limits of neutral constructivism. The study of neutral constructivism paves the way for further developments of interactive proof systems, which is of strategic importance for verification of software, and in particular, correctness-by-construction software.

Registration

Attendance at talks is open to all. The registration deadline for other conference activities has now passed, but for any inquiries please email the organisers at mloc19@math.su.se.

Schedule and practicalities

Talks run from Tuesday 20/8 to Friday 23/8, 9:30–18:00 daily, along with a conference reception Tuesday evening, excursion Thursday afternoon, and dinner on Thursday evening. Full schedule and abstracts.

All talks will take place in the SU Mathematics Department, Kräftriket, building 5, room 14 (just inside entrance B): map. Further practical information (transport, accommodation, etc) is here.

Invited speakers

  • Douglas S. Bridges, University of Canterbury, Christchurch, New Zealand
  • Thierry Coquand, Chalmers and Göteborg University, Sweden
  • Martín Escardó, University of Birmingham, England
  • Makoto Fujiwara, Meiji University, Japan
  • Nicola Gambino, Leeds University, England
  • Henri Lombardi, Université Franche-Comté, France
  • Maria Emilia Maietti, University of Padova, Italy
  • Takako Nemoto, JAIST, Japan
  • Iosif Petrakis, Ludwig Maximilian University of Munich, Germany
  • Thomas Streicher, TU Darmstadt, Germany
  • Hideki Tsuiki, Kyoto University, Japan
  • Chuangjie Xu, Ludwig Maximilian University of Munich, Germany
  • Keita Yokoyama, JAIST, Japan

Programme committee

  • Hajime Ishihara, JAIST, Japan (co-chair)
  • Tatsuji Kawai, JAIST, Japan
  • Peter LeFanu Lumsdaine, Stockholm University
  • Anders Mörtberg, Stockholm University
  • Erik Palmgren, Stockholm University (co-chair)

Local organisation committee

  • Menno de Boer
  • Guillaume Brunerie
  • Johan Lindberg
  • Peter LeFanu Lumsdaine
  • Anna Montaruli
  • Anders Mörtberg
  • Erik Palmgren

Sponsors