Abstract
<jats:p>Работа устраняет отношение принадлежности (∈) из оснований, заменяя его бинарным различением. На этой базе строится гиперкубическая онтология, которая: 1) даёт прямую вычислительную семантику для теории зависимых типов, 2) явно строит континуум как факторпространство, локализуя источник неконструктивности, 3) предоставляет инструмент для перевода конструктивных фрагментов классической математики (от ZFC до анализа) в язык конечных спецификаций. Это предлагается как единый метаязык для явного, алгоритмического переосмысления математических оснований.</jats:p>
Show More
Keywords
для
оснований
как
Работа
устраняет