Доказуемо рекурсивные функции
Вычислимая функция  называется доказуемо рекурсивной в данной формальной теории  , если существует алгоритм её вычисления такой, что в можно доказать утверждение «для любого  существует  такой, что  ». В математической логике такие функции изучаются по двум причинам. Во-первых, для данной программы нас часто интересует доказательство её корректности, в частности вопрос о том, завершает ли она работу при любых исходных данных. С другой стороны, варьируя функцию  мы можем ставить для теории сколь угодно сложные (вплоть до невыполнимости) задачи на доказательство. Тем самым, доказуемо рекурсивные функции могут быть использованы для изучения и сравнения между собой различных формальных теорий. Такой подход приводит к построению функций, имеющих катастрофически большой рост, и к наиболее впечатляющим на сегодняшний день примерам недоказуемых комбинаторных утверждений. Мы начнем с понятия машины Тьюринга и вычислимой функции. Затем мы разберемся в том, как формальная арифметика может говорить о вычислениях, и убедимся, что она фактически имеет свой «внутренний» язык программирования. Затем мы поймем, что для любых разумных систем аксиом их запас доказуемо рекурсивных функций никак не может исчерпывать все вычислимые всюду определенные функции. Отсюда мы выведем первую теорему Гёделя о неполноте. Дальнейший рассказ пойдет о том, что можно сказать о классах доказуемо рекурсивных функций для конкретных теорий и о связанных с этим открытых проблемах в математической логике. На этом пути мы встретим различные фрагменты арифметики Пеано, иерархию Гжегорчика быстрорастущих функций, а также теоремы Париха и Парсонса–Минца, описывающие классы доказуемо рекурсивных функций для теорий, получающихся ограничением аксиомы индукции в арифметике.
Беклемишев Лев Дмитриевич — член-корреспондент РАН, доктор физико-математических наук.
Летняя школа «Современная математика» имени Виталия Арнольда, г. Дубна
21-25 июля 2018 г.
Похожее
-
Лев Беклемишев
Классическая логика высказываний исходит из предположения о том, что любые высказывания либо истинны, либо ложны. Логика доказуемости отражает более глубокую картину мира, осознанную после теорем Гёделя о неполноте: истинность высказывания, вообще говоря, не равносильна его доказуемости. Можно ли — и если да, то как — говорить на уровне логики о доказуемости или недоказуемости высказываний, наряду с их истинностью или ложностью? Программа: Логика высказываний и её модели. Модальная логика, модели Крипке. Логика Гёделя-Лёба GL. Теорема о полноте логики GL по Крипке на конечных деревьях. Формальная арифметика Пеано. Гёделева нумерация. Теорема о неподвижной точке. Формулы доказуемости и непротиворечивости. Теоремы Гёделя, Россера и Лёба. Доказуемость как модальность: арифметическая интерпретация логики GL. Замкнутые модальные формулы, последовательность Тьюринга, локальная рефлексия. Существование и единственность модально определимых неподвижных точек (теорема де Йонга).
-
Лев Беклемишев
Разные варианты выбора неопределяемых понятий. Система аксиом Тарского (по-видимому, самая простая из известных). Роль аксиом непрерывности с точки зрения различия логики первого и второго порядков. Модели и синтаксические интерпретации формальных теорий. Несколько классических интерпретаций, в том числе взаимная интерпретируемость гиперболической и евклидовой геометрии, элементарной геометрии Тарского и элементарной теории поля вещественных чисел, интерпретация теории поля вещественных чисел в арифметике натуральных чисел. Теоремы Тарского о полноте аксиоматики и о существовании алгоритма, распознающего истинность утверждений элементарной геометрии.
-
Лев Беклемишев
Какую часть математических доказательств можно поручить компьютеру? Какие существуют виды интерактивных систем поиска математических доказательств? В чем заключается теорема о четырех красках? И как она была доказана? Математик Лев Беклемишев о теории множеств, интерактивных системах и проблеме о четырех красок.
-
Алексей Семёнов
«Качественная» теория алгоритмов (не касающаяся понятия сложности вычислений) может быть построена на интуитивном представлении о том, что такое алгоритм. Такого представления, при некотором его уточнении, оказывается достаточно для того, чтобы доказать первые базовые теоремы теории алгоритмов. В лекции будет приведено указанное уточнение, определено понятие вычислимости и понятие породимости («выводимости в формальной системе»), доказано несколько теорем, другие теоремы — предложены в качестве задач. Будут приведены и примеры т.н. «уточнения понятия алгоритма». Для понимания лекции желательно умение читать по-русски, знание латинского алфавита и представление о натуральном ряде.
-
Алексей Сосинский
Теорема Гёделя, наряду с открытием теории относительности, квантовой механики и ДНК, обычно рассматривается как крупнейшее научное достижение ХХ века. Почему? В чем ее суть? Каково ее значение? Эти вопросы в своей лекции раскрывает Алексей Брониславович Сосинский, математик, профессор Независимого московского университета, офицер Ордена академических пальм Французской Республики, лауреат премии Правительства РФ в области образования 2012 года. В частности, были даны несколько разных ее формулировок, описаны три подхода к ее доказательству (Колмогорова, Чейтина и самого Гёделя), и объяснено ее значение для математики, физики, компьютерной науки и философии.
-
Владимир Успенский
Знаменитая Теорема Гёделя о неполноте имеет две версии — синтаксическую (объявленную и доказанную самим Гёделем) и семантическую (чаще всего фигурирующую в популярных рассуждениях о великой Теореме). Семантическая версия утверждает, что какую бы систему формальных доказательств ни придумать, в языке найдутся истинные утверждения, не доказуемые в рамках предложенной системы. Таким образом, семантическая версия исходит из того, что некоторые выражения языка выражают осмысленные утверждения, являющиеся истинными или ложными. Синтаксическая версия не опирается на то, что какие бы то ни было выражения языка имеют какой-то смысл, она смотрит на выражения как на синтаксические конструкции, то есть как на цепочки символов, организованные по определённым правилам.
-
Алексей Семёнов
Попытки дать математические определения понятий формального доказательства, истинности, формализованной деятельности по инструкции привели к построению математической логики и теории алгоритмов — области математики, результаты которой сформировали и продолжают формировать основы информатики и влиять на практическое использование цифровых технологий. Важнейшие результаты данной области, наряду с указанными определениями — это результаты о невозможности, в свою очередь тесно связанные с результатами об универсальности и диагональными конструкциями.
-
Беклемишев Лев
В чем заключается аксиоматический метод? Как развивалось понятие аксиомы? Кем был разработан аксиоматический метод? Какое место он занимает в математике? И какой критике подвергается этот метод? Математик Лев Беклемишев о неевклидовой геометрии, системе аксиом Гильберта и смысле в математике.
-
Лев Беклемишев
В докладе рассмотрены два класса объектов, имеющих различную природу, но неожиданным образом аналогичные по своим свойствам. С одной стороны, так называемые алгебры доказуемости, возникающие при изучении свойств формальной доказуемости в арифметических теориях. С другой стороны, топологические пространства, наделённые одной или несколькими разреженными топологиями, то есть такими, что любое непустое подмножество X имеет хотя бы одну изолированную точку.
-
Владимир Успенский
В отличие от метрической теории алгоритмов, дескриптивная теория не занимается измерением ресурсов (таких как время, объём памяти), затрачиваемых при применении алгоритма к его возможным исходным данным (в другой терминологии — к его входам). Её интересует лишь, возможен алгоритм для решения данной задачи или нет. Начальные понятия дескриптивной теории алгоритмов суть: конструктивный обьект, алгоритм, число шагов алгоритма, вычислимая функция, перечислимое множество, разрешимое множество, сводимость нумераций, главная вычислимая нумерация, вычислимая операция.
Далее >>>
|
|
