Zbiór Hintikki

Z Wikipedii

Masz nowe wiadomości (różnica z poprzednią wersją).

Zbiór Hintikki (ang. Hintikki's set) to maksymalnie wysycony (ang. saturated) zbiór generowany przez pewien niesprzeczny zbiór formuł logicznych.

Zbiór taki:

nie zawiera jednocześnie $\ x$ i $\neg x$ (wystarczy postawić ten warunek dla literałów, ponieważ rozszerza się on automatycznie na inne formuły)
jest wysycony, czyli dla każdej formuły zawiera też:
- dla każdego zawiera p i q
  - lub też ogólniej dla każdego koniunkcyjnego operatora binarnego $α$ zawiera $α 1$ i $α 2$
- dla każdego zawiera p lub q (lub też oba)
  - lub też ogólniej dla każdego dysjunkcyjnego operatora binarnego $β$ zawiera $β 1$ lub $β 2$
- dla każdego $\neg \neg x$ zawiera $x$
- dla każdego zawiera wszystkie formuły powstałe przez podstawienie dowolnych formuł pod x w φ(x)
  - dla każdego $\neg \exists x . \phi(x)$ zawiera wszystkie formuły powstałe przez podstawienie dowolnych formuł pod $x$ w $\neg \phi(x)$
- dla każdego zawiera przynajmniej jedną formułę powstałą przez podstawienie pewnej formuły pod x w φ(x)
  - dla każdego $\neg \forall x . \phi(x)$ zawiera przynajmniej jedną formułę powstałą przez podstawienie pewnej formuły pod $x$ w $\neg \phi(x)$
- podobnie dla wszystkich innych reguł rozpatrywanej logiki.

Jak widać, o ile dla formuł rachunku zdań zbiór Hintikki będzie skończony, to niekoniecznie będzie to miało miejsce dla formuł rachunku predykatów rzędu pierwszego i wyższych, gdyż kwantyfikator ogólny generuje nieskończoną ilość formuł.

Tworzenie zbioru Hintikki jest działaniem niedeterministycznym (widząc $p \or q$ nie wiemy czy należy dodać $p$ czy też $q$ , widząc $\exists x . \phi(x)$ mamy nieskończoną liczbę możliwości), więc jest to twór raczej teoretyczny niż stosowany w informatyce.

Twierdzenie Hintikki (ang. Hintikki's lemma) mówi, że jeśli istnieje zbiór Hintikki zawierający dane formuły, to istnieje też model, który je spełnia.

[edytuj] Dowód twierdzenia Hintikki dla rachunku zdań

Niech głębokość formuły $d (x)$ wynosi 0 dla zmiennych zdaniowych, dla innych formuł natomiast:

$d(\neg \neg x) = 1 + d(x)$

d (α) = 1 + max(d (α 1), d (α 1))

d (β) = 1 + max(d (β 1), d (β 1))

Przeprowadzimy teraz indukcję strukturalną.
Ponieważ każda zmienna zdaniowa występuje tylko negatywnie lub tylko pozytywnie, możemy ustalić w modelu takie wartościowanie zmiennych zdaniowych, które nie przeczy żadnej formule o głebokości 0.

Jeśli model można znaleźć dla wszystkich formuł o głębokości $n$ , to można go znaleźć również dla formuł o głębokości $n + 1$ . Rozważmy więc dowolną formułę o głębokości $n + 1$ , zaś wraz z nią następujące przypadki:

jeśli formułą tą jest $\neg \neg x$ , to $x$ należy do zbioru i ma głębokość $n$ . Ponieważ mają one równe wartości dla każdego wartościowania, więc spełniona jest również $\neg \neg x$ .
jeśli formułą tą jest $α$ , to zarówno $α 1$ , jak i $α 2$ mają głębokość co najwyżej $n$ i należą do zbioru Hintikki. Ponieważ zarówno $α 1$ , jak i $α 2$ są spełnione, spełniona jest też $α$ .
jeśli formułą tą jest $β$ , to albo $β 1$ albo $β 2$ o głębokości równej co najwyżej $n$ należą do zbioru Hintikki. Ponieważ która z nich należy do zbioru i jest spełniona, więc spełniona jest też formuła $β$ .

Tak więc formuła dowolnej głębokości ze zbioru Hintikki jest spełniona przez nasz model, co kończy dowód.

Zobacz też: przegląd zagadnień z zakresu matematyki

Źródło: "http://pl.wikipedia.org../../../z/b/i/Zbi%C3%B3r_Hintikki_a2d2.html"

Kategoria: Teoria obliczeń

Zbiór Hintikki

Z Wikipedii

[edytuj] Dowód twierdzenia Hintikki dla rachunku zdań

Views

nawigacja

techniczne

zmiany

Szukaj