Метаматематика

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

Метаматематика
Разработчик(и)	Норман МакГилл
Первоначальный выпуск	0,07 в июне 2005 г .; 19 лет назад
Стабильная версия	0.198 / 7 августа 2021 г .; 2 года назад
Репозиторий	github .с /метаматематика /метамат-exe ;
Написано в	АНСИ С
Операционная система	Линукс , Виндовс , МакОС
Тип	Компьютерная проверка доказательств
Лицензия	Стандартная общественная лицензия GNU ( отделение Creative Commons Public Domain для баз данных)
Веб-сайт	метаматематика .org

Metamath — это формальный язык и связанная с ним компьютерная программа ( помощник по доказательствам ) для архивирования и проверки математических доказательств. ^[2] С использованием Metamath было разработано несколько баз данных доказанных теорем, охватывающих стандартные результаты в области логики , теории множеств , теории чисел , алгебры , топологии и анализа , среди других. ^[3]

К 2023 году Metamath была использована для доказательства 74 ^[4] из 100 теорем конкурса «Формализация 100 теорем». ^[5] По крайней мере 19 проверяющих используют формат Metamath. ^[6] Веб-сайт Metamath предоставляет базу данных формализованных теорем, которую можно просматривать в интерактивном режиме. ^[7]

Язык метаматематики [ править ]

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

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

Основы языка [ править ]

Набор символов, которые можно использовать для построения формул, объявляется с помощью $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)$ . Итак, теперь Метаматия использует предпосылку 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 как:

\vdash \varphi \quad \&\quad \vdash (\varphi \rightarrow \psi )\quad \Rightarrow \quad \vdash \psi

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

Базы данных Metamath [ править ]

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

Metamath Proof Explorer [ править ]

Metamath Proof Explorer (записанный в set.mm ) является основной базой данных. Он основан на классической логике первого порядка и теории множеств ZFC (с добавлением теории множеств Тарского-Гротендика , когда это необходимо, например, в теории категорий ). База данных поддерживается более тридцати лет (первые доказательства в set.mm датированы сентябрем 1992 года). База данных содержит, среди прочего, разработки в области теории множеств (ординалы и кардиналы, рекурсия, эквиваленты аксиомы выбора, гипотеза континуума...), построения действительных и комплексных систем счисления, теории порядка, теории графов, абстрактная алгебра, линейная алгебра, общая топология, вещественный и комплексный анализ, гильбертово пространство, теория чисел и элементарная геометрия. ^[11]

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

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

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

Исследователь новых фондов [ править ]

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

Обозреватель логики высшего порядка [ править ]

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

Базы данных без проводников [ править ]

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

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

Используя дизайнерские идеи, реализованные в 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).

См. также [ править ]

Ссылки [ править ]

^ «Выпуск 0.198» . 8 августа 2021 г. Проверено 27 июля 2022 г.
^ Мегилл, Норман; Уилер, Дэвид А. (2 июня 2019 г.). Метаматематика: компьютерный язык для математических доказательств (второе изд.). Моррисвилл, Северная Каролина, США: Lulu Press . п. 248. ИСБН 978-0-359-70223-7 .
^ Мегилл, Норман. «Что такое Метаматия?» . Домашняя страница Метаматемы .
^ Метаматематика 100.
^ «Формализация 100 теорем» .
^ Мегилл, Норман. «Известные средства проверки доказательств Metamath» . Проверено 8 октября 2022 г.
^ «Содержание списка теорем — исследование метаматематических доказательств» . us.metamath.org . Проверено 4 сентября 2023 г.
^ Видейк, Фрик. «Семнадцать искателей мира» (PDF) . стр. 103–105 . Проверено 14 октября 2023 г.
^ Мегилл, Норман. «Как работают доказательства» . Домашняя страница Metamath Proof Explorer .
^ Мегилл, Норман. «Известные средства проверки доказательств Metamath» . Проверено 8 октября 2022 г.
^ Уиллер, Дэвид А. «Вклады в Metamath set.mm, просмотренные с помощью Gource до 4 октября 2019 г.» . Ютуб . Архивировано из оригинала 19 декабря 2021 г.
^ Мегилл, Норман. «Чтение предложений» . Метаматематика .
^ Лине, Фредерик. «Система метаматематики, основанная на естественной дедукции» . Архивировано из оригинала 28 декабря 2012 г.
^ Левиен, Раф. «Гилберт» .
^ Арпиайнен, Юха. «Представление Бурбаки» . Архивировано из оригинала 28 декабря 2012 г.
^ Клоостер, Марникс. «Презентация Хм» . Архивировано из оригинала 02 апреля 2012 г.
^ О'Кэт, Мел. «Презентация mmj2» . Архивировано из оригинала 19 декабря 2013 года.
^ Хейл, Уильям. «Презентация ммида» . Архивировано из оригинала 28 декабря 2012 г.

Внешние ссылки [ править ]

Метаматематика : официальный сайт.
Что математики думают о Метаматике : мнения о Метаматике.

[wikidata-7d32d1a3a149e85be2acb3831539d0106d3c08f6-v12-1] «Выпуск 0.198» . 8 августа 2021 г. Проверено 27 июля 2022 г.

[metamath-book-2] Мегилл, Норман; Уилер, Дэвид А. (2 июня 2019 г.). Метаматематика: компьютерный язык для математических доказательств (второе изд.). Моррисвилл, Северная Каролина, США: Lulu Press . п. 248. ИСБН 978-0-359-70223-7 .

[3] Мегилл, Норман. «Что такое Метаматия?» . Домашняя страница Метаматемы .

[4] Метаматематика 100.

[5] «Формализация 100 теорем» .

[6] Мегилл, Норман. «Известные средства проверки доказательств Metamath» . Проверено 8 октября 2022 г.

[7] «Содержание списка теорем — исследование метаматематических доказательств» . us.metamath.org . Проверено 4 сентября 2023 г.

[8] Видейк, Фрик. «Семнадцать искателей мира» (PDF) . стр. 103–105 . Проверено 14 октября 2023 г.

[howpswork-9] Мегилл, Норман. «Как работают доказательства» . Домашняя страница Metamath Proof Explorer .

[10] Мегилл, Норман. «Известные средства проверки доказательств Metamath» . Проверено 8 октября 2022 г.

[gource-11] Уиллер, Дэвид А. «Вклады в Metamath set.mm, просмотренные с помощью Gource до 4 октября 2019 г.» . Ютуб . Архивировано из оригинала 19 декабря 2021 г.

[reading-12] Мегилл, Норман. «Чтение предложений» . Метаматематика .

[natmm-13] Лине, Фредерик. «Система метаматематики, основанная на естественной дедукции» . Архивировано из оригинала 28 декабря 2012 г.

[ghilbert-14] Левиен, Раф. «Гилберт» .

[bourbaki-15] Арпиайнен, Юха. «Представление Бурбаки» . Архивировано из оригинала 28 декабря 2012 г.

[Hmm-16] Клоостер, Марникс. «Презентация Хм» . Архивировано из оригинала 02 апреля 2012 г.

[mmj2-17] О'Кэт, Мел. «Презентация mmj2» . Архивировано из оригинала 19 декабря 2013 года.

[mmide-18] Хейл, Уильям. «Презентация ммида» . Архивировано из оригинала 28 декабря 2012 г.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[11]

[12]

[13]

[14]

[15]

[16]

[17]

[18]