Twierdzenie
Niech T b¦dzie tabel¡ zako«czon¡ dla formuªy A. Forrmuªa A jest niespeªnialna wtw, gdy ka»dy jej li±¢ jest domkni¦ty.
Wniosek
Metoda tabel semantycznych jest procedur¡ decyzyjn¡
rozstrzygaj¡c¡ prawdziwo±¢ formuª rachunku zda«.
Dowód Z tw. o zatrzymywaniu mamy, »e konstrukcja tabeli dla 6 A ko«czy si¦ utworzeniem tabeli sko«czonej. Z poprzedniego wniosku mamy, »e A jest prawdziwa wtw, gdy tabela jest domkni¦ta.
Dowód poprawno±ci
Poka»emy ogólniejsz¡ wªasno±¢: jesli poddrzewo o korzeniu n jest domkni¦te, to zbiór formuª U(n) jest niespeªnialny.
Indukcja po wysoko±ci h drzewa U(n).
Podstawa indukcji. Je±li h = 0, to n jest li±ciem. Wtedy T jest domkni¦ta, a U(n) zawiera par¦ literaªów komplementarnych.
Zatem U(n) jest niespeªnialny.
Krok indukcyjny. Je±li h > 0, to do tworzenia potomka u»yto reguªy typu α lub β.
Przypadek 1. U»yto reguªy typu α. U(n) = {A1∧A2} ∪U0, a U(n0) = {A1,A2} ∪U0. Wysoko±¢ n0 wynosi h − 1 i z zaªo»enia indukcyjnego otrzymujemy, »e U(n0) jest niespeªnialny, gdy»
poddrzewo o korzeniu n0 jest domkni¦te.We¹my dowolne warto±ciowanie v zbioru U. Mamy jeszcze dwa przypadki:
1 Dla pewnej formuªy A0∈U0 mamy v(A0) =0.
2 Dla jednej z formuª A1,A2 mamy v(Ai) =0
Za ka»dym razem otrzymujemy, »e v(A) = 0, dla dobranych A, a z dowolno±i warto±ciowania otrzymujemy, »e U(n) jest niespeªnialny.
Przypadek 2. U»yto reguªy typu β. U(n) = {B1∨B2} ∪U0, U(n0) = {B1} ∪U0 i U(n”) = {B2} ∪U0. Z zaªo»enia indukcyjnego U(n0),U(n”) s¡ niespeªnialne. Niech v b¦dzie dowolnym
warto±ciowaniem.
Te» wnioskujemy, »e B ∈ U(n) nie jest speªnione przy warto±ciowaniu v. Z dowolnosci v otrzymujemy tez¦.
Trzeba wykaza¢ te», »e je±li A jest formuª¡ niespeªnialn¡, to ka»da tabela dla A jest domkni¦ta. To jest trudne zadanie. Z tego powodu wyka»emy nieco inne twierdzenie.
Mianowicie, wyka»emy, je±li pewna tabela dla formuªy A jest otwarta, to A jest speªnialna.
De nicja
Mówimy, »e zbiór formuª U jest zbiorem Hintikki wtw, gdy
1 Dla ka»dego atomu p wyst¦puj¡cego w pewnej formule z U zachodzi p /∈ U lub ¬p /∈ U.
2 Je±li α ∈ U jest typu α, to α1, α2 ∈U.
3 Je±li β ∈ U jest typu β, to β1 ∈U lub β2 ∈U.
Twierdzenie
Niech l bedzie otwartym li±ciem w zako«czonej tabeli semantycznej T . Niech U = SiUi, po wszystkich i na gaª¦zi z korzenia do wierzchoªka l. Wtedy U jest zbiorem Hintikki.
Dowód
Je±li literaª m wyst¡pi pierwszy raz w U(n), to wyst¡pi na drodze z U(n) do U(l). Oznacza to, »e wszystkie literaªy z U nale»¡ do U(l). Gaª¡¹ ta jest otwarta, wi¦c nie zawiera pary literaªów komplementarnych, czyli pierwszy warunek zachodzi.
Niech α ∈ U b¦dzie typu α, a w pewnym wierzchoªku n u»yto reguªy typu α. Z konstrukcji tabeli wynika, »e oba jej skladniki nale»¡ do U(n0) ⊆U, czyli warunek drugi te» jest speªniony.
Trzeci przypadek rozwa»amy analogicznie.
Twierdzenie (Lemat Hintikki) Ka»dy zbiór Hintikki jest speªnialny.
Niech {p1, . . . ,pn}b¦dzie zbiorem wszystkich formuª atomowych wyst¦puj¡cych w formuªach ze zbioru U. De niujemy
warto±ciowanie wzorami:
v(p) =
1 p ∈ U
0 ¬p ∈ U
1 p 6∈ U i ¬p 6∈ U
Dowód twierdzenia o peªno±ci
Z przedostatniego twierdzenia wiemy, »e zbiór formuª U
wyst¦pujacych w otwartej gaª¦zi drzewa T jest zbiorem Hintikki. Z nast¦pnego, istnieje model U, a A wyst¦puje w korzeniu T . St¡d A ∈ U i model U jest modelem A.
