Jaki paradygmat automatycznego dowodzenia twierdzeń jest odpowiedni dla formalizacji w stylu Principia Mathematica?

11

Posiadam książkę, która zainspirowana Principia Mathematica (PM) Russella i logicznym pozytywizmem próbuje sformalizować konkretną dziedzinę, określając aksjomaty i wydając z nich twierdzenia. Krótko mówiąc, próbuje zrobić dla swojej dziedziny to, co PM próbował zrobić dla matematyki. Podobnie jak PM, został napisany, zanim możliwe było automatyczne udowodnienie twierdzenia (ATP).

Próbuję przedstawić te aksjomaty we współczesnym systemie ATP i staram się wydedukować twierdzenia, początkowo tezę wydedukowane przez autora (ręcznie). Nie korzystałem wcześniej z systemu ATP i biorąc pod uwagę mnóstwo opcji (HOL, Coq, Isabelle i wiele innych), każda z ich mocnymi i słabymi stronami oraz zamierzonymi zastosowaniami, trudno jest zdecydować, który jest odpowiedni dla mojej konkretnej cel, powód.

Formalizm autora ściśle odzwierciedla PM. Istnieją klasy (zestawy?), Klasy klas itd. Do 6 poziomów hierarchii. Istnieje logika pierwszego rzędu i prawdopodobnie wyższego rzędu. Biorąc pod uwagę związek z PM, początkowo badałem Metamath, ponieważ kilka twierdzeń o PM zostało udowodnionych w MetaMath przez innych ludzi. Jednak Metamath jest oczywiście weryfikatorem dowodów, a nie systemem ATP.

Przeglądając opisy różnych systemów ATP, dostrzegam kilka cech, takich jak implementacje teorii typów Kościoła, konstruktywne teorie typów, intuicyjne teorie typów, teoria zestawów typów / typów bez typu, dedukcja naturalna, typy rachunku lambda, polimorfizm, teoria funkcji rekurencyjnych oraz istnienie równości (lub nie). Krótko mówiąc, każdy system wydaje się implementować zupełnie inny język i musi być odpowiedni do formalizowania różnych rzeczy. Zakładam, że istniejące biblioteki do formalizowania matematyki nie są istotne dla mojego celu.

Wszelkie porady dotyczące cech, których powinienem szukać przy wyborze ATP, lub wszelkie inne porady, które możesz uzyskać po przeczytaniu tego pytania, byłyby bardzo mile widziane. W celach informacyjnych znajduje się przykładowa strona z książki. Niestety, podobnie jak PM, jest w notacji Peano-Russella.

Strona z książki

Książka -

„The Axiomatic Method in Biology” (1937), JH Woodger, A. Tarski, WF Floyd

Aksjomaty zaczynają się od zwykłego. Na przykład,

1.1.2 x jest sumą α jeśli α jest zawarte w częściach x , a jeśli y jest dowolną częścią x zawsze występuje z należące do α mającego części wspólne z częściami y :

S=Dfx^α^{αPx:.(y):yPx..(z).zα.PyPzΛ}

Ponownie zauważ, że jest to notacja Peano-Russella (notacja Principia).

Późniejsze aksjomaty mają zawartość biologiczną, taką jak:

7.4.2 Gdy gamety dwóch członków klasy mendlowskiej jednoczą się w pary, tworząc zygoty, prawdopodobieństwo zjednoczenia danej pary jest równe prawdopodobieństwu drugiej pary.

Z tego, co rozumiem, był to postulat genetyki Mendla.

Pomijam w tym celu notację, ponieważ ma ona trzy linie i opiera się na wcześniej zdefiniowanej treści.

Przykład twierdzenia -

Twierdzenie

To najwyraźniej ma sensowną interpretację w genezie mendlowskiej, czego, nie będąc historykiem biologii, nie rozumiem. W książce wydedukowano ją ręcznie.

Dzięki!

Atrija
źródło
Czy istnieje historyczne zainteresowanie dokładnym podążaniem za książką, czy może wystarczy wyciągnąć jej istotę (podstawowa konfiguracja i aksjomaty) i sformalizować teorię w dostępny nowoczesny system?
Andrej Bauer
@andrej: Tak, moim celem jest wyodrębnienie i sformalizowanie istoty w nowoczesnym systemie. Nie byłoby konieczne dedukowanie każdego twierdzenia wydanego ręcznie w książce. Byłoby raczej fajnie wydedukować twierdzenia, których nie ma w książce, na podstawie aksjomatów w książce.
Atriya
5
W takim przypadku powinieneś zrozumieć tekst, a następnie zrobić to w jakimkolwiek asystencie dowodowym i / lub dowodzie twierdzącym, który najlepiej pasuje do twojego celu.
Andrej Bauer,

Odpowiedzi:

8

Principia Mathematica była w dużej mierze odpowiedzią na różne paradoksy odkryte w logice matematycznej na przełomie XX i XXI wieku. Jednak sama praca, która często była ukośnie chwalona jako „nieczytelne arcydzieło”, jest nieco niezdarna i powstały bardziej nowoczesne fundamenty. Aby opisać większość matematyki, masz kilka możliwości: teoria kategorii jest jedna, teoria typów była popularna w niektórych projektach jako rozszerzenie rachunku lambda, ale najlepiej rozumiana i najbardziej fundamentalna jest prawdopodobnie teoria mnogości.

ZFC ZFCZFC

NBGNBGZFCNBGZFC. Moim zdaniem powodem, dla którego ta teoria jest najbardziej odpowiednia do automatycznego rozumowania, jest jej wyrazistość w logice pierwszego rzędu, która dopuszcza skuteczny, solidny i kompletny rachunek dowodowy, a skończona aksjatyzacja oznacza, że ​​można ją stosować z rozdzielczością pierwszego rzędu, która daje nam schludny wynik: jeśli orzeczenie jest rozstrzygalne, w końcu zostanie znaleziony dowód.

Logika zdań nie jest wystarczająco ekspresyjna, a logika wyższego rzędu, choć o wiele bardziej ekspresyjna, nie dopuszcza skutecznego, solidnego i pełnego rachunku dowodowego. Logika pierwszego rzędu z teorią zbiorów pozwala reprezentować i mapować teorie logiczne wyższego rzędu, więc dla podstaw jest to najsłodszy punkt ... z wyjątkiem możliwości nierozstrzygalnych instrukcji (dzięki Gödelowi), dlatego teorie pierwszego rzędu o wystarczającej randze kwantyfikatora są często określane jako częściowo rozstrzygalne.

NBG

Współcześni asystenci dowodowi są często mniej zainteresowani podstawami z paradygmatu Principia Mathematia i są bardziej przydatni w dowodzeniu twierdzeń w codziennej pracy, a więc mają pewne wsparcie dla fragmentów logiki wyższego rzędu, rozwiązywania SAT / SMT, teorii typów i innych podejścia bardziej nieformalne i mniej fundamentalne. Ale jeśli próbujesz zrobić coś takiego jak Principia Mathematica , najlepiej sprawdza się twierdzenie o rozstrzygnięciu pierwszego rzędu z całkowicie aksjomatyczną teorią zbiorów pierwszego rzędu.

NBG

NBGNBG

Zadaniem, które masz pod ręką, jeśli chcesz spróbować zdefiniować teorię w kategoriach teorii mnogości, jest znalezienie relacyjnych definicji predykatów, które są oddzielone od teorii mnogości, co pozwoli ci dokonać predykatów w kategoriach teorii mnogości. Ponownie, przykładem tego jest sposób definiowania arytmetyki Peano w teorii mnogości, która sama w sobie nie ma definicji liczb, dodawania, mnożenia, a nawet równości. Jako przykład zestawu teoretycznej definicji relacji takiej jak równość, możemy zdefiniować ją w kategoriach członkostwa jako takiego:

Spore ostrzeżenie: krzywa uczenia się w tym zakresie jest naprawdę bardzo stroma. Jeśli zamierzasz to kontynuować, możesz znaleźć się na kilka lat, zanim podejmiesz pełny problem, tak jak moje doświadczenie. Być może zechcesz zbadać teorię z mniej fundamentalnego podejścia, zanim podejmiesz ogromne zadanie osadzenia jej w podstawowym języku dla wszystkiego. W końcu niekoniecznie musisz myśleć o niezliczonych zestawach genów mieszających się.

dezakin
źródło
1
Wielkie dzięki za tę szczegółową i wyjaśniającą odpowiedź! Kilka pytań: 1. Wikipedia stwierdza, że ​​„Schemat zastępowania aksjomatów nie jest konieczny do udowodnienia większości twierdzeń zwykłej matematyki” i że nie był to jeden z oryginalnych aksjomatów Z (został dodany przez F). Czy to możliwe, że moje twierdzenia byłyby możliwe do udowodnienia bez tego, negując w ten sposób potrzebę NBG? Oczywiście, przypuszczam, że żaden automatyczny dowód do twierdzenia nie zezwalałby na użycie {ZFC - schemat zastępczy aksjomatu}, gdyby to w ogóle było możliwe?
Atriya,
2. Biorąc pod uwagę, że logika pierwszego rzędu + teoria zbiorów jest najlepsza dla fundacji, zakładam, że HOL / Isabelle / PVS / itp. (Wszystkie wyższego rzędu) są dla mnie zbyt nadmiarowe? Czy wszystko oparte na teorii typów (Coq i in.) Jest nieodpowiednie? W związku z tym, takie jak Prover9 / Vampire / SNARK byłyby odpowiednie? Mam pewne wcześniejsze doświadczenia z SNARK. Potrafi obsłużyć wielokrotnie posortowaną logikę pierwszego rzędu z jednakową rozdzielczością, ale nie jestem pewien, jak przedstawić w niej teorię zbiorów.
Atriya,
1
Zautomatyzowane dowody twierdzeń mogą wykorzystywać schematy aksjomatyczne, ale utrudniają ich implementację. Prover9 ich nie obsługuje. O ile pamiętam, HOL, Isabelle, Coq popierają teorię zbiorów pierwszego rzędu i prawdopodobnie są w porządku dla twojego projektu. Chociaż możesz osadzić inne teorie w NBG, nie jest to absolutnie konieczne. Nie musimy osadzać arytmetyki Peano w NBG, aby udowodnić rzeczy dotyczące liczb ... ale pomaga to w nauce i zrozumieniu logicznej struktury.
dezakin
Zawsze możesz później osadzić swoją teorię w teorii mnogości, definiując predykaty teorii w kategoriach predykatu członkostwa. Nie martwiłbym się, że Twój projekt będzie od razu absolutnie fundamentalny. Można to zrobić później.
dezakin
Wygląda więc na to, że praktycznie każdy prover - nawet tak różny jak Coq, HOL i Prover9 - może być użyty do mojego projektu. W takich przypadkach, jaka byłaby inteligentna strategia decyzyjna? Nie znam wszystkich oprócz SNARK. „Ideałem” jest odkrycie nowych twierdzeń w zapewnionym systemie aksjomatów.
Atriya,
8

Kilka punktów:

  1. ,

  2. Każdy nowoczesny interaktywny asystent dowodowy z pewnością będzie miał wyrazistość, aby sformalizować i udowodnić swoje oświadczenia, jak sugerował Andrej. W rzeczywistości, ponieważ wydaje się, że istnieją pewne stwierdzenia, w tym arytmetyka, rozsądnie byłoby zastosować system taki jak Isabelle , Coq lub HOL, które mają już obszerne teorie do traktowania wyrażeń arytmetycznych. Mój nacisk na nowoczesność nie jest zbiegiem okoliczności: od Automath poczyniono wielkie postępy w zakresie użyteczności i szczerze sądzę, że zrobiłbyś sobie krzywdę, wykorzystując wszystko, co nie zostało aktywnie rozwinięte od lat 90. (gdybyś mógł je zdobyć pracować!)

  3. LATEX

cody
źródło
Dzięki! Jest to rodzaj ogólnej porady, której szukałem. Oznaczenie tej odpowiedzi jako zaakceptowanej. W miarę postępu będę prawdopodobnie miał bardziej szczegółowe / techniczne pytania.
Atriya
Teoria zbiorów jest stworzona dla logiki pierwszego rzędu. Możesz zredukować całą matematykę do teorii pierwszego rzędu za pomocą tylko jednego predykatu: członkostwo. Stamtąd można konstruować definicje unii, przecięcia, podzbioru, właściwego podzbioru i innych relacji. Prover9 jest całkowicie odpowiedni.
dezakin
N
Prover9 często wykorzystuje ustalone konstrukcje liczb naturalnych. Sprawdź problemy teorii liczb i aksjomaty teorii liczb w TPTP. Definiują teorię liczb jako definicje teorii mnogości. Heurystyka wymagana przez ATP do udowodnienia twierdzenia o rozdzielczości jest właśnie tym, który klauzulę wybrać dla listy użytecznej podczas wyszukiwania pustej klauzuli, a teoria mnogości nie jest żadnym specjalnym wyjątkiem. Inne teorie są zdefiniowane w teorii mnogości przez relacyjne predykaty.
dezakin