Zbiór Hintikki

Zbiór Hintikki (ang. Hintikka 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 $p\land q$ zawiera $p$ i $q$
    • lub też ogólniej dla każdego koniunkcyjnego operatora binarnego $\alpha$ zawiera $\alpha _{1}$ i $\alpha _{2}$
  • dla każdego $p\lor q$ zawiera $p$ lub $q$ (lub też oba)
    • lub też ogólniej dla każdego dysjunkcyjnego operatora binarnego $\beta$ zawiera $\beta _{1}$ lub $\beta _{2}$
  • dla każdego $\neg \neg x$ zawiera $x$
  • dla każdego $\forall x.\phi (x)$ zawiera wszystkie formuły powstałe przez podstawienie dowolnych formuł pod $x$ w $\phi (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 $\exists x.\phi (x)$ zawiera przynajmniej jedną formułę powstałą przez podstawienie pewnej formuły pod $x$ w $\phi (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\lor 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. Hintikka’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.

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(\alpha )=1+\max(d(\alpha _{1}),d(\alpha _{1}))$

$d(\beta )=1+\max(d(\beta _{1}),d(\beta _{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łębokoś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 $\alpha ,$ to zarówno $\alpha _{1},$ jak i $\alpha _{2}$ mają głębokość co najwyżej $n$ i należą do zbioru Hintikki. Ponieważ zarówno $\alpha _{1},$ jak i $\alpha _{2}$ są spełnione, spełniona jest też $\alpha .$
• jeśli formułą tą jest $\beta ,$ to albo $\beta _{1}$ albo $\beta _{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 $\beta .$

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ż

• Jaakko Hintikka