[logic-ml] Talk by G. Sambin and M. Maietti [13 Mar 15:30-]

[Shinya Katsumata]

京都大学数理解析研究所の勝股です。

3月13日15:30から、University of PadovaのGiovanni Sambin氏とMaria
Emilia Maietti氏に以下の講演をしていただくことになりましたので、ご連絡
いたします。どうぞお気軽にお越しください。
==========
Time:    15:30-17:30, 13 Mar, 2015
Place:    Rm 478, Research Building 2, Main Campus, Kyoto University
    http://www.kyoto-u.ac.jp/en/access/yoshida/main.html (See 34)
    京都大学 本部構内 総合研究2号館 4階478号室
    http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm (34番の建物)

Speaker: Giovanni Sambin and Maria Emilia Maietti (University of Padova)

Title:

1 A new foundation of constructive mathematics 50 years after Bishop's FCA
2 Why developing mathematics in a two-level foundation

Abstract:
--- 1. Giovanni Sambin ---
A new foundation of constructive mathematics 50 years after
Bishop's FCA

Bishop's book Foundations of constructive analysis, 1967, briefly
CFA, showed that constructive mathematics can be emancipated from
the subjective views of its founder Brouwer.  That single book
started the process turning constructive mathematics into a rich
and lively research field and community, as it is today.

While standing on the shoulders of such giants, after almost
fifty years it is our task to see further.  Some epochal changes
which took place after 1967 provide motivations and support.
Outside mathematics:

1. Evolutionary thought has expanded its range of application and
   is now commonly accepted in science, except in
   mathematics. The main challenge awaiting us is to pass from a
   static, transcendent view of mathematics to a dynamic, human
   one.
2. The power of computers and other tools has enormously
   increased. Their active role in mathematical research will
   certainly also increase. This requires fully detailed formal
   systems for the foundation of mathematics.
3. Diffusion of information technology makes our world intensely
   connected. One feels the need of a framework which allows for
   a plurality of different world views.

Moreover, inside mathematics:

1. new branches have been created,
2. other branches besides analysis have been constructivized,
   such as algebra and topology.

The talk will give a preliminary view on a new foundational
system inspired by these facts, first introduced in 2005 and
later developed by M. E. Maietti and myself and called the
Minimalist Foundation, shortly MF.

Aims of MF include:

1. to permit the development of constructive mathematics,
   including topology, in agreement with a dynamic
   view (different levels of abstractions, real and ideal
   entities,...),
2. to provide a framework in which virtually all foundations of
   mathematics can be expressed by adding some assumptions (hence
   the adjective minimalist) and hence in particular a good
   setting for reverse mathematics,
3. to allow formalization of mathematics in a computer language,
4. to express the computational content of mathematics.

More specifically MF keeps:

1. an effective notion of set different from an ideal notion of
   collection
2. the notions of operation (with instructions) distinct from
   that of function (without instructions),
3. a positive notion of existence

We wish to know that MF is consistent by a proof, not by faith or
feelings.  One can prove much more than consistency for MF,
namely a normalization theorem, a realizability interpretation,
implementation in a proof-assistant.  We conclude the talk by
showing that one needs a theory with two levels of abstraction,
thus providing a good introduction to Maietti's talk.

--- 2. Maria Emilia Maietti ---
Why developing mathematics in a two-level foundation

We provide motivations for developing mathematics in a two-level
formal system following the ideas put forward in joint work with
G. Sambin in [MS05].

There we introduced the notion of two-level system to found
constructive mathematics but it turned out that the same notion
can be accomodated to develop mathematics in general with
computer-aided formalization of its proofs.

A main motivating example of such foundations is the Minimalist
Foundation for constructive mathematics which was ideated in
[MS05] and completed into two levels in [M09].  Its peculiarity
is that it is compatible with most relevant constructive and
classical foundations at the "right level". Another perculiarity
is that its design makes use of different languages: mostly that
of type theory, but also that of category theory and axiomatic
set theory.

[MS05] M.E. Maietti and G. Sambin "Toward a minimalist foundation
      for constructive mathematics" in L. Crosilla and
      P. Schuster eds., ''From Sets and Types to Topology and
      Analysis: Practicable Foundations for Constructive
      Mathematics", Oxford University Press, 2005

[M09] M.E. Maietti "A minimalist two-level foundation for
      constructive mathematics" Annals of Pure and Applied Logic
      160(2009):319-354