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



Pobieranie 6.74 Mb.
Strona52/57
Data25.10.2017
Rozmiar6.74 Mb.
1   ...   49   50   51   52   53   54   55   56   57
otoczki Skolema (Skolem hull). Dla danego systemu A weźmy wszystkie funktory Skolema s x , dla każdej formuły  i każdej zmiennej x . Niech E  A , oraz zdefiniujmy rosnący ciąg zbiorów następująco: E0 = E , En + 1 jest zbiorem wszystkich elementów postaci s x (a1 , ...) , gdzie  jest dowolną formułą, x jest dowolną zmienną, oraz a1 , ...  En . Fakt, że ciąg jest rosnący wynika natychmiast z użycia funktora Skolema dla formuły x (x = y) i zmiennej x . Otoczką Skolema dla zbioru E w systemie A nazywamy zbiór S(E) = .

Podstawowym zastosowaniem tej konstrukcji jest następujące twierdzenie.



TWIERDZENIE 14.2. Dla danego systemu A i dowolnego E  A , otoczka Skolema S(E) jest uniwersum elementarnego podsystemu systemu A .

Dowód. Zaczniemy od dowodu, że S(E) jest uniwersum podsystemu A . W tym celu zauważmy, że jeśli c jest stałą, oraz jest reprezentowana przez element cA w systemie A , to cA jest wartością funkcji Skolema sx (x = c) x , więc cA. Podobnie, jeśli F jest funktorem oraz a = FA(a1 , ... , am) , dla pewnych a1 , ... , am  S(E) , to a jest wartością funkcji Skolema sx (x =) x na a1 , ... , am . A więc, z definicji S(E) , mamy a  S(E) . To pokazuje, że S(E) jest uniwersum podsystemu A .

Aby wykazać, że S(E) jest uniwersum elementarnego podsystemu systemu A , wystarczy sprawdzić, że S(E) spełnia warunki z Kryterium Vaughta (Twierdzenie 5.1).

Niech więc  będzie formułą o zmiennych x , x1 , ... , xn i niech a : X  S(E) będzie wartościowaniem takim, że A╞ x [a] . Wtedy biorąc funktor Skolema s x mamy a = s x(a1 , ... , an) gdzie a(xa) spełnia  w A . Ale z definicji a  S(E) , więc S(E) spełniając Kryterium Vaughta jest uniwersum elementarnego podsystemu systemu A .

Spróbujemy teraz przerobić tę konstrukcję na syntaktykę. Prowadzi nas to do następującej sytuacji. Dla danego zbioru zdań T języka L tworzymy nowy język L * przez dodanie dla każdej formuły  o zmiennych x , x1 , ... , xn , nowego symbolu funkcyjnego S x mającego arność równą ilości zmiennych wolnych w formule x  (czyli n). Obok dodania nowych symboli, do T dodajemy zbiór TS następujących formuł: x1 ... xnx (x , x1 , ... , xn)  ( S x(x1 , ... , xn), x1 , ... , xn) . Ponieważ, jak zauważyliśmy przy konstrukcji semantycznej, każdy system A możemy wydłużyć do systemu A* dla języka L * przez dodefiniowanie funktorów Skolema, więc jako bezpośredni wniosek, z tej konstrukcji otrzymujemy następujący fakt.



FAKT 14.3. Jeśli  jest niesprzecznym zbiorem zdań języka L , to T* = T  TS jest niesprzecznym zbiorem zdań języka L * .

Język L * nazywamy skolemizacją języka L , natomiast T* – skolemizacją zbioru T . Zauważmy przy tym następujący fakt.



FAKT. 14.4. (i) Każdy system A dla języka L ma wydłużenie do systemu A* języka L * .

(ii) Jeśli T jest niesprzeczną teorią języka L , to jej skolemizacja T* jest niesprzeczną teorią języka L * .

(iii) Niech A i B będą systemami języka L , niech B* będzie wydłużeniem systemu B będącym modelem TS . Niech A* będzie wydłużeniem systemu A do modelu TS . Jeśli A*  B* , to A  B .

Dowód. (i) jest faktycznie przeformułowaniem Faktu 14.1. Natomiast (ii) jest bezpośrednim z tego wnioskiem. Natomiast (iii) jest zastosowaniem Kryterium Tarskiego – Vaughta do tej sytuacji.

Idealna sytuacja z funktorami Skolema występuje wtedy, gdy można je explicité nazwać lub przynajmniej zdefiniować. Prowadzi to do następującego pojęcia.



DEFINICJA. Mówimy, że teoria T języka L ma wbudowane funktory Skolema jeśli dla każdej formuły x  o zmiennych x1 , ... , xn istnieje n – argumentowy term t x języka L taki, że

T├ x1 ... xnx (x , x1 , ... , xn)  (t x (x1 , ... , xn) , x1 , ... , xn) .

FAKT 14.4. Niech T będzie dowolnym zbiorem zdań języka L . Wtedy istnieje wydłużenie L+ języka L oraz rozszerzenie T+ zbioru T takie, że T+ ma wbudowane funktory Skolema. Co więcej, każdy model T ma rozszerzenie będące modelem T+ .

Dowód. Możemy kopiować nasze postępowanie z rozważanego już przypadku semantycznego. Startujemy z języka L0 = L i danego niesprzecznego zbioru zdań T0 = T . Teraz definiujemy wstępujący ciąg języków Ln+1 = (Ln)* i zbiorów formuł Tn+1 = Tn  (Tn)S . Niech L + = n Ln oraz T+ = n Tn . Ponieważ każda formuła języka L + posiada skończenie wiele znaków, więc jest formułą języka L n , co za tym idzie ma swoje funktory Skolema nazwane w języku L n + 1 . Konstrukcja semantyczna, opisana na początku, pokazuje jak można model T wydłużyć do modelu T+ .

Dodajmy jeszcze wniosek bardzo wygodny przy dalszych rozważaniach.



WNIOSEK. 14.5. Jeśli T ma wbudowane funktory Skolema, to dla każdych dwóch modeli A i B teorii T , jeśli A  B , to A  B .

Wniosek ten prowadzi do następnego ważnego pojęcia.



DEFINICJA. Mówimy, że teoria T jest modelowo zupełna (model complete) jeśli dla każdych dwóch modeli A i B teorii T , jeśli A  B , to A  B .

Tak więc teoria z wbudowanymi funktorami Skolema jest modelowo zupełna. Jest to przyjemny fakt semantyczny mający jednak głębokie konsekwencje syntaktyczne.



TWIERDZENIE. 14.6. Teoria T jest modelowo zupełna iff dla każdej formuły egzystencjalnej  istnieje formuła uniwersalna  taka, że  T  .

Dowód. Przypuśćmy, że T jest modelowo zupełna w języku L oraz niech  będzie formułą egzystencjalną. Możemy założyć, że T  {} jest niesprzeczne. Niech x1 , ... , xn będą zmiennymi wolnymi formuły  , niech d1 , ... , dn będą nowymi stałymi, wtedy, po podstawieniu ( , ... ,

Pobieranie 6.74 Mb.

Share with your friends:
1   ...   49   50   51   52   53   54   55   56   57




©operacji.org 2020
wyślij wiadomość

    Strona główna