Metamath — это формальный язык и связанная с ним компьютерная программа ( помощник по доказательству ) для архивирования и проверки математических доказательств. [2] С использованием Metamath было разработано несколько баз данных доказанных теорем, охватывающих стандартные результаты в логике , теории множеств , теории чисел , алгебре , топологии и анализе , среди прочих. [3]
К 2023 году Metamath использовался для доказательства 74 [4] из 100 теорем конкурса «Формализация 100 теорем». [5] По крайней мере 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 термин s $. вп $ф вфф П $. вк $ф вфф Q $.$( Определите "wff" (часть 1) $) мы $а wff t = r $.$( Определите "wff" (часть 2) $) wim $a wff ( P -> Q ) $.
Аксиомы и правила вывода указываются с помощью $aутверждений вместе с ${утверждениями $}для области действия блока и необязательными $e(существенными гипотезами) утверждениями; например:
$( Аксиома состояния a1 $) а1 $а |- ( т = р -> ( т = с -> р = с ) ) $.$( Аксиома состояния a2 $) а2 $а |- ( т + 0 ) = т $. ${ мин $e |- P $. маж $e |- ( P -> Q ) $.$( Определить правило вывода modus ponens $) мп $а |- 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 tze $ за семестр 0 1,2 tpl $ срок ( t + 0 ) 3,1 мы $ а wff ( t + 0 ) = t 1,1 мы $ а wff t = t 1 а2 $ а |- ( т + 0 ) = т 1,2 tpl $ срок ( t + 0 ) 7,1 weq $ a wff ( t + 0 ) = t 1,2 tpl $ срок ( t + 0 ) 9,1 weq $ a wff ( t + 0 ) = t 1,1 мы $ а wff t = t 10,11 wim $ a wff ( ( t + 0 ) = t -> t = t ) 1 а2 $ а |- ( т + 0 ) = т 1,2 tpl $ срок ( t + 0 ) 14,1,1 a1 $ a |- ( ( t + 0 ) = t -> ( ( t + 0 ) = t -> t = t ) ) 8,12,13,15 mp $ a |- ( ( t + 0 ) = t -> t = t ) 4,5,6,16 мп $ а |- т = т «Существенная» форма доказательства опускает синтаксические детали, оставляя более традиционное представление:
а2 $ а |- ( т + 0 ) = т а2 $ а |- ( т + 0 ) = т а1 $ а |- ( ( т + 0 ) = т -> ( ( т + 0 ) = т -> т = т ) ) 2,3 mp $ а |- ( ( т + 0 ) знак равно т -> т = т ) 1,4 мп $ а |- т = т Все шаги доказательства 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 в память, проверять доказательства базы данных, изменять базу данных (в частности, добавляя доказательства) и записывать их обратно в хранилище.
В нем есть команда proof , которая позволяет пользователям вводить доказательство, а также механизмы поиска существующих доказательств.
Программа Metamath может преобразовывать операторы в нотацию HTML или TeX ; например, она может вывести аксиому modus ponens из set.mm как:
Многие другие программы могут обрабатывать базы данных Metamath, в частности, существует не менее 19 верификаторов доказательств для баз данных, использующих формат Metamath. [10]
На сайте Metamath размещено несколько баз данных, в которых хранятся теоремы, полученные из различных аксиоматических систем. Большинство баз данных ( файлы .mm ) имеют связанный интерфейс, называемый «Explorer», который позволяет интерактивно перемещаться по утверждениям и доказательствам на сайте, в удобном для пользователя виде. Большинство баз данных используют систему формальной дедукции Гильберта, хотя это не является обязательным требованием.
Metamath Proof Explorer (записанный в set.mm ) является основной базой данных. Она основана на классической логике первого порядка и теории множеств ZFC (с добавлением теории множеств Тарского-Гротендика при необходимости, например, в теории категорий ). База данных поддерживается уже более тридцати лет (первые доказательства в set.mm датированы сентябрем 1992 года). База данных содержит разработки, среди прочего, теории множеств (ординалы и кардиналы, рекурсия, эквиваленты аксиомы выбора, гипотеза континуума...), построения систем действительных и комплексных чисел, теории порядка, теории графов, абстрактной алгебры, линейной алгебры, общей топологии, действительного и комплексного анализа, гильбертовых пространств, теории чисел и элементарной геометрии. [11]
Metamath Proof Explorer ссылается на множество учебников, которые можно использовать вместе с Metamath. [12] Таким образом, люди, интересующиеся изучением математики, могут использовать Metamath вместе с этими книгами и проверять, соответствуют ли доказанные утверждения литературе.
Эта база данных развивает математику с конструктивной точки зрения, начиная с аксиом интуиционистской логики и продолжая системами аксиом конструктивной теории множеств .
Эта база данных развивает математику на основе теории множеств «Новых оснований» Куайна .
Эта база данных начинается с логики высшего порядка и выводит эквиваленты аксиом логики первого порядка и теории множеств ZFC.
На сайте Metamath размещено несколько других баз данных, которые не связаны с explorers, но тем не менее заслуживают внимания. База данных 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 к формальному кодированию системных проверок, они также реализуют свои собственные новые концепции.
Mel O'Cat разработал систему под названием Mmj2 , которая предоставляет графический пользовательский интерфейс для ввода доказательств. [17] Первоначальная цель Mel O'Cat состояла в том, чтобы позволить пользователю вводить доказательства, просто печатая формулы и позволяя Mmj2 находить соответствующие правила вывода для их соединения. В Metamath, напротив, вы можете вводить только названия теорем. Вы не можете вводить формулы напрямую. Mmj2 также имеет возможность вводить доказательство вперед или назад (Metamath позволяет вводить доказательство только назад). Более того, Mmj2 имеет настоящий грамматический анализатор (в отличие от Metamath). Это техническое различие приносит больше комфорта пользователю. В частности, Metamath иногда колеблется между несколькими формулами, которые он анализирует (большинство из них бессмысленны), и просит пользователя сделать выбор. В Mmj2 этого ограничения больше не существует.
Существует также проект Уильяма Хейла по добавлению графического пользовательского интерфейса к Metamath под названием Mmide . [18] Пол Чепмен, в свою очередь, работает над новым браузером доказательств, который имеет подсветку, позволяющую вам видеть указанную теорему до и после подстановки.
Milpgame — помощник по доказательствам и проверяющий (он показывает сообщение только в случае возникновения ошибки) с графическим пользовательским интерфейсом для языка Metamath (set.mm), написанный Филиппом Чернатеску, это приложение Java с открытым исходным кодом (лицензия MIT) (кроссплатформенное приложение: Windows, Linux, Mac OS). Пользователь может ввести демонстрацию (доказательство) в двух режимах: вперед и назад относительно доказываемого утверждения. Milpgame проверяет, правильно ли сформировано утверждение (имеет синтаксический верификатор). Он может сохранять незаконченные доказательства без использования теоремы dummylink. Демонстрация отображается в виде дерева, утверждения отображаются с использованием определений HTML (определено в главе о наборе текста). Milpgame распространяется как Java .jar (JRE версии 6, обновление 24, написанное в IDE NetBeans).
