Logika prof dr hab. Bogdan WĘglorz rachunek zdań, algebry uniwersalne. Systemy relacyjne



Pobieranie 6.74 Mb.
Strona42/57
Data25.10.2017
Rozmiar6.74 Mb.
1   ...   38   39   40   41   42   43   44   45   ...   57

RA([t] , ... , [t]) iff R(t , ... , t)  S .

Przejdźmy więc do pozostałych formuł. Dla negacji wynika to z faktu, że dla dowolnego  albo  albo   jest w S . Równie łatwo zauważyć, że jeśli twierdzenie zachodzi dla  i  , to zachodzi też dla    .



Rozpatrzmy więc przypadek, gdy  = x  . Prowadzimy dowód przez kontrapozycję, więc przypuśćmy, że A╞ x [p] nie zachodzi. Czyli zachodzi A╞ x [p] . To znaczy, że istnieje takie

a  A , że modyfikacja ppodstawienia p polegająca na położeniu p’(x) = a spełnia  , czyli

A╞ [p’] , lub mówiąc jeszcze inaczej, że nie zachodzi A╞ [p’] . Ponieważ elementy A są klasami równoważności termów, więc a = [t] , dla pewnego termu t . Innymi słowy na warunek A╞ [p’] możemy patrzeć jak na A╞ [p()] lub jeszcze inaczej, A╞ () [p] . Zmieniając (jeśli trzeba) zmienne znajdujemy formułę  logicznie równoważną  , taką, że podstawienie x t jest właściwe dla  . Ponieważ warunek A╞ [p’] nie zachodzi więc A╞ () [p] też nie zachodzi, konsekwentnie nie zachodzi też A╞ () [p] . Z założenia indukcyjnego mamy więc ()  S . To jednak pokazuje, że x   S , bo x   () jest aksjomatem logiki. W końcu logiczna równoważność  i  pociąga za sobą (jak zauważyliśmy) logiczną równoważność x  i x  . Ostatecznie mamy więc x   S . Innymi słowy udowodniliśmy, że x   S pociąga za sobą warunek A╞ x [p] .

Odwrotnie przypuśćmy teraz, że x   S . Wtedy jednak (x )  S , lub inaczej mówiąc



Pobieranie 6.74 Mb.

Share with your friends:
1   ...   38   39   40   41   42   43   44   45   ...   57




©operacji.org 2020
wyślij wiadomość

    Strona główna