RUS  ENG ЖУРНАЛЫ   ПЕРСОНАЛИИ   ОРГАНИЗАЦИИ   КОНФЕРЕНЦИИ   СЕМИНАРЫ   ВИДЕОТЕКА   ЛИЧНЫЙ КАБИНЕТ
Видеотека
Архив
Популярное видео

Поиск
RSS
Новые поступления





Для просмотра файлов Вам могут потребоваться






Летняя школа «Современная математика» имени Виталия Арнольда, 2018
21 июля 2018 г. 17:15–18:30, г. Дубна, Московская область, г. Дубна, дом отдыха «Ратмино»
 


Доказуемо рекурсивные функции, занятие 1

Л. Д. Беклемишев
Видеозаписи:
MP4 2,071.9 Mb
MP4 940.7 Mb

Количество просмотров:
Эта страница:131
Видеофайлы:65

Л. Д. Беклемишев


Видео не загружается в Ваш браузер:
  1. Установите Adobe Flash Player    

  2. Проверьте с Вашим администратором, что из Вашей сети разрешены исходящие соединения на порт 8080
  3. Сообщите администратору портала о данной ошибке

Аннотация: Вычислимая функция $f: \mathbb{N}\rightarrow \mathbb{N}$ называется доказуемо рекурсивной в данной формальной теории $T$, если существует алгоритм её вычисления такой, что в $T$ можно доказать утверждение «для любого $x$ существует $y$ такой, что $f(x)=y$». В математической логике такие функции изучаются по двум причинам. Во-первых, для данной программы нас часто интересует доказательство её корректности, в частности вопрос о том, завершает ли она работу при любых исходных данных. С другой стороны, варьируя функцию $f$ мы можем ставить для теории $T$ сколь угодно сложные (вплоть до невыполнимости) задачи на доказательство. Тем самым, доказуемо рекурсивные функции могут быть использованы для изучения и сравнения между собой различных формальных теорий. Такой подход приводит к построению функций, имеющих катастрофически большой рост, и к наиболее впечатляющим на сегодняшний день примерам недоказуемых комбинаторных утверждений. Мы начнем с понятия машины Тьюринга и вычислимой функции. Затем мы разберемся в том, как формальная арифметика может говорить о вычислениях, и убедимся, что она фактически имеет свой «внутренний» язык программирования. Затем мы поймем, что для любых разумных систем аксиом $T$ их запас доказуемо рекурсивных функций никак не может исчерпывать все вычислимые всюду определенные функции. Отсюда мы выведем первую теорему Гёделя о неполноте. Дальнейший рассказ пойдет о том, что можно сказать о классах доказуемо рекурсивных функций для конкретных теорий и о связанных с этим открытых проблемах в математической логике. На этом пути мы встретим различные фрагменты арифметики Пеано, иерархию Гжегорчика быстрорастущих функций, а также теоремы Париха и Парсонса–Минца, описывающие классы доказуемо рекурсивных функций для теорий, получающихся ограничением аксиомы индукции в арифметике.

Website: https://www.mccme.ru/dubna/2018/courses/beklemishev.html
Цикл лекций

ОТПРАВИТЬ: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru
 
Обратная связь:
 Пользовательское соглашение  Регистрация  Логотипы © Математический институт им. В. А. Стеклова РАН, 2019