Метамат - Metamath

Метамат
Metamath logo.png
Разработчики) Норман Мегилл
Репозиторий Отредактируйте это в Викиданных
Написано в ANSI C
Операционная система Linux , Windows , macOS
Тип Компьютерная проверка документов
Лицензия Стандартная общественная лицензия GNU ( Creative Commons Public Domain Dedication для баз данных)
Интернет сайт metamath .org

Metamath - это формальный язык и связанная с ним компьютерная программа (программа проверки доказательств ) для архивирования, проверки и изучения математических доказательств. Несколько баз данных доказанных теорем были разработаны с использованием Metamath покрытия стандартные результаты в логике , теории множеств , теории чисел , алгебре , топологии и анализа , среди других.

По состоянию на декабрь 2020 года, множество доказанных теорем с использованием Metamath является одним из крупнейших органов формализованной математики, содержащего , в частности , доказательство 74 из 100 теорем «Формализация 100 теорем» вызова, что делает его третьим после HOL света и Изабелл , но до Coq , Mizar , ProofPower , Lean , Nqthm , ACL2 и Nuprl . Существует не менее 17 верификаторов для баз данных, использующих формат Metamath.

Этот проект является первым в своем роде, который позволяет интерактивно просматривать свою формализованную базу данных теорем в виде обычного веб-сайта.

Язык метаматов

Язык Metamath - это метаязык , подходящий для разработки самых разных формальных систем . В языке Metamath нет встроенной конкретной логики. Вместо этого его можно просто рассматривать как способ доказать, что правила вывода (утвержденные как аксиомы или доказанные позже) могут быть применены. Самая большая база данных доказанных теорем соответствует традиционной теории множеств ZFC и классической логике, но существуют и другие базы данных, и другие могут быть созданы.

Дизайн языка Metamath ориентирован на простоту; язык, используемый для формулировки определений, аксиом, правил вывода и теорем, состоит только из нескольких ключевых слов, и все доказательства проверяются с использованием одного простого алгоритма, основанного на подстановке переменных (с необязательными оговорками, какие переменные должны оставаться различными после замены).

Основы языка

Набор символов, которые можно использовать для построения формул, объявляется с помощью операторов $c(постоянные символы) и $v(переменные символы); Например:

$( Declare the constant symbols we will use $)
    $c 0 + = -> ( ) term wff |- $.
$( Declare the metavariables we will use $)
    $v t r s P Q $.

Грамматика формул определяется с помощью комбинации $f(плавающих (переменных) гипотез) и $a(аксиоматических утверждений) операторов; Например:

$( Specify properties of the metavariables $)
    tt $f term t $.
    tr $f term r $.
    ts $f term s $.
    wp $f wff P $.
    wq $f wff Q $.
$( Define "wff" (part 1) $)
    weq $a wff t = r $.
$( Define "wff" (part 2) $)
    wim $a wff ( P -> Q ) $.

Аксиомы и правила вывода указываются вместе с $aоператорами, ${а также $}для определения области видимости блока и необязательными $e(существенные гипотезы) операторами; Например:

$( State axiom a1 $)
    a1 $a |- ( t = r -> ( t = s -> r = s ) ) $.
$( State axiom a2 $)
    a2 $a |- ( t + 0 ) = t $.
    ${
       min $e |- P $.
       maj $e |- ( P -> Q ) $.
$( Define the modus ponens inference rule $)
       mp  $a |- Q $.
    $}

Использование одной конструкции, $aоператоров, для захвата синтаксических правил, схем аксиом и правил вывода предназначено для обеспечения уровня гибкости, аналогичного логическим структурам более высокого порядка, без зависимости от системы сложных типов.

Доказательства

Теоремы (и производные правила вывода) записываются с $pутверждениями; Например:

$( Prove a theorem $)
    th1 $p |- t = t $=
  $( Here is its proof: $)
       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
       tt tze tpl tt tt a1 mp mp
     $.

Обратите внимание на включение доказательства в $pутверждение. Это сокращает следующее подробное доказательство:

tt            $f term t
tze           $a term 0
1,2 tpl       $a term ( t + 0 )
3,1 weq       $a wff ( t + 0 ) = t
1,1 weq       $a wff t = t
1 a2          $a |- ( t + 0 ) = t
1,2 tpl       $a term ( t + 0 )
7,1 weq       $a wff ( t + 0 ) = t
1,2 tpl       $a term ( t + 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 a2          $a |- ( t + 0 ) = t
1,2 tpl       $a term ( 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 mp   $a |- t = t

«Основная» форма доказательства опускает синтаксические детали, оставляя более традиционное представление:

a2             $a |- ( t + 0 ) = t
a2             $a |- ( t + 0 ) = t
a1             $a |- ( ( t + 0 ) = t -> ( ( t + 0 ) = t -> t = t ) )
2,3 mp         $a |- ( ( t + 0 ) = t -> t = t )
1,4 mp         $a |- 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 - это оригинальная программа, созданная для управления базами данных, написанными с использованием языка Metamath. Он имеет текстовый интерфейс (командная строка) и написан на языке C. Он может считывать базу данных Metamath в память, проверять доказательства базы данных, изменять базу данных (в частности, добавляя доказательства) и записывать их обратно в хранилище.

В нем есть команда доказательства, которая позволяет пользователям вводить доказательство, а также механизмы поиска существующих доказательств.

Программа Metamath может преобразовывать операторы в нотацию HTML или TeX ; например, он может выводить аксиому modus ponens из set.mm как:

Многие другие программы могут обрабатывать базы данных Metamath, в частности, существует не менее 17 верификаторов доказательств для баз данных, использующих формат Metamath.

Базы данных Metamath

На веб-сайте Metamath размещено несколько баз данных, в которых хранятся теоремы, полученные из различных аксиоматических систем. Большинство баз данных ( файлы .mm ) имеют связанный интерфейс, называемый «проводником», который позволяет перемещаться по утверждениям и доказательствам в интерактивном режиме на веб-сайте в удобной для пользователя форме. Большинство баз данных используют систему формального вывода Гильберта, хотя это не является обязательным требованием.

Metamath Proof Explorer

Metamath Proof Explorer
Метамат-теорема-avril1-indexed.png
Доказательство Metamath Proof Explorer
Тип сайта
Интернет-энциклопедия
Главное управление Соединенные Штаты Америки
Владелец Норман Мегилл
Сделано Норман Мегилл
URL us .metamath .org / mpeuni / mmset .html
Коммерческий Нет
Регистрация Нет

Metamath Proof Explorer (записанный в set.mm ) является основной и, безусловно, самой большой базой данных, с более чем 23000 доказательств в ее основной части по состоянию на июль 2019 года. Она основана на классической логике первого порядка и теории множеств ZFC (с добавление теории множеств Тарского-Гротендика, когда это необходимо, например, в теории категорий ). База данных поддерживается более двадцати лет (первые доказательства в set.mm датированы августом 1993 г.). База данных содержит разработки, среди других областей, теории множеств (ординалы и кардиналы, рекурсия, эквиваленты выбранной аксиомы, гипотеза континуума ...), построение систем действительных и комплексных чисел, теория порядка, теория графов, абстрактная алгебра, линейная алгебра, общая топология, вещественный и комплексный анализ, гильбертовы пространства, теория чисел и элементарная геометрия. Эта база данных была впервые создана Норманом Мегиллом, но по состоянию на 04.10.2019 было 48 участников (включая Нормана Мегилла).

Metamath Proof Explorer ссылается на многие учебники, которые можно использовать вместе с Metamath. Таким образом, люди, заинтересованные в изучении математики, могут использовать Metamath в связи с этими книгами и проверить соответствие доказанных утверждений литературным.

Интуиционистский исследователь логики

Эта база данных развивает математику с конструктивной точки зрения, начиная с аксиом интуиционистской логики и заканчивая системами аксиом конструктивной теории множеств .

Исследователь новых основ

Эта база данных развивает математику на основе теории множеств « Новые основы Куайна » .

Исследователь логики высшего порядка

Эта база данных начинается с логики более высокого порядка и выводит эквиваленты аксиом логики первого порядка и теории множеств ZFC.

Базы данных без проводников

На веб-сайте Metamath есть несколько других баз данных, которые не связаны с исследователями, но, тем не менее, заслуживают внимания. База данных peano.mm, написанная Робертом Соловеем, формализует арифметику Пеано . База данных нат.мм формализует естественный вывод . База данных 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

Проверки доказательств

Используя идеи дизайна, реализованные в Metamath, Раф Левиен реализовал очень маленькую программу проверки правописания mmverify.py всего на 500 строках кода Python.

Ghilbert - похожий, хотя и более сложный язык, основанный на mmverify.py. Левиен хотел бы реализовать систему, в которой несколько человек могли бы сотрудничать, и его работа подчеркивает модульность и связь между небольшими теориями.

Используя основополагающие работы Левьена, многие другие реализации принципов проектирования Metamath были реализованы для самых разных языков. Юха Арпиайнен реализовал свою собственную проверку на Common Lisp под названием Bourbaki, а Марникс Клоостер написал программу проверки на Haskell под названием Hmm .

Хотя все они используют общий подход Metamath к кодированию формальной системы проверки, они также реализуют собственные новые концепции.

Редакторы

Мел О'Кат разработал систему под названием Mmj2 , которая предоставляет графический пользовательский интерфейс для подтверждения ввода. Первоначальная цель Мела О'Ката заключалась в том, чтобы позволить пользователю вводить доказательства, просто набирая формулы и позволяя Mmj2 найти подходящие правила вывода для их соединения. В Metamath, наоборот, вы можете вводить только названия теорем. Вы не можете вводить формулы напрямую. Mmj2 также имеет возможность вводить доказательство вперед или назад (Metamath позволяет вводить доказательство только назад). Более того, в Mmj2 есть настоящий грамматический синтаксический анализатор (в отличие от Metamath). Это техническое отличие приносит пользователю больше комфорта. В частности, Metamath иногда колеблется между несколькими формулами, которые он анализирует (большинство из них бессмысленны), и просит пользователя выбрать. В Mmj2 этого ограничения больше нет.

Существует также проект Уильяма Хейла по добавлению графического пользовательского интерфейса в Metamath под названием Mmide . Пол Чепмен, в свою очередь, работает над новым браузером доказательств, в котором есть подсветка, позволяющая увидеть указанную теорему до и после того, как была сделана подстановка.

Milpgame - это помощник по проверке и проверка (он показывает сообщение только о том, что что-то пошло не так) с графическим пользовательским интерфейсом для языка Metamath (set.mm), написанным Филипом Чернатеску, это приложение Java с открытым исходным кодом (лицензия MIT) ( кроссплатформенное приложение: Window, Linux, Mac OS). Пользователь может войти в демонстрацию (доказательство) в двух режимах: вперед и назад относительно утверждения, которое необходимо доказать. Milpgame проверяет, правильно ли сформирован оператор (имеет синтаксический верификатор). Он может сохранить незаконченные доказательства без использования теоремы фиктивной ссылки. Демонстрация представлена ​​в виде дерева, операторы показаны с использованием определений html (определенных в главе о наборе текста). Milpgame распространяется как Java .jar (обновление 24 JRE версии 6, написанное в IDE NetBeans).

Смотрите также

использованная литература

внешние ссылки