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

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