Важно понимать, что множества сами по себе никуда не денутся. Замена, о которой говорит Воеводский, происходит на более низком уровне: связка «логика первого порядка + аксиомы ZFC» заменяется на HoTT. Считается, что аксиомы ZFC работающих математиков всё равно не интересуют (кроме специалистов по логике), и в современном виде необходимая математикам теория множеств гораздо лучше формализуется с помощью ETCS.
ETCS инспирирована теорией категорий (но не базируется на ней): в качестве базовых объектов берутся функция и множество (в ZFC базовые объекты — множество и элемент множества), и элементы множества A в ETCS определяются как функции из фиксированного одноэлементного множества в множество A (т.к. эти функции взаимно-однозначно соответствуют элементам A), а «одноэлементность» в свою очередь можно определить как свойство множества иметь ровно одну функцию из любого множества в себя. Подробное изложение для нематематиков можно найти здесь: arxiv.org/abs/1212.6543 Там же можно узнать, почему математики не используют ZFC (например, потому, что число пи в этой системе аксиом является множеством).
В HoTT в свою очередь можно строить объекты, которые работают ровно так, как те штуки, которые описывает ETCS. Эти штуки в HoTT называются множества.
Возможно, следующий отрывок интервью Владимира Воеводского (кстати говоря, лауреата Филдсовской премии), в котором он описывает историю создания HoTT, поможет понять, зачем нужна эта теория и что вообще происходит:
… Параллельно я искал подходы к проблеме накопления ошибок в работах по чистой математике. Было ясно, что единственное решение — это создание языка, на котором математические доказательства могут писаться людьми в такой форме, что это можно будет проверять на компьютере. Вплоть до 2005 года мне казалось, что это задача намного более сложная чем задача исторической генетики, которой я занимался. Во многом это ощущение было результатом устоявшегося и очень распространенного среди математиков мнения, что абстрактную математику невозможно разумным образом формализовать настолько аккуратно, чтобы ее «понимал» компьютер.
В 2005 мне удалось сформулировать несколько идей, которые неожиданно открыли новый подход к одной из основных проблем в основаниях современной математики. Проблему эту можно неформально сформулировать как вопрос о том, как правильно формализовать интуитивное понимание того, что «одинаковые» математические объекты имеют одинаковые свойства. Аргументы, основанные на этом принципе, очень часто используются в современных математических доказательствах, но существующие основания математики (теория множеств Цермело-Френкеля) совершенно неприспособлены для формализации таких аргументов.
Я был очень хорошо знаком с этой проблемой и думал о ней еще в 1989 году, когда Миша Капранов и я работали над теорией поли-катергорий. Тогда нам казалось, что ее решить невозможно. То, что мне удалось понять в 2005 году, скомбинировав идеи теории гомотопий (части современной топологии) и теории типов (части современной теории языков программирования), было совершенно удивительно, и открывало реальные возможности построения того самого языка, на котором люди могут писать доказательства, которые сможет проверять компьютер. Дальше был большой перерыв в моей математической деятельности. [...] К идеям, связанным с компьютерной проверкой доказательств, я вернулся только летом 2009, когда мне стало окончательно ясно, что с исторической генетикой ничего не получается. И буквально через несколько месяцев случились два события, которые продвинули эти идеи от общих наметок, над которыми, я думал, придется работать еще не один год, до стадии, на которой я смог заявить, что я придумал новые основания математики, которые позволят решить проблему компьютерной проверки доказательств. Сейчас это называется «унивалентные основания математики» и ими занимаются как математики, так и теоретики языков программирования. Я почти не сомневаюсь, что эти основания вскоре заменят теорию множеств и что проблему языка абстрактной математики, который будут «понимать» компьютеры можно считать в основном решенной. [...] Первые примеры языков того класса с которыми я работаю, были созданы в конце 1970-ых и известны под названием «Martin-Lof type theories». Удивительным образом языки были, программные системы использующие эти языки создавались и даже становились популярными (особенно система «Coq» которую создали французы), но понимания того, о чем эти языки позволяют говорить, не было. Получалось, что используется только очень небольшая часть возможностей языка, та, которая, как теперь ясно, позволяет говорить про множества. Язык же в целом позволяет говорить про гомотомические типы любого уровня сложности. Разрыв, как ты понимаешь, огромный. Как следствие сами языки не совершенствовались, потому что было не ясно, что можно менять, а что нельзя. Теперь, когда мы понимаем, что в этих языках существенно, а что нет, открывается возможность сделать их значительно более «мощными» и, как следствие, более удобными для практического использования.
ETCS инспирирована теорией категорий (но не базируется на ней): в качестве базовых объектов берутся функция и множество (в ZFC базовые объекты — множество и элемент множества), и элементы множества A в ETCS определяются как функции из фиксированного одноэлементного множества в множество A (т.к. эти функции взаимно-однозначно соответствуют элементам A), а «одноэлементность» в свою очередь можно определить как свойство множества иметь ровно одну функцию из любого множества в себя. Подробное изложение для нематематиков можно найти здесь: arxiv.org/abs/1212.6543 Там же можно узнать, почему математики не используют ZFC (например, потому, что число пи в этой системе аксиом является множеством).
В HoTT в свою очередь можно строить объекты, которые работают ровно так, как те штуки, которые описывает ETCS. Эти штуки в HoTT называются множества.
… Параллельно я искал подходы к проблеме накопления ошибок в работах по чистой математике. Было ясно, что единственное решение — это создание языка, на котором математические доказательства могут писаться людьми в такой форме, что это можно будет проверять на компьютере. Вплоть до 2005 года мне казалось, что это задача намного более сложная чем задача исторической генетики, которой я занимался. Во многом это ощущение было результатом устоявшегося и очень распространенного среди математиков мнения, что абстрактную математику невозможно разумным образом формализовать настолько аккуратно, чтобы ее «понимал» компьютер.
В 2005 мне удалось сформулировать несколько идей, которые неожиданно открыли новый подход к одной из основных проблем в основаниях современной математики. Проблему эту можно неформально сформулировать как вопрос о том, как правильно формализовать интуитивное понимание того, что «одинаковые» математические объекты имеют одинаковые свойства. Аргументы, основанные на этом принципе, очень часто используются в современных математических доказательствах, но существующие основания математики (теория множеств Цермело-Френкеля) совершенно неприспособлены для формализации таких аргументов.
Я был очень хорошо знаком с этой проблемой и думал о ней еще в 1989 году, когда Миша Капранов и я работали над теорией поли-катергорий. Тогда нам казалось, что ее решить невозможно. То, что мне удалось понять в 2005 году, скомбинировав идеи теории гомотопий (части современной топологии) и теории типов (части современной теории языков программирования), было совершенно удивительно, и открывало реальные возможности построения того самого языка, на котором люди могут писать доказательства, которые сможет проверять компьютер. Дальше был большой перерыв в моей математической деятельности. [...] К идеям, связанным с компьютерной проверкой доказательств, я вернулся только летом 2009, когда мне стало окончательно ясно, что с исторической генетикой ничего не получается. И буквально через несколько месяцев случились два события, которые продвинули эти идеи от общих наметок, над которыми, я думал, придется работать еще не один год, до стадии, на которой я смог заявить, что я придумал новые основания математики, которые позволят решить проблему компьютерной проверки доказательств. Сейчас это называется «унивалентные основания математики» и ими занимаются как математики, так и теоретики языков программирования. Я почти не сомневаюсь, что эти основания вскоре заменят теорию множеств и что проблему языка абстрактной математики, который будут «понимать» компьютеры можно считать в основном решенной. [...] Первые примеры языков того класса с которыми я работаю, были созданы в конце 1970-ых и известны под названием «Martin-Lof type theories». Удивительным образом языки были, программные системы использующие эти языки создавались и даже становились популярными (особенно система «Coq» которую создали французы), но понимания того, о чем эти языки позволяют говорить, не было. Получалось, что используется только очень небольшая часть возможностей языка, та, которая, как теперь ясно, позволяет говорить про множества. Язык же в целом позволяет говорить про гомотомические типы любого уровня сложности. Разрыв, как ты понимаешь, огромный. Как следствие сами языки не совершенствовались, потому что было не ясно, что можно менять, а что нельзя. Теперь, когда мы понимаем, что в этих языках существенно, а что нет, открывается возможность сделать их значительно более «мощными» и, как следствие, более удобными для практического использования.