🧠🤖ВЛАДИМИР ВОЕВОДСКИЙ и КОМПЬЮТЕРНАЯ ПРОВЕРКА ДОКАЗАТЕЛЬСТВ Часть 2. Становление унивалентных оснований 🏛 Идея логических оснований витала в воздухе ещё с конца XIX в. Начиная с работ Фреге, пытавшегося показать, что арифметика может быть полностью выведена из логики. Затем воодушевленное начало XX в. — программа Гильберта, Principia Mathematica Рассела и Уайтхеда. 📉Но уже в середине XX в. после работ Гёделя интерес подостыл и сформировалось мнение, что программа логических оснований, хотя и интересна, как самостоятельная отрасль математики, но мало полезна практически. 🧩Наработанные идеи расползлись по разным математическим дисциплинам. Но как оказалось только затем, чтобы вновь объединиться и дополниться новыми в УНИВАЛЕНТНЫХ ОСНОВАНИЯХ. Сегодня тезисно подсветим эти идеи. А подробно пройдемся по ним уже в следующих постах. 🧠 1. Конструктивизм ➡️Развитие интуиционизма и конструктивной логики. В таких теориях, от “существования” требуется возможность предъявить/построить объект - они идеально ложатся на почву теории вычислимости. ➡️Открытие структурной взаимосвязи между доказательствами и вычислениями. В частности работы Карри - Ховарда. Они позволили: ✅ теоремы понимать — как типы; ✅ доказательства — как программы; ✅ процесс доказательства — как вычислительную процедуру. 🏗 2. Структурализм ➡️Развитие идей структурализма, начиная с работ Дедекинда по натуральным числам. ➡️ Формирование современного математического структурализма в работах Бенасеррафа, Патнэма, Резника, Шапиро и других. ➡️Развитие современных фундаментальных теорий (типов и категорий) на основе структурализма. Немного поясню важность структурного подхода: Возьмём, например натуральные числа. В теории множеств их можно закодировать разными способами: 1️⃣ по Цермело; 2️⃣ по фон Нейману; 3️⃣ ... 🔎 В виде множеств такие натуральные числа окажутся разными объектами с разными теоретико-множественными свойствами — хотя “по смыслу” это одна и та же арифметическая структура. Структурный подход напротив, позволяет исключить неуникальность представлений. 🌐 3. Топология Связь между теорией типов и топологией (в частности теорией гомотопий), уже не такая очевидная, но именно её открытие Владимиром Воеводским сыграло ключевую роль в становлении УНИВАЛЕНТНЫХ ОСНОВАНИЙ. ➡️От закона Лейбница о тождественности неразличимых. Где уже прослеживалась мысль о том, что объекты можно считать равными в определённом контексте, на определённом уровне абстракции. ➡️К идеям унивалентности, как обобщений, позволяющих работать с изоморфизмами, равенствами, эвивалентностями на одном уровне. Ведь очень часто в математике мы бы хотели считать равными именно “контекстуально” равные. ☕️🍩Как в известном примере гомотопической эквивалентности кружки и бублика. А теории, содержащие аксиому унивалентности как раз позволяют безболезненно, без дополнительных доказательств переносить свойства между структурно равными объектами. ➡️ И наконец к идеям Владимира Воеводского - добавить аксиому унивалентности и гомотопическую семантику к теории типов. 🔗Итак, идеи конструктивизма, структурного подхода, теории типов, топологии, вычислимости и теории доказательств в итоге соединились в программу УНИВАЛЕНТНЫХ ОСНОВАНИЙ. Продолжение следует...