Zbiór Hintikki
pojęcie logiki / Z Wikipedii, wolnej encyclopedia
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 i (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 i
- lub też ogólniej dla każdego koniunkcyjnego operatora binarnego zawiera i
- dla każdego zawiera lub (lub też oba)
- lub też ogólniej dla każdego dysjunkcyjnego operatora binarnego zawiera lub
- dla każdego zawiera
- dla każdego zawiera wszystkie formuły powstałe przez podstawienie dowolnych formuł pod w
- dla każdego zawiera wszystkie formuły powstałe przez podstawienie dowolnych formuł pod w
- dla każdego zawiera przynajmniej jedną formułę powstałą przez podstawienie pewnej formuły pod w
- dla każdego zawiera przynajmniej jedną formułę powstałą przez podstawienie pewnej formuły pod w
- podobnie dla wszystkich innych reguł rozpatrywanej logiki.
- dla każdego zawiera i
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 nie wiemy czy należy dodać czy też widząc 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.