Лекции - Математическая логика

Подождите немного. Документ загружается.

IV. Åñëè ρ – ðåôëåêñèâíîå, ìîíîòîííîå è òðàíçèòèâíîå îòíî-

øåíèå, òî ñëåäóþùèå äâà óñëîâèÿ ýêâèâàëåíòíû:

1) (Ã)

Ã, ; Ã,

ÀÂ À Â

ρρ¬

ρ¬

⎛⎞

⎜⎟

⎝⎠

;

2) (Δ

) (Δ

)

;

(( \{ }) ( \ { }))

AAA

Δρ Δρ¬

Δ∪Δ ρ¬

⎛⎞

⎜⎟

⎝⎠

Òàêèì îáðàçîì, äëÿ êàæäîãî êîñâåííîãî ïðàâèëà â îïðåäåëå-

íèè ïîíÿòèÿ ñîõðàíåíèÿ êîñâåííûì ïðàâèëîì îòíîøåíèÿ ρ òàêæå

ìîæíî çàìåíèòü îïðåäåëÿþùåå óñëîâèå íà ýêâèâàëåíòíîå.

✰

Êàê óæå îòìå÷àëîñü, ìíîãèå âàæíûå òåîðåìû î

ñâîéñòâàõ îòíîøåíèÿ N

-âûâîäèìîñòè èìåþò

ñëåäóþùèé âèä: «Äëÿ ëþáîãî ìíîæåñòâà ôîð-

ìóë Ã è ëþáîé N

-âûâîäèìîé èç Ã ôîðìóëû F

ìíîæåñòâî ôîðìóë Ã íàõîäèòñÿ â îòíîøåíèè ρ ñ F», ãäå ρ – íåêî-

òîðîå îòíîøåíèå ìåæäó êîíå÷íûìè ìíîæåñòâàìè ôîðìóë è ôîð-

ìóëàìè. Ñèìâîëè÷åñêè óòâåðæäåíèÿ òàêîãî âèäà ìîæíî çàïèñû-

âàòü ñëåäóþùèì îáðàçîì:

(Ã) (F) (Ã



F → ÃρF).

Â ñèëó èíäóêòèâíîãî îïðåäåëåíèÿ äåðåâà N

-âûâîäà, óòâåðæ-

äåíèÿ óêàçàííîãî âèäà ìîæíî äîêàçûâàòü ñ ïîìîùüþ îáû÷íîãî

ïðèíöèïà ìàòåìàòè÷åñêîé èíäóêöèè ïî íàòóðàëüíîìó ïàðàìåòðó –

âûñîòå äåðåâà N

-âûâîäà. Îäíàêî òàêèå äîêàçàòåëüñòâà ÿâëÿþòñÿ

âåñüìà ãðîìîçäêèìè. Íàøà áëèæàéøàÿ öåëü – ñôîðìóëèðîâàòü è

äîêàçàòü óòâåðæäåíèå, íàçûâàåìîå ïðèíöèïîì èíäóêöèè äëÿ

-âûâîäîâ âî âòîðîé ôîðìå, èñïîëüçîâàíèå êîòîðîãî ïîçâîëÿåò

ïîëó÷èòü áîëåå ïðîñòûå äîêàçàòåëüñòâà òàêîãî âèäà òåîðåì.

Íî ñíà÷àëà ñôîðìóëèðóåì è äîêàæåì ïðèíöèï èíäóêöèè äëÿ

-âûâîäîâ â ïåðâîé ôîðìå. Åãî ñóòü çàêëþ÷àåòñÿ â ñëåäóþùåì.

S Ïðè îïðåäåëåííûõ óñëîâèÿõ íà îòíîøåíèå ρ ìíîæåñòâî çåëåíûõ ëè-

ñòüåâ âñÿêîãî äåðåâà N

-âûâîäà íàõîäèòñÿ â îòíîøåíèè ρ ñ åãî êîðíåì.

! ÒÅÎÐÅÌÀ (ïðèíöèï èíäóêöèè äëÿ N

-âûâîäîâ, ïåðâàÿ ôîðìà).

Ïóñòü ρ – îòíîøåíèå ìåæäó êîíå÷íûìè ìíîæåñòâàìè ôîðìóë è

ôîðìóëàìè.

Åñëè 1) îòíîøåíèå ρ ðåôëåêñèâíî è ìîíîòîííî,

è 2) âñå N

-ïðàâèëà ñîõðàíÿþò îòíîøåíèå ρ,

òî äëÿ ëþáûõ Δ, F è äëÿ ëþáîãî N

-Δ-F-âûâîäà âûïîëíÿåòñÿ ΔρF.

Принцип

индукции

для N

&выводов

Äîêàçàòåëüñòâî. Äîñòàòî÷íî äîêàçàòü âîçâðàòíîé èí-

äóêöèåé ïî íàòóðàëüíîìó ïàðàìåòðó k (âûñîòå äåðåâà) ñëåäóþùåå

óòâåðæäåíèå: êàêîâû áû íè áûëè íàòóðàëüíîå ÷èñëî k, ìíîæåñòâî

ôîðìóë Δ, ôîðìóëà F è äåðåâî N

-Δ-F-âûâîäà âûñîòû k, Δ íàõîäèòñÿ

â îòíîøåíèè ρ ñ F, ò. å.

(k) (

D) (Δ) (F) (

D =

& h(

D) = k → ΔρF)

èëè, êîðî÷å, (k) (

) (h(

) = k → ΔρF).

Áàçèñ èíäóêöèè. Ïóñòü

– N

-Δ-F-âûâîä âûñîòû 0, ò. å.

– ýòî ôîðìóëà F è Δ = {F}. Â ñèëó óñëîâèÿ 1 îòíîøåíèå ρ

ðåôëåêñèâíî, à çíà÷èò, ΔρF.

Øàã èíäóêöèè. Ïóñòü k – ïðîèçâîëüíîå íàòóðàëüíîå ÷èñëî.

Äîïóñòèì, ÷òî äëÿ ëþáûõ Δ è F è äëÿ ëþáîãî N

-Δ-F-âûâîäà,

âûñîòà êîòîðîãî íå ïðåâîñõîäèò k, èìååò ìåñòî ΔρF (ïðåäïîëîæå-

íèå èíäóêöèè).

Ïóñòü Δ – ïðîèçâîëüíîå ìíîæåñòâî ôîðìóë, F – ïðîèçâîëüíàÿ

ôîðìóëà è

– ïðîèçâîëüíûé N

-Δ-F-âûâîä, âûñîòà êîòîðîãî

ðàâíà k + 1. Äîêàæåì, ÷òî âûïîëíÿåòñÿ ΔρF. Ðàññìîòðèì âñå âîç-

ìîæíûå ñëó÷àè ïîñòðîåíèÿ äåðåâà

â ñîîòâåòñòâèè ñ èíäóêòèâ-

íûì îïðåäåëåíèåì N

-âûâîäà.

1. Ïóñòü

ïîëó÷åíî ïî êàêîìó-ëèáî ïðÿìîìó N

-ïðàâèëó

...

(n = 1, 2), ò. å.

...

ΔΔ

, ãäå F

, …, F

, F – íåêîòî-

ðûé íàáîð ôîðìóë, ñîîòâåòñòâóþùèé ýòîìó ïðàâèëó, è Δ = Δ

∪ …

... ∪ Δ

. Òîãäà âûñîòà êàæäîãî èç äåðåâüåâ

(i = 1, …, n) íå

ïðåâîñõîäèò k, à çíà÷èò, ïî ïðåäïîëîæåíèþ èíäóêöèè âûïîëíÿåò-

ñÿ Δ

ρF

, …, Δ

ρF

. Êðîìå òîãî, Δ

⊆ Δ äëÿ êàæäîãî i (i = 1, …, n).

Îòñþäà â ñèëó ìîíîòîííîñòè îòíîøåíèÿ ρ èìååì ΔρF

, …, ΔρF

Ïîñêîëüêó ïðàâèëà çàêëþ÷åíèÿ ñîõðàíÿþò îòíîøåíèå ρ, ïîëó÷à-

åì, ÷òî ΔρF.

2. Ïóñòü

ïîñòðîåíî ñ ïîìîùüþ êîñâåííîãî ïðàâèëà ⊃â, ò. å.

äëÿ íåêîòîðûõ ôîðìóë A è Â âûïîëíÿåòñÿ:

⊃

, F



A ⊃ B

è Δ = Δ

\ {A}. Òîãäà Δ

⊆ Δ ∪ {À}. Êðîìå òîãî, âûñîòà

ðàâíà k,

à çíà÷èò, ïî ïðåäïîëîæåíèþ èíäóêöèè Δ

ρÂ. Îòñþäà â ñèëó ìîíî-

òîííîñòè ρ ïîëó÷àåì, ÷òî Δ ∪ {A}ρB. Ïîñêîëüêó ïðàâèëî ⊃â ñîõðà-

íÿåò îòíîøåíèå ρ, èìååì Δρ(A ⊃ B), ò. å. ΔρF.

3. Ïóñòü

ïîñòðîåíî ñ ïîìîùüþ êîñâåííîãî ïðàâèëà ∨ó,

ò. å.

123

AB C C

ΔΔΔ

∨

DDD

, F



Ñ, à Δ = Δ

∪ (Δ

\ {A}) ∪ (Δ

\ {B}).

Òîãäà Δ

⊆ Δ, Δ

⊆ Δ ∪ {A}, Δ

⊆ Δ ∪ {B}. Êðîìå òîãî, âûñîòà êàæäîãî

èç äåðåâüåâ

∨

íå ïðåâîñõîäèò k, à çíà÷èò, ïî ïðåäïîëî-

æåíèþ èíäóêöèè Δ

ρ(À ∨ Â); Δ

ρC è Δ

ρÑ. Ñëåäîâàòåëüíî, â ñèëó

ìîíîòîííîñòè îòíîøåíèÿ ρ èìååì: Δρ(À ∨ Â); Δ ∪ {A}ρC è

Δ ∪ {Â}ρÑ. Îòñþäà, ïîñêîëüêó ïðàâèëî ∨ó ñîõðàíÿåò îòíîøåíèå ρ,

ïîëó÷àåì ΔρÑ, ò. å. ΔρF.

4. Ïóñòü

ïîñòðîåíî ñ ïîìîùüþ êîñâåííîãî ïðàâèëà ¬â,

ò. å.

ΔΔ

, F



¬À, Δ = (Δ

\ {A}) ∪ (Δ

\ {A}). Òîãäà

⊆ Δ ∪ {A} è Δ

⊆ Δ ∪ {À}. Êðîìå òîãî, âûñîòà êàæäîãî èç äåðåâüåâ

íå ïðåâîñõîäèò k, à çíà÷èò, ïî ïðåäïîëîæåíèþ èíäóê-

öèè Δ

ρÂ è Δ

ρ¬Â. Îòñþäà â ñèëó ìîíîòîííîñòè ρ ïîëó÷àåì, ÷òî

Δ ∪ {A}ρÂ è Δ ∪ {A}ρ¬Â. Òîãäà, ïîñêîëüêó ïðàâèëî ¬â ñîõðàíÿåò

îòíîøåíèå ρ, âûïîëíÿåòñÿ Δρ¬À, ò. å. ΔρF.

Èòàê, ñîãëàñíî èíäóêòèâíîìó îïðåäåëåíèþ äåðåâà N

-âûâîäà,

ìû ðàññìîòðåëè âñå âîçìîæíûå ñëó÷àè ïîñòðîåíèÿ

, ïîëó÷àÿ

êàæäûé ðàç ΔρF, ÷åì çàâåðøèëè øàã èíäóêöèè. Òàêèì îáðàçîì,

äëÿ ëþáîãî íàòóðàëüíîãî k è ëþáîãî N

-Δ-F-âûâîäà âûñîòû k âû-

ïîëíÿåòñÿ ΔρF. 

★ Çàìåòèì, ÷òî åñëè îïðåäåëåíèå ïîíÿòèÿ ñîõðàíåíèÿ N

-ïðàâèëà-

ìè îòíîøåíèÿ ρ èçìåíèòü â ñîîòâåòñòâèè ñ óòâåðæäåíèÿìè I–IV

äàííîãî ïàðàãðàôà, îòìå÷åííûìè

★, òî â ôîðìóëèðîâêå ïðèíöèïà

èíäóêöèè äëÿ N

-âûâîäîâ èç óñëîâèÿ 1 ìîæíî óäàëèòü òðåáîâàíèå

ìîíîòîííîñòè îòíîøåíèÿ ρ.

✰

Ïóñòü ρ

è ρ

– îòíîøåíèÿ ìåæäó êîíå÷íûìè ìíîæåñòâàìè ôîð-

ìóë è ôîðìóëàìè. Áóäåì ãîâîðèòü, ÷òî îòíîøåíèå ρ

ñîãëàñîâàíî

ñ îòíîøåíèåì ρ

, åñëè äëÿ ëþáîãî ìíîæåñòâà ôîðìóë Ã è ëþáîé

ôîðìóëû F, òàêèõ ÷òî Ãρ

F, âûïîëíÿåòñÿ Ãρ

F, ò. å. åñëè

(Ã) (F) (Ãρ

F → Ãρ

F).

Â ÷àñòíîñòè, îòíîøåíèå N

-âûâîäèìîñòè



ñîãëàñîâàíî ñ îò-

íîøåíèåì ρ, åñëè äëÿ ëþáîãî ìíîæåñòâà ôîðìóë Ã è ëþáîé

-âûâîäèìîé èç Ã ôîðìóëû F âûïîëíÿåòñÿ ÃρF, ò. å. åñëè

(Ã) (F) (Ã



F → ÃρF).

Íàïðèìåð, îòíîøåíèå N

-âûâîäèìîñòè ñîãëàñîâàíî ñ îòíîøå-

íèåì N

-âûâîäèìîñòè, ïîñêîëüêó ðàíåå áûëî äîêàçàíî:

(Ã) (F) (Ã



F → Ã



F).

Ïîçæå áóäåò äîêàçàíî, ÷òî îòíîøåíèÿ N

-âûâîäèìîñòè è

-âûâîäèìîñòè ñîãëàñîâàíû ñ îòíîøåíèåì ñåìàíòè÷åñêîãî ñëå-

äîâàíèÿ:

(Ã) (F) (Ã



F → Ã



F).

Òåîðåìû âèäà «Äëÿ ëþáîãî ìíîæåñòâà ôîðìóë Ã è ëþáîé

-âûâîäèìîé èç Ã ôîðìóëû F ìíîæåñòâî ôîðìóë Ã íàõîäèòñÿ â

îòíîøåíèè ρ ñ F», èñïîëüçóÿ íîâóþ òåðìèíîëîãèþ, ìîæíî ïåðå-

ôîðìóëèðîâàòü òàê: «Îòíîøåíèå N

-âûâîäèìîñòè ñîãëàñîâàíî ñ îò-

íîøåíèåì ρ». Êàê óæå îòìå÷àëîñü, äëÿ äîêàçàòåëüñòâà òàêîãî âèäà

óòâåðæäåíèé î÷åíü ïîëåçíîé ÿâëÿåòñÿ ñëåäóþùàÿ òåîðåìà.

! ÒÅÎÐÅÌÀ (ïðèíöèï èíäóêöèè äëÿ N

-âûâîäîâ, âòîðàÿ ôîðìà). Ïóñòü

ρ – îòíîøåíèå ìåæäó êîíå÷íûìè ìíîæåñòâàìè ôîðìóë è ôîðìóëàìè.

Åñëè 1) îòíîøåíèå ρ ðåôëåêñèâíî è ìîíîòîííî,

è 2) âñå N

-ïðàâèëà ñîõðàíÿþò îòíîøåíèå ρ,

òî îòíîøåíèå N

-âûâîäèìîñòè ñîãëàñîâàíî ñ îòíîøåíèåì ρ,

ò. å. (Ã) (F) (Ã



F → ÃρF).

Äîêàçàòåëüñòâî. Ïóñòü Ã è F – òàêèå, ÷òî Ã



F, à

åñòü N

-Δ-F-âûâîä òàêîé, ÷òî Δ ⊆ Ã. Òîãäà, ñîãëàñíî ïðèíöèïó

èíäóêöèè äëÿ N

-âûâîäîâ â ïåðâîé ôîðìå, ΔρF. Îòñþäà â ñèëó

ìîíîòîííîñòè ρ ñëåäóåò, ÷òî ÃρF. 

Çàìå÷àíèå 2. Ìîæíî äîêàçàòü, ÷òî â îáåèõ ôîðìàõ ïðèíöèïà

èíäóêöèè äëÿ N

-âûâîäîâ óñëîâèå 1 ìîæíî çàìåíèòü íà óñëîâèå

1': îòíîøåíèå ρ êâàçèðåôëåêñèâíî. 

S Ïðèíöèï èíäóêöèè äëÿ N

-âûâîäîâ (âòîðàÿ ôîðìà) ïðåäîñòàâ-

ëÿåò äîñòàòî÷íîå óñëîâèå ñîãëàñîâàííîñòè îòíîøåíèÿ N

-âûâîäèìî-

ñòè



ñ îòíîøåíèåì ρ.

Âîçíèêàåò âîïðîñ, íàñêîëüêî óäîáíî ïîëüçîâàòüñÿ ýòèì äîñòàòî÷-

íûì óñëîâèåì, ò. å. íàñêîëüêî ïðîñòî ïðîâåðèòü, ÷òî îòíîøåíèå ρ

óäîâëåòâîðÿåò óñëîâèÿì 1 è 2 èç ïðèíöèïà èíäóêöèè äëÿ N

-âûâîäîâ.

Ïðîâåðêà óñëîâèÿ 1 ïðàêòè÷åñêè íå ïðåäñòàâëÿåò íèêàêîé ñëîæíîñòè.

Êàê ïðàâèëî, íåòðóäíî ïðîâåðèòü è óñëîâèå 2, èñïîëüçóÿ îïðåäåëåíèå

ïîíÿòèÿ ñîõðàíåíèÿ N

-ïðàâèëàìè îòíîøåíèÿ ρ. Îäíàêî ñëåäóþùåå óò-

âåðæäåíèå ïîçâîëÿåò ñäåëàòü ýòó ïðîâåðêó åùå áîëåå ïðîñòîé.

Ãîâîðÿ îá óñëîâíûõ ïðàâèëàõ, äëÿ ïðîñòîòû èçëîæåíèÿ îãðà-

íè÷èìñÿ ñõåìàìè âèäà

]

[

(ò. å. ñ îäíîé áåçóñëîâíîé è îäíîé

óñëîâíîé ïîñûëêàìè).

ÓÒÂÅÐÆÄÅÍÈÅ (êðèòåðèé ñîõðàíåíèÿ îòíîøåíèÿ ρ). Ïóñòü ρ –

ðåôëåêñèâíîå, ìîíîòîííîå è òðàíçèòèâíîå îòíîøåíèå ìåæäó ìíî-

æåñòâàìè ôîðìóë è ôîðìóëàìè.

1. Ïðÿìàÿ ñõåìà çàêëþ÷åíèé

...

ñîõðàíÿåò îòíîøåíèå ρ

òîãäà è òîëüêî òîãäà, êîãäà äëÿ ëþáîãî íàáîðà ôîðìóë F

, ..., F

, F,

ñîîòâåòñòâóþùåãî ýòîé ñõåìå, {F

, ..., F

}ρF (÷òî áóäåì çàïèñûâàòü

òàê: {

, …,

}ρ

2. Åñëè ïðàâèëà ⊃â è ⊃ó ñîõðàíÿþò ρ, òî ñëåäóþùèå óñëîâèÿ

ýêâèâàëåíòíû:

à) êîñâåííàÿ ñõåìà

]

[

ñîõðàíÿåò îòíîøåíèå ρ;

á) ïðÿìàÿ ñõåìà

⊃

EH G

ñîõðàíÿåò îòíîøåíèå ρ;

â) äëÿ ëþáûõ ôîðìóë Å, F, G è H, ñîîòâåòñòâóþùèõ ñõåìå èç

ï. (á), {E, H ⊃ G}ρF ({

⊃

}ρ

Äîêàçàòåëüñòâî.

1. Ïóñòü ñõåìà

...

ñîõðàíÿåò îòíîøåíèå ρ è ïóñòü F

, …, F

F – ïðîèçâîëüíûé íàáîð ôîðìóë, ñîîòâåòñòâóþùèé ýòîé ñõåìå.

Äîêàæåì, ÷òî {F

, …, F

}ρF. Îáîçíà÷èì ÷åðåç Ã ìíîæåñòâî ôîðìóë

, …, F

}. Òîãäà â ñèëó ðåôëåêñèâíîñòè è ìîíîòîííîñòè ρ èìååì

ÃρF

, …, ÃρF

. Îòñþäà, ïîñêîëüêó ñõåìà

...

ñîõðàíÿåò ρ, ïîëó-

÷àåì, ÷òî ÃρF, ò. å. {F

, …, F

}ρF.

Äîêàæåì îáðàòíîå. Äîïóñòèì, ÷òî äëÿ ëþáîãî íàáîðà ôîðìóë

, …, F

, F, ñîîòâåòñòâóþùåãî ñõåìå

...

, {F

, …, F

}ρF. Ïóñòü

Ã – ïðîèçâîëüíîå ìíîæåñòâî ôîðìóë òàêîå, ÷òî ÃρF

, …, ÃρF

Òîãäà, ïîñêîëüêó ρ òðàíçèòèâíî, èç óñëîâèé ÃρF

, …, ÃρF

, …, F

}ρF ïîëó÷àåì, ÷òî ÃρF.

2. Ïåðåéäåì ê êîñâåííûì ñõåìàì. Ñíà÷àëà äîêàæåì ýêâèâà-

ëåíòíîñòü ïðåäëîæåíèé (à) è (á). Ïîñêîëüêó ïðàâèëà ⊃â è ⊃ó ñî-

õðàíÿþò ρ, òî Ã ∪ {H}ρG òîãäà è òîëüêî òîãäà, êîãäà Ãρ(H ⊃ G).

Ñëåäîâàòåëüíî, ýêâèâàëåíòíû è ñëåäóþùèå äâà óñëîâèÿ

EHG

Γρ Γ ρ

Γρ

;)

EHG

Γρ Γρ( ⊃

Γρ

à çíà÷èò, (à) ↔ (á).

Ýêâèâàëåíòíîñòü ïðåäëîæåíèé (á) è (â) âûòåêàåò èç ï. 1.



Ñîãëàñíî ï. 1 äîêàçàííîé òåîðåìû, íàïðèìåð, ïðàâèëî &â ñî-

õðàíÿåò îòíîøåíèå ρ òîãäà è òîëüêî òîãäà, êîãäà äëÿ ëþáûõ ôîð-

ìóë À è Â âûïîëíÿåòñÿ {À,Â}ρ(À & Â), ò. å.

(À) (Â) ({À, Â}ρ(À & Â)).

Çàìå÷àíèå 3. Ðàññóæäàÿ àíàëîãè÷íî òîìó, êàê ìû ðàññóæäàëè â

ï. 2, è ó÷èòûâàÿ, ÷òî ïðè äîêàçàòåëüñòâå öåïî÷êè (â) → (á) → (à)

èñïîëüçóåòñÿ òîëüêî òî, ÷òî ρ òðàíçèòèâíî è ïðàâèëî ⊃â ñîõðàíÿåò

ρ, ìîæíî äîêàçàòü ñëåäóþùåå.

Ïóñòü ρ – òðàíçèòèâíîå îòíîøåíèå, à ïðàâèëî ⊃â ñîõðàíÿåò ρ.

Òîãäà:

1) åñëè äëÿ ëþáûõ ôîðìóë À, Â, Ñ

{À ∨ Â, À ⊃ Ñ, Â ⊃ Ñ}ρÑ,

òî êîñâåííîå ïðàâèëî ∨ó ñîõðàíÿåò îòíîøåíèå ρ;

2) åñëè äëÿ ëþáûõ ôîðìóë À è Â

{À ⊃ Â, À ⊃ ¬Â

}ρ¬À,

òî êîñâåííîå ïðàâèëî ¬â ñîõðàíÿåò îòíîøåíèå ρ.

Òàêèì îáðàçîì, åñëè ïðàâèëî ⊃â ñîõðàíÿåò òðàíçèòèâíîå îò-

íîøåíèå ρ, òî äëÿ äîêàçàòåëüñòâà òîãî, ÷òî ïðàâèëà ∨ó è ¬â ñîõðà-

íÿþò îòíîøåíèå ρ, äîñòàòî÷íî äîêàçàòü, ÷òî âûïîëíÿþòñÿ ñîîò-

âåòñòâåííî óñëîâèÿ èç ï. 1 è 2 äàííîãî çàìå÷àíèÿ. 

Âåðíåìñÿ ê îáñóæäåíèþ ñâÿçè ìåæäó îòíîøå-

íèÿìè N

-âûâîäèìîñòè è N

-âûâîäèìîñòè, à

òàêæå ìåæäó êëàññàìè N

-âûâîäèìûõ è N

-âû-

âîäèìûõ ôîðìóë.

Теорема Гливенко

Íàì óæå èçâåñòíî, ÷òî åñëè ôîðìóëà N

-âûâîäèìà, òî îíà

-âûâîäèìà. Îáðàòíîå íåâåðíî, ÷òî áóäåò äîêàçàíî ïîçæå. Îäíà-

êî ñïðàâåäëèâî ñëåäóþùåå óòâåðæäåíèå, èçâåñòíîå êàê òåîðåìà

Ãëèâåíêî

: åñëè ôîðìóëà N

-âûâîäèìà, òî åå äâîéíîå îòðèöàíèå

-âûâîäèìî.

Ñèìâîëè÷åñêè ýòî óòâåðæäåíèå ìîæíî çàïèñàòü òàê:

(F) (



F →



¬¬F).

Ñíà÷àëà äîêàæåì áîëåå ñèëüíîå óòâåðæäåíèå. Ïðè ýòîì áóäåì

èñïîëüçîâàòü ñëåäóþùåå îáîçíà÷åíèå: ¬¬Ã  {¬¬À | À ∈ Ã}.

ÓÒÂÅÐÆÄÅÍÈÅ. Äëÿ ëþáîé ôîðìóëû F è ëþáîãî ìíîæåñòâà

ôîðìóë Ã, åñëè Ã



F , òî ¬¬Ã



¬¬F.

Ñèìâîëè÷åñêè ýòî óòâåðæäåíèå ìîæíî çàïèñàòü òàê:

(Ã) (F) (Ã



F → ¬¬Ã



¬¬F).

Äîêàçàòåëüñòâî. Âîñïîëüçóåìñÿ ïðèíöèïîì èíäóêöèè

äëÿ N

-âûâîäîâ (âî âòîðîé ôîðìå). Â êà÷åñòâå îòíîøåíèÿ ρ âîçüìåì

îòíîøåíèå, çàäàâàåìîå ñëåäóþùèì îáðàçîì:

ÃρF

def

←⎯⎯→

¬¬Ã



¬¬F.

Äîêàæåì, ÷òî (Ã) (F) (Ã



F → ÃρF). Ñîãëàñíî ïðèíöèïó èí-

äóêöèè äëÿ N

-âûâîäîâ, äîñòàòî÷íî äîêàçàòü, ÷òî îòíîøåíèå ρ ðåô-

ëåêñèâíî è ìîíîòîííî, à âñå N

-ïðàâèëà ñîõðàíÿþò îòíîøåíèå ρ.

Ðåôëåêñèâíîñòü è ìîíîòîííîñòü îòíîøåíèÿ ρ ñëåäóåò èç ðåô-

ëåêñèâíîñòè è ìîíîòîííîñòè îòíîøåíèÿ



ñîîòâåòñòâåííî.

Äëÿ äîêàçàòåëüñòâà òîãî, ÷òî âñå ïðÿìûå N

-ïðàâèëà ñîõðàíÿ-

þò îòíîøåíèå ρ, â ñèëó êðèòåðèÿ ñîõðàíåíèÿ îòíîøåíèÿ ρ (ï. 1),

äîñòàòî÷íî ïðîâåðèòü, ÷òî äëÿ ëþáûõ ôîðìóë A è B âûïîëíÿåòñÿ:

(&)

AB A

¬¬ ¬¬

;

(&)

AB B

¬¬ ¬¬

;

,(&)

AB AB

¬¬ ¬¬ ¬¬

;

()

AAB

¬¬ ¬¬ ∨

;

()

BAB

¬¬ ¬¬ ∨

;

,( )

AAB B

¬¬ ¬¬ ⊃ ¬¬

;

Â. È. Ãëèâåíêî (1897–1940) – ñîâåòñêèé ìàòåìàòèê, ëîãèê.

AA B

¬¬ ¬¬¬ ¬¬

;

¬¬¬¬ ¬¬

Âñå ýòè óòâåðæäåíèÿ ìîæíî ëåãêî äîêàçàòü ïîñòðîåíèåì ñîîò-

âåòñòâóþùèõ äåðåâüåâ N

-âûâîäà, ÷òî îñòàâëÿåì ÷èòàòåëþ â êà÷å-

ñòâå óïðàæíåíèÿ.

Íåòðóäíî ïðîâåðèòü, ÷òî êîñâåííûå ïðàâèëà òàêæå ñîõðàíÿþò

îòíîøåíèå ρ, à èìåííî, äëÿ ëþáûõ À, Â, Ñ è Ã:

Ã,

Ã()

¬¬ ¬¬ ¬¬

¬¬ ¬¬ ⊃



;

Ã, ; Ã,

AB A B

¬¬ ¬¬ ¬¬ ¬¬ ¬¬ ¬¬¬

¬¬ ¬¬¬





;

Ã, ; Ã,

Ã, ( )

AC BC

AB C

¬¬ ¬¬ ¬¬ ¬¬ ¬¬ ¬¬

¬¬ ¬¬ ∨ ¬¬





Äîêàæåì, ê ïðèìåðó, ÷òî ïðàâèëî ⊃â ñîõðàíÿåò îòíîøåíèå ρ,

ò. å. óòâåðæäåíèå 7. Äîïóñòèì, ÷òî ¬¬Ã,¬¬À



¬¬Â. Ïóñòü

¬¬Δ ¬¬

¬¬

(ãäå Δ ⊆ Ã) åñòü íåêîòîðîå äåðåâî N

-âûâîäà ñ êîðíåì

¬¬Â è ìíîæåñòâîì çåëåíûõ ëèñòüåâ, ñîäåðæàùåìñÿ â ìíîæåñòâå

¬¬Ã ∪ {¬¬À}. Èñïîëüçóÿ ýòî äåðåâî âûâîäà, ïîñòðîèì äåðåâî

-âûâîäà ñ êîðíåì ¬¬(À ⊃ Â), ìíîæåñòâî çåëåíûõ ëèñòüåâ êîòî-

ðîãî ¬¬Δ ñîäåðæèòñÿ â ìíîæåñòâå ¬¬Ã:

(4)

(3)

(2)

(1)

[] [ ]

[( )]

[]

[( )]

()

ÀB

⊃

¬⊃

¬¬Δ ¬¬

⊃

¬⊃

¬¬¬

¬¬ ⊃

Òàêèì îáðàçîì, äîêàçàíî, ÷òî ¬¬Ã



¬¬(À ⊃ Â).

Äîêàçàòåëüñòâî îñòàëüíûõ ïóíêòîâ ïîñòðîåíèåì ñîîòâåòñòâóþ-

ùèõ äåðåâüåâ N

-âûâîäà îñòàâëÿåì ÷èòàòåëþ â êà÷åñòâå ïîëåçíîãî

è íåñëîæíîãî óïðàæíåíèÿ.



Êàê ñëåäñòâèå äîêàçàííîé òåîðåìû, ïðè ïóñòîì ìíîæåñòâå Ã

ïîëó÷àåì èçâåñòíóþ òåîðåìó, îòðàæàþùóþ ñâÿçü ìåæäó êëàññàìè

-âûâîäèìûõ è N

-âûâîäèìûõ ôîðìóë.

! ÒÅÎÐÅÌÀ (Ãëèâåíêî). Äëÿ ëþáîé ôîðìóëû ßËÂ, åñëè ýòà ôîð-

ìóëà N

-âûâîäèìà, òî N

-âûâîäèìî åå äâîéíîå îòðèöàíèå, ò. å.

(F) (



F →



¬¬F).

Çàìå÷àíèå 4. Äîêàçàòåëüñòâî äâóõ ïîñëåäíèõ òåîðåì èìååò

êîíñòðóêòèâíûé õàðàêòåð, ÷òî ïîçâîëÿåò ïîñòðîèòü àëãîðèòì,

êîòîðûé äëÿ ëþáûõ ôîðìóëû F è ìíîæåñòâà ôîðìóë Δ âñÿêèé

-Δ-F- âûâîä ïåðåðàáàòûâàåò â N

-¬¬Δ-¬¬F-âûâîä (â ÷àñòíîñòè,

ïðè ïóñòîì Δ).



Âåñüìà çàìå÷àòåëüíûì ÿâëÿåòñÿ åùå îäíî ñëåäñòâèå äîêàçàí-

íîãî âûøå óòâåðæäåíèÿ.

ÑËÅÄÑÒÂÈÅ. Äëÿ ëþáîãî ìíîæåñòâà ôîðìóë Ã è ëþáîé ôîð-

ìóëû F:

1) Ã



¬F òîãäà è òîëüêî òîãäà, êîãäà Ã



¬F;



¬F òîãäà è òîëüêî òîãäà, êîãäà



¬F.

Äîêàçàòåëüñòâî.

1. Î÷åâèäíî, åñëè Ã



¬F, òî Ã



¬F. Äîêàæåì îáðàòíîå.

Ïóñòü Ã



¬F. Òîãäà, ñîãëàñíî äîêàçàííîìó âûøå óòâåðæäåíèþ,

¬¬Ã



¬¬¬F. Êðîìå òîãî, ¬¬¬F



¬F. Äåéñòâèòåëüíî, ñîîòâåò-

ñòâóþùåå äåðåâî N

-âûâîäà èìååò ñëåäóþùèé âèä:

â(2)

â(1)

[][ ]

¬¬¬

¬¬

Ñëåäîâàòåëüíî, â ñèëó òðàíçèòèâíîñòè îòíîøåíèÿ N

-âûâîäè-

ìîñòè, ¬¬Ã



¬F. Êðîìå òîãî, Ã



¬¬Ã, ïîñêîëüêó À



¬¬À

äëÿ ëþáîé ôîðìóëû À. Òàêèì îáðàçîì, Ã



¬F.

2. Óòâåðæäåíèå ï. 2 ïîëó÷àåòñÿ èç óòâåðæäåíèÿ ï. 1 ïðè ïóñòîì

ìíîæåñòâå Ã.



§ 2.7. Õàðàêòåðèñòèêè ñèñòåì§ 2.7. Õàðàêòåðèñòèêè ñèñòåì

§ 2.7. Õàðàêòåðèñòèêè ñèñòåì

åñòåñòâåííîãî âûâîäàåñòåñòâåííîãî âûâîäà

åñòåñòâåííîãî âûâîäà

Â ïðåäûäóùèõ ïàðàãðàôàõ áûëè ïîñòðîåíû äâå

îñíîâíûå ñèñòåìû åñòåñòâåííîãî âûâîäà: N

è N

. Âîçíèêàåò

öåëûé ðÿä âîïðîñîâ, ñâÿçàííûõ ñî ñâîéñòâàìè ýòèõ ñèñòåì, îò-

âåòû íà êîòîðûå òàê èëè èíà÷å õàðàêòåðèçóþò îòíîøåíèÿ N

- è

-âûâîäèìîñòè, êëàññû N

- è N

-âûâîäèìûõ ôîðìóë. Ïðåæäå

÷åì ïåðå÷èñëèòü ýòè âîïðîñû è ââåñòè õàðàêòåðèñòèêè ñèñòåì

åñòåñòâåííîãî âûâîäà, ðàñøèðèì êëàññ ðàññìàòðèâàåìûõ

ñèñòåì.

Íàðÿäó ñ ñèñòåìàìè N

è N

áóäåì ðàññìàòðèâàòü ñèñòåìû, êî-

òîðûå ïîëó÷àþòñÿ èç ýòèõ ñèñòåì çàìåíîé íà íîâûå èëè óäàëåíè-

åì íåêîòîðûõ èç èõ ïðàâèë, à òàêæå äîáàâëåíèåì íîâûõ ïðàâèë.

Äëÿ îáîçíà÷åíèÿ ïðîèçâîëüíûõ ñèñòåì èç ðàñøèðåííîãî êëàññà

áóäåì èñïîëüçîâàòü ñèìâîëû N, N

, N

. Äëÿ òàêèõ ñèñòåì îñíîâ-

íûå îïðåäåëåíèÿ (N-Δ-F-âûâîäà, îòíîøåíèÿ N-âûâîäèìîñòè, ñî-

õðàíåíèÿ N-ïðàâèëîì îòíîøåíèÿ ρ, ñîãëàñîâàííîñòè îòíîøåíèÿ

N-âûâîäèìîñòè ñ îòíîøåíèåì ρ è ò. ï.) ôîðìóëèðóþòñÿ àíàëîãè÷-

íî òîìó, êàê ýòî ñäåëàíî äëÿ ñèñòåì N

è N

(ñ ó÷åòîì èçìåíåíèÿ

ìíîæåñòâà ïðàâèë). Êðîìå òîãî, äëÿ ïðîèçâîëüíîé ñèñòåìû åñòå-

ñòâåííîãî âûâîäà N ìîæíî ñôîðìóëèðîâàòü è äîêàçàòü ïðèíöèï

èíäóêöèè äëÿ N-âûâîäîâ àíàëîãè÷íî òîìó, êàê ýòî ñäåëàíî äëÿ

ñèñòåì N

è N

S Â ýòîì ïàðàãðàôå áóäóò ðàññìîòðåíû ñëåäóþùèå õàðàêòåðèñòè-

êè ñèñòåì åñòåñòâåííîãî âûâîäà:

1) íåïðîòèâîðå÷èâîñòü;

2) ñåìàíòè÷åñêàÿ êîððåêòíîñòü;

3) ñåìàíòè÷åñêàÿ ïîëíîòà (èëè ïîëíîòà îòíîñèòåëüíî êëàññà

òàâòîëîãèé);

4) ñèíòàêñè÷åñêàÿ ïîëíîòà (èëè äåäóêòèâíàÿ ïîëíîòà);

5) íåçàâèñèìîñòü ïðàâèë çàêëþ÷åíèÿ.

Ïóñòü N – ïðîèçâîëüíàÿ ñèñòåìà åñòåñòâåííî-

ãî âûâîäà.

Ñèñòåìó åñòåñòâåííîãî âûâîäà N íàçûâàþò

ïðîòèâîðå÷èâîé ñèñòåìîé, åñëè ñóùåñòâóåò ôîð-

ìóëà F òàêàÿ, ÷òî



F è



¬F, è íåïðîòèâîðå-

÷èâîé, åñëè òàêîé ôîðìóëû íå ñóùåñòâóåò.

Непротиворечивость

систем естественного

вывода