[kisoron-ml] JAIST Logic Seminar Series

[Hajime Ishihara]

皆様

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

問合せ先：
石原　哉
北陸先端科学技術大学院大学 情報科学研究科
e-mail: ishihara at 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

-- 
Professor Hajime Ishihara
School of Information Science
Japan Advanced Institute of Science and Technology
1-1 Asahidai, Nomi, Ishikawa 923-1292, Japan
Tel: +81-761-51-1206
Fax: +81-761-51-1149
ishihara at jaist.ac.jp
http://www.jaist.ac.jp/~ishihara