🧠🤖ВЛАДИМИР ВОЕВОДСКИЙ и КОМПЬЮТЕРНАЯ ПРОВЕРКА ДОКАЗАТЕЛЬСТВ Часть 3. Аксиома унивалентности ❤️Начнём с самого сердца. 💭Помните в позапрошлом посте мы заявили в качестве одной из проблем использования теоретико-множественных основ в мире компьютерных доказательств - огромное количество лемм о переносе свойств вдоль изоморфизмов (далее буду использовать более широкое понятие эквивалентности) . Простой пример: тип BOOL и условный тип BIN {0,1} очевидно эквивалентны друг другу - в них явная биекция между элементами. Но они будут не равны как типы, если у них разные конструкторы/описания или они по-разному “заданы”. Причём отсутствие равенства в этом случае не позволит нам воспользоваться, таким привычным законом Лейбница: Если x = y, то для любого свойства P: из P(x) следует P(y). И для переноса свойств (так называемый transport(P): P(BOOL) -> P(BIN)) потребуется дополнительное доказательство правомерности такого переноса. ⚔️ Конфликт “равенств” Если обобщить эту проблему - при использовании языка логики совместно с теорией образуется этакий языковой конфликт в понятиях “равенства”. Даже лучше сказать - онтологическое несоответствие: 🟦 1) логического равенства, как утверждения; 🟩 2) понятия эквивалентности, как структурного соответствия (чем зачастую математики и пользуются в доказательствах). 🟦 1-ое Про правила вывода, стандартную игру с формулами, слепое равенство во всех контекстах 🟩 2-ое Про структурный подход, т.е. не про полную неразличимую идентичность объектов, а про равенство «структур», равенство поведения. 🦆Как в известном утином тесте: “Если выглядит как утка, плавает как утка и т.п. - перед вами утка” Немного про структурализм говорили в видео про фундаментальные теории: https://www.youtube.com/watch?v=Gt8ypZDIPKE&t=275s Грубо говоря равенство зависит от представления, а эквивалентность от сути. 🤝 Почему раньше об этом не задумывались? Пока дело не дошло до компьютерной формализации, допускалось довольно вольное отношение к доказательствам. На практике эквивалентные объекты бездоказательно используются как равные, подразумевая "молчаливый" перенос свойств между структурами. Просто делается вид, что не имеет значения какая из «эквивалентных копий» используется, и они рассматриваются, как один и тот же математический объект. 😈Своего рода систематическая небрежность, помогающая сэкономить время, иногда даже в шутку называемая «злоупотреблением обозначениями». 🚫Но в теории множеств нельзя автоматически отождествлять эквивалентные объекты как равные. И такое "замалчивание" в компьютерных доказательствах недопустимо, так что приходится все эти бесконечные переносы свойств между структурами формализовать. Рутина, от которой спасала компьютерная проверка заменяется рутиной формализации таких переносов. ❗️Вот почему были необходимы другие основания. В которых мы бы могли без зазрения совести говорить, что эквивалентные объекты аксиоматически имеют те же привилегии, что и равные. ✨Основания с АКСИОМОЙ УНИВАЛЕНТНОСТИ: (A=B)≃(A≃B)