Конструктивная математика
Принцип исключенного третьего говорит, что любое утверждение либо истинно, либо ложно. В этом курсе мы откажемся от принципа исключенного третьего. Мы не сможем ни доказывать от противного, ни перебирать случаи. Зато все наши доказательства будут в каком-то смысле конструктивны: доказательство существования объекта всегда можно будет превратить в компьютерную программу, которая строит этот объект.
На практике конструктивные доказательства полезнее неконструктивных. Например, если вы хотите доказать, что у вас дома есть ключи, конструктивное доказательство «Вот они, на столе под стопкой бумаг» полезнее неконструктивного «Вчера я зашел с ними домой, и с тех пор никто из дома не выходил».
Другой пример: чтобы конструктивно доказать, что последовательность стремится к нулю, надо научиться по числу  предъявлять номер, начиная с которого все члены последовательности лежат в интервале  .
Я расскажу о некоторых утверждениях конструктивной математики и о её связи с компьютерными системами доказательств.
Для понимания курса желательно уметь работать с логическими формулами вроде
(для любого положительного  найдётся натуральное  , такое что для  модуль разности  меньше ).
Кроме того, может быть полезно (но это не обязательно) знать определение действительных чисел и какую-нибудь аксиоматику формальной логики.
Кудряшов Юрий Георгиевич
Летняя школа «Современная математика», г. Дубна
24-27 июля 2017 г.
Похожее
-
Лев Беклемишев
Какую часть математических доказательств можно поручить компьютеру? Какие существуют виды интерактивных систем поиска математических доказательств? В чем заключается теорема о четырех красках? И как она была доказана? Математик Лев Беклемишев о теории множеств, интерактивных системах и проблеме о четырех красок.
-
Thomas Fernique
Теорема о четырёх красках утверждает, что всякую расположенную на сфере карту можно раскрасить четырьмя красками так, чтобы любые две области, имеющие общий участок границы, были раскрашены в разные цвета. В виде проблемы она была сформулирована в 1852 году — и доказана в 1976-м лишь с помощью компьютера. Такое решение не всем понравилось, и некоторые до сих пор ждут доказательства, которое можно проверить без компьютера. Другие (как великий математик Владимир Воеводский) — наоборот, стали развивать автоматическую проверку правильности доказательств на компьютере… В курсе мы разберем доказательство теоремы о четырёх красках (это простая комбинаторика, доступная любому школьнику), а также обсудим сегодняшнее использование компьютера в математике (надо примерно знать, что такое компьютер).
-
Математики из Университета Техаса в Остине с помощью компьютерных методов решили задачу о булевых пифагоровых тройках. Полная запись решения занимает около 200 терабайт, что делает его самым большим доказательством из существующих. На решение задачи ушло два дня непрерывной работы 800-процессорного суперкомпьютера.
-
Наталия Гончарук, Юрий Кудряшов
Грубо говоря, это гладкое отображение, которое растягивает в одних направлениях и сжимает в других. Про диффеоморфизмы Аносова было сформулировано много гипотез общего характера. Многие из них до сих пор открыты, несмотря на большой интерес, которых они вызывают. На первых двух занятиях мы обсудим различные свойства линейного отображения двумерного тора, заданного формулой (x, y) → (2x+y, x+y): устойчивое и неустойчивое направления, перемешивание, транзитивность, плотность периодических орбит. Кроме того, мы построим марковское разбиение, которое позволяет связать этот диффеоморфизм с цепью Маркова. На третьем занятии мы дадим общее определение диффеоморфизма Аносова и построим пример диффеоморфизма, действующий на более сложном многообразии. Последнее занятие будет посвящено открытым вопросам о диффеоморфизмах Аносова.
-
Владимир Успенский
Если в качестве значений переменных разрешается брать только элементы носителя, язык называют элементарным языком, или языком первого порядка. Если же в качестве значений переменных разрешается брать также функции и отношения, язык называют языком второго порядка. Выразительные возможности языков первого порядка довольно ограничены. Например, на языке первого порядка можно сообщить, что носитель содержит ровно 17 элементов, но невозможно выразить его конечность. На языке второго порядка выразить конечность носителя возможно. Возникает совершенно естественное недоумение: а зачем тогда пользоваться языками первого порядка с их бедными выразительными средствами, не лучше ли пользоваться языками второго порядка?
-
Алексей Семёнов
Высказывания математического языка (в том числе, содержащие переменные, от значения которых зависит истинность утверждений) можно записывать на формальном языке математической логики. (Например, можно использовать значок ∀ вместо выражения «для всех».) Однако даже и без точного описания языка математической логики (которое, впрочем, будет дано) можно понять, что значит объяснить (выразить) одно из свойств чисел через другое, например, выразить свойство «быть простым числом» через свойство «делиться». В лекции будут рассмотрены примеры задач, относящихся к выразимости и невыразимости. Среди высказываний математического языка можно выделить те, которые не содержать переменных и называть их утверждениями. Было бы хорошо иметь общий способ, пусть даже и очень громоздкий, который про любое утверждение, касающееся чисел (или иных математических объектов) и отношений между ними, позволяет установить, истинно оно или ложно. Будут приведены примеры, когда такой способ есть, и когда его нет.
-
Алексей Семёнов
Основные достижения математической логики относятся к математическим исследованиям математических рассуждений (эти исследования даже назвали метаматематикой). Однако методами математической логики можно изучать человеческие рассуждения не только из области математики. При построении математических моделей таких рассуждений используются, в частности, модальные логики. Самыми известными среди них являются логики возможности и необходимости. Для строящихся при этом логических языков определяются: семантика, т.н. «возможных миров» (семантика Крипке) и исчисление (аксиоматическая система), позволяющее формализовать рассуждения. Во многих случаях удаётся достичь полного соответствия между семантикой и исчислением (совпадения истинности и выводимости). В лекции будут приведены некоторые примеры модальных логик и доказано указанное соответствие для одной из них — естественной и хорошо известной.
-
Михаил Раскин
Все мы знаем, что математика доказывает импликации. Другими словами, мы доказываем не то, что какое-то утверждение верно, а то, что оно следует из принятых нами аксиом. Но при этом часто недооценивается, насколько сильно можно поменять набор аксиом. Одно из базовых понятий математики, на которых видна степень условности выбора конкретного набора аксиом – понятие множества. Сначала оно казалось совершенно очевидным. К сожалению, этот подход привёл к противоречиям. После этого стали развиваться разные способы работать со множествами не приходя к парадоксам. Понятие множества используется во многих разделах математики, из-за чего работать со множествами обычно учат постепенно, по кусочкам добавляя факты как естественные и самоочевидные основы, пока не получится теория, носящая имя ZFC. Из-за этого часто оказывается заметён под ковёр тот факт, что ZFC лишь один из возможных вариантов и что замена оснований теории множеств совсем не обязана рушить другие разделы математики. Курс будет посвящён рассказу о том, что может быть проблемой при пользовании какой-то аксиоматикой и сколь разнообразны варианты. Предварительные требования будут изменены в соответствии со знаниями и интересами аудитории; я надеюсь, что обозначения →, ∀, ∨, ∈, ∈, ∪, … всё же всем знакомы и привычны настолько, что ошибочно кажутся понятными.
-
Наталия Гончарук, Юрий Кудряшов
Параллельный перенос, поворот, поворотная гомотетия, композиция инверсии и осевой симметрии — частные случаи дробно-линейных отображений комплексной плоскости (в общем случае дробно-линейное отображение плоскости — это отображение, при котором точка z=x+iy переходит в точку (az+b)/(cz+d)). Как известно, инверсия выворачивает круг наизнанку: то, что было внутри, оказывается снаружи, и наоборот. Говорят, что набор дробно-линейных отображений f_1,…,f_g порождает группу Шоттки, если есть набор замкнутых жордановых кривых γ_1,…,γ_g, таких что: 1) Области, ограниченные кривыми γ_j, не пересекаются; 2) Под действием отображения f_j точки внутри γ_{2j-1} оказываются снаружи γ_{2j}, а точки снаружи γ_{2j-1} — внутри γ_{2j}.
-
Юрий Матиясевич
Метод координат, придуманный Рене Декартом, позволяет переформулировать любую задачу «на доказательство» из элементарной (грубо говоря, «школьной») геометрии в виде высказывания о вещественных числах. А что делать потом? Ведь уже для корней алгебраических уравнений пятой степени с одной неизвестной не существует явной формулы «в радикалах», а при переводе геометрических утверждений на алгебраический язык будут возникать сложные утверждения, содержащие много переменных, связанных как кванторами существования (это «неизвестные»), так и кванторами общности (это «параметры»). К счастью, польский логик и математик Альфред Тарский нашел в сороковые годы двадцатого столетия универсальный метод, позволяющий узнавать истинность или ложность любого высказывания про конечное множество вещественных чисел. Первоначальное авторское изложение этого метода занимало целую книгу и было очень трудно для восприятия. С тех пор многие авторы упрощали метод Тарского, и сегодня этот замечательный результат может быть доказан со всеми деталями за два часа и, надеюсь, понят старшеклассниками и младшекурсниками.
Далее >>>
|
|
