Лекции 2-11. Математическая логика (до колка) (1161869), страница 8
Текст из файла (страница 8)
ϕ[ψ] = ψ. Î÷åâèäíî.ÒÅÎÐÅÌÀ Î ÐÀÂÍÎÑÈËÜÍÎÉ ÇÀÌÅÍÅÈíäóêòèâíûé ïåðåõîä. ϕ[ψ] = ∀xϕ1[ψ](x).Ïî èíäóêòèâíîìó ïðåäïîëîæåíèþ, åñëè |= ψ ≡ χ, òî â ëþáîéèíòåðïåðòàöèè I è äëÿ ëþáîãî ýëåìåíòà d ∈ DI âåðíîI |= ϕ1 [ψ](d) → ϕ1 [ψ/χ](d)I |= ϕ1 [ψ/χ](d) → ϕ1 [ψ](d)Çíà÷èò,I |= ∀x(ϕ1 [ψ](x) → ϕ1 [ψ/χ](x))I |= ∀x(ϕ1 [ψ/χ](x) → ϕ1 [ψ](x))Êàê ñëåäóåò èç ïðèìåðà |= ∀x(A → B) → (∀xA → ∀xB)(ñì. Ëåêöèÿ 3 ),I |= ∀xϕ1 [ψ](x) → ∀xϕ1 [ψ/χ](x))I |= ∀xϕ1 [ψ/χ](x) → ∀xϕ1 [ψ](x))(Îñòàëüíûå ñëó÷àè ôîðìóëû ϕ ñàìîñòîÿòåëüíî.)ÒÅÎÐÅÌÀ Î ÐÀÂÍÎÑÈËÜÍÎÉ ÇÀÌÅÍÅÐàâíîñèëüíûå çàìåíû ïîçâîëÿþò óïðîùàòü ôîðìóëû,ïîëíîñòüþ ñîõðàíÿÿ ïðè ýòîì èõ çíà÷åíèå (ñìûñë).ÒÅÎÐÅÌÀ Î ÐÀÂÍÎÑÈËÜÍÎÉ ÇÀÌÅÍÅÐàâíîñèëüíûå çàìåíû ïîçâîëÿþò óïðîùàòü ôîðìóëû,ïîëíîñòüþ ñîõðàíÿÿ ïðè ýòîì èõ çíà÷åíèå (ñìûñë).ÏðèìåðÄîêàçàòü îáùåçíà÷èìîñòü ôîðìóëû ∀xP(x) → ∃xP(x).ÒÅÎÐÅÌÀ Î ÐÀÂÍÎÑÈËÜÍÎÉ ÇÀÌÅÍÅÐàâíîñèëüíûå çàìåíû ïîçâîëÿþò óïðîùàòü ôîðìóëû,ïîëíîñòüþ ñîõðàíÿÿ ïðè ýòîì èõ çíà÷åíèå (ñìûñë).ÏðèìåðÄîêàçàòü îáùåçíà÷èìîñòü ôîðìóëû ∀xP(x) → ∃xP(x).|= ∀xP(x) → ∃xP(x) ≡ ¬∀xP(x) ∨ ∃xP(x)|= ϕ → ψ ≡ ¬ϕ ∨ ψÏîñêîëüêóÒÅÎÐÅÌÀ Î ÐÀÂÍÎÑÈËÜÍÎÉ ÇÀÌÅÍÅÐàâíîñèëüíûå çàìåíû ïîçâîëÿþò óïðîùàòü ôîðìóëû,ïîëíîñòüþ ñîõðàíÿÿ ïðè ýòîì èõ çíà÷åíèå (ñìûñë).ÏðèìåðÄîêàçàòü îáùåçíà÷èìîñòü ôîðìóëû ∀xP(x) → ∃xP(x).|= ∀xP(x) → ∃xP(x) ≡ ¬∀xP(x) ∨ ∃xP(x)|= ¬∀xP(x) ∨ ∃xP(x) ≡ ∃x¬P(x) ∨ ∃xP(x)|= ¬∀xϕ ≡ ∃x¬ϕÏîñêîëüêóÒÅÎÐÅÌÀ Î ÐÀÂÍÎÑÈËÜÍÎÉ ÇÀÌÅÍÅÐàâíîñèëüíûå çàìåíû ïîçâîëÿþò óïðîùàòü ôîðìóëû,ïîëíîñòüþ ñîõðàíÿÿ ïðè ýòîì èõ çíà÷åíèå (ñìûñë).ÏðèìåðÄîêàçàòü îáùåçíà÷èìîñòü ôîðìóëû ∀xP(x) → ∃xP(x).|= ∀xP(x) → ∃xP(x) ≡ ¬∀xP(x) ∨ ∃xP(x)|= ¬∀xP(x) ∨ ∃xP(x) ≡ ∃x¬P(x) ∨ ∃xP(x)|= ∃x¬P(x) ∨ ∃xP(x) ≡ ∃x¬P(x) ∨ ∃yP(y )|= ∃x ϕ(x) ≡ ∃y ϕ(y )ÏîñêîëüêóÒÅÎÐÅÌÀ Î ÐÀÂÍÎÑÈËÜÍÎÉ ÇÀÌÅÍÅÐàâíîñèëüíûå çàìåíû ïîçâîëÿþò óïðîùàòü ôîðìóëû,ïîëíîñòüþ ñîõðàíÿÿ ïðè ýòîì èõ çíà÷åíèå (ñìûñë).ÏðèìåðÄîêàçàòü îáùåçíà÷èìîñòü ôîðìóëû ∀xP(x) → ∃xP(x).|= ∀xP(x) → ∃xP(x) ≡ ¬∀xP(x) ∨ ∃xP(x)|= ¬∀xP(x) ∨ ∃xP(x) ≡ ∃x¬P(x) ∨ ∃xP(x)|= ∃x¬P(x) ∨ ∃xP(x) ≡ ∃x¬P(x) ∨ ∃yP(y )|= ∃x¬P(x) ∨ ∃yP(y ) ≡ ∃x∃y (¬P(x) ∨ P(y ))|= ∃xϕ(x) ∨ ψ ≡ ∃x(ϕ(x) ∨ ψ)ÏîñêîëüêóÒÅÎÐÅÌÀ Î ÐÀÂÍÎÑÈËÜÍÎÉ ÇÀÌÅÍÅÐàâíîñèëüíûå çàìåíû ïîçâîëÿþò óïðîùàòü ôîðìóëû,ïîëíîñòüþ ñîõðàíÿÿ ïðè ýòîì èõ çíà÷åíèå (ñìûñë).ÏðèìåðÄîêàçàòü îáùåçíà÷èìîñòü ôîðìóëû ∀xP(x) → ∃xP(x).|= ∀xP(x) → ∃xP(x) ≡ ¬∀xP(x) ∨ ∃xP(x)|= ¬∀xP(x) ∨ ∃xP(x) ≡ ∃x¬P(x) ∨ ∃xP(x)|= ∃x¬P(x) ∨ ∃xP(x) ≡ ∃x¬P(x) ∨ ∃yP(y )|= ∃x¬P(x) ∨ ∃yP(y ) ≡ ∃x∃y (¬P(x) ∨ P(y ))Òàêèì îáðàçîì, âîïðîñ îá îáùåçíà÷èìîñòè ∀xP(x) → ∃xP(x)ñâîäèòñÿ ê âîïðîñó îá îáùåçíà÷èìîñòè ∃x∃y (¬P(x) ∨ P(y ))ÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÎïðåäåëåíèåÇàìêíóòàÿ ôîðìóëà ϕ íàçûâàåòñÿ ïðåäâàðåííîé íîðìàëüíîéôîðìîé (ÏÍÔ) , åñëèϕ = Q1 x1 Q2 x2 .
. . Qn xn M(x1 , x2 , . . . , xn ),ãäåIIQ1 x1 Q2 x2 . . . Qn xn êâàíòîðíàÿ ïðèñòàâêà , ñîcòîÿùàÿèç êâàíòîðîâ Q1, Q2, . . . , Qn ,M(x1 , x2 , . . . , xn ) ìàòðèöà áåñêâàíòîðíàÿêîíúþíêòèâíàÿ íîðìàëüíàÿ ôîðìà (ÊÍÔ), ò. å.M(x1 , x2 , . . . , xn ) = D1 & D2 & . . . & DN ,ãäå Di = Li1 ∨ Li2 ∨ · · · ∨ Lik äèçúþíêòû , ñîñòîÿùèå èçëèòåð Lij = Aij èëè Lij = ¬Aij , ãäå Aij àòîìàðíàÿôîðìóëà.iÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÏðèìåð∀x∃y ∃z∀u (P(x) & ¬R(x, u) & (¬P(y ) ∨ R(x, z))),êâàíòîðíàÿ ïðèñòàâêà: ∀x∃y ∃z∀uìàòðèöà: P(x) & ¬R(x, u) & (¬P(y )äèçúþíêòû: D1 = P(x),D2 = ¬R(x, u),D3 = ¬P(y ) ∨ R(x, z)∨ R(x, z))ÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÒåîðåìà î ÏÍÔÄëÿ ëþáîé çàìêíóòîé ôîðìóëû ϕ ñóùåñòâóåòðàâíîñèëüíàÿ ïðåäâàðåííàÿ íîðìàëüíàÿ ôîðìà ψ.ÄîêàçàòåëüñòâîÇàìêíóòóþ ôîðìóëó ϕ ìîæíî ïðèâåñòè ê ÏÍÔ ïðèìåíåíèåìðàâíîñèëüíûõ ïðåîáðàçîâàíèé.
Ïîêàæåì, êàê ýòî íàäî äåëàòüíà ïðèìåðå ôîðìóëûϕ = ¬ ∃x( (P(x) & (∀xP(x) → ∃yR(x, y ))) → ∃yR(x, y ) )ÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî1. Ïåðåèìåíîâàíèå ïåðåìåííûõ. ∀Ïðèìåíÿåì ðàâíîñèëüíîñòè |= ∃ x ϕ(x)≡∀∃y ϕ(y )ϕ = ¬ ∃x( (P(x) & (∀xP(x) → ∃yR(x, y ))) → ∃yR(x, y ) )¬ ∃x1 ( (P(x1 ) & (∀x2 P(x2 ) → ∃yR(x1 , y))) → ∃yR(x1 , y) )¬ ∃x1 ( (P(x1 ) & (∀x2 P(x2 ) → ∃y1 R(x1 , y1 ))) → ∃y2 R(x1 , y2 ) )ÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî2. Óäàëåíèå èìïëèêàöèé.Ïðèìåíÿåì ðàâíîñèëüíîñòü |=ϕ → ψ ≡ ¬ϕ ∨ ψÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî2.
Óäàëåíèå èìïëèêàöèé.¬ ∃x1 ( (P(x1 ) & (∀x2 P(x2 )→∃y1 R(x1 , y1 ))) → ∃y2 R(x1 , y2 ) )ÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî2. Óäàëåíèå èìïëèêàöèé.¬ ∃x1 ( (P(x1 ) & (∀x2 P(x2 )→∃y1 R(x1 , y1 ))) → ∃y2 R(x1 , y2 ) )¬ ∃x1 ( ¬(P(x1 ) & (¬∀x2 P(x2 )∨∃y1 R(x1 , y1 ))) ∨ ∃y2 R(x1 , y2 ) )ÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî3.
Ïðîäâèæåíèå îòðèöàíèÿ âãëóáü.Ïðèìåíÿåì ðàâíîñèëüíîñòè|= ¬¬ϕ ≡ ϕ,∨|= ¬(ϕ &∨ ψ) ≡ ¬ϕ & ¬ψ ,|= ¬ ∀∃ xϕ ≡∃∀x¬ϕÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî3. Ïðîäâèæåíèå îòðèöàíèÿ âãëóáü.¬ ∃x1 ( ¬(P(x1 ) & (¬∀x2 P(x2 ) ∨ ∃y1 R(x1 , y1 ))) ∨ ∃y2 R(x1 , y2 ) )ÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî3. Ïðîäâèæåíèå îòðèöàíèÿ âãëóáü.¬ ∃x1 ( ¬(P(x1 ) & (¬∀x2 P(x2 ) ∨ ∃y1 R(x1 , y1 ))) ∨ ∃y2 R(x1 , y2 ) )∀x1 ¬( ¬(P(x1 ) & (¬∀x2 P(x2 ) ∨ ∃y1 R(x1 , y1 ))) ∨ ∃y2 R(x1 , y2 ) )ÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî3. Ïðîäâèæåíèå îòðèöàíèÿ âãëóáü.¬ ∃x1 ( ¬(P(x1 ) & (¬∀x2 P(x2 ) ∨ ∃y1 R(x1 , y1 ))) ∨ ∃y2 R(x1 , y2 ) )∀x1 ¬( ¬(P(x1 ) & (¬∀x2 P(x2 ) ∨ ∃y1 R(x1 , y1 ))) ∨ ∃y2 R(x1 , y2 ) )∀x1 ( ¬¬(P(x1 ) & (¬∀x2 P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ¬∃y2 R(x1 , y2 ) )ÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî3.
Ïðîäâèæåíèå îòðèöàíèÿ âãëóáü.¬ ∃x1 ( ¬(P(x1 ) & (¬∀x2 P(x2 ) ∨ ∃y1 R(x1 , y1 ))) ∨ ∃y2 R(x1 , y2 ) )∀x1 ¬( ¬(P(x1 ) & (¬∀x2 P(x2 ) ∨ ∃y1 R(x1 , y1 ))) ∨ ∃y2 R(x1 , y2 ) )∀x1 ( ¬¬(P(x1 ) & (¬∀x2 P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ¬∃y2 R(x1 , y2 ) )∀x1 ( (P(x1 ) & (¬∀x2 P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )ÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî3. Ïðîäâèæåíèå îòðèöàíèÿ âãëóáü.¬ ∃x1 ( ¬(P(x1 ) & (¬∀x2 P(x2 ) ∨ ∃y1 R(x1 , y1 ))) ∨ ∃y2 R(x1 , y2 ) )∀x1 ¬( ¬(P(x1 ) & (¬∀x2 P(x2 ) ∨ ∃y1 R(x1 , y1 ))) ∨ ∃y2 R(x1 , y2 ) )∀x1 ( ¬¬(P(x1 ) & (¬∀x2 P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ¬∃y2 R(x1 , y2 ) )∀x1 ( (P(x1 ) & (¬∀x2 P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )∀x1 ( (P(x1 ) & (∃x2 ¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )ÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî4. Âûíåñåíèå êâàíòîðîâ ¾íàðóæó¿.Ïðèìåíÿåìðàâíîñèëüíîñòè|= ∀∃ xϕ(x)&ψ ≡ ∀∃ x(ϕ(x)&ψ),|= ∀∃ xϕ(x) ∨ ψ ≡ ∀∃ x(ϕ(x) ∨ ψ),&|= ϕ &∨ ψ ≡ ψ ∨ ϕ.ÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî4.
Âûíåñåíèå êâàíòîðîâ ¾íàðóæó¿.∀x1 ( (P(x1 ) & (∃x2 ¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )ÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî4. Âûíåñåíèå êâàíòîðîâ ¾íàðóæó¿.∀x1 ( (P(x1 ) & (∃x2 ¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )∀x1 ( (P(x1 ) & ∃x2 (¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )ÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî4. Âûíåñåíèå êâàíòîðîâ ¾íàðóæó¿.∀x1 ( (P(x1 ) & (∃x2 ¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )∀x1 ( (P(x1 ) & ∃x2 (¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )∀x1 ( ∃x2 (P(x1 ) & (¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )ÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî4.
Âûíåñåíèå êâàíòîðîâ ¾íàðóæó¿.∀x1 ( (P(x1 ) & (∃x2 ¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )∀x1 ( (P(x1 ) & ∃x2 (¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )∀x1 ( ∃x2 (P(x1 ) & (¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )∀x1 ∃x2 ( (P(x1 ) & (¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )è òàê äàëåå...ÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî4.
Âûíåñåíèå êâàíòîðîâ ¾íàðóæó¿.∀x1 ( (P(x1 ) & (∃x2 ¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )∀x1 ( (P(x1 ) & ∃x2 (¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )∀x1 ( ∃x2 (P(x1 ) & (¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )∀x1 ∃x2 ( (P(x1 ) & (¬P(x2 ) ∨ ∃y1 R(x1 , y1 ))) & ∀y2 ¬R(x1 , y2 ) )è òàê äàëåå...∀x1 ∃x2 ∃y1 ∀y2 ( (P(x1 ) & (¬P(x2 ) ∨ R(x1 , y1 ))) & ¬R(x1 , y2 ) )ÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî5. Ïðèâåäåíèå ìàòðèöû ê êîíúþíêòèâíîé íîðìàëüíîé ôîðìå.Ïðèìåíÿåì çàêîíû áóëåâîé àëãåáðû.ÏÐÅÄÂÀÐÅÍÍÛÅ ÍÎÐÌÀËÜÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî5. Ïðèâåäåíèå ìàòðèöû ê êîíúþíêòèâíîé íîðìàëüíîé ôîðìå.ψ = ∀x1 ∃x2 ∃y1 ∀y2 (P(x1 ) & (¬P(x2 ) ∨ R(x1 , y1 )) & ¬R(x1 , y2 ) ) ðåçóëüòàòå ïîëó÷àåì ôîðìóëó ψ, êîòîðàÿI ÿâëÿåòñÿ ïðåäâàðåííîé íîðìàëüíîé ôîðìîé,I ðàâíîñèëüíà èñõîäíîé ôîðìóëå ϕ.ÎÁÙÀß ÑÕÅÌÀ ÌÅÒÎÄÀ ÐÅÇÎËÞÖÈÉÈñõîäíàÿôîðìóëà-ϕÑÑÔϕ2Ñèñòåìàäèçúþíêòîâ¬ϕ?ÏÍÔϕ1?SϕÎòðèöàíèå-Ðåçîëþòèâíûé âûâîäïóñòîãî äèçúþíêòà èç ñèñòåìû SϕÑÊÎËÅÌÎÂÑÊÈÅ ÑÒÀÍÄÀÐÒÍÛÅ ÔÎÐÌÛÎïðåäåëåíèåÏðåäâàðåííàÿ íîðìàëüíàÿ ôîðìà âèäàϕ = ∀xi1 ∀xi2 .
. . ∀xim M(xi1 , xi2 , . . . , xim ),â êîòîðîé êâàíòîðíàÿ ïðèñòàâêà íå ñîäåðæèò êâàíòîðîâ ∃,íàçûâàåòñÿ ñêîëåìîâñêîé ñòàíäàðòíîé ôîðìîé (ÑÑÔ) .Ïðèìåðû ÑÑÔ∀x1 ∀y2 (P(x1 ) & (¬P(f (x1 )) ∨ R(x1 , g (x1 ))) & ¬R(x1 , y2 ) )R(c1 , f (c1 , c2 )) ∨ P(c2 )ÑÊÎËÅÌÎÂÑÊÈÅ ÑÒÀÍÄÀÐÒÍÛÅ ÔÎÐÌÛÒåîðåìà î ÑÑÔÄëÿ ëþáîé çàìêíóòîé ôîðìóëû ϕ ñóùåñòâóåò òàêàÿñêîëåìîâñêàÿ ñòàíäàðòíàÿ ôîðìà ψ, ÷òîϕ âûïîëíèìàÄîêàçàòåëüñòâî⇐⇒ψ âûïîëíèìà.Âîñïîëüçóåìñÿ ëåììîé îá óäàëåíèè êâàíòîðîâ ñóùåñòâîâàíèÿ .ÑÊÎËÅÌÎÂÑÊÈÅ ÑÒÀÍÄÀÐÒÍÛÅ ÔÎÐÌÛËåììà îá óäàëåíèè êâàíòîðîâ ñóùåñòâîâàíèÿÏóñòü ϕ = ∀x1∀x2 .
. . ∀xk ∃xk+1 ϕ0(x1, x2, . . . , xk , xk+1) çàìêíóòàÿ(k)ôîðìóëà, k ≥ 0, è k -ìåñòíûé ôóíêöèîíàëüíûéñèìâîë f íå ñîäåðæèòñÿ â ôîðìóëå ϕ.Òîãäà ôîðìóëà ϕ âûïîëíèìà â òîì è òîëüêî òîì ñëó÷àå,êîãäà âûïîëíèìà ôîðìóëà(k)ψ = ∀x1 ∀x2 . . . ∀xk ϕ0 (x1 , x2 , . . . , xk , fÄîêàçàòåëüñòâî ëåììû.(x1 , x2 , . . . , xk )).(⇐ ) Ïóñòü I ìîäåëü äëÿ ψ.Òîãäà äëÿ ëþáîãî íàáîðà d1, d2, . .
. , dk ∈ DI èìååò ìåñòîI |= ϕ0 [d1 , d2 , . . . , dk , f (k) (d1 , d2 , . . . , dk )],ò. å. äëÿ ëþáîãî íàáîðà d1, d2, . . . , dk ∈ DI ñóùåñòâóåò òàêîéýëåìåíò dk+1 = f (k)(d1, d2, . . . , dk ), ÷òîI |= ϕ0 [d1 , d2 , . . . , dk , dk+1 ].Ýòî îçíà÷àåò, ÷òî I |= ∀x1∀x2 . . . ∀xk ∃xk+1ϕ0.ÑÊÎËÅÌÎÂÑÊÈÅ ÑÒÀÍÄÀÐÒÍÛÅ ÔÎÐÌÛÄîêàçàòåëüñòâî ëåììû îá óäàëåíèè∃.(⇒ ) Ïóñòü I ìîäåëü äëÿ ϕ. Òîãäà äëÿ ëþáîãî íàáîðàd1 , d2 , .
. . , dk ∈ DI ñóùåñòâóåò òàêîé ýëåìåíò dk+1 ∈ DI , ÷òîI |= ϕ0 [d1 , d2 , . . . , dk , dk+1 ].Ïóñòü f : DIk → DI ýòî íåêîòîðàÿ ôóíêöèÿ, âû÷èñëÿþùàÿäëÿ êàæäîãî íàáîðà d1, d2, . . . , dk ∈ DI òàêîé ýëåìåíòdk+1 = f(d1 , d2 , . . . , dk ), ÷òîI |= ϕ0 [d1 , d2 , .
. . , dk , dk+1 ].Ðàññìîòðèì èíòåðïðåòàöèþ I 0, êîòîðàÿ îòëè÷àåòñÿ îò I òîëüêîòåì, ÷òî îöåíêîé ôóíêöèîíàëüíîãî ñèìâîëà f (k) ÿâëÿåòñÿôóíêöèÿ f .Òîãäà äëÿ ëþáîãî íàáîðà d1, d2, . . . , dk âåðíîI 0 |= ϕ0 [d1 , d2 , . . . , dk , f (k) (d1 , d2 , . . . , dk )]. (ïî÷åìó? )Ýòî îçíà÷àåò, ÷òîI 0 |= ∀x1 ∀x2 . . . ∀xk ϕ0 (x1 , x2 , . . . , xk , f (k) (x1 , x2 , . . . , xk )).ÑÊÎËÅÌÎÂÑÊÈÅ ÑÒÀÍÄÀÐÒÍÛÅ ÔÎÐÌÛÏðîäîëæåíèå äîêàçàòåëüñòâà òåîðåìû îá ÑÑÔÓäàëÿåì ïî î÷åðåäè êâàíòîðû ñóùåñòâîâàíèÿ ñ ïîìîùüþëåììû.ϕ = ∀x1 . . .
∀xk ∃xk+1 ∀xk+2 . . . ∀xm ∃xm+1 . . .ϕ0 (x1 , . . . , xk , xk+1 , xk+2 . . . xm , xm+1 , . . . )ϕ0 = ∀x1 . . . ∀xk ∀xk+2 . . . ∀xm ∃xm+1 . . .ϕ0 (x1 , . . . , xk , f (x1 , . . . , xk ), xk+2 . . . xm , xm+1 , . . . )ϕ00 = ∀x1 . . . ∀xk ∀xk+2 . . . ∀xm . . .ϕ0 (x1 , . . . , xk , f (x1 , . . . , xk ), xk+2 . . . xm , g (x1 , .
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
