Pomysł na nowy język do weryfikacji dowodów

[matmatmm]

Zainspirowany systemem Mizar (który jednak wydał mi się niewystarczający) wymyśliłem własny język do zapisu dowodów matematycznych w logice pierwszego rzędu. Język ten póki co nie zaimplementowany jako realny program, ale potencjalnie jest to możliwe. Niestety moja wiedza informatyczna i umiejętności programistyczne są dalece niewystarczające, żeby to zrobić w sensowny sposób. Postanowiłem najpierw pokazać zasady tego języka i być może poznać Waszą opinię.

Wersja bazowa

Poniżej dowód własności \(\displaystyle{ A\cup B=B\cup A}\).

Kod: Zaznacz cały

PREDICATES eq{2} in{2}
SYMBOLS union{2}
AXIOMS 
axiom_ext : forall A, forall B, (forall x, (x in A <-> x in B) -> A=B);
union_def : forall A, forall B, forall x, (x in union(A,B) <-> (x in A \/ x in B));
PROOF
FIX A,B
    A1:  forall x, (x in union(A,B) <-> x in union(B,A)) -> union(A,B)=union(B,A)  INSTANT axiom_ext WITH union(A,B),union(B,A);
    FIX x
        B1: x in union(A,B) <-> (x in A \/ x in B) INSTANT union_def WITH A,B,x;
        B2: x in union(B,A) <-> (x in B \/ x in A) INSTANT union_def WITH B,A,x;
            x in union(A,B) <-> x in union(B,A) TAUTO p<->(a\/b), q<->(b\/a) |- p<->q FROM B1,B2;
    HENCE
    A2: forall x, (x in union(A,B) <-> x in union(B,A)) GEN;
        union(A,B)=union(B,A) TAUTO p->q, p |- q FROM A1, A2;
HENCE
forall A, forall B, union(A,B)=union(B,A) GEN;
QED

Jak wiadomo w logice pierwszego rzędu można ograniczyć się do kwantyfikatora ogólnego i dwóch spójników logicznych. W tym przypadku będą to negacja i implikacja. W prezentowanym kodzie używam innych spójników, ale oczywiście nie jest to konieczne.

Potrzebujemy jeszcze symboli relacyjnych i symboli funkcyjnych.
Kod zaczyna się od deklaracji wszystkich predykatów:

Kod: Zaznacz cały

PREDICATES eq{2} in{2}

PREDICATES to słowo klucz. eq oraz in to nazwy użytkownika, a w nawiasach klamrowych mamy liczbę argumentów. W tym przypadku eq interpretujemy jako równość, a in jako należenie do zbioru (czyli jest to język teorii mnogości). Zamiast pisać eq(x,y) można pisać w pseudokodzie x=y, a zamiast in(x,y) można x in y.

Deklarujemy, że nasz język zawiera symbol funkcyjny union o dwóch argumentach.

Kod: Zaznacz cały

SYMBOLS union{2}

Przyjmujemy dwa aksjomaty:

Kod: Zaznacz cały

AXIOMS 
axiom_ext : forall A, forall B, (forall x, (x in A <-> x in B) -> A=B);
union_def : forall A, forall B, forall x, (x in union(A,B) <-> (x in A \/ x in B));

axiom_ext oraz union_def to etykiety użytkownika. axiom_ext to aksjomat ekstensjonalności. union_def to definicja sumy, (którą należy właśnie przyjąć jako aksjomat, gdyż symbol union jest po prostu częścią języka).

Mamy teraz kilka metod wnioskowania:

1. TAUTO - podstawienie pod tautologię rachunku zdań. Schemat jest taki:

opcjonalna_etykieta : formuła TAUTO lista_przesłanek |- konkluzja FROM etykiety_przesłanek

W powyższym przykładzie

Kod: Zaznacz cały

union(A,B)=union(B,A) TAUTO p->q, p |- q FROM A1, A2;

union(A,B)=union(B,A) to formuła, którą wnioskujemy. Odpowiada ona literze q.
Literze p odpowaida formuła forall x, (x in union(A,B) <-> x in union(B,A)), która ma etykietę A2.
\(\displaystyle{ p\rightarrow q,p\vdash q}\) jest regułą w rachunku zdań.

2. INSTANT - podstawienie termu pod wolne wystąpienia zmiennej \(\displaystyle{ x}\) w formule postaci \(\displaystyle{ \forall x, \varphi(x)}\). Schemat:

opcjonalna_etykieta: formuła INSTANT etykieta_przesłanki WITH lista_termów

Przesłanka o danej etykiecie musi być postaci forall x1, ..., forall xn, ... gdzie n jest liczbą termów. Są one podstawiane w kolejności wypisania. Z tą regułą jest pewien problem, gdyż czasem takie bezpośrednie podstawienie może skutkować tym, że jakaś zmienna z podstawianego termu stanie się związana w powstałej formule. Wtedy trzeba najpiew dokonać podmiany zmiennych związanych.

3. GEN - generalizacja po zmiennych. Schemat

FIX lista_zmiennych
formuła 1;
...
formuła n;
HENCE forall x1,...,forall xk, formuła n GEN

Idea jest taka jak w dowodach nieformalnych: dowodząc jakieś zdanie typu 'dla każdego x', najpierw ustalamy x. Zasada jest taka, że w ogóle nie wolno używać zmiennych wcześniej nie ustalonych.

4. DEDUCT - dedukcja - implementacja twierdzenia o dedukcji znanego z logiki. Schemat:

ASSUME założenie;
formuła 1;
...
formuła n;
HENCE założenie -> formuła n DEDUCT

W powyższym dowodzie ta reguła nie była potrzebna, ale mam wrażenie, że jest konieczna (w przeciwieństwie do klasycznego systemu dowodzenia).

W najbliższym czasie postaram się opisać tutaj wersję rozszerzoną, która daje dużo większe możliwości. Co myślicie?

Ukryta treść:    

Da się tu udowodnić sprzeczność?

[Slup]

To może wyjaśnij, czemu to ma być lepsze i różne od Mizara.

Po dodaniu (schematu) aksjomatu
\(\displaystyle{ \forall_x\left(\phi \rightarrow \psi\right) \rightarrow \left(\forall_x\,\phi \rightarrow \forall_x\,\psi\right)}\)
schemat dedukcji będzie zbędny. Tzn. będzie można go otrzymać jako metatwierdzenie.

Żeby uniknąć problemów z podstawieniem termów możesz dodać regułę, która pozwala rozszerzyć język o nowe symbole relacyjne, które są nazwami formuł (coś w rodzaju deskrypcji Russella, chociaż on stosował je do nazw – operator jota z PM). Takie rozszerzenie jest konserwatywne.

Ukryta treść:    

Uwaga na marginesie. Schematy we współczesnej logice formalnej w jawny sposób wprowadził Hilbert ("schemata") i jego szkoła (Behmann, Bernays, Ackermann) w związku z programem formalizacji. Moim zdaniem nazwę zaczerpnął od Kanta (schemat transcendentalny).

[matmatmm]

To może wyjaśnij, czemu to ma być lepsze i różne od Mizara.

Nie znam Mizara aż tak dobrze, ale moje odczucie jest takie, że został on stworzony właściwie dokładnie po to, żeby rozwijać matematykę od teorii mnogości. Aksjomaty ZFC chyba są wbudowane w system i to łącznie z niestandardowym aksjomatem Tarskiego. Całość jest obudowana mnóstwem skrótów np. polecenia wproadzające nowe symbole albo operatory tworzenia nowych zbiorów. Ciężko oddzielić co rzeczywiście jest jakby "jądrem" systemu. Kroki dowodowe uzasadnia się często skrótowo, bo system sam próbuje wszystko dopasować.

Po dodaniu (schematu) aksjomatu
\(\displaystyle{ \forall_x\left(\phi \rightarrow \psi\right) \rightarrow \left(\forall_x\,\phi \rightarrow \forall_x\,\psi\right)}\)
schemat dedukcji będzie zbędny. Tzn. będzie można go otrzymać jako metatwierdzenie.

Tak, zdaję sobie z tego sprawę, jednak chciałbym, żeby wszystkie twierdzenia rachunku predykatów (czyli teorii bez aksjomatów właściwych) były dowodliwe bez dodatkowych aksjomatów w systemie.

Żeby uniknąć problemów z podstawieniem termów możesz dodać regułę, która pozwala rozszerzyć język o nowe symbole relacyjne, które są nazwami formuł (coś w rodzaju deskrypcji Russella, chociaż on stosował je do nazw – operator jota z PM). Takie rozszerzenie jest konserwatywne.

Dokładnie to planowałem w wersji rozszerzonej (poniżej przykład). Nie wiem jednak, czemu miałoby to rozwiązać problemy z podstawieniem termów. Myślałem raczej, żeby system nie przyjmował wnioskowania tego typu.

Formuła

Kod: Zaznacz cały

forall x, forall y, (x=y -> (phi(x)<->phi(y))

mogłaby być aksjomatem teorii z równością. Przy odwołaniu do niej trzebaby zadeklarować, czym jest phi.