🧠🤖ВЛАДИМИР ВОЕВОДСКИЙ и КОМПЬЮТЕРНАЯ ПРОВЕРКА ДОКАЗАТЕЛЬСТВ Часть 1. Почему не теория множеств? ❓Каким должен быть фундамент математики, пригодный как для человеческого мышления, так и для компьютерной верификации? По мнению Воеводского он должен включать следующие три компонента. 1) 🧾 Формальная система вывода Язык + правила вывода. Полностью формальные, так что корректность записи доказательства может быть проверена компьютерной программой. 2) 🧠 Семантический слой Придаёт смысл предложениям этого языка в терминах ментальных объектов, интуитивно понятных человеку. 3) 🧰 Механизм кодирования идей Позволяет человеку кодировать математические идеи в терминах объектов, на языке этой формальной системы. Стоит заметить, что к моменту формирования Воеводским новых основ уже существовали системы компьютерной верификации, формализующие теорию множеств в её различных интерпретациях: Mizar, Metamath, Isabelle/ZF и т.д. ❓ Чем же теория множеств, как основа не угодила г-ну Воеводскому? 🔹 Первый компонент теории множеств: два «слоя» 1) Логика предикатов — общий механизм построения систем вывода. 2) Конкретная система аксиом и операций, построенная на этом механизме, чаще всего ZFC. Для машинной верификации и удобства синтаксиса терпимо, но есть пара моментов. • 🌳Доказательства — не программы, а деревья формул с пошаговой проверкой; • 🔢Нет естественной “вычислительной” интерпретации; • 👨‍💻Для человека форма доказательств довольно "низкоуровневая": кванторы, подстановки, перестановки формул, приходится постоянно вручную раскручивать определения. Но в конце концов всё это не смертельно, можно построить синтаксис для доказательств не на логике первого порядка, а на более “удобной”: логике высших порядков, теории типов и т.п. 🔹 Второй компонент теории множеств: интуиция иерархий Он основан на способности человека интуитивно понимать иерархии. Фактически, аксиомы теории множеств можно рассматривать как совокупность свойств, которым такие иерархии удовлетворяют. Чаще всего в качестве подобной интуиции рассматривается кумулятивная иерархия множеств. 📦Ящики в ящиках - супер интуитивно. Здесь вообще никаких вопросов. 🔹 Третий компонент теории множеств: кодирование математики Кодирование математических свойств и объектов в терминах иерархий множеств. ❗️И как раз тут начинаются основные проблемы. Любой объект превращается в огромную вложенную конструкцию {{{…}}} из множеств. • 🧰Структуры кодируются множествами с дополнительными данными. • 🧱Привычная для математиков работа “по модулю изоморфизма” в таких объектах, превращается в рутинное доказательство огромного количества лемм о переносе свойств вдоль изоморфизмов. ✨Надеюсь теперь вы в общих чертах понимаете причины, побудившие Воеводского создать новые основания, более “удобные” для компьютерной проверки доказательств - УНИВАЛЕНТНЫЕ ОСНОВАНИЯ. О них в следующем посте🚀