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 $\mathrm{\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\wedge 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\vee 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 $\mathrm{\neg }\mathrm{\neg }x$ zawiera $x$
  • dla każdego $\mathrm{\forall }x.\varphi (x)$ zawiera wszystkie formuły powstałe przez podstawienie dowolnych formuł pod $x$ w $\varphi (x)$
    • dla każdego $\mathrm{\neg }\mathrm{\exists }x.\varphi (x)$ zawiera wszystkie formuły powstałe przez podstawienie dowolnych formuł pod $x$ w $\mathrm{\neg }\varphi (x)$
  • dla każdego $\mathrm{\exists }x.\varphi (x)$ zawiera przynajmniej jedną formułę powstałą przez podstawienie pewnej formuły pod $x$ w $\varphi (x)$
    • dla każdego $\mathrm{\neg }\mathrm{\forall }x.\varphi (x)$ zawiera przynajmniej jedną formułę powstałą przez podstawienie pewnej formuły pod $x$ w $\mathrm{\neg }\varphi (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\vee q$ nie wiemy czy należy dodać $p$ czy też $q,$ widząc $\mathrm{\exists }x.\varphi (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(\mathrm{\neg }\mathrm{\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 $\mathrm{\neg }\mathrm{\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ż $\mathrm{\neg }\mathrm{\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