RUS  ENG JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PERSONAL OFFICE
 Forthcoming seminars Seminar calendar List of seminars Archive by years Register a seminar Search RSS Forthcoming seminars

You may need the following programs to see the files

Colloquium of the Steklov Mathematical Institute of Russian Academy of Sciences
December 5, 2013 16:00, Moscow, Steklov Mathematical Institute of RAS, Conference Hall (8 Gubkina)

Probably recursive functions

L. D. Beklemishev
 Video records: Flash Video 692.6 Mb Flash Video 4,150.0 Mb MP4 692.6 Mb

Abstract: A computable function $f\colon N\to N$ is called provably recursive in a formal theory $T$ if there is an algorithm computing $f$ such that the statement “for all $x$ there is a $y$ such that $f(x)=y$” is provable in $T$. Such functions are studied in mathematical logic for two main reasons. Firstly, given a program we are often interested in proving its correctness, in particular, that its computation terminates on any input. The development of program verification methods is an important topic in Computer Science. On the other hand, we can use provably recursive functions to study and compare various formal theories. This approach leads to the study of functions of exorbitant growth rates and to the most impressive examples, as of today, of unprovable combinatorial statements.