皆様

リュブリャナ大学のAndrej Bauer教授の講演のお知らせです。 ふるってご参加ください。

問合せ先： 石原　哉 北陸先端科学技術大学院大学 情報科学研究科 e-mail: ishihara@jaist.ac.jp

-------------------------------------------------- * JAIST Logic Seminar Series *

* This seminar is held as a part of the EU FP7 Marie Curie Actions IRSES project COMPUTAL (http://computal.uni-trier.de/).

Date: Friday 20 September, 2013, 15:00-17:00

Place: JAIST, Collaboration room 6 (I-57g) (Access: http://www.jaist.ac.jp/english/location/access.html)

Speaker: Professor Andrej Bauer (University of Ljubljana, Slovenia)

Title: A higher inductive construction of the real numbers

Abstract: Homotopy type theory [1] is a foundation of mathematics based on Martin-Löf type theory extended with the Univalence axiom and higher inductive types. The latter allow us to present mathematical objects as inductive types generated by point and path constructors. For instance, the circle is represented by a type with a point and a loop satisfying the "circle induction" principle. In the first part I shall review higher inductive types.

In the second part of the talk I shall look at a higher inductive construction of real numbers. Ordinary higher inductive types do not seem to suffice -- instead we have to use a higher inductive-inductive definition which simultaneously constructs the reals and a proximity relation on them. We thus obtain a type of real numbers which satisfies a principle of "real induction". We can prove properties of reals by induction!

From a logical point of view the construction is interesting because it avoids the axiom of choice, impredicativity (powersets), and excluded middle. Nevertheless, the resulting theory still allows us to develop the basics of real analysis as usual.

The work described in the talk is joint work of the members of the Univalent foundations project [2].

References:

[1] Univalent Foundations Project: "Homotopy type theory: Univalent foundations of Mathematics", http://homotopytypetheory.org/book/

[2] Univalent Foundations Project, Institute for Advanced Study, Princeton, http://www.math.ias.edu/sp/univalent