Metamath — это формальный язык и связанная с ним компьютерная программа ( помощник по доказательствам ) для архивирования и проверки математических доказательств. [2] С использованием Metamath было разработано несколько баз данных доказанных теорем, охватывающих стандартные результаты в логике , теории множеств , теории чисел , алгебре , топологии и анализе , среди других. [3]
По состоянию на сентябрь 2023 года [обновлять]набор доказанных с помощью Metamath теорем включает 74 [4] из 100 теорем задачи «Формализация 100 теорем», [5] что делает его пятым после Isabelle , HOL Light , Coq и Lean . Существует как минимум 19 средств проверки доказательств, использующих формат Metamath. [6] Веб-сайт Metamath предоставляет базу данных формализованных теорем, которую можно просматривать в интерактивном режиме. [7]
Язык Metamath — это метаязык формальных систем . В языке Metamath нет встроенной какой-либо конкретной логики. Вместо этого его можно рассматривать как способ доказать, что правила вывода (утвержденные как аксиомы или доказанные позже) могут быть применены. Самая большая база данных доказанных теорем основана на традиционной логике первого порядка и теории множеств ZFC . [8]
Дизайн языка Metamath (используемый для формулировки определений, аксиом, правил вывода и теорем) ориентирован на простоту; он содержит лишь несколько [ необходимо уточнение ] ключевых слов. Доказательства проверяются с помощью алгоритма, основанного на подстановке переменных . Алгоритм также имеет дополнительные оговорки о том, какие переменные должны оставаться разными после замены. [9]
Набор символов, которые можно использовать для построения формул, объявляется с помощью операторов $c(постоянные символы) и $v(переменные символы); например:
$( Объявите константные символы, которые мы будем использовать $) $c 0 + = -> ( ) термин wff |- $.$( Объявите метапеременные, которые мы будем использовать $) $vtrs PQ$.
Грамматика формул задается с использованием комбинации утверждений $f(гипотезы плавающего типа (типа переменной)) и $aутверждений (аксиоматического утверждения); например:
$( Укажите свойства метапеременных $) tt $f срок t $. tr$f срок r$. ts $f term s $. wp $f wff P $. wq $f wff Q $.$( Определите «wff» (часть 1) $) weq $a wff t = r $.$( Определите «wff» (часть 2) $) wim $a wff (P -> Q) $.
Аксиомы и правила вывода определяются с помощью $aоператоров вместе с ${и $}для определения области действия блока, а также необязательных $e(существенных гипотез) операторов; например:
$( Аксиома состояния a1 $) a1 $a |- ( t = r -> ( t = s -> r = s )) $.$( Аксиома состояния a2 $) а2 $а |- ( т + 0 ) = т $. ${ min $e |- P$. maj $e |- ( P -> Q ) $.$( Определить правило вывода modus ponens $) mp$a |- Q$. $}Использование одной конструкции, $aоператоров, для фиксации синтаксических правил, схем аксиом и правил вывода предназначено для обеспечения уровня гибкости, аналогичного логическим структурам более высокого порядка, без зависимости от сложной системы типов.
Теоремы (и производные правила вывода) записываются с помощью $pутверждений; например:
$( Докажите теорему $) th1 $p |- t = t $= $( Вот доказательство: $) tt tze tpl tt weq tt tt weq tt a2 tt tze tpl tt weq tt tze tpl tt weq tt tt weq wim tt a2 тт зе тпл тт тт а1 мп мп $.
Обратите внимание на включение доказательства в $pутверждение. Он сокращает следующее подробное доказательство:
tt $ f срок t цзе $ срок 0 _ 1,2 тпл $ в семестр ( т + 0 ) 3,1 weq $ a wff ( t + 0 ) = t 1,1 weq $ a wff t = t 1 а2 $ а |- ( т + 0 ) знак равно т 1,2 тпл $ в семестр ( т + 0 ) 7,1 weq $ a wff ( t + 0 ) = t 1,2 тпл $ в семестр ( т + 0 ) 9,1 weq $ a wff ( t + 0 ) = t 1,1 weq $ a wff t = t 10,11 wim $ a wff ( ( t + 0 ) = t -> t = t ) 1 а2 $ а |- ( т + 0 ) знак равно т 1,2 тпл $ в семестр ( т + 0 ) 14,1,1 a1 $ a |- ( ( т + 0 ) знак равно т -> ( ( т + 0 ) = т -> т = т ) ) 8,12,13,15 mp $ a |- ( ( t + 0 ) = t -> t = t ) 4,5,6,16 мп $ а |- t = t «Существенная» форма доказательства упускает из виду синтаксические детали, оставляя более традиционное представление:
а2 $ а |- ( т + 0 ) знак равно т а2 $ а |- ( т + 0 ) знак равно т а1 $ а |- ( ( т + 0 ) знак равно т -> ( ( т + 0 ) знак равно т -> т = т ) ) 2,3 mp $ a |- ( ( т + 0 ) знак равно т -> т = т ) 1,4 мп $ а |- t = t На всех этапах доказательства Metamath используется одно правило замены, которое представляет собой простую замену переменной выражением, а не правильную замену, описанную в работах по исчислению предикатов . Правильная замена в базах данных Metamath, которые ее поддерживают, представляет собой производную конструкцию, а не встроенную в сам язык Metamath.
Правило замены не делает никаких предположений об используемой логической системе и требует только правильного выполнения замен переменных.
Вот подробный пример того, как работает этот алгоритм. Шаги 1 и 2 теоремы 2p2e4в Metamath Proof Explorer ( set.mm ) изображены слева. Давайте объясним, как Metamath использует свой алгоритм подстановки, чтобы проверить, что шаг 2 является логическим следствием шага 1, когда вы используете теорему opreq2i. Шаг 2 гласит, что (2 + 2) = (2 + (1 + 1)) . Это вывод теоремы opreq2i. Теорема opreq2iутверждает, что если A = B , то ( CFA ) = ( CFB ) . Эта теорема никогда не появится в таком загадочном виде в учебнике, но ее грамотная формулировка банальна: когда две величины равны, одну можно заменить в ходе операции. Чтобы проверить доказательство, Metamath пытается объединить ( CFA ) = ( CFB ) с (2 + 2) = (2 + (1 + 1)) . Есть только один способ сделать это: объединить C с 2 , F с + , A с2 и B с (1 + 1) . Итак, теперь Metamath использует предпосылку opreq2i. Эта посылка гласит, что A = B. В результате предыдущих вычислений Metamath знает, что A следует заменить на2 и B на (1 + 1) . Посылка A = B становится 2=( 1 + 1 ) , и, таким образом, генерируется шаг 1. В свою очередь шаг 1 унифицирован с df-2. df-2является определением числа 2и утверждает, что 2 = ( 1 + 1 ). Здесь унификация — это просто вопрос констант и она проста (нет проблем с заменой переменных). Итак, проверка завершена, и эти два шага доказательства 2p2e4верны.
Когда Metamath объединяет ( 2 + 2 ) с B , он должен проверить соблюдение синтаксических правил. На самом деле B имеет тип, classпоэтому Metamath должен проверить, что (2 + 2) также является типизированным class.
Программа Metamath — это оригинальная программа, созданная для управления базами данных, написанными на языке Metamath. Он имеет текстовый интерфейс (командной строки) и написан на C. Он может считывать базу данных Metamath в память, проверять доказательства базы данных, изменять базу данных (в частности, добавляя доказательства) и записывать их обратно в хранилище.
Он имеет команду доказательства , которая позволяет пользователям вводить доказательство, а также механизмы поиска существующих доказательств.
Программа Metamath может преобразовывать операторы в нотацию HTML или TeX ; например, он может вывести аксиому modus ponens из set.mm как:
Многие другие программы могут обрабатывать базы данных Metamath, в частности, существует как минимум 19 средств проверки для баз данных, использующих формат Metamath. [10]
На веб-сайте Metamath размещено несколько баз данных, в которых хранятся теоремы, полученные из различных аксиоматических систем. Большинство баз данных ( файлы .mm ) имеют соответствующий интерфейс, называемый «Проводник», который позволяет удобно перемещаться по утверждениям и доказательствам на веб-сайте в интерактивном режиме. В большинстве баз данных используется система формального вывода Гильберта , хотя это не является обязательным требованием.
Metamath Proof Explorer (записанный в set.mm ) — это основная и, безусловно, самая большая база данных, в основной части которой по состоянию на июль 2019 года содержится более 23 000 доказательств. Она основана на классической логике первого порядка и теории множеств ZFC (с добавление теории множеств Тарского-Гротендика , когда это необходимо, например, в теории категорий ). База данных поддерживается более тридцати лет (первые доказательства в set.mm датированы сентябрем 1992 года). База данных содержит, среди прочего, разработки в области теории множеств (ординалы и кардиналы, рекурсия, эквиваленты аксиомы выбора, гипотеза континуума...), построения действительных и комплексных систем счисления, теории порядка, теории графов, абстрактная алгебра, линейная алгебра, общая топология, вещественный и комплексный анализ, гильбертово пространство, теория чисел и элементарная геометрия. Эта база данных была впервые создана Норманом Мегиллом, но по состоянию на 4 октября 2019 г. в ней приняли участие 48 участников (включая Нормана Мегилла). [11]
Metamath Proof Explorer ссылается на множество учебников, которые можно использовать вместе с Metamath. [12] Таким образом, люди, заинтересованные в изучении математики, могут использовать Metamath в связи с этими книгами и убедиться, что доказанные утверждения соответствуют литературе.
Эта база данных развивает математику с конструктивной точки зрения, начиная с аксиом интуиционистской логики и заканчивая системами аксиом конструктивной теории множеств .
Эта база данных развивает математику на основе теории множеств «Новые основы» Куайна .
Эта база данных начинается с логики высшего порядка и выводит эквиваленты аксиом логики первого порядка и теории множеств ZFC.
На веб-сайте Metamath размещено еще несколько баз данных, не связанных с исследователями, но, тем не менее, заслуживающих внимания. База данных peano.mm, написанная Робертом Соловеем, формализует арифметику Пеано . База данных nat.mm [13] формализует естественный вывод . База данных miu.mm формализует головоломку MU на основе формальной системы MIU, представленной у Гёделя, Эшера, Баха .
На веб-сайте Metamath также размещено несколько старых баз данных, которые больше не поддерживаются, такие как «Hilbert Space Explorer», в котором представлены теоремы, относящиеся к теории гильбертова пространства , которые теперь объединены в Metamath Proof Explorer, и «Quantum Logic Explorer». , который развивает квантовую логику , начиная с теории ортомодулярных решеток.
Поскольку Metamath имеет очень общее представление о том, что такое доказательство (а именно, дерево формул, связанных правилами вывода), и в программное обеспечение не встроена какая-либо конкретная логика, Metamath можно использовать с такими разными видами логики, как логики в стиле Гильберта или секвенции. -ориентированной логики или даже с помощью лямбда-исчисления .
Однако Metamath не обеспечивает прямой поддержки систем естественной дедукции . Как отмечалось ранее, база данных nat.mm формализует естественный вычет. Вместо этого Metamath Proof Explorer (с его базой данных set.mm ) использует набор соглашений, которые позволяют использовать подходы естественного вывода в рамках логики в стиле Гильберта.
Используя дизайнерские идеи, реализованные в Metamath, Раф Левиен реализовал очень небольшую программу проверки доказательств mmverify.py , состоящую всего из 500 строк кода Python.
Ghilbert — похожий, но более сложный язык, основанный на mmverify.py. [14] Левиен хотел бы реализовать систему, в которой могли бы сотрудничать несколько человек, и его работа подчеркивает модульность и связь между небольшими теориями.
Благодаря плодотворной работе Левина было реализовано множество других реализаций принципов проектирования Metamath для самых разных языков. Юха Арпиайнен реализовал свою собственную программу проверки доказательств на Common Lisp под названием Bourbaki [15], а Марникс Клоостер написал на Haskell программу проверки доказательств под названием Hmm . [16]
Хотя все они используют общий подход Metamath к формальному кодированию средств проверки системы, они также реализуют собственные новые концепции.
Мел О'Кэт разработал систему под названием Mmj2 , которая предоставляет графический пользовательский интерфейс для ввода доказательств. [17] Первоначальная цель Мела О'Кэта заключалась в том, чтобы позволить пользователю вводить доказательства, просто набирая формулы и позволяя Mmj2 найти подходящие правила вывода для их соединения. В Metamath, наоборот, вы можете вводить только названия теорем. Вы не можете вводить формулы напрямую. Mmj2 также имеет возможность вводить доказательство вперед или назад (Metamath позволяет вводить доказательство только назад). Более того, в Mmj2 есть настоящий парсер грамматики (в отличие от Metamath). Эта техническая разница приносит пользователю больше комфорта. В частности, Metamath иногда колеблется между несколькими анализируемыми формулами (большинство из них бессмысленны) и просит пользователя сделать выбор. В Mmj2 этого ограничения больше нет.
Существует также проект Уильяма Хейла по добавлению в Metamath графического пользовательского интерфейса под названием Mmide . [18] Пол Чепмен, в свою очередь, работает над новым браузером доказательств, который имеет подсветку, позволяющую видеть указанную теорему до и после замены.
Milpgame — это помощник по проверке и проверке (он показывает сообщение только о том, что что-то пошло не так) с графическим пользовательским интерфейсом для языка Metamath (set.mm), написанным Филипом Чернатеску. Это Java-приложение с открытым исходным кодом (лицензия MIT) ( кроссплатформенное приложение: Windows, Linux, Mac OS). Пользователь может ввести демонстрацию (доказательство) в двух режимах: вперед и назад относительно доказывающего утверждения. Milpgame проверяет, правильно ли сформирован оператор (имеет ли синтаксический верификатор). Он может сохранять незавершенные доказательства без использования теоремы о фиктивной ссылке. Демонстрация представлена в виде дерева, операторы показаны с использованием определений HTML (определенных в главе о верстке). Milpgame распространяется как Java .jar(JRE версии 6, обновление 24, написанное в среде IDE NetBeans).
