Metamath - Metamath

Metamath Proof Explorer
	Důkaz Metamath Proof Explorer
Typ webu	Online encyklopedie
Sídlo společnosti	USA
Majitel	Norman Megill
Vytvořil	Norman Megill
URL	us .metamath .org /mpeuni /mmset .html
Komerční	Ne
Registrace	Ne

Metamath
Vývojáři	Norman Megill
Úložiště
Napsáno	ANSI C.
Operační systém	Linux , Windows , macOS
Typ	Kontrola pomocí počítače
Licence	GNU General Public License ( Public Commain Dedication pro databáze Creative Commons )
webová stránka	metamath .org

Metamath je formální jazyk a související počítačový program ( kontrola důkazů ) pro archivaci, ověřování a studium matematických důkazů. Pomocí Metamathu bylo vyvinuto několik databází prokázaných vět, které pokrývají standardní výsledky mimo jiné z logiky , teorie množin , teorie čísel , algebry , topologie a analýzy .

V prosinci 2020 je soubor prokázaných vět pomocí Metamathu jedním z největších těles formalizované matematiky, který obsahuje zejména důkazy o 74 ze 100 teorémů výzvy „Formalizace 100 vět “ , čímž se stal třetím po HOL Light a Isabelle , ale před Coq , Mizar , ProofPower , Lean , Nqthm , ACL2 a Nuprl . Pro databáze používající formát Metamath existuje nejméně 17 ověřovatelů důkazů.

Tento projekt je první svého druhu, který umožňuje interaktivní procházení jeho formalizované databáze teorémů ve formě běžné webové stránky.

Jazyk Metamath

Jazyk Metamath je metajazyk , vhodný pro vývoj široké škály formálních systémů . Jazyk Metamath v sobě nemá žádnou konkrétní logiku. Místo toho lze jednoduše považovat za způsob, jak dokázat, že lze použít odvozovací pravidla (tvrdená jako axiomy nebo prokázaná později). Největší databáze osvědčených vět se řídí konvenční teorií množin ZFC a klasickou logikou, ale existují i jiné databáze a lze vytvořit další.

Jazykový design Metamath je zaměřen na jednoduchost; jazyk používaný k určení definic, axiomů, odvozovacích pravidel a vět se skládá pouze z několika klíčových slov a všechny důkazy se kontrolují pomocí jednoho jednoduchého algoritmu založeného na nahrazení proměnných (s volitelnými ustanoveními, pro které proměnné musí zůstat odlišné po provedení střídání).

Jazykové základy

Sada symbolů, které lze použít pro konstrukci vzorců, je deklarována pomocí příkazů $c(konstantní symboly) a $v(variabilní symboly); například:

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

Gramatika pro vzorce je specifikována kombinací příkazů $f(plovoucí (proměnný typ) hypotéz) a $a(axiomatické tvrzení); například:

$( 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 ) $.

Axiomy a odvozovací pravidla jsou uvedeny na $aprohlášení spolu s ${i $}s blokovou stanovení rozsahu a nepovinných $e(základních hypotéz) závěrce; například:

$( 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 $.
    $}

Použití jedné konstrukce, $apříkazů k zachycení syntaktických pravidel, schémat axiomů a odvozovacích pravidel má zajistit úroveň flexibility podobnou logickým rámcům vyššího řádu bez závislosti na systému komplexního typu.

Důkazy

Věty (a odvozená pravidla odvozování) jsou psány s $ppříkazy; například:

$( 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
     $.

Všimněte si zahrnutí důkazu do $pprohlášení. Zkracuje následující podrobný důkaz:

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

„Základní“ forma důkazu eliduje syntaktické detaily a zanechává konvenčnější prezentaci:

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

Střídání

Důkaz krok za krokem

Všechny kroky důkazu Metamathu používají jediné substituční pravidlo, které je pouze jednoduchým nahrazením proměnné výrazem, a nikoli správnou substitucí popsanou v pracích na predikátovém počtu . Správná náhrada v databázích Metamath, které ji podporují, je odvozený konstrukt místo jednoho zabudovaného do samotného jazyka Metamath.

Pravidlo nahrazování nevytváří žádný předpoklad o používaném logickém systému a vyžaduje pouze správné nahrazení proměnných.

Zde je podrobný příklad toho, jak tento algoritmus funguje. Kroky 1 a 2 věty 2p2e4v Metamath Proof Explorer ( set.mm ) jsou znázorněny vlevo. Vysvětlíme, jak Metamath používá svůj substituční algoritmus ke kontrole, že krok 2 je logickým důsledkem kroku 1, když použijete větu opreq2i. Krok 2 uvádí, že $(2 + 2) = (2 + (1 + 1))$ . Je to závěr věty opreq2i. Věta opreq2iříká, že pokud $A = B$ , pak $(CFA) = (CFB)$ . Tato věta by se pod touto záhadnou formou v učebnici nikdy neobjevila, ale její gramotná formulace je banální: když jsou dvě veličiny stejné, lze jednu při operaci nahradit druhou. Chcete -li zkontrolovat důkaz, Metamath se pokusí sjednotit $(CFA) = (CFB)$ s $(2 + 2) = (2 + (1 + 1))$ . Existuje pouze jeden způsob, jak to udělat: sjednocení $C$ s $2$ , $F$ s $+$ , $A$ s2 a $B$ s $(1 + 1)$ . Metamath nyní používá premisu opreq2i. Tento předpoklad se uvádí, že $A = B$ . V důsledku svého předchozího výpočtu Metamath ví, že $A$ by mělo být nahrazeno2 a $B$ o $(1 + 1)$ . Předpoklad $A = B se$ stává $2 = (1 + 1),$ a proto je generován krok 1. Na druhé straně je krok 1 sjednocen s df-2. df-2je definice čísla 2a uvádí to 2 = ( 1 + 1 ). Zde je sjednocení jednoduše otázkou konstant a je jednoduché (žádný problém proměnných, které je třeba nahradit). Ověření je tedy dokončeno a tyto dva kroky důkazu 2p2e4jsou správné.

Když Metamath sjednocuje $(2 + 2)$ s $B$ , musí zkontrolovat, zda jsou respektována syntaktická pravidla. Ve skutečnosti má $B$ typ, classtakže Metamath musí zkontrolovat, zda je také napsáno $(2 + 2)$ class .

Kontrola důkazu Metamath

Program Metamath je původní program vytvořený pro manipulaci s databázemi napsanými pomocí jazyka Metamath. Má textové rozhraní (příkazový řádek) a je napsán v jazyce C. Dokáže načíst databázi Metamath do paměti, ověřit korektury databáze, upravit databázi (zejména přidáním důkazů) a zapsat je zpět do úložiště.

Má příkaz dokázat, který umožňuje uživatelům zadat důkaz spolu s mechanismy pro vyhledávání existujících důkazů.

Program Metamath dokáže převádět příkazy na notaci HTML nebo TeX ; například může vygenerovat modus ponens axiom ze souboru set.mm jako:

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

Mnoho dalších programů může zpracovávat databáze Metamath, zejména existuje nejméně 17 ověřovatelů pro databáze, které používají formát Metamath.

Databáze Metamath

Web Metamath hostí několik databází, které ukládají věty odvozené z různých axiomatických systémů. Většina databází ( soubory .mm ) má přidružené rozhraní, které se nazývá „Průzkumník“ a které umožňuje uživateli interaktivně procházet prohlášeními a důkazy na webových stránkách. Většina databází používá Hilbertův systém formálního odpočtu, i když to není podmínkou.

Metamath Proof Explorer

Metamath Proof Explorer (zaznamenaný v souboru set.mm ) je hlavní a zdaleka největší databází s více než 23 000 důkazy v jeho hlavní části k červenci 2019. Je založen na klasické logice prvního řádu a teorii množin ZFC (s v případě potřeby doplnění teorie množin Tarski-Grothendieck , například v teorii kategorií ). Databáze byla udržována více než dvacet let (první důkazy v souboru set.mm jsou ze srpna 1993). Databáze obsahuje mimo jiné vývoj teorie množin (ordinály a kardinály, rekurze, ekvivalenty axiomu volby, hypotéza kontinua ...), konstrukci reálných a komplexních číselných systémů, teorii řádu, teorii grafů, abstraktní algebra, lineární algebra, obecná topologie, reálná a komplexní analýza, Hilbertovy prostory, teorie čísel a elementární geometrie. Tuto databázi nejprve vytvořil Norman Megill, ale od 10. 10. 2019 tam bylo 48 přispěvatelů (včetně Normana Megilla).

Metamath Proof Explorer odkazuje na mnoho učebnic, které lze použít ve spojení s Metamath. Lidé se zájmem o studium matematiky tedy mohou v souvislosti s těmito knihami použít Metamath a ověřit si, že prokázaná tvrzení odpovídají literatuře.

Intuitionistic Logic Explorer

Tato databáze rozvíjí matematiku z konstruktivního hlediska, počínaje axiomy intuicionistické logiky a pokračujícími axiomovými systémy konstruktivní teorie množin .

Nový Průzkumník základů

Tato databáze rozvíjí matematiku z teorie množin Quine's New Foundations .

Průzkumník logiky vyššího řádu

Tato databáze začíná logikou vyššího řádu a odvozuje ekvivalenty axiomů logiky prvního řádu a teorie množin ZFC.

Databáze bez průzkumníků

Web Metamath hostí několik dalších databází, které nejsou spojeny s průzkumníky, ale přesto stojí za zmínku. Databáze peano.mm napsaná Robertem Solovayem formalizuje aritmetiku Peano . Databáze nat.mm formalizuje přirozený odpočet . Databáze miu.mm formalizuje hádanku MU na základě formálního systému MIU uvedeného v Gödel, Escher, Bach .

Starší průzkumníci

Web Metamath také hostí několik starších databází, které již nejsou udržovány, jako například „Hilbert Space Explorer“, který představuje věty týkající se Hilbertovy vesmírné teorie, které byly nyní sloučeny do Metamath Proof Explorer, a „Quantum Logic Explorer“ , která rozvíjí kvantovou logiku počínaje teorií ortomodulárních mřížek.

Přirozená dedukce

Protože Metamath má velmi obecný koncept toho, co je důkaz (konkrétně strom vzorců propojených odvozovacími pravidly) a v softwaru není vložena žádná konkrétní logika, lze Metamath použít s různými druhy logiky, které se liší od logiky nebo sekvencí ve stylu Hilberta -založená logika nebo dokonce s lambda kalkulem .

Metamath však neposkytuje žádnou přímou podporu pro systémy přirozeného odpočtu . Jak již bylo uvedeno dříve, databáze nat.mm formalizuje přirozený odpočet. Metamath Proof Explorer (s databází set.mm ) místo toho používá sadu konvencí, které umožňují použití přístupů přirozené dedukce v logice ve stylu Hilberta.

Další díla spojená s Metamathem

Důkaz dáma

Pomocí návrhových nápadů implementovaných v Metamathu implementoval Raph Levien velmi malou kontrolu důkazů, mmverify.py , pouze na 500 řádcích kódu Pythonu.

Ghilbert je podobný, i když propracovanější jazyk založený na mmverify.py. Levien by chtěl implementovat systém, kde by mohlo spolupracovat několik lidí a jeho práce klade důraz na modularitu a propojení mezi malými teoriemi.

Pomocí klíčových prací Levien bylo implementováno mnoho dalších implementací principů návrhu Metamath pro širokou škálu jazyků. Juha Arpiainen implementoval ve Common Lispu vlastní kontrolní kontrolu s názvem Bourbaki a Marnix Klooster zakódoval v Haskellu kontrolní kontrolu s názvem Hmm .

Přestože všichni používají celkový přístup Metamath k formálnímu kódování kontroly systému, implementují také vlastní nové koncepty.

Redaktoři

Mel O'Cat navrhl systém nazvaný Mmj2 , který poskytuje grafické uživatelské rozhraní pro zadávání důkazů. Počátečním cílem Mel O'Cat bylo umožnit uživateli zadávat důkazy jednoduchým zadáním vzorců a nechat Mmj2 najít příslušná odvozovací pravidla pro jejich připojení. V Metamathu naopak můžete zadávat pouze názvy vět. Vzorce nesmíte zadávat přímo. Mmj2 má také možnost zadat důkaz dopředu nebo dozadu (Metamath umožňuje pouze zadat důkaz zpět). Kromě toho má Mmj2 skutečný analyzátor gramatiky (na rozdíl od Metamathu). Tento technický rozdíl přináší uživateli větší pohodlí. Zejména Metamath někdy váhá mezi několika vzorci, které analyzuje (většina z nich je bezvýznamná) a žádá uživatele, aby si vybral. V Mmj2 toto omezení již neexistuje.

Existuje také projekt Williama Halea na přidání grafického uživatelského rozhraní do Metamathu s názvem Mmide . Paul Chapman zase pracuje na novém korektním prohlížeči, který má zvýraznění, které vám umožní vidět odkazovanou větu před a po provedení substituce.

Milpgame je korektní asistent a kontrola (zobrazuje zprávu, jen se něco pokazilo) s grafickým uživatelským rozhraním pro jazyk Metamath (set.mm), které napsal Filip Cernatescu, je to open source (licence MIT) Java aplikace ( multiplatformní aplikace: Window, Linux, Mac OS). Uživatel může zadat ukázku (důkaz) ve dvou režimech: dopředu a dozadu vzhledem k prohlášení, které má dokázat. Milpgame zkontroluje, zda je příkaz dobře formulován (má syntaktický ověřovač). Může uložit nedokončené důkazy bez použití dummylinkové věty. Demonstrace je zobrazena jako strom, příkazy jsou zobrazeny pomocí definic html (definovaných v kapitole sazby). Milpgame je distribuován jako Java .jar (JRE verze 6 aktualizace 24 napsaná v NetBeans IDE).

Viz také

Reference

externí odkazy

Metamath : oficiální webové stránky.
Co si o Metamathu myslí matematici : názory na Metamatha.

Languages

In other projects