Метамат

Програмер(и)	Норман Мегил
Прво издање	0.07 у јун 2005; пре 21 године (2005-06)
Стабилно издање	0.198  / 7 август 2021
Репозиторијум	github.com/metamath/metamath-exe
Написан у	ANSI C
Оперативни систем	Линукс, Виндоус, macOS
Тип	Проверавање доказа уз помоћ рачунара
Лиценца	ГНУ-ова општа јавна лиценца (Кријејтив комонс Посвета јавном власништву за базе података)
Веб-сајт	us.metamath.org

Метамат (енгл. Metamath) јесте формални језик и придружени рачунарски програм (асистент за доказивање) за архивирање и верификацију математичких доказа.^[1] Развијено је неколико база података доказаних теорема помоћу Метамата, које покривају стандардне резултате у логици, теорији скупова, теорији бројева, алгебри, топологији и анализи, између осталог.^[2]

До 2023. године, Метамат је коришћен за доказивање 74^[3] од 100 теорема из изазова „Формализовање 100 теорема” (енгл. Formalizing 100 Theorems).^[4] Најмање 19 проверавача доказа користи Метамат формат.^[5] Веб-сајт Метамата пружа базу података формализованих теорема које се могу интерактивно прегледати.^[6]

Језик Метамат је метајезик за формалне системе. Језик Метамат нема уграђену специфичну логику. Уместо тога, може се сматрати начином доказивања да се правила закључивања (наведена као аксиоме или касније доказана) могу применити. Највећа база података доказаних теорема прати конвенционалну логику првог реда и ЗФЦ теорију скупова.^[7]

Дизајн језика Метамат (који се користи за навођење дефиниција, аксиома, правила закључивања и теорема) фокусиран је на једноставност. Докази се проверавају помоћу алгоритма заснованог на супституцији променљивих. Алгоритам такође има опционе услове о томе које променљиве морају остати различите након извршене супституције.^[8]

Скуп симбола који се могу користити за конструкцију формула декларише се помоћу израза $c (константни симболи) и $v (променљиви симболи); на пример:

$( Декларишемо константне симболе које ћемо користити $)
    $c 0 + = -> ( ) term wff |- $.
$( Декларишемо метапроменљиве које ћемо користити $)
    $v t r s P Q $.

Граматика за формуле се специфицира комбинацијом израза $f (хипотезе променљивог типа) и $a (аксиоматске тврдње); на пример:

$( Специфицирамо својства метапроменљивих $)
    tt $f term t $.
    tr $f term 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 (суштинске хипотезе); на пример:

$( Наводимо аксиом а1 $)
    a1 $a |- ( t = r -> ( t = s -> r = s ) ) $.
$( Наводимо аксиом а2 $)
    a2 $a |- ( t + 0 ) = t $.
    ${
       min $e |- P $.
       maj $e |- ( P -> Q ) $.
$( Дефинишемо правило закључивања модус поненс $)
       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
       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

Сви кораци доказа у Метамату користе једно правило супституције, што је само једноставна замена променљиве изразом, а не права супституција описана у радовима о предикатском рачуну. Права супституција, у базама података Метамата које је подржавају, је изведени конструкт, а не онај уграђен у сам језик Метамат.

Правило супституције не претпоставља ништа о логичком систему који се користи и захтева само да су супституције променљивих исправно извршене.

Ево детаљног примера како овај алгоритам функционише. Кораци 1 и 2 теореме 2p2e4 у Metamath Proof Explorer-у (set.mm) приказани су лево. Објаснимо како Метамат користи свој алгоритам супституције да провери да ли је корак 2 логична последица корака 1 када користите теорему opreq2i. Корак 2 наводи да је ( 2 + 2 ) = ( 2 + ( 1 + 1 ) ). То је закључак теореме opreq2i. Теорема opreq2i наводи да ако је A = B, онда је (C F A) = (C F B). Ова теорема се никада не би појавила у овом криптичном облику у уџбенику, али њена дословна формулација је банална: када су две величине једнаке, једна се може заменити другом у операцији. Да би проверио доказ, Метамат покушава да уједини (C F A) = (C F B) са ( 2 + 2 ) = ( 2 + ( 1 + 1 ) ). Постоји само један начин да се то уради: уједињавањем C са 2, F са +, A са 7000200000000000000♠2 и B са ( 1 + 1 ). Сада Метамат користи премису opreq2i. Ова премиса наводи да је A = B. Као последица претходног прорачуна, Метамат зна да A треба заменити са 7000200000000000000♠2, а B са ( 1 + 1 ). Премиса A = B постаје 2=( 1 + 1 ) и тако се генерише корак 1. Заузврат, корак 1 се уједињује са df-2. df-2 је дефиниција броја 2 и наводи да је 2 = ( 1 + 1 ). Овде је уједињење једноставно питање константи и праволинијско је (нема проблема са променљивима за супституцију). Тако је верификација завршена и ова два корака доказа 2p2e4 су тачна.

Када Метамат уједини ( 2 + 2 ) са B, мора да провери да ли су синтаксичка правила поштована. Заправо B има тип class, па Метамат мора да провери да ли је и ( 2 + 2 ) типа class.

Програм Метамат је оригинални програм креиран за манипулацију базама података написаним помоћу језика Метамат. Има текстуални (командна линија) интерфејс и написан је у језику C. Може да учита базу података Метамат у меморију, верификује доказе базе података, модификује базу података (посебно додавањем доказа) и поново их упише у складиште.

Има команду prove која омогућава корисницима да унесу доказ, заједно са механизмима за претрагу постојећих доказа.

Програм Метамат може да конвертује изјаве у HTML или TeX нотацију; на пример, може да избаци аксиом модус поненса из set.mm као:

${\displaystyle \vdash \varphi \quad \&\quad \vdash (\varphi \rightarrow \psi )\quad \Rightarrow \quad \vdash \psi }$

Многи други програми могу да обрађују базе података Метамат, а посебно постоји најмање 19 проверавача доказа за базе података које користе Метамат формат.^[9]

Веб-сајт Метамат хостује неколико база података које чувају теореме изведене из различитих аксиоматских система. Већина база података (датотеке .mm) има придружени интерфејс, назван „Explorer”, који омогућава интерактивно кретање кроз изјаве и доказе на веб-сајту, на начин прилагођен кориснику. Већина база података користи Хилбертов систем формалне дедукције, иако то није услов.

Metamath Proof Explorer
Доказ из Metamath Proof Explorer-а
Веб-адреса	us.metamath.org/mpeuni/avril1.html
Комерцијалност	Не
Тип	Онлајн енциклопедија
Регистрација	Не
Власник	Норман Мегил
Творац	Норман Мегил

Metamath Proof Explorer (забележен у set.mm) је главна база података. Заснован је на класичној логици првог реда и ЗФЦ теорији скупова (са додатком теорије скупова Тарски-Гротендик када је то потребно, на пример у теорији категорија). База података се одржава више од тридесет година (први докази у set.mm датирају из септембра 1992. године). База података садржи развоје, између осталих области, теорије скупова (ординали и кардинали, рекурзија, еквиваленти аксиоме избора, хипотеза континуума...), конструкцију система реалних и комплексних бројева, теорију поретка, теорију графова, апстрактну алгебру, линеарну алгебру, општу топологију, реалну и комплексну анализу, Хилбертове просторе, теорију бројева и елементарну геометрију.^[10]

Metamath Proof Explorer референцира многе уџбенике који се могу користити у комбинацији са Метаматом.^[11] Тако, људи заинтересовани за проучавање математике могу користити Метамат у вези са овим књигама и проверити да ли се доказане тврдње подударају са литературом.

Ова база података развија математику са конструктивистичке тачке гледишта, почевши од аксиома интуиционистичке логике и настављајући са аксиоматским системима конструктивистичке теорије скупова.

Ова база података развија математику из Квајнове (Quine) теорије скупова Нове основе.

Ова база података почиње са логиком вишег реда и изводи еквиваленте аксиома логике првог реда и ЗФЦ теорије скупова.

Веб-сајт Метамат хостује неколико других база података које нису повезане са explorer-има, али су ипак вредне пажње. База података peano.mm коју је написао Роберт Соловеј формализује Пеанову аритметику. База података nat.mm^[12] формализује природну дедукцију. База података miu.mm формализује МУ загонетку засновану на формалном систему МИУ представљеном у књизи Гедел, Ешер, Бах.

Веб-сајт Метамат такође хостује неколико старијих база података које се више не одржавају, као што је „Hilbert Space Explorer”, који представља теореме које се односе на теорију Хилбертовог простора, а које су сада спојене у Metamath Proof Explorer, и „Quantum Logic Explorer”, који развија квантну логику почевши од теорије ортомодуларних решетки.

Пошто Метамат има веома генерички концепт онога што је доказ (наиме, стабло формула повезаних правилима закључивања) и у софтвер није уграђена никаква специфична логика, Метамат се може користити са врстама логике различитим као што су логике Хилбертовог стила или логике засноване на секвентима, па чак и са ламбда рачуном.

Међутим, Метамат не пружа директну подршку за системе природне дедукције. Као што је раније напоменуто, база података nat.mm формализује природну дедукцију. Metamath Proof Explorer (са својом базом података set.mm) уместо тога користи скуп конвенција које омогућавају употребу приступа природне дедукције унутар логике Хилбертовог стила.

Користећи дизајнерске идеје имплементиране у Метамату, Раф Левин је имплементирао веома мали проверач доказа, mmverify.py, са само 500 линија Пајтон кода.

Ghilbert је сличан, иако разрађенији језик заснован на mmverify.py.^[13] Левин би желео да имплементира систем у којем би неколико људи могло да сарађује, а његов рад наглашава модуларност и везу између малих теорија.

Користећи Левинов семени рад, многе друге имплементације дизајнерских принципа Метамата су имплементиране за широк спектар језика. Јуха Арпијаинен је имплементирао сопствени проверач доказа у Common Lisp-у назван Bourbaki^[14], а Марникс Клостер је кодирао проверач доказа у Хаскелу назван Hmm.^[15]

Иако сви користе целокупни приступ Метамата кодирању проверача формалних система, они такође имплементирају нове сопствене концепте.

Мел О'Кет је дизајнирао систем назван Mmj2, који пружа графички кориснички интерфејс за унос доказа.^[16] Првобитни циљ Мел О'Кета био је да омогући кориснику да уноси доказе једноставним куцањем формула и пуштањем Mmj2 да пронађе одговарајућа правила закључивања како би их повезао. У Метамату, напротив, можете уносити само имена теорема. Не можете директно уносити формуле. Mmj2 такође има могућност уноса доказа унапред или уназад (Метамат омогућава само унос доказа уназад). Штавише, Mmj2 има прави граматички парсер (за разлику од Метамата). Ова техничка разлика доноси већу удобност кориснику. Конкретно, Метамат се понекад двоуми између неколико формула које анализира (већина њих је бесмислена) и тражи од корисника да изабере. У Mmj2 ово ограничење више не постоји.

Постоји и пројекат Вилијама Хејла за додавање графичког корисничког интерфејса Метамату назван Mmide.^[17] Пол Чепман заузврат ради на новом прегледачу доказа, који има истицање које вам омогућава да видите референцирану теорему пре и после извршене супституције.

Milpgame је асистент за доказивање и проверач (приказује поруку само ако нешто пође по злу) са графичким корисничким интерфејсом за језик Метамат (set.mm), написан од стране Филипа Чернатескуа. То је апликација отвореног кода (МИТ лиценца) написана у Јави (крос-платформска апликација: Виндоус, Линукс, Мек ОС). Корисник може унети демонстрацију (доказ) у два режима: унапред и уназад у односу на изјаву коју треба доказати. Milpgame проверава да ли је изјава добро формирана (има синтаксички верификатор). Може да сачува недовршене доказе без употребе dummylink теореме. Демонстрација се приказује као стабло, изјаве се приказују помоћу html дефиниција (дефинисаних у поглављу о слагању). Milpgame се дистрибуира као Јава .jar (JRE верзија 6 ажурирање 24 написано у NetBeans IDE).

• Аутоматско доказивање теорема
• Доказ уз помоћ рачунара
• Асистент за доказивање

• Metamath: званични веб-сајт.
• Шта математичари мисле о Метамату: мишљења о Метамату.