Исследователи использовали метаматематические методы, чтобы показать, что некоторые теоремы, которые на первый взгляд кажутся различными, на самом деле логически эквивалентны. Сохранить статью Прочитать позже
В обратной математике исследователи заменяют аксиомы — основы математических систем — теоремами, которые они хотят доказать.
Введение
Когда дело доходит до сложных задач, компьютерщики, похоже, заходят в тупик. Рассмотрим, например, печально известную задачу поиска кратчайшего маршрута туда и обратно, проходящего через каждый город на карте ровно один раз. Все известные методы решения этой «задачи коммивояжёра» работают ужасно медленно на картах с большим количеством городов, и исследователи подозревают, что лучшего способа нет. Но никто не знает, как это доказать.
Более 50 лет исследователи в области теории сложности вычислений пытались превратить интуитивные утверждения вроде «задача коммивояжёра сложна» в незыблемые математические теоремы, но без особого успеха. Всё чаще они ищут строгие ответы на смежный и более туманный вопрос: почему их доказательства не увенчались успехом?
Эта работа, рассматривающая процесс математического доказательства как объект математического анализа, является частью весьма непростой области, называемой метаматематикой. Метаматематики часто тщательно изучают базовые предположения, или аксиомы, которые служат отправными точками для всех доказательств. Они изменяют аксиомы, с которых начинают, а затем исследуют, как эти изменения влияют на то, какие теоремы они могут доказать. Используя метаматематику для изучения теории сложности, исследователи пытаются определить, что различные наборы аксиом могут и не могут доказать относительно вычислительной сложности. Они надеются, что это поможет им понять, почему их попытки доказать сложность задач не увенчались успехом.
В статье, опубликованной в прошлом году, три исследователя предложили новый подход к решению этой проблемы. Они перевернули формулу, которой математики пользовались тысячелетиями: вместо того, чтобы начинать со стандартного набора аксиом и доказывать теорему, они заменили одну из аксиом теоремой, а затем доказали эту аксиому. Они использовали этот подход, называемый обратной математикой, чтобы доказать, что многие различные теоремы в теории сложности на самом деле полностью эквивалентны.
«Я был удивлён, что им удалось сделать так много», — сказал Марко Кармосино, специалист по теории сложности в IBM. «Люди посмотрят на это и скажут: „Вот что привело меня в метаматематику“».
Доказательства голубей
История статьи по обратной математике началась летом 2022 года, когда Лицзе Чэнь, специалист по теории сложности, работающий сейчас в Калифорнийском университете в Беркли, завершал работу над докторской диссертацией. У него появилось много свободного времени, и он решил посвятить несколько месяцев изучению метаматематики.
«Поскольку я заканчивал учёбу, мне особо нечем было заниматься, — сказал Чэнь. — Я решил, что мне стоит узнать что-то новое».
Читая, Чэнь задумался о разделе теории сложности, называемом сложностью коммуникации, который изучает информацию, которой должны обмениваться два или более человека для выполнения определённых задач. Одна из простейших задач в области сложности коммуникации, называемая «проблемой равенства», похожа на совместную игру. Два игрока начинают с отдельных строк из нулей и единиц (или битов). Их цель — как можно меньше общаться, чтобы определить, одинаковы ли их строки. Простейшая стратегия — просто отправить полную строку другому для проверки. Есть ли способ улучшить ситуацию?
Теоретики сложности доказали десятилетия назад, что ответ — нет. Чтобы решить задачу равенства, игрокам необходимо отправить как минимум столько битов, сколько содержится в полной строке. Теоретики утверждают, что эта длина строки — «нижняя граница» необходимого объёма обмена данными.
Чэнь не интересовался самой нижней границей задачи равенства — его интересовало, как её доказали исследователи. Все известные доказательства основаны на простой теореме, называемой принципом «ящика», которая гласит, что если поместить некоторое количество голубей в меньшее количество ячеек, то по крайней мере в одной ячейке должно оказаться больше одной птицы. Это может показаться очевидным, но это может оказаться удивительно мощным инструментом в теории сложности и не только.
Чэнь наткнулся на интригующую мысль о том, что связь между проблемой равенства и принципом «ящика» может быть и обратной. Принцип «ящика» легко использовать для доказательства нижней границы проблемы равенства. Можно ли вместо этого использовать нижнюю границу для доказательства принципа «ящика»?
Странное равенство
Чэнь обсудил свою идею с Цзяту Ли, в то время студентом Университета Цинхуа, с которым Чэнь недавно сотрудничал над другой статьей. Чтобы сделать связь строгой, им нужно было выбрать набор аксиом для работы. Исследователи метаматематики предпочитают использовать аксиомы, которые более ограничены, чем типичные. Эти более слабые аксиомы позволяют легче устанавливать точные связи между различными теоремами. Чэнь и Ли решили работать с популярным набором аксиом, называемым PV1. PV1 достаточно силен, чтобы доказать некоторые важные теоремы о вычислительной сложности сам по себе. Добавьте конкретную версию принципа «ящика» в качестве дополнительной аксиомы, и вы также сможете доказать нижнюю границу проблемы равенства. В декабре 2022 года Ли и Чэнь формально показали, что, как и подозревал Чэнь, доказательство также работает, если поменять местами две теоремы.
Игорь Оливейра помог доказать, что многие различные теоремы на самом деле эквивалентны.
Тот факт, что нижнюю границу задачи равенства можно доказать, используя принцип «ящика» или наоборот, подразумевает, что в логической структуре PV1 эти две теоремы полностью эквивалентны. Когда Ли и Чэнь обсудили результат с Игорем Оливейрой, специалистом по теории сложности из Уорикского университета, они поняли, что их метод обратной математики может быть применим и к теоремам в других обширных областях теории сложности. В течение следующих месяцев они систематически доказали эквивалентности для многих других теорем.
«Сначала у нас было всего две равнозначные вещи, — сказал Чэнь. — Но теперь у нас целая сеть вещей».
Самая поразительная связь, обнаруженная командой, связывает ту же версию принципа «ящика» с одной из первых теорем, с которыми студенты сталкиваются на вводных курсах теории сложности. Эта «классическая теорема-бумер», как её охарактеризовал Кармозино, устанавливает нижнюю границу времени, необходимого теоретическому компьютеру, называемому одноленточной машиной Тьюринга, для определения того, является ли строка нулей и единиц палиндромом (то есть одинаково ли она читается в прямом и обратном порядке). Ли, Чэнь и Оливейра использовали метод обратной математики, чтобы доказать, что в рамках PV1 эта теорема о нижней границе палиндрома эквивалентна принципу «ящика».
«Если бы вы мне это рассказали, я бы не поверил», — сказал Чэнь. «Это звучит очень нелепо».
Эквивалентность нижней границы палиндрома и принципа «ящика» удивительна, поскольку эти две теоремы на первый взгляд настолько различны. Принцип «ящика» по своей сути не имеет никакого отношения к вычислениям: это простое утверждение о счёте. Нижняя граница палиндрома, с другой стороны, — это утверждение о конкретной модели вычислений. Новый результат подразумевает, что такие, казалось бы, узкие теоремы на самом деле более общие, чем кажутся.
«Это говорит о том, что нижние границы сложности, которые мы хотим понять, гораздо более фундаментальны», — сказал Оливейра.
Неизведанная территория
Эта новая сеть эквивалентностей также помогла выявить ограничения PV1. У исследователей уже были основания полагать, что принцип «ящика» невозможно доказать, исходя только из аксиом PV1, поэтому результаты Ли, Чэня и Оливейры подразумевают, что другие их эквивалентные теоремы также, вероятно, недоказуемы в PV1.
«Я думаю, это прекрасно», — сказал Ян Пич, специалист по теории сложности из Оксфордского университета, доказавший важный результат о мощности PV1 в 2014 году. Но он предупредил, что подход обратной математики может быть наиболее полезен для выявления новых связей между уже доказанными исследователями теоремами. «Насколько мы можем судить, это мало что говорит нам о сложности утверждений, которые мы не знаем, как доказать».
Понимание этой неизведанной территории остаётся далёким достижением для исследователей метаматематики. Но это не умерило энтузиазма Ли к этой теме. Он поступил в аспирантуру Массачусетского технологического института в 2023 году и недавно написал 140-страничное руководство по метаматематике для специалистов по теории сложности. Это один из примеров более широкой тенденции: после десятилетий относительной безвестности метаматематика всё больше привлекает внимание широкого круга исследователей, которые привносят в эту область новые перспективы.
«Люди устали от застоя, — сказал Кармозино. — Пора просто сделать шаг назад и заложить фундамент».
Источник: www.quantamagazine.org
