Dowód asystent do pisania matematyki

12

Chciałbym pisać matematyczne dowody przy pomocy asystenta dowodu. Wszystko zostanie napisane przy użyciu logiki pierwszego rzędu (z równością) i naturalnej dedukcji. Tłem jest teoria mnogości (ZF). Na przykład, jak mogę napisać następujący dowód?

Aksjomat:∀x∀y(x=y↔∀z(z∈x↔z∈y))

Twierdzenie:∀x∀y(∀z(z∉x)∧∀z(z∉y)→x=y)

Oznacza to, że pusty zestaw jest unikalny.

Używanie papieru i długopisu jest dla mnie trywialne, ale tak naprawdę potrzebuję oprogramowania, które pomoże mi w sprawdzeniu poprawności.

Dziękuję Ci.

lo.logic software proof-assistants Kaveh
źródło
11
Najpierw musisz wybrać asystenta dowodu. Używam Coq , ale jest wiele innych . Niektóre z nich są oparte na logice pierwszego rzędu, więc będą lepiej dopasowane do twoich potrzeb. Następnie musisz zobowiązać się do nauki asystenta dowodu. W ciągu kilku dni powinieneś być w stanie zakodować proste twierdzenia, takie jak powyższe, i je udowodnić. Nie oczekuj, że zrobimy to za Ciebie. Nic się nie nauczysz w ten sposób.
Dave Clarke
5
Jeśli interesuje Cię teoria mnogości, a nie teoria typów, to Isabelle jest prawdopodobnie najprostszym systemem. Coq będzie wydawał się dziwny i zagmatwany.
Mark Reitblatt
2
Myślę, że aksjomat, który napisałeś, nie jest logiką pierwszego rzędu, ale logiką drugiego rzędu. Jest tak, ponieważ w pierwszym przypadku zmienne obejmują tylko jednostki, podczas gdy w drugim zmienne mogą obejmować zarówno jednostki, jak i zbiory. Wydaje się, że w danym aksjomatyce, i są zestawy, a jest indywidualne. y zxyz
MS Dousti
9
@Sadeq: W ZF i tak nie są podstawowe elementy wszechświata? Powinieneś być w stanie powiedzieć rzeczy takie jak „dla wszystkich zbiorów” w logice pierwszego rzędu, co dzieje się w tym aksjomacie.
Robin Kothari
9
@Sadeq, to, co powiedział Robin, jest poprawne, jest teorią pierwszego rzędu, a aksjomat zapisany w pytaniu jest również pierwszym rzędem. W wszystko jest tylko zbiorem, nie ma nic jako jednostek vs. zestawów. (Na marginesie, nie trzeba przechodzić do obiektów drugiego lub wyższego rzędu, aby rozmawiać o różnych rodzajach zmiennych, potrzebne są tylko różne rodzaje, logika drugiego i wyższego rzędu jest zupełnie inna niż logika wielu sortowań). Z FZFZF
Kaveh

Odpowiedzi:

13

Zarówno Coq, jak i Isabelle mogą to zrobić.

[Coq] Oto artykuł omawiający sposób kodowania ZFC w CIC, na którym oparty jest Coq.

Benjamin Werner: Zestawy w typach, Typy w zestawach (1997). http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.55.1709

[Isabelle] Jest biblioteka dla ZF.

http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/library/ZF/index.html

yhirai
źródło
3
Chociaż ten artykuł jest całkiem fajny, myślę, że bardziej pragmatyczne byłoby po prostu dodanie gatunków (zmiennych typu) i aksjomatów, aby bezpośrednio zakodować aksjomatyczną teorię ZF, a następnie wykonać dowody bezpośrednio odwołując się do tych aksjomatów. Kodowanie ma raczej na celu pokazanie, że teorie są powiązane siłą ekspresji.
cody
2
Powinienem dodać, że realizacja tych pomysłów została wykonana
cody
9

Przeniesiono z komentarza na sugestię Kaveha

Najpierw musisz wybrać asystenta dowodu. Używam Coq , ale jest wiele innych . Coq opiera się na logice wyższego rzędu (tak zwany rachunek konstrukcji indukcyjnych). Inni asystenci ds. Dowodu opierają się na logice pierwszego rzędu, więc mogą być bardziej dostosowane do twoich potrzeb (modulo komentarze powyżej).

Następnie musisz zobowiązać się do nauki asystenta dowodu. Powiązany dokument to samouczek, jak zdobyć znajomość z Coq. Zostanie ekspertem Coq wymaga lat poświęcenia i praktyki, ale proste twierdzenia można udowodnić po południu. Kluczem do nauki Coq lub innego asystenta dowodu jest robienie dowodów, takich jak te w powiązanym dokumencie. Samo czytanie papieru niewiele pomoże, ponieważ całe doświadczenie interakcji z asystentem dowodu nie może być dobrze przekazane na papierze.

W ciągu kilku dni powinieneś być w stanie zakodować proste twierdzenia, takie jak powyższe, i je udowodnić. Nie oczekuj, że zrobimy to za Ciebie. Nic się nie nauczysz w ten sposób.

Kiedy uda ci się udowodnić te twierdzenia, możesz opublikować tutaj swoje odpowiedzi i być może zostawić kilka komentarzy na temat swoich doświadczeń.

Czy jesteś gotowy na wyzwanie?

Dave Clarke
źródło
4
Coq to rozsądny wybór; jeśli jednak xddz5 naprawdę chce pracować w teorii zbiorów ZF, a nie w teorii typów, być może Mizar jest bardziej odpowiedni.
Timothy Chow,
8

Istnieje wiele artykułów matematycznych napisanych przy użyciu asystenta sprawdzającego Mizara: http://mizar.org/fm/

Radu GRIGore
źródło
3
Jaka jest obsługa narzędzi dla Mizar?
Dave Clarke
Nie użyłem tego.
Radu GRIGore,
5

Dave Clarke sugeruje Coq, ale tak naprawdę Isabelle wydaje się lepszym pomysłem, ponieważ ma bibliotekę dla ZF . Isabelle jest również bardzo dojrzała i zawiera szeroką gamę taktyk i rozszerzeń.

Nie korzystałem osobiście z Mizara, ale równie dobrze może być dobrze.

Liam O'Connor
źródło
2

jak mogę napisać następujący dowód?

W Isabelle / ZF możesz napisać coś takiego 

theory csthquestion imports Main

begin

theorem empty_unique:
shows "\<forall> x.\<forall>y.(\<forall>z. (z\<notin>x)) \<and> (\<forall>z.(z\<notin>y)) \<longrightarrow> x=y"
    by auto

end

Jak widać Isabelle automatycznie to potwierdza. Oczywiście, jeśli naprawdę chcesz, możesz napisać bardziej szczegółowy dowód.


źródło
2

To samo twierdzenie jest sprawdzonym przykładem (patrz przykład 11) w samouczku dołączonym do mojego oprogramowania DC Proof 2.0. Pobierz go bezpłatnie z mojej strony internetowej http://www.dcproof.com

Dan Christensen
źródło
1
To jest mała sprzedaż dla tej strony. Czy mógłbyś przedstawić jakieś informacje w sposób bezstronny, aby powiedzieć, w jaki sposób twoje oprogramowanie jest odpowiednie do problemu? Być może link do filmu lub zrzut ekranu z tej pochodnej jest wykonywany?
Charles Stewart
1
Oto dowód: dcproof.com/EmptySetUnique.htm Na mojej stronie znajduje się film pokazujący działanie systemu.
Dan Christensen,