Metamath

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

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

Језик Метамат

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

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

Основе језика

Скуп симбола који се могу користити за конструкцију формула декларише се помоћу израза $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 наводи да је Шаблон:Math. То је закључак теореме opreq2i. Теорема opreq2i наводи да ако је Шаблон:Math, онда је Шаблон:Math. Ова теорема се никада не би појавила у овом криптичном облику у уџбенику, али њена дословна формулација је банална: када су две величине једнаке, једна се може заменити другом у операцији. Да би проверио доказ, Метамат покушава да уједини Шаблон:Math са Шаблон:Math. Постоји само један начин да се то уради: уједињавањем Шаблон:Magenta са Шаблон:Magenta, Шаблон:Magenta са Шаблон:Math, Шаблон:Magenta са Шаблон:Val и Шаблон:Magenta са Шаблон:Math. Сада Метамат користи премису opreq2i. Ова премиса наводи да је Шаблон:Math. Као последица претходног прорачуна, Метамат зна да Шаблон:Magenta треба заменити са Шаблон:Val, а Шаблон:Magenta са Шаблон:Math. Премиса Шаблон:Math постаје Шаблон:Math и тако се генерише корак 1. Заузврат, корак 1 се уједињује са df-2. df-2 је дефиниција броја 2 и наводи да је 2 = ( 1 + 1 ). Овде је уједињење једноставно питање константи и праволинијско је (нема проблема са променљивима за супституцију). Тако је верификација завршена и ова два корака доказа 2p2e4 су тачна.

Када Метамат уједини Шаблон:Math са Шаблон:Magenta, мора да провери да ли су синтаксичка правила поштована. Заправо Шаблон:Magenta има тип class, па Метамат мора да провери да ли је и Шаблон:Math типа class.

Проверач доказа Метамат

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

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

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

$⊢\phi \mathrm{\&}⊢(\phi \to \psi )\Rightarrow ⊢\psi$

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

Базе података Метамат

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

Metamath Proof Explorer

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

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

Intuitionistic Logic Explorer

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

New Foundations Explorer

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

Higher-Order Logic Explorer

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

Базе података без explorer-а

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

Старији explorer-и

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

Природна дедукција

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

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

Други радови повезани с Метаматом

Проверачи доказа

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

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

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

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

Уређивачи

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

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

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

Види још

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

Спољашње везе

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