Metamatyka
 | |
| Deweloperzy | Normana Megilla |
|---|---|
| Pierwsze wydanie | 0,07 w czerwcu 2005 r |
| Wersja stabilna |  0,198 / 7 sierpnia 2021
|
| Magazyn | |
| Napisane w | ANSI C |
| System operacyjny | Linux , Windows , macOS |
| Typ | Sprawdzanie dowodu wspomagane komputerowo |
| Licencja | Powszechna Licencja Publiczna GNU ( Creative Commons Public Domain Dedication dla baz danych) |
| Strona internetowa | |
Metamath to formalny język i związany z nim program komputerowy ( weryfikator dowodów ) do archiwizacji, weryfikacji i badania dowodów matematycznych. Kilka baz danych udowodnionych twierdzeń zostało opracowanych przy użyciu Metamath, obejmujących między innymi standardowe wyniki w logice , teorii mnogości , teorii liczb , algebrze , topologii i analizie .
Od lutego 2022 r. Zbiór udowodnionych twierdzeń wykorzystujących Metamath jest jednym z największych zbiorów sformalizowanej matematyki, zawierającym w szczególności dowody 74 ze 100 twierdzeń wyzwania „Formalizacja 100 twierdzeń”, co daje mu czwarte miejsce po HOL Light , Isabelle i Coq , ale przed Mizarem , ProofPower , Lean , Nqthm , ACL2 i Nuprl . Istnieje co najmniej 19 weryfikatorów sprawdzających dla baz danych korzystających z formatu Metamath.
Projekt ten jest pierwszym tego rodzaju, który pozwala na interaktywne przeglądanie sformalizowanej bazy twierdzeń w formie zwykłej strony internetowej.
Język metamatyczny
Język Metamath jest metajęzykiem , odpowiednim do tworzenia szerokiej gamy systemów formalnych . Język Metamath nie ma w sobie żadnej określonej logiki. Zamiast tego można to po prostu uznać za sposób udowodnienia, że można zastosować reguły wnioskowania (potwierdzone jako aksjomaty lub udowodnione później). Największa baza danych udowodnionych twierdzeń jest zgodna z konwencjonalną ZFC i klasyczną logiką, ale istnieją inne bazy danych i można tworzyć inne.
Projekt języka Metamath koncentruje się na prostocie; język używany do formułowania definicji, aksjomatów, reguł wnioskowania i twierdzeń składa się tylko z kilku słów kluczowych, a wszystkie dowody są sprawdzane za pomocą jednego prostego algorytmu opartego na podstawieniu zmiennych (z opcjonalnymi zastrzeżeniami, które zmienne muszą pozostać odrębne po dokonaniu podstawienia).
Podstawy języka
Zestaw symboli, których można użyć do konstruowania formuł, jest deklarowany za pomocą instrukcji $c (symbole stałe) i $v (symbole zmienne); Na przykład:
$( Zadeklaruj symbole stałych, których będziemy używać $) $c 0 + = -> ( ) termin wff |- $. $( Zadeklaruj metazmienne, których będziemy używać $) $vtrs PQ $.
Gramatyka formuł jest określona za pomocą kombinacji instrukcji $f (hipotezy zmiennoprzecinkowe) i $a (twierdzenie aksjomatyczne); Na przykład:
$( Określ właściwości metazmiennych $) tt $f term t $. tr $f termin r $. ts $f termin s $. wp $f wff P $. wq $f wff Q $. $( Zdefiniuj "wff" (część 1) $) weq $a wff t = r $. $( Zdefiniuj "wff" (część 2) $) wim $a wff ( P -> Q ) $.
Aksjomaty i reguły wnioskowania są określone za pomocą instrukcji $a wraz z ${ i $} dla określania zakresu bloków i opcjonalnymi instrukcjami $e (zasadnicze hipotezy); Na przykład:
$( aksjomat stanu a1 $) a1 $a |- ( t = r -> ( t = s -> r = s ) ) $. $( aksjomat stanu a2 $) a2 $a |- ( t + 0 ) = t $. ${ min $e |- P $. maj $e |- ( P -> Q ) $. $( Zdefiniuj regułę wnioskowania modus ponens $) mp $a |- Q $. $}
Używanie jednej konstrukcji, instrukcji $a , do uchwycenia reguł składniowych, schematów aksjomatów i reguł wnioskowania ma zapewnić poziom elastyczności podobny do struktur logicznych wyższego rzędu bez zależności od złożonego systemu typów.
Dowody
Twierdzenia (i pochodne reguły wnioskowania) są zapisywane za pomocą instrukcji $p ; Na przykład:
$( Udowodnij twierdzenie $) th1 $p |- t = t $= $( Oto jego dowód: $) 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 $.
Zwróć uwagę na włączenie dowodu w instrukcji $p . Skrótuje następujący szczegółowy dowód:
0
0
0
tt $ f wyraz t tze $ wyraz 1,2 tpl $ wyraz ( t + ) 3,1 weq $ za wff ( t + ) = t 1,1 weq $ a wff t = t 1 a2 $ za | - ( t + ) = t 1,2 tpl $ _ 0
0
0
0
0
wyraz ( t + ) 7,1 weq $ a wff ( t + ) = t 1,2 tpl $ wyraz ( t + ) 9,1 weq $ a wff ( t + ) = t 1,1 weq $ a wff t = t 10,11 wim $ a wff ( _ _ 0
0
0
0 0 ( t + ) = t -> t = t ) 1 za2 $ za |- ( t + ) = t 1,2 tpl $ za wyraz ( t + ) 14,1,1 a1 $ za |- ( ( t + ) = t -> ( ( t + ) = t
0
-> t = t ) ) 8,12,13,15 mp $ za |- ( ( t + ) = t -> t = t ) 4,5,6,16 mp $ za |- t = t
„Istotna” forma dowodu pomija szczegóły składniowe, pozostawiając bardziej konwencjonalną prezentację:
0
0
0 0
za2 $ za |- ( t + ) = t za2 $ za |- ( t + ) = t za1 $ za |- ( ( t + ) = t -> ( ( t + ) = t -> t = t ) ) 2,3 mp $ za |- ( ( ( 0
t + ) = t -> t = t ) 1,4 mp $ za |- t = t
Podstawienie
Wszystkie etapy sprawdzania metamath używają jednej reguły podstawienia, która jest po prostu prostym zastąpieniem zmiennej wyrażeniem, a nie właściwym podstawieniem opisanym w pracach nad rachunkiem predykatów . Właściwe podstawienie w bazach danych Metamath, które je obsługują, jest konstruktem pochodnym, a nie wbudowanym w sam język Metamath.
Reguła podstawienia nie przyjmuje żadnych założeń dotyczących używanego systemu logicznego i wymaga jedynie prawidłowego wykonania podstawień zmiennych.
Oto szczegółowy przykład działania tego algorytmu. Kroki 1 i 2 twierdzenia 2p2e4 w Metamath Proof Explorer ( set.mm ) są przedstawione po lewej stronie. Wyjaśnijmy, w jaki sposób Metamath używa swojego algorytmu podstawienia, aby sprawdzić, czy krok 2 jest logiczną konsekwencją kroku 1, gdy używasz twierdzenia opreq2i . Krok 2 stwierdza, że (2 + 2) = (2 + (1 + 1)) . Jest to konkluzja twierdzenia opreq2i . Twierdzenie opreq2i mówi, że jeśli A = B , to ( CFA ) = ( CFB ) . To twierdzenie nigdy nie pojawiłoby się w podręczniku w tej tajemniczej formie, ale jego literackie sformułowanie jest banalne: kiedy dwie wielkości są równe, jedną można zastąpić drugą w operacji. Aby sprawdzić dowód, Metamath próbuje ujednolicić ( CFA ) = ( CFB ) z (2 + 2) = (2 + (1 + 1)) . Jest na to tylko jeden sposób: połączenie C z 2 , F z + , A z 2 i B z ( 1 + 1 ) . Więc teraz Metamath używa założenia opreq2i . Ta przesłanka stwierdza, że A = B . W wyniku wcześniejszych obliczeń Metamath wie, że A powinno zostać zastąpione przez 2 , a B przez (1 + 1) . Założenie A = B staje się 2=( 1 + 1 ) i dlatego generowany jest krok 1. Z kolei krok 1 jest ujednolicony z df-2 . df-2 jest definicją liczby 2 i stwierdza to 2 = ( 1 + 1 ) . Tutaj ujednolicenie jest po prostu kwestią stałych i jest proste (nie ma problemu z zastępowaniem zmiennych). Więc weryfikacja jest zakończona i te dwa kroki dowodu 2p2e4 są poprawne.
Kiedy Metamath ujednolica ( 2 + 2 ) z B, musi sprawdzić, czy przestrzegane są zasady składniowe. W rzeczywistości B ma klasę typu, więc Metamath musi sprawdzić, czy (2 + 2) jest również wpisaną klasą .
Sprawdzanie sprawdzające metamath
Program Metamath to oryginalny program stworzony do manipulowania bazami danych napisanymi przy użyciu języka Metamath. Ma interfejs tekstowy (wiersz poleceń) i jest napisany w C. Może wczytywać bazę danych Metamath do pamięci, weryfikować dowody bazy danych, modyfikować bazę danych (w szczególności dodając dowody) i zapisywać je z powrotem do pamięci.
Posiada polecenie dowodzenia , które umożliwia użytkownikom wprowadzenie dowodu, wraz z mechanizmami wyszukiwania istniejących dowodów.
Program Metamath może konwertować instrukcje na notację HTML lub TeX ; na przykład może wypisać modus ponens z set.mm jako:
Wiele innych programów może przetwarzać bazy danych Metamath, w szczególności istnieje co najmniej 19 weryfikatorów dowodów dla baz danych korzystających z formatu Metamath.
Bazy danych metamath
Witryna Metamath zawiera kilka baz danych, które przechowują twierdzenia pochodzące z różnych systemów aksjomatycznych. Większość baz danych ( .mm ) ma powiązany interfejs, zwany „Eksploratorem”, który umożliwia interaktywną nawigację po oświadczeniach i dowodach na stronie internetowej, w sposób przyjazny dla użytkownika. Większość baz danych korzysta z systemu dedukcji Hilberta, chociaż nie jest to wymagane.
Eksplorator dowodów metamatycznych
 Dowód Metamath Proof Explorer
| |
Rodzaj witryny |
Encyklopedia internetowa |
|---|---|
| Siedziba | USA |
| Właściciel | Normana Megilla |
| Stworzone przez | Normana Megilla |
| Adres URL | |
| Handlowy | NIE |
| Rejestracja | NIE |
Metamath Proof Explorer (zapisany w set.mm ) jest główną i zdecydowanie największą bazą danych, z ponad 23 000 dowodów w swojej głównej części według stanu na lipiec 2019 r. Opiera się na klasycznej logice pierwszego rzędu i teorii mnogości ZFC (z dodatkiem teorii mnogości Tarskiego-Grothendiecka w razie potrzeby, na przykład w teorii kategorii ). Baza danych prowadzona jest od ponad dwudziestu lat (pierwsze dowody w set.mm są datowane na sierpień 1993 r.). Baza danych zawiera między innymi opracowania teorii mnogości (liczby porządkowe i kardynalne, rekurencja, odpowiedniki aksjomatu wyboru, hipoteza continuum...), konstrukcji systemów liczb rzeczywistych i zespolonych, teorii rzędów, teorii grafów, algebry abstrakcyjnej, algebry liniowej, topologii ogólnej, analizy rzeczywistej i zespolonej, przestrzeni Hilberta, teorii liczb i elementarnej geometrii. Ta baza danych została po raz pierwszy utworzona przez Normana Megilla, ale na dzień 04.10.2019 było 48 współtwórców (w tym Norman Megill).
Metamath Proof Explorer odwołuje się do wielu podręczników, których można używać w połączeniu z Metamath. Dlatego osoby zainteresowane studiowaniem matematyki mogą korzystać z Metamath w połączeniu z tymi książkami i sprawdzać, czy udowodnione twierdzenia odpowiadają literaturze.
Intuicjonistyczny eksplorator logiki
Ta baza danych rozwija matematykę z konstruktywnego punktu widzenia, zaczynając od aksjomatów logiki intuicjonistycznej i kontynuując systemy aksjomatów konstruktywnej teorii mnogości .
Eksplorator nowych podstaw
teorii mnogości New Foundations Quine'a .
Eksplorator logiki wyższego rzędu
Ta baza danych zaczyna się od logiki wyższego rzędu i wyprowadza odpowiedniki aksjomatów logiki pierwszego rzędu i teorii mnogości ZFC.
Bazy danych bez eksploratorów
Witryna Metamath zawiera kilka innych baz danych, które nie są powiązane z odkrywcami, ale mimo to są godne uwagi. Baza danych peano.mm napisana przez Roberta Solovaya formalizuje arytmetykę Peano . Baza danych nat.mm formalizuje dedukcję naturalną . Baza danych miu.mm formalizuje układankę MU opartą na systemie formalnym MIU przedstawionym w Gödel, Escher, Bach .
Starsi odkrywcy
Witryna Metamath zawiera również kilka starszych baz danych, które nie są już utrzymywane, takich jak „Hilbert Space Explorer”, który przedstawia twierdzenia dotyczące teorii przestrzeni Hilberta , które zostały teraz połączone w Metamath Proof Explorer, oraz „Quantum Logic Explorer”, który rozwija logikę kwantową , zaczynając od teorii sieci ortomodularnych.
Dedukcja naturalna
Ponieważ Metamath ma bardzo ogólną koncepcję tego, czym jest dowód (mianowicie drzewo formuł połączonych regułami wnioskowania), a oprogramowanie nie zawiera żadnej konkretnej logiki, Metamath może być używany z tak różnymi gatunkami logiki, jak logika w stylu Hilberta lub logika oparta na sekwencjach, a nawet z rachunkiem lambda .
Jednak Metamath nie zapewnia bezpośredniego wsparcia dla naturalnych systemów dedukcyjnych. Jak wspomniano wcześniej, baza danych nat.mm formalizuje dedukcję naturalną. Metamath Proof Explorer (ze swoją bazą danych set.mm ) zamiast tego używa zestawu konwencji, które pozwalają na stosowanie metod naturalnej dedukcji w ramach logiki w stylu Hilberta.
Inne prace związane z Metamath
Warcaby dowodowe
Korzystając z pomysłów projektowych zaimplementowanych w Metamath, Raph Levien zaimplementował bardzo mały moduł sprawdzania poprawności, mmverify.py , zawierający zaledwie 500 wierszy kodu Pythona.
Ghilbert to podobny, choć bardziej rozbudowany język oparty na mmverify.py. Levien chciałby wdrożyć system, w którym kilka osób mogłoby współpracować, a jego praca kładzie nacisk na modułowość i połączenie między małymi teoriami.
Wykorzystując przełomowe prace Leviena, w wielu różnych językach wdrożono wiele innych implementacji zasad projektowania Metamath. Juha Arpiainen zaimplementował swój własny moduł sprawdzania poprawności w Common Lisp o nazwie Bourbaki, a Marnix Klooster zakodował moduł sprawdzania dowodów w Haskell o nazwie Hmm .
Chociaż wszyscy używają ogólnego podejścia Metamath do formalnego kodowania sprawdzającego system, wdrażają również własne nowe koncepcje.
Redaktorzy
Mel O'Cat zaprojektował system o nazwie Mmj2 , który zapewnia graficzny interfejs użytkownika do wprowadzania dowodów. Początkowym celem Mel O'Cat było umożliwienie użytkownikowi wprowadzenia dowodów poprzez proste wpisanie formuł i pozwolenie Mmj2 na znalezienie odpowiednich reguł wnioskowania, aby je połączyć. Natomiast w Metamath możesz wprowadzać tylko nazwy twierdzeń. Nie możesz wprowadzać formuł bezpośrednio. Mmj2 ma również możliwość wprowadzenia dowodu w przód lub w tył (Metamath pozwala tylko na wpisanie dowodu wstecz). Ponadto Mmj2 ma prawdziwy parser gramatyczny (w przeciwieństwie do Metamath). Ta różnica techniczna zapewnia użytkownikowi większy komfort. W szczególności Metamath czasami waha się między kilkoma analizowanymi formułami (większość z nich jest bezsensowna) i prosi użytkownika o wybór. W Mmj2 to ograniczenie już nie istnieje.
Istnieje również projekt Williama Hale'a mający na celu dodanie graficznego interfejsu użytkownika do Metamath o nazwie Mmide . Z kolei Paul Chapman pracuje nad nową przeglądarką dowodową, która ma podświetlanie, które pozwala zobaczyć odnośne twierdzenie przed i po dokonaniu podstawienia.
Milpgame to asystent sprawdzania i sprawdzania (pokazuje komunikat tylko, że coś poszło nie tak) z graficznym interfejsem użytkownika dla języka Metamath (set.mm), napisany przez Filipa Cernatescu, jest to aplikacja Java typu open source (licencja MIT) (aplikacja wieloplatformowa: Window, Linux, Mac OS). Użytkownik może wprowadzić demonstrację (dowód) w dwóch trybach: do przodu i do tyłu w stosunku do oświadczenia do udowodnienia. Milpgame sprawdza, czy zdanie jest dobrze sformułowane (posiada weryfikator składni). Może zapisywać niedokończone dowody bez użycia twierdzenia dummylink. Demonstracja jest pokazana jako drzewo, instrukcje są pokazane przy użyciu definicji html (zdefiniowanych w rozdziale dotyczącym składu). Milpgame jest dystrybuowany jako Java .jar (JRE wersja 6 aktualizacja 24 napisana w NetBeans IDE).
Zobacz też
Linki zewnętrzne
- Metamath : oficjalna strona internetowa.
- Co matematycy myślą o Metamath : opinie na temat Metamath.