| « poprzedni punkt | następny punkt » |
Definicja 8.5.1
Formułę α rachunku predykatów nazywamy tautologią (lub prawem rachunku funkcyjnego), jeżeli jej wartością jest prawda, niezależnie od wartości zmiennych oraz interpretacji symboli relacyjnych i funkcyjnych w niej występujących, tzn. dla każdej struktury STR i dla każdego wartościowania v zmiennych w tej strukturze mamy STR, v |= α.
Zbiór tautologii rachunku zdań jest zbiorem "wzorców" dla tautologii rachunku predykatów. Mamy bowiem następujący lemat:
Lemat 8.5.1
Jeśli α jest tautologią rachunku zdań, to podstawiając za zmienne zdaniowe występujące w α dowolne formuły rachunku funkcyjnego otrzymujemy tautologię rachunku predykatów.
Nie będziemy tu przeprowadzać dokładnego dowodu tego lematu, przypomnimy tylko, że jeśli α jest tautologią rachunku zdań, to niezależnie od wartości zmiennych zdaniowych w niej występujących, a więc konkretnych zdań, które możemy wstawić w ich miejsce, wartością formuły jest prawda.
Przykład 8.5.1
Formuła (p ∨ ¬p) jest tautologią rachunku zdań, zatem formuły (x ≤y ∨ ¬ x ≤y), (( ∃y)(x + y >z) ∨ ¬ ( ∃y)(x + y >z)) są tautologiami rachunku predykatów. Natomiast formuła (x ≤y ∨ x>y) nie jest tautologią, bo relacja ≤ nie musi być uzupełnieniem relacji >. Możemy wybrać jako interpretację relacji > zwykłą relację większości w strukturze liczb rzeczywistych, a jako interpretację relacji ≤, np. relację =. W konsekwencji, przy tak wybranej interpretacji, nie zawsze wartością formuły (x ≤y ∨ x>y) jest prawda. Krótko mówiąc, formuła ¬ (x ≤y) jest w zbiorze liczb rzeczywistych równoważna formule (x > y), ale przy innej interpretacji symboli relacyjnych ≤ i >, w innym zbiorze nie musi tak być.
Zamiast " α jest tautologią rachunku funkcyjnego" piszemy krótko |= α. Jeśli przez Xstr oznaczymy zbiór wszystkich formuł prawdziwych w pewnej strukturze STR, to zbiór tautologii TAUT jest przecięciem teoriomnogościowym wszystkich zbiorów Xstr.
Tautologie rachunku predykatów są schematami funkcji zdaniowych prawdziwych w dowolnym zbiorze. Prawdziwość tych wyrażeń nie wynika z przyjętego znaczenia dla symboli pozalogicznych, czy z przyjętego wartościowania zmiennych, a jest konsekwencją jedynie tylko struktury wyrażenia. Następujący lemat przedstawia kilka przykładów tautologii.
Lemat 8.5.2
Dla dowolnych formuł α(x) i β(x) następujące formuły są tautologiami rachunku predykatów:
Dowód.
Ad (1) Dla przykładu podamy dowód dla formuły ( ∀x) α(x) → ( ∃x) α (x). Gdyby ta implikacja była fałszywa przy pewnej interpretacji formuły α(x) w pewnej strukturze STR o niepustym uniwersum X, wtedy byłoby {x ∈ X: α(x) }=X oraz {x ∈ X: α(x)} byłby zbiorem pustym. Czyli X byłby też zbiorem pustym, sprzeczność.
Ad (2) Niech STR będzie ustaloną strukturą oraz v niech będzie pewnym wartościowaniem. Jeśli STR, v|= ¬ ( ∀x) α(x) wtedy wartościowanie v nie spełnia formuły ( ∀x) α(x). Oznacza to, że nie dla wszystkich a wstawionych w miejsce x w wartościowaniu v spełniona jest formuła α(x). Oznaczmy taką wartość dla x przez b. Mamy STR, v(b/x) |= ¬ α(x). Zatem, zgodnie z definicją semantyki dla kwantyfikatora egzystencjalnego mamy STR,v |= (( ∃x) ¬ α(x)).
Dowód pozostałych dwóch równoważności pozostawiamy Czytelnikowi.
Uwaga Tautologia wymieniona w powyższym lemacie jako druga, nosi nazwę prawa de Morgana.
Przykład 8.5.2
Zadanie 8.5.1 Udowodnić, że dla dowolnej formuły α(x) i dowolnej formuły β, w której x nie jest zmienną wolną, formuła ( ∃x)( α(x) ∧ β) ↔ (( ∃x) α(x) ∧ β) jest tautologią rachunku predykatów (prawo włączania i wyłączania kwantyfikatora egzystencjalnego).
Rozwiązanie. Trzeba pokazać, że wartość formuły po lewej i po prawej stronie równoważności jest taka sama w każdej strukturze STR i dla każdego wartościowania v:
STR,v|=( ∃x)( α(x) ∧ β) wttw STR,v(a/x)|= ( α(x) ∧ β) dla pewnego a wttw dla pewnego a, STR,v(a/x)|= α(x)oraz STR,v(a/x)|= β wttw STR,v|= ( ∃x) α(x)oraz STR,v|= β (ponieważ wartość formuły β nie zależy od wartości zmiennej x) wttw STR,v|= ( ∃x) α(x) ∧ β.
Pytanie 8.5.1 Która z następujących formuł jest tautologią rachunku predykatów?
| « poprzedni punkt | następny punkt » |