«Качественная» теория алгоритмов (не касающаяся понятия сложности вычислений) может быть построена на интуитивном представлении о том, что такое алгоритм. Такого представления, при некотором его уточнении, оказывается достаточно для того, чтобы доказать первые базовые теоремы теории алгоритмов. В лекции будет приведено указанное уточнение, определено понятие вычислимости и понятие породимости («выводимости в формальной системе»), доказано несколько теорем, другие теоремы — предложены в качестве задач. Будут приведены и примеры т.н. «уточнения понятия алгоритма». Для понимания лекции желательно умение читать по-русски, знание латинского алфавита и представление о натуральном ряде.

Высказывания математического языка (в том числе, содержащие переменные, от значения которых зависит истинность утверждений) можно записывать на формальном языке математической логики. (Например, можно использовать значок ∀ вместо выражения «для всех».) Однако даже и без точного описания языка математической логики (которое, впрочем, будет дано) можно понять, что значит объяснить (выразить) одно из свойств чисел через другое, например, выразить свойство «быть простым числом» через свойство «делиться». В лекции будут рассмотрены примеры задач, относящихся к выразимости и невыразимости. Среди высказываний математического языка можно выделить те, которые не содержать переменных и называть их утверждениями. Было бы хорошо иметь общий способ, пусть даже и очень громоздкий, который про любое утверждение, касающееся чисел (или иных математических объектов) и отношений между ними, позволяет установить, истинно оно или ложно. Будут приведены примеры, когда такой способ есть, и когда его нет.

Основные достижения математической логики относятся к математическим исследованиям математических рассуждений (эти исследования даже назвали метаматематикой). Однако методами математической логики можно изучать человеческие рассуждения не только из области математики. При построении математических моделей таких рассуждений используются, в частности, модальные логики. Самыми известными среди них являются логики возможности и необходимости. Для строящихся при этом логических языков определяются: семантика, т.н. «возможных миров» (семантика Крипке) и исчисление (аксиоматическая система), позволяющее формализовать рассуждения. Во многих случаях удаётся достичь полного соответствия между семантикой и исчислением (совпадения истинности и выводимости). В лекции будут приведены некоторые примеры модальных логик и доказано указанное соответствие для одной из них — естественной и хорошо известной.

Вычислимая функция f:N→N называется доказуемо рекурсивной в данной формальной теории T, если существует алгоритм её вычисления такой, что в T можно доказать утверждение «для любого x существует y такой, что f(x)=y». В математической логике такие функции изучаются по двум причинам. Во-первых, для данной программы нас часто интересует доказательство её корректности, в частности вопрос о том, завершает ли она работу при любых исходных данных. С другой стороны, варьируя функцию f мы можем ставить для теории T сколь угодно сложные (вплоть до невыполнимости) задачи на доказательство. Тем самым, доказуемо рекурсивные функции могут быть использованы для изучения различных формальных теорий. Такой подход приводит к наиболее впечатляющим на сегодняшний день примерам недоказуемых комбинаторных утверждений. Мы начнем с понятия машины Тьюринга и вычислимой функции. Разберемся, как формальная арифметика может говорить о вычислениях. Поймем, что для любых разумных систем аксиом T их запас доказуемо рекурсивных функций никак не может исчерпывать все вычислимые всюду определенные функции. Отсюда выведем первую теорему Гёделя о неполноте.

В связи с разными точками зрения на природу математики рассматриваются вопросы о метаматематическом понятии истины и возможности убедительного доказательства истинности математических теорем.

Знаменитая Теорема Гёделя о неполноте имеет две версии — синтаксическую (объявленную и доказанную самим Гёделем) и семантическую (чаще всего фигурирующую в популярных рассуждениях о великой Теореме). Семантическая версия утверждает, что какую бы систему формальных доказательств ни придумать, в языке найдутся истинные утверждения, не доказуемые в рамках предложенной системы. Таким образом, семантическая версия исходит из того, что некоторые выражения языка выражают осмысленные утверждения, являющиеся истинными или ложными. Синтаксическая версия не опирается на то, что какие бы то ни было выражения языка имеют какой-то смысл, она смотрит на выражения как на синтаксические конструкции, то есть как на цепочки символов, организованные по определённым правилам.

Доказательность — главнейшая особенность математики, науки, представляющей образцы точности рассуждений. Но понятие доказательства долгое время не имело точного математического определения. О парадоксах в теории множеств и основаниях математики — академик РАН Юрий Ершов.

Разные варианты выбора неопределяемых понятий. Система аксиом Тарского (по-видимому, самая простая из известных). Роль аксиом непрерывности с точки зрения различия логики первого и второго порядков. Модели и синтаксические интерпретации формальных теорий. Несколько классических интерпретаций, в том числе взаимная интерпретируемость гиперболической и евклидовой геометрии, элементарной геометрии Тарского и элементарной теории поля вещественных чисел, интерпретация теории поля вещественных чисел в арифметике натуральных чисел. Теоремы Тарского о полноте аксиоматики и о существовании алгоритма, распознающего истинность утверждений элементарной геометрии.

В докладе рассмотрены два класса объектов, имеющих различную природу, но неожиданным образом аналогичные по своим свойствам. С одной стороны, так называемые алгебры доказуемости, возникающие при изучении свойств формальной доказуемости в арифметических теориях. С другой стороны, топологические пространства, наделённые одной или несколькими разреженными топологиями, то есть такими, что любое непустое подмножество X имеет хотя бы одну изолированную точку.

На протяжении большей части XX столетия в «чистой» математике царило замечательное единодушие относительно того, как нужно представлять результаты. Весь предмет сводился к комплексу теорем, каждая из которых, в конечном счете, выводилась из фиксированного набора аксиом путем так называемого строгого логического доказательства. В отдельных разделах математики, таких, например, как арифметика Пеано, справедливость аксиоматики выглядела самоочевидной, однако во многих случаях аксиомы попросту очерчивали рассматриваемую область вопросов. Для математиков, если только они не выходили за рамки математики, выступая в роли философов-любителей, принципиального различия между изобретением и открытием новых концепций не было.