LOGIKA ALGORYTMICZNA 2. Posta´c normalna Skolema i H-interpretacje. Niech formu la φ j¸ezyka L ma posta´c normaln¸a φ = Q

LOGIKA ALGORYTMICZNA

2. Posta´c normalna Skolema i H-interpretacje.

Niech formu la φ j¸ezyka L ma posta´c normaln¸a φ = Q₁x₁...Q_nx_nψ, gdzie Q_i ∈ {∀, ∃} i ψ nie zawiera kwantyfikator´ow. Dla ka˙zdego kwantyfikatora Q_r (1 ≤ r ≤ n) postaci ∃ wykonujemy nast¸epuj¸ace przekszta lcenie formu ly φ i j¸ezyka L.

Je´sli cz¸e´s´c prefiksu Q₁x₁...Q_r−1x_r−1 nie zawiera kwantyfikator´ow ∀, to rozszerzamy L o nowy symbol sta lej c_r, skre´slamy Q_rx_r z prefiksu formu ly φ i zast¸epujemy ka˙zde wyst¸epowanie x_r w ψ przez c_r.

Je´sli w Q₁x₁...Q_r−1x_r−1 wszystkie wyst¸epowania kwantyfikatora ∀ oznac- zone s¸a przez Q_s1, ..., Q_sm, 1 ≤ s₁ < ... < s_m < r, to rozszerzamy L o nowy symbol funkcyjny F_r^m, skre´slamy Q_rx_r z prefiksu formu ly φ i zast¸epujemy ka˙zde wyst¸epowanie x_r w ψ przez F_r(x_s1, ..., x_sm).

W wyniku tych przekszta lce´n otrzymujemy nowy j¸ezyk L₀ i now¸a formu l¸e φ₀. Symbole zbioru L0 \ L nazywane s¸a sta lymi lub funkcjami Skolema, a formu la φ0 jest nazywana postaci¸a Skolema formu ly φ.

Twierdzenie 2.1. Formu la φ jest sprzeczna wtedy i tylko wtedy, gdy jest sprzeczna jej posta´c Skolema φ0.

Dow´od jest oparty na stwierdzeniu nast¸epuj¸acego zadania.

2.2. Niech formu la φ ma posta´c ∀x₁...∀x_r−1∃x_rQ_r+1x_r+1...Q_nx_nψ, 1 ≤ r ≤ n.

Niech

φ₁ = ∀x₁...∀x_r−1Q_r+1x_r+1...Q_nx_nψ^x_{f (x}^r

1,...,xr−1),

gdzie f jest nowym symbolem funkcyjnym. Udowodni´c, ˙ze φ jest sprzeczna wtedy i tylko wtedy, gdy φ₁ jest sprzeczna.

2.3. Znale´z´c posta´c Skolema nast¸epuj¸acych formu l:

(a) ∀x∃y∀z∃v∃wP (x, y, z, v, w);

(b) ∀x∃y∃z(¬P (x, y) ∧ (Q(x, z) ∨ R(x, y, z))).

2.4. (a) Pokaza´c, ˙ze je´sli formu la φ znajduje si¸e w postaci normalnej i nie zawiera kwantyfikator´ow ∃, to dla ka˙zdej pary struktur N < M warunek M |= φ implikuje N |= φ.

(b) Pokaza´c, ˙ze je´sli formu la φ znajduje si¸e w postaci normalnej i nie zawiera kwantyfikator´ow ∀, to dla ka˙zdej pary struktur N < M warunek N |= φ implikuje M |= φ.

2.5. H-interpretacje. Niech Γ b¸edzie zbiorem formu l j¸ezyka L. Zak ladamy,

˙ze formu ly s¸a w postaci Skolema i L sk lada si¸e z symboli wyst¸epuj¸acych w Γ (tzn.

zawiera odpowiednie sta le i funkcje Skolema). Budujemy (indukcyjnie) uniwersum Herbranda H∞ zbioru Γ w spos´ob nast¸epuj¸acy.

1

Je´sli pewne formu ly z Γ maj¸a wyst¸epowania sta lych, to przez H₀ oznaczamy zbi´or wszystkich sta lych wyst¸epuj¸acych w Γ. W przeciwnym przypadku niech H₀ = {c}, gdzie c jest nowym symbolem sta lej. Na kroku i + 1 niech H_i+1 jest sum¸a zbioru H_i i zbioru wszystkich term´ow postaci F (t₁, ..., t_n), gdzie t_i ∈ H_i, 1 ≤ i ≤ n, i symbol funkcyjny F wyst¸epuje w Γ. Niech H∞ = ^S{H_i : i ∈ ω}. Elementy zbioru H_i nazywane s¸a sta lymi poziomu i.

H-struktur¸a nazywamy dowoln¸a L-struktur¸e na zbiorze H_∞, gdzie sta le s¸a in- terpretowane przez ich symbole z H₀, a ka˙zdy symbol funkcyjny F jest interpre- towany przez funkcj¸e, kt´ora ka˙zdemu ci¸agowi h₁, ..., h_n ∈ H_i przyporz¸adkowuje sta l¸a F (h₁, ..., h_n) ∈ H_i+1.

Ka˙zd¸a interpretacj¸a zmiennych zbioru Γ w H-strukturze nazywamy H-interpretacj¸a zbioru Γ.

Twierdzenie 2.6. Niech φ b¸edzie formu l¸a w postaci Skolema, nie zawieraj¸acej zmiennych wolnych i podformu l postaci t = t⁰. Wtedy φ jest sprzeczna wtedy i tylko wtedy, gdy φ jest falszywa wzgl¸edem ka˙zdej H-interpretacji zbioru {φ}.

Dow´od jest oparty na nast¸epuj¸acej konstrukcji. Niech M b¸edzie pewn¸a L-struktur¸a.

Niech τ b¸edzie odwzorowaniem H₀ → M , odwzorowuj¸acym symbole sta lych w ich M -interpretacje. Rozszerzamy τ do odwzorowania τ^∗ : H∞ → M zgodnie z regu l¸a:

τ^∗(F (t₁, ..., t_n)) = F (τ^∗(t₁), ..., τ^∗(t_n)). Dla ka˙zdej relacji P ⊆ M^m struktury M definiujemy relacj¸e P^∗ na H_∞^m w nast¸epuj¸acy spos´ob:

(h₁, ..., h_m) ∈ P^∗ ↔ (τ^∗(h₁), ..., τ^∗(h_m)) ∈ P.

Niech M^∗ b¸edzie H-struktur¸a okre´slon¸a przez wszystkie relacje P^∗. Udowodni´c:

2.7. Je´sli M |= φ, to M^∗ |= φ.

2.8. Zadania. 1. Znale´z´c zbi´or sta lych poziomu 2 nast¸epuj¸acych formu l:

(a) P (a) ∧ (¬P (x) ∨ P (f (x)));

(b) P (f (x), a, g(y), b).

2. Znale´z´c H-interpretacj¸e M^∗ odpowiadaj¸ac¸a strukturze M = (N, s¹, P¹, 3), gdzie s(x) jest funkcj¸a x + 1, relacja P wyr´o˙znia liczby parzyste i τ przeprowadza liczb¸e 3 w sta l¸a 3 ∈ H₀.

2