皆様
リュブリャナ大学のAndrej Bauer教授の講演のお知らせです。 ふるってご参加ください。
問合せ先： 石原 哉 北陸先端科学技術大学院大学 情報科学研究科 e-mail: [email protected]
-------------------------------------------------- * 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
皆様
Munich Center for Mathematical Philosophy のMatthias Schirn 教授の講演を 開催いたします。 ふるってご参加ください。
問い合わせ先： 佐野勝彦 北陸先端科学技術大学院大学 情報科学研究科 e-mail: [email protected]
----------------------------------------------- * JAIST Logic Seminar Series *
Date: Tuesday 22 October, 2013, *15:00*-
Place: JAIST, Collaboration room 7 (I-56) (Access: http://www.jaist.ac.jp/english/location/access.html)
Speaker: Prof. Dr. Matthias Schirn (Munich Center for Mathematical Philosophy)
Title: HILBERT'S FINITISM, THE CONCEPT OF INFINITY, AND THE DECISION PROBLEM
Abstract: See http://www.jaist.ac.jp/~v-sano/seminars/Matthias_Schirn.pdf
皆様
University of Liverpool のDavide Grossi 教授の講演を 開催いたします。 どうぞふるってご参加ください。
問い合わせ先： 佐野勝彦 北陸先端科学技術大学院大学 情報科学研究科 e-mail: [email protected]
----------------------------------------------- * JAIST Logic Seminar Series *
Date: 1st November October, 2013, *15:30*-
Place: JAIST, Collaboration room 6 (I-57g) (Access: http://www.jaist.ac.jp/english/location/access.html)
Speaker: Davide Grossi (University of Liverpool)
Title: Interfaces between Epistemic Logic and Abstract Argumentation
Abstract: In this talk I will explore some connections between the theory of abstract argumentation and epistemic logic. In the first part I will propose an analysis of solution concepts from abstract argumentation in terms of dynamic epistemic logic. In the second part I will sketch a two-dimensional logic for the analysis of argument-based beliefs. All in all, the aim of my talk will be to lay some bridges between these two (apparently) very different approaches to the formalization of knowledge.
-
Hajime Ishihara