[logic-ml] JAIST Logic Seminar Series

[Hajime Ishihara]

皆様

LMUミュンヘンのHelmut Schwichtenberg先生の講演のお知らせです。
どうぞふるってご参加ください。

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

* JAIST Logic Seminar Series *

* The seminar below is held as a part of JSPS Core-to-Core Program,
A. Advanced Research Networks and EU Horizon 2020
Marie Skłodowska-Curie actions RISE project CID
(http://www.jaist.ac.jp/logic/ja/core2core, http://cid.uni-trier.de/).

Date: Wednesday 6 March, 2019, 15:20-17:00

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

Speaker: Professor Helmut Schwichtenberg (Mathematisches Institut, LMU 
Muenchen)

Title: Equality and extensionality

Abstract:
We sketch a theory of computable functionals (TCF) based on
finitary algebras given by their constructors.  Its intended semantics
admits non-total functionals.  For closed algebras of level zero we
allow infinite stream-like objects.  For higher types we define
(pointwise) equality as a logical relation, and extensionality by
diagonalization of equality.  We define realizability and -- in the
spirit of Kolmogorov (1932) -- add an invariance axiom: every
computationally relevant (c.r.) formula A is equivalent to the
existence of an extensional realizer of A.  Then we can prove (ordinary
and dependent) choice, and also a soundness theorem stating that the
computational content extracted from a proof of a c.r. formula A
realizes A.