Лекции 2-11. Математическая логика (до колка) (Лекции 2014), страница 8

PDF-файл Лекции 2-11. Математическая логика (до колка) (Лекции 2014), страница 8 Математическая логика и логическое программирование (53796): Лекции - 8 семестрЛекции 2-11. Математическая логика (до колка) (Лекции 2014) - PDF, страница 8 (53796) - СтудИзба2019-09-192019-09-19zzyxelСтудИзба

Лекции 2014229

Описание файла

Файл "Лекции 2-11. Математическая логика (до колка)" внутри архива находится в папке "Лекции 2014". PDF-файл из архива "Лекции 2014", который расположен в категории "". Всё это находится в предмете "математическая логика и логическое программирование" из 8 семестр, которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .

Просмотр PDF-файла онлайн

Текст 8 страницы из PDF

ϕ[ψ] = ψ. Î÷åâèäíî.ÒÅÎÐÅÌÀ Î ÐÀÂÍÎÑÈËÜÍÎÉ ÇÀÌÅÍÅÈíäóêòèâíûé ïåðåõîä. ϕ[ψ] = ∀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 ) )è òàê äàëåå...∀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 , .

Поделитесь ссылкой:

Ставлю 10/10
Все нравится, очень удобный сайт, помогает в учебе. Кроме этого, можно заработать самому, выставляя готовые учебные материалы на продажу здесь. Рейтинги и отзывы на преподавателей очень помогают сориентироваться в начале нового семестра. Спасибо за такую функцию. Ставлю максимальную оценку.

Лучшая платформа для успешной сдачи сессии
Познакомился со СтудИзбой благодаря своему другу, очень нравится интерфейс, количество доступных файлов, цена, в общем, все прекрасно. Даже сам продаю какие-то свои работы.

Студизба ван лав ❤
Очень офигенный сайт для студентов. Много полезных учебных материалов. Пользуюсь студизбой с октября 2021 года. Серьёзных нареканий нет. Хотелось бы, что бы ввели подписочную модель и сделали материалы дешевле 300 рублей в рамках подписки бесплатными.

Отличный сайт
Лично меня всё устраивает - и покупка, и продажа; и цены, и возможность предпросмотра куска файла, и обилие бесплатных файлов (в подборках по авторам, читай, ВУЗам и факультетам). Есть определённые баги, но всё решаемо, да и администраторы реагируют в течение суток.

Маленький отзыв о большом помощнике!
Студизба спасает в те моменты, когда сроки горят, а работ накопилось достаточно. Довольно удобный сайт с простой навигацией и огромным количеством материалов.

Студ. Изба как крупнейший сборник работ для студентов
Тут дофига бывает всего полезного. Печально, что бывают предметы по которым даже одного бесплатного решения нет, но это скорее вопрос к студентам. В остальном всё здорово.

Спасательный островок
Если уже не успеваешь разобраться или застрял на каком-то задание поможет тебе быстро и недорого решить твою проблему.

Всё и так отлично
Всё очень удобно. Особенно круто, что есть система бонусов и можно выводить остатки денег. Очень много качественных бесплатных файлов.

Отзыв о системе "Студизба"
Отличная платформа для распространения работ, востребованных студентами. Хорошо налаженная и качественная работа сайта, огромная база заданий и аудитория.

Отличный помощник
Отличный сайт с кучей полезных файлов, позволяющий найти много методичек / учебников / отзывов о вузах и преподователях.

Отлично помогает студентам в любой момент для решения трудных и незамедлительных задач
Хотелось бы больше конкретной информации о преподавателях. А так в принципе хороший сайт, всегда им пользуюсь и ни разу не было желания прекратить. Хороший сайт для помощи студентам, удобный и приятный интерфейс. Из недостатков можно выделить только отсутствия небольшого количества файлов.

Спасибо за шикарный сайт
Великолепный сайт на котором студент за не большие деньги может найти помощь с дз, проектами курсовыми, лабораторными, а также узнать отзывы на преподавателей и бесплатно скачать пособия.