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

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.

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ą $\alpha$ jeśli $\alpha$ jest zawarte w częściach $x$ , a jeśli $y$ jest dowolną częścią $x$ zawsze występuje $z$ należące do $\alpha$ mającego części wspólne z częściami $y$ :

$$S{ = }_{ Df }\hat { x } \hat { \alpha } \{ \alpha \subset \vec { { P }^{ ‘ } } x:.(y):yPx.\supset .(\exists z).z\in \alpha .\vec { { P }^{ ‘ } } y\cap \vec { { P }^{ ‘ } } z\neq \Lambda \}$$

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 -

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!

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.

$\sf ZFC$$\sf\ ZFC$$\sf ZFC$

$\sf NBG$$\sf NBG$$\sf ZFC$$\sf NBG$$\sf ZFC$. 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.

$\sf 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.

$\sf NBG$

$\sf NBG$$\sf NBG$

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:

$\forall$$\forall$$\in$$\leftrightarrow$$\in$$\leftrightarrow$

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ę.

Kilka punktów:

1. $\in$$\cap, \subset$

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$