Классическая логика высказываний исходит из предположения о том, что любые высказывания либо истинны, либо ложны. Логика доказуемости отражает более глубокую картину мира, осознанную после теорем Гёделя о неполноте: истинность высказывания, вообще говоря, не равносильна его доказуемости. Можно ли — и если да, то как — говорить на уровне логики о доказуемости или недоказуемости высказываний, наряду с их истинностью или ложностью? Решение было, по существу, предложено ещё Гёделем, а потом эта область активно развивалась начиная с 60-х годов XX века.
Язык логики доказуемости, наряду с обычными связками логики высказываний, содержит одноместные связки, обозначаемые □ и ◊. При этом □ A выражает доказуемость высказывания A, а ◊ A его непротиворечивость. Какие принципы логики доказуемости следует считать тавтологиями, то есть верными (подумайте: истинными или доказуемыми?) независимо от смысла элементарных высказываний, из которых они построены?
Слушателям рекомендуется подумать, следует ли считать тавтологиями следующие примеры:
□ A & □ B → □(A & B)
□ (A ∨ B) → □ A ∨ □ B
□ A → □□ A
◊ A → □ ◊ A
□ A → A
Как можно описать множество всех тавтологий логики доказуемости? Есть ли алгоритм, распознающий тавтологичность?
Для понимания рассказа будет полезно общее знакомство с теоремами Гёделя о неполноте и иметь представление о формальных системах, построенных на базе логики предикатов, таких как формальная арифметика Пеано. Разумеется, от слушателей НЕ требуется помнить многочисленные технические детали.
Классическая логика высказываний исходит из предположения о том, что любые высказывания либо истинны, либо ложны. Логика доказуемости отражает более глубокую картину мира, осознанную после теорем Гёделя о неполноте: истинность высказывания, вообще говоря, не равносильна его доказуемости. Можно ли — и если да, то как — говорить на уровне логики о доказуемости или недоказуемости высказываний, наряду с их истинностью или ложностью? Программа: Логика высказываний и её модели. Модальная логика, модели Крипке. Логика Гёделя-Лёба GL. Теорема о полноте логики GL по Крипке на конечных деревьях. Формальная арифметика Пеано. Гёделева нумерация. Теорема о неподвижной точке. Формулы доказуемости и непротиворечивости. Теоремы Гёделя, Россера и Лёба. Доказуемость как модальность: арифметическая интерпретация логики GL. Замкнутые модальные формулы, последовательность Тьюринга, локальная рефлексия. Существование и единственность модально определимых неподвижных точек (теорема де Йонга).
Вычислимая функция f:N→N называется доказуемо рекурсивной в данной формальной теории T, если существует алгоритм её вычисления такой, что в T можно доказать утверждение «для любого x существует y такой, что f(x)=y». В математической логике такие функции изучаются по двум причинам. Во-первых, для данной программы нас часто интересует доказательство её корректности, в частности вопрос о том, завершает ли она работу при любых исходных данных. С другой стороны, варьируя функцию f мы можем ставить для теории T сколь угодно сложные (вплоть до невыполнимости) задачи на доказательство. Тем самым, доказуемо рекурсивные функции могут быть использованы для изучения различных формальных теорий. Такой подход приводит к наиболее впечатляющим на сегодняшний день примерам недоказуемых комбинаторных утверждений. Мы начнем с понятия машины Тьюринга и вычислимой функции. Разберемся, как формальная арифметика может говорить о вычислениях. Поймем, что для любых разумных систем аксиом T их запас доказуемо рекурсивных функций никак не может исчерпывать все вычислимые всюду определенные функции. Отсюда выведем первую теорему Гёделя о неполноте.
Разные варианты выбора неопределяемых понятий. Система аксиом Тарского (по-видимому, самая простая из известных). Роль аксиом непрерывности с точки зрения различия логики первого и второго порядков. Модели и синтаксические интерпретации формальных теорий. Несколько классических интерпретаций, в том числе взаимная интерпретируемость гиперболической и евклидовой геометрии, элементарной геометрии Тарского и элементарной теории поля вещественных чисел, интерпретация теории поля вещественных чисел в арифметике натуральных чисел. Теоремы Тарского о полноте аксиоматики и о существовании алгоритма, распознающего истинность утверждений элементарной геометрии.
Теорема Гёделя о неполноте — едва ли не самая знаменитая теорема математики. Она утверждает, что какие бы способы доказывания ни предложить, в любом достаточно богатом языке найдутся истинные, но не доказуемые утверждения. Богатство языка есть его способность выражать факты. Оказывается, что для целей теоремы Гёделя богатство языка достаточно понимать как его способность выражать принадлежность натуральных чисел перечислимым множествам.
Знаменитая Теорема Гёделя о неполноте имеет две версии — синтаксическую (объявленную и доказанную самим Гёделем) и семантическую (чаще всего фигурирующую в популярных рассуждениях о великой Теореме). Семантическая версия утверждает, что какую бы систему формальных доказательств ни придумать, в языке найдутся истинные утверждения, не доказуемые в рамках предложенной системы. Таким образом, семантическая версия исходит из того, что некоторые выражения языка выражают осмысленные утверждения, являющиеся истинными или ложными. Синтаксическая версия не опирается на то, что какие бы то ни было выражения языка имеют какой-то смысл, она смотрит на выражения как на синтаксические конструкции, то есть как на цепочки символов, организованные по определённым правилам.
Курс занятий посвящен тому, что в математике сделать нельзя. Но речь пойдет не о запрещенных действиях (типа деления на ноль или квадратуры круга), а об отсутствии общих методов для решения некоторых широких классов задач. Начиная от определения вычислимой функции (через машину Тюринга), мы узнаем про существование универсальной вычислимой функции, и как следствие – о существовании не вычислимых функций. Отсюда мы поймем, какие задачи никакой компьютер (даже сколь угодно мощный) решить не может в принципе. Затем мы определим «Колмогоровскую сложность» и изучим ряд ее «нехороших» свойств, именно, не вычислимость некоторых связанных с ней характеристик. Эти свойства сыграют решающую роль в доказательстве теоремы Гёделя о неполноте – одного из самых значительных научных открытий ХХ-го века.
Аксиоматические системы, такие как арифметика Пеано и ее фрагменты, являются традиционными объектами изучения в математической логике. В докладе будет рассказано о сравнительно новом подходе к изучению таких систем с алгебраической точки зрения. Будут описаны алгебраические структуры, возникающие при изучении формальной доказуемости, и приведены некоторые применения этих структур к вопросу о порядках роста вычислимых функций для фрагментов арифметики и к построению простых утверждений комбинаторного характера, независимых от аксиом арифметики Пеано. Также будет рассказано о топологической точке зрения на алгебры доказуемости, которая приводит к изучению некоторого интересного класса пространств.
В чем заключается аксиоматический метод? Как развивалось понятие аксиомы? Кем был разработан аксиоматический метод? Какое место он занимает в математике? И какой критике подвергается этот метод? Математик Лев Беклемишев о неевклидовой геометрии, системе аксиом Гильберта и смысле в математике.
В докладе рассмотрены два класса объектов, имеющих различную природу, но неожиданным образом аналогичные по своим свойствам. С одной стороны, так называемые алгебры доказуемости, возникающие при изучении свойств формальной доказуемости в арифметических теориях. С другой стороны, топологические пространства, наделённые одной или несколькими разреженными топологиями, то есть такими, что любое непустое подмножество X имеет хотя бы одну изолированную точку.
Какую часть математических доказательств можно поручить компьютеру? Какие существуют виды интерактивных систем поиска математических доказательств? В чем заключается теорема о четырех красках? И как она была доказана? Математик Лев Беклемишев о теории множеств, интерактивных системах и проблеме о четырех красок.
Знаменитая Теорема Гёделя о неполноте имеет две версии — синтаксическую (объявленную и доказанную самим Гёделем) и семантическую (чаще всего фигурирующую в популярных рассуждениях о великой Теореме). Семантическая версия утверждает, что какую бы систему формальных доказательств ни придумать, в языке найдутся истинные утверждения, не доказуемые в рамках предложенной системы. Таким образом, семантическая версия исходит из того, что некоторые выражения языка выражают осмысленные утверждения, являющиеся истинными или ложными. Синтаксическая версия не опирается на то, что какие бы то ни было выражения языка имеют какой-то смысл, она смотрит на выражения как на синтаксические конструкции, то есть как на цепочки символов, организованные по определённым правилам.