Лекции - Математическая логика
Подождите немного. Документ загружается.
201
Íàêîíåö, åñëè ïðè èñïîëüçîâàíèè ïðàâèëà ∃ó îòêàçàòüñÿ îò
îãðàíè÷åíèé â ï. (Ð
4
), òî ïðèäåòñÿ ïðèçíàòü äåðåâîì âûâîäà ñëå-
äóþùåå äåðåâî ôîðìóë:
1
() [ ()]
()
xP x P x
Px
∃
. Òîãäà ïî ïðàâèëó ⊃â áóäåò
âûâîäèìîé ôîðìóëà ∃õ P(õ) ⊃ P(õ), êîòîðàÿ òàêæå íå ÿâëÿåòñÿ îá-
ùåçíà÷èìîé.
Äîêàçàòåëüñòâî òîãî, ÷òî ïðèâåäåííûå â êà÷åñòâå ïðèìåðîâ ôîð-
ìóëû íåîáùåçíà÷èìû, îñòàâëÿåì ÷èòàòåëþ êàê íåñëîæíîå, íî ïî-
ëåçíîå óïðàæíåíèå.
Çàìå÷àíèå 2. Õîòÿ Ð(x)
PN
/
>õ P(õ), ìîæíî äîêàçàòü, ÷òî äëÿ
ëþáîé ôîðìóëû À:
1)
PN
À òîãäà è òîëüêî òîãäà, êîãäà
PN
>õ À;
2)
PN
À òîãäà è òîëüêî òîãäà, êîãäà
PN
ÀR, ãäå ÀR – çàìûêàíèå
ôîðìóëû À (ñì. òåîðåìó î çàìûêàíèè â § 5.2).
Ðàññìîòðèì åùå íåñêîëüêî âàæíûõ ïðèìåðîâ
äåðåâüåâ PN-âûâîäà.
1. ∃õ ¬À
PN
¬>x À
в
у
2
1
(2)
y
(1)
[]
[]
xA
A
A
xA
xA
xA
∀
¬
∃
∀
¬
∃¬
¬∀
¬∀
2. >x ¬À
PN
¬∃õ À
у
в
у
у
(2)
(1)
2
1
[]
[]
xA
A
A
xA
xA
xA
xA
xA
∃
¬
∀
¬
∀¬
¬
¬∀ ¬
∃
∀¬
¬∀ ¬
¬∃
3. ¬>õ À
PN
∃õ ¬À
в
в
в
â
(2)
(1)
2
1
[]
[]
A
xA
xA
A
A
xA
xA
xA
xA
∃
∀
¬
¬
¬
∃¬
¬∃ ¬
¬¬
¬∀
∀
¬¬∃ ¬
∃¬
Примеры деревьев
PN
&
вывода
202
4. >õ (À & B)
PN
>õ À & >õ B
(&) (&)
&&
&
xA B x A B
AB AB
AB
xA xB
xA xB
∀∀
∀∀
∀∀
5. >õ À & >õ B
PN
>õ (À & B)
&&
&
(&)
xA xB xA xB
xA xB
AB
AB
xA B
∀∀∀∀
∀∀
∀
6. >õ À ∨ >õ B
PN
>õ (À ∨ B)
(1)
11
y
[] []
()()
()
xA xB
AB
AB AB
xA xB
xA B xA B
xA B
∨
∀∀
∨∨
∀∨∀
∀∨ ∀∨
∀∨
7. ∃õ (À ∨ B)
PN
∃õ À ∨ ∃õ B
22
1
(2)
(1)
ó
ó
[] []
[]
()
AB
xA xB
AB
xA xB xA xB
xA B
xA xB
xA xB
∨
∃
∃∃
∨
∃∨∃ ∃∨∃
∃∨
∃∨∃
∃∨∃
8. ∃õ À ∨ ∃õ B
PN
∃õ (À ∨ B)
23
11
(2) (3)
(1)
ó
y
[] []
[] []
() ()
() ()
()
ó
AB
AB AB
xA B xA B
xA xB
xA xB
xA B xA B
xA B
∃∃
∨
∨∨
∃∨ ∃∨
∃∃
∃∨∃
∃∨ ∃∨
∃∨
9. >õ (À ⊃ Â)
PN
>õ À ⊃ >õ Â
1
(1)
â
[] ( )
xA x A B
AAB
B
xB
xA xB
⊃
∀∀⊃
⊃
∀
∀⊃∀
203
ÓÏÐÀÆÍÅÍÈÅ
Äîêàæèòå ïîñòðîåíèåì äåðåâà PN-âûâîäà (À, Â – ïðîèçâîëü-
íûå ôîðìóëû ßËÏ):
1) åñëè
PN
À ⊃ Â, òî
PN
>õ À ⊃ >õ Â;
2) åñëè
PN
À ⊃ Â, òî
PN
∃õ À ⊃ ∃õ Â;
3) åñëè
PN
À
~
Â, òî
PN
>õ À
~
>õ Â;
4) åñëè
PN
À
~
Â, òî
PN
∃õ À
~
∃õ Â.
§ 4.4. Ïðèíöèï èíäóêöèè§ 4.4. Ïðèíöèï èíäóêöèè
§ 4.4. Ïðèíöèï èíäóêöèè§ 4.4. Ïðèíöèï èíäóêöèè
§ 4.4. Ïðèíöèï èíäóêöèè
äëÿ äëÿ
äëÿ äëÿ
äëÿ
PNPN
PNPN
PN
-âûâîäîâ-âûâîäîâ
-âûâîäîâ-âûâîäîâ
-âûâîäîâ
Ïîíÿòèå ñîõðàíåíèÿ PN-ïðàâèëîì îòíîøåíèÿ
ρ (ãäå ρ – îòíîøåíèå ìåæäó êîíå÷íûìè ìíîæåñòâàìè ôîðìóë è
ôîðìóëàìè ßËÏ) äëÿ âñåõ áåñêâàíòîðíûõ ïðàâèë çàêëþ÷åíèÿ ìîæ-
íî îïðåäåëèòü àíàëîãè÷íî òîìó, êàê ýòî ñäåëàíî äëÿ N-ïðàâèë â
§ 2.6. Äîáàâèì ÷åòûðå íîâûõ ïóíêòà äëÿ êâàíòîðíûõ ïðàâèë.
Îïðåäåëåíèå ñîõðàíåíèÿ PN-ïðàâèëîì îòíîøåíèÿ
ρρ
ρρ
ρ. Áóäåì ãî-
âîðèòü, ÷òî:
1) ïðàâèëî >â ñîõðàíÿåò îòíîøåíèå ρ, åñëè äëÿ ëþáîé ôîðìóëû
À è äëÿ ëþáîãî ìíîæåñòâà ôîðìóë Δ, íè â îäíó èç ôîðìóë
êîòîðîãî íå âõîäèò ñâîáîäíî õ, âûïîëíÿåòñÿ óñëîâèå
ρ
ρ
À
À
Δ
Δ∀x
(åñëè ΔρÀ, òî Δρ>x À);
2) ïðàâèëî ∃â ñîõðàíÿåò îòíîøåíèå ρ, åñëè äëÿ ëþáîãî ìíîæå-
ñòâà ôîðìóë Δ, ëþáîé ôîðìóëû À è ëþáîãî À-õ-äîïóñòèìîãî
òåðìà t âûïîëíÿåòñÿ óñëîâèå
ρ
ρ
()
Àt
xÀ
Δ
Δ∃
;
3) ïðàâèëî >ó ñîõðàíÿåò îòíîøåíèå ρ, åñëè äëÿ ëþáîãî ìíîæå-
ñòâà ôîðìóë Δ, ëþáîé ôîðìóëû À è ëþáîãî À-õ-äîïóñòèìîãî
òåðìà t âûïîëíÿåòñÿ óñëîâèå
ρ
ρ ()
xÀ
Àt
Δ∀
Δ
;
4) ïðàâèëî ∃ó ñîõðàíÿåò îòíîøåíèå ρ, åñëè äëÿ ëþáûõ ìíîæåñòâ
ôîðìóë Δ
1
è Δ
2
è ëþáîé ôîðìóëû Ñ òàêèõ, ÷òî íè â îäíó ôîð-
ìóëó èç ìíîæåñòâà Δ
2
\ {A} è â ôîðìóëó Ñ íå âõîäèò ñâîáîäíî õ,
âûïîëíÿåòñÿ óñëîâèå
2
12
1
\
ρ ; ρ
(({}))ρ
xÀ C
ÀC
Δ∃ Δ
Δ∪ Δ
.
204
Ñîîòâåòñòâóþùèå ñâîéñòâà îòíîøåíèÿ PN-âûâîäèìîñòè
PN
(èç § 4.3) îçíà÷àþò, ÷òî âñå PN-ïðàâèëà ñîõðàíÿþò îòíîøåíèå
PN
,
à ñîîòâåòñòâóþùèå ñâîéñòâà îòíîøåíèÿ ñåìàíòè÷åñêîãî ñëåäîâà-
íèÿ â ëîãèêå ïðåäèêàòîâ
ËÏ
(èç § 3.6) îçíà÷àþò, ÷òî âñå PN-ïðà-
âèëà ñîõðàíÿþò îòíîøåíèå
ËÏ
. Âñå PN-ïðàâèëà ñîõðàíÿþò òàêæå
îòíîøåíèå
M-ñëåäîâàíèÿ äëÿ ëþáîé èíòåðïðåòàöèè M ñèãíàòó-
ðû σ.
Çàìå÷àíèå. Ìîæíî äîêàçàòü, ÷òî åñëè îòíîøåíèå ρ ðåôëåêñèâ-
íî, òðàíçèòèâíî è ìîíîòîííî, òî:
1) ïðàâèëî >ó ñîõðàíÿåò îòíîøåíèå ρ òîãäà è òîëüêî òîãäà,
êîãäà äëÿ ëþáîé ôîðìóëû À è ëþáîãî À-õ-äîïóñòèìîãî òåðìà t
âûïîëíÿåòñÿ óñëîâèå >õÀρÀ(t);
2) ïðàâèëî ∃â ñîõðàíÿåò îòíîøåíèå ρ òîãäà è òîëüêî òîãäà,
êîãäà äëÿ ëþáîé ôîðìóëû À è ëþáîãî À-õ-äîïóñòèìîãî òåðìà t
âûïîëíÿåòñÿ óñëîâèå À(t)ρ∃õÀ;
3) ïðàâèëî ∃ó ñîõðàíÿåò îòíîøåíèå ρ òîãäà è òîëüêî òîãäà,
êîãäà äëÿ ëþáûõ Δ, À è Ñ òàêèõ, ÷òî õ íå âõîäèò ñâîáîäíî íè â îäíó
ôîðìóëó èç Δ è â ôîðìóëó Ñ, âûïîëíÿåòñÿ
, ρ
, ρ
ÀC
ÀC
Δ
Δ∃
x
.
 § 2.6 ñôîðìóëèðîâàí è äîêàçàí ïðèíöèï èíäóêöèè äëÿ ïðî-
ïîçèöèîíàëüíûõ ñèñòåì åñòåñòâåííîãî âûâîäà. Èñïîëüçîâàíèå ýòîãî
ïðèíöèïà ïîçâîëèëî ñóùåñòâåííî óïðîñòèòü äîêàçàòåëüñòâà ìíî-
ãèõ âàæíûõ òåîðåì î ñâîéñòâàõ òàêèõ ñèñòåì.
Ñôîðìóëèðóåì è äîêàæåì òåïåðü àíàëîãè÷íûé ïðèíöèï èí-
äóêöèè äëÿ ïðåäèêàòíûõ ñèñòåì åñòåñòâåííîãî âûâîäà, ñóòü êîòî-
ðîãî çàêëþ÷àåòñÿ â ñëåäóþùåì:
S Ïðè îïðåäåëåííûõ óñëîâèÿõ íà îòíîøåíèå ρ, ìíîæåñòâî çåëå-
íûõ ëèñòüåâ âñÿêîãî äåðåâà PN-âûâîäà íàõîäèòñÿ â îòíîøåíèè ρ ñ
åãî êîðíåì.
! ÒÅÎÐÅÌÀ (ïðèíöèï èíäóêöèè äëÿ PN-âûâîäîâ, ïåðâàÿ ôîðìà).
Ïóñòü ρ – îòíîøåíèå ìåæäó êîíå÷íûìè ìíîæåñòâàìè ôîðìóë è
ôîðìóëàìè ßËÏ.
Åñëè 1) ρ ðåôëåêñèâíî è ìîíîòîííî,
è 2) âñå PN-ïðàâèëà ñîõðàíÿþò îòíîøåíèå ρ,
òî äëÿ ëþáûõ Δ, F è ëþáîãî PN-Δ-F-âûâîäà âûïîëíÿåòñÿ ΔρF.
205
Äîêàçàòåëüñòâî. Äîñòàòî÷íî äîêàçàòü âîçâðàòíîé èíäóê-
öèåé ïî íàòóðàëüíîìó ïàðàìåòðó k (âûñîòå äåðåâà) ñëåäóþùåå óò-
âåðæäåíèå:
Êàêîâû áû íè áûëè íàòóðàëüíîå ÷èñëî k, ìíîæåñòâî ôîðìóë Δ,
ôîðìóëà F è äåðåâî PN-Δ-F-âûâîäà âûñîòû k, âûïîëíÿåòñÿ ΔρF.
Ñèìâîëè÷åñêè ýòî óòâåðæäåíèå ìîæíî çàïèñàòü òàê:
(k) (
D
) (Δ) (F) (
D
=
F
Δ
D
& h(
D
) = k → ΔρF).
Áàçèñ èíäóêöèè. Ïóñòü
F
Δ
D
åñòü PN-Δ-F-âûâîä âûñîòû 0, ò. å.
F
Δ
D
åñòü ôîðìóëà F è Δ = {F}. Òîãäà ΔρF â ñèëó ðåôëåêñèâíîñòè ρ.
Øàã èíäóêöèè. Ïóñòü k – ïðîèçâîëüíîå íàòóðàëüíîå ÷èñëî. Äî-
ïóñòèì, ÷òî äëÿ ëþáûõ Δ è F è äëÿ ëþáîãî PN-Δ-F-âûâîäà, âûñîòà
êîòîðîãî íå ïðåâîñõîäèò k, èìååò ìåñòî ΔρF (ïðåäïîëîæåíèå èíäóê-
öèè).
Ïóñòü Δ – ïðîèçâîëüíîå ìíîæåñòâî ôîðìóë, F – ïðîèçâîëüíàÿ
ôîðìóëà è
F
Δ
D
– ïðîèçâîëüíûé PN-Δ-F-âûâîä, âûñîòà êîòîðîãî
ðàâíà k + 1. Äîêàæåì, ÷òî ΔρF.
Ðàññìîòðèì âñå âîçìîæíûå ñëó÷àè ïîñòðîåíèÿ äåðåâà
F
Δ
D
â
ñîîòâåòñòâèè ñ èíäóêòèâíûì îïðåäåëåíèåì PN-Δ-F-âûâîäà.
Ðàññóæäåíèÿ â ïóíêòàõ, îòíîñÿùèõñÿ ê áåñêâàíòîðíûì PN-
ïðàâèëàì, àíàëîãè÷íû ðàññóæäåíèÿì, ïðîâåäåííûì äëÿ ñîîòâåò-
ñòâóþùèõ ïðàâèë ïðè äîêàçàòåëüñòâå ïðèíöèïà èíäóêöèè äëÿ N
k
-
âûâîäîâ (§ 2.6). Îñòàåòñÿ ðàññìîòðåòü ÷åòûðå ñëó÷àÿ êâàíòîðíûõ
ïðàâèë:
1. Ïóñòü
F
Δ
D
ïîëó÷åíî ïî ïðàâèëó >â, ò. å.
F
Δ
D
=
A
õÀ
Δ
∀
D
, F
>x À
è ïåðåìåííàÿ õ íå âõîäèò ñâîáîäíî íè â îäíó ôîðìóëó èç Δ. Òîãäà
âûñîòà
A
Δ
D
ðàâíà k è, ñîãëàñíî ïðåäïîëîæåíèþ èíäóêöèè, ΔρÀ.
Îòñþäà, ïîñêîëüêó ïðàâèëî >â ñîõðàíÿåò ρ, ïîëó÷àåì Δρ>xÀ, ò. å.
ΔρF.
2. Ïóñòü
F
Δ
D
ïîëó÷åíî ïî ïðàâèëó ∃â, ò. å.
F
Δ
D
=
()
At
õÀ
Δ
∃
D
, F
∃x À
è òåðì t – À-õ-äîïóñòèì. Òîãäà âûñîòà
()At
Δ
D
ðàâíà k, à çíà÷èò, ñî-
ãëàñíî ïðåäïîëîæåíèþ èíäóêöèè, ΔρÀ(t). Îòñþäà, ïîñêîëüêó ïðàâè-
ëî ∃â ñîõðàíÿåò ρ, ïîëó÷àåì Δρ∃xÀ, ò. å. ΔρF.
206
3. Ñëó÷àé ïðàâèëà >ó ðàññìàòðèâàåòñÿ àíàëîãè÷íî ï. 2.
4. Ïóñòü äåðåâî âûâîäà
F
Δ
D
ïîëó÷åíî ñ ïîìîùüþ ïðàâèëà ∃ó, ò. å.
F
Δ
D
=
12
õÀ C
C
ΔΔ
∃
DD
, ïåðåìåííàÿ õ íå âõîäèò ñâîáîäíî íè â îäíó ôîð-
ìóëó èç ìíîæåñòâà Δ
2
\ {A} è â ôîðìóëó Ñ, F
Ñ, Δ = Δ
1
∪ (Δ
2
\ {A}).
Òîãäà âûñîòû äåðåâüåâ
хА
1
Δ
∃
D
è
C
2
Δ
D
íå ïðåâîñõîäÿò k, à çíà÷èò,
ñîãëàñíî ïðåäïîëîæåíèþ èíäóêöèè, Δ
1
ρ∃õÀ è Δ
2
ρÑ. Îòñþäà, ïî-
ñêîëüêó ïðàâèëî ∃ó ñîõðàíÿåò ρ, ïîëó÷àåì Δ
1
∪ (Δ
2
\ {A})ρÑ,
ò. å. ΔρF.
Ýòèì çàâåðøàåòñÿ ðàññìîòðåíèå âñåõ âîçìîæíûõ ñëó÷àåâ ïîñò-
ðîåíèÿ äåðåâà
F
Δ
D
è äîêàçàòåëüñòâî òåîðåìû.
★ Óñëîâèå ìîíîòîííîñòè îòíîøåíèÿ ρ èñïîëüçóåòñÿ äëÿ ïóíê-
òîâ, îòíîñÿùèõñÿ ê áåñêâàíòîðíûì ïðàâèëàì (ñì. äîêàçàòåëüñòâî
ïðèíöèïà èíäóêöèè äëÿ N
c
-âûâîäîâ, § 2.6). Åñëè íåìíîãî ïîä-
êîððåêòèðîâàòü îïðåäåëåíèå ïîíÿòèÿ ñîõðàíåíèÿ PN-ïðàâèëàìè îòíî-
øåíèÿ ρ â ñîîòâåòñòâèè ñ óòâåðæäåíèÿìè I–IV § 2.6, îòìå÷åííûìè
★,
ìîæíî ñîâñåì îòêàçàòüñÿ îò òðåáîâàíèÿ ìîíîòîííîñòè â ôîðìóëè-
ðîâêå ïðèíöèïà èíäóêöèè â ïåðâîé ôîðìå.
✰
Áóäåì ãîâîðèòü, ÷òî îòíîøåíèå PN-âûâîäèìîñòè ñîãëàñîâàíî ñ
îòíîøåíèåì ρ, åñëè äëÿ ëþáîãî êîíå÷íîãî ìíîæåñòâà ôîðìóë à è
ëþáîé ôîðìóëû F èç âûâîäèìîñòè Ã
PN
F ñëåäóåò ÃρF, ò. å. åñëè
(Ã) (F) (Ã
PN
F → ÃρF).
Ñëåäñòâèåì ïðèíöèïà èíäóêöèè äëÿ PN-âûâîäîâ â ïåðâîé ôîð-
ìå ÿâëÿåòñÿ ñëåäóþùàÿ òåîðåìà, êîòîðàÿ ñóùåñòâåííî îáëåã÷àåò
äîêàçàòåëüñòâî óòâåðæäåíèé âèäà: «Êàêîâû áû íè áûëè êîíå÷íîå
ìíîæåñòâî ôîðìóë Ã è PN-âûâîäèìàÿ èç Ã ôîðìóëà F, ìíîæåñòâî
ôîðìóë Ã íàõîäèòñÿ â îòíîøåíèè ρ ñ F» èëè, äðóãèìè ñëîâàìè:
«Îòíîøåíèå PN-âûâîäèìîñòè ñîãëàñîâàíî ñ îòíîøåíèåì ρ».
! ÒÅÎÐÅÌÀ (ïðèíöèï èíäóêöèè äëÿ PN-âûâîäîâ, âòîðàÿ ôîðìà).
Åñëè 1) ρ ðåôëåêñèâíî è ìîíîòîííî,
è 2) âñå PN-ïðàâèëà ñîõðàíÿþò îòíîøåíèå ρ,
òî îòíîøåíèå PN-âûâîäèìîñòè ñîãëàñîâàíî ñ îòíîøåíèåì ρ.
Äîêàçàòåëüñòâî. Ïóñòü Ã è F – òàêèå, ÷òî Ã
PN
F, à
F
Δ
D
– PN-Δ-F-âûâîä òàêîé, ÷òî Δ ⊆ Ã. Òîãäà, â ñèëó ïåðâîé ôîðìû
207
ïðèíöèïà èíäóêöèè äëÿ PN-âûâîäîâ, ΔρF. Îòñþäà, â ñèëó ìîíî-
òîííîñòè ρ, äåëàåì âûâîä, ÷òî ÃρF.
Áëàãîäàðÿ ïðèíöèïó èíäóêöèè äëÿ ÐN-âûâîäîâ (âî âòîðîé ôîð-
ìå) ïîëó÷àåì äîñòàòî÷íîå óñëîâèå äëÿ ñîãëàñîâàííîñòè îòíîøåíèÿ
PN
ñ ðåôëåêñèâíûì è ìîíîòîííûì îòíîøåíèåì ρ. Òàêèì óñëîâèåì
ÿâëÿåòñÿ óñëîâèå ñîõðàíåíèÿ îòíîøåíèÿ ρ âñåìè PN-ïðàâèëàìè.
Àíàëîãè÷íî ñëó÷àþ ïðîïîçèöèîíàëüíûõ ñèñòåì, èñïîëüçîâà-
íèå ïðèíöèïà èíäóêöèè äëÿ PN-âûâîäîâ ñóùåñòâåííî óïðîùàåò
äîêàçàòåëüñòâî ìíîãèõ âàæíûõ òåîðåì î ñâîéñòâàõ ïðåäèêàòíûõ
ñèñòåì.
Òåïåðü ââåäåì ïîíÿòèå ïðîèçâîäíîãî PN-ïðàâèëà àíàëîãè÷íî
òîìó, êàê ýòî áûëî ñäåëàíî äëÿ ñèñòåì N
k
è N
i
.
!
Ñõåìó R íàçûâàþò ïðîèçâîäíûì PN-ïðàâèëîì, åñëè îíà ñîõðà-
íÿåò îòíîøåíèå PN-âûâîäèìîñòè.
Àíàëîãè÷íî ïðîïîçèöèîíàëüíîìó ñëó÷àþ ëåãêî äîêàçàòü, ÷òî
ïðÿìàÿ ñõåìà
...
n
1
FF
F
ÿâëÿåòñÿ ïðîèçâîäíûì PN-ïðàâèëîì òîãäà è
òîëüêî òîãäà, êîãäà
F
1
, …, F
n
PN
F.
Ñîãëàñíî ýòîìó êðèòåðèþ, ìîæíî äîêàçàòü ïîñòðîåíèåì ñîîò-
âåòñòâóþùèõ äåðåâüåâ PN-âûâîäà, ÷òî, íàïðèìåð, ñëåäóþùèå ñõå-
ìû ÿâëÿþòñÿ ïðîèçâîäíûìè PN-ïðàâèëàìè (À, Â, Ñ – ïðîèçâîëü-
íûå ôîðìóëû ßËÏ):
1)
() ( ( ) ( ))
()
At x Ax Bx
Bt
∀⊃
, ãäå òåðì t À⊃Â-õ-äîïóñòèì;
2)
(() ()) ()
()
xAx Bx Bt
At
∀⊃ ¬
¬
, ãäå òåðì t À⊃Â-õ-äîïóñòèì;
3)
()
xC A
CxA
∀⊃
⊃∀
, ãäå õ íå âõîäèò ñâîáîäíî â Ñ;
4)
()
xA C
xA C
∀⊃
∃⊃
, ãäå õ íå âõîäèò ñâîáîäíî â Ñ;
5)
[()]
&
()
– ñ îãðàíè÷åíèÿìè, àíàëîãè÷íûìè
îãðàíè÷åíèÿì äëÿ ïðàâèëà ó
.
Ax
BB
xA x
¬
¬∃
∃
208
Òàêæå ìîæíî ïîñòðîåíèåì äåðåâüåâ âûâîäà äîêàçàòü, ÷òî äëÿ
ëþáûõ ïðåäèêàòíûõ ôîðìóë À è Ñ, åñëè ïåðåìåííàÿ õ íå âõîäèò
ñâîáîäíî â Ñ, òî:
1)
PN
PN
CA
CxA
⊃
⊃∀
; 2)
PN
PN
AC
xA C
⊃
∃⊃
; 3)
() &
()
Ax B B
xAx
⊃¬
¬∃
.
§ 4.5. Îñíîâíûå õàðàêòåðèñòèêè§ 4.5. Îñíîâíûå õàðàêòåðèñòèêè
§ 4.5. Îñíîâíûå õàðàêòåðèñòèêè§ 4.5. Îñíîâíûå õàðàêòåðèñòèêè
§ 4.5. Îñíîâíûå õàðàêòåðèñòèêè
ïðåäèêàòíûõ ñèñòåìïðåäèêàòíûõ ñèñòåì
ïðåäèêàòíûõ ñèñòåìïðåäèêàòíûõ ñèñòåì
ïðåäèêàòíûõ ñèñòåì
Ïðè ïîñòðîåíèè ïðåäèêàòíîé ñèñòåìû åñòåñòâåí-
íîãî âûâîäà â êà÷åñòâå ÿçûêà ñèñòåìû ìîæíî âçÿòü ëþáîé ôðàã-
ìåíò ßËÏ, ñîõðàíèâ òå æå ïðàâèëà çàêëþ÷åíèÿ. Ïðåäèêàòíóþ ñè-
ñòåìó ñ ÿçûêîì ßËÏ
σ
áóäåì îáîçíà÷àòü ÷åðåç P
σ
N. Äëÿ âñÿêîé
òàêîé ñèñòåìû ñïðàâåäëèâû âñå óòâåðæäåíèÿ, äîêàçàííûå âûøå
äëÿ ñèñòåìû PN, â ÷àñòíîñòè ñïðàâåäëèâ ïðèíöèï èíäóêöèè äëÿ
P
σ
N-âûâîäîâ.
Ñèñòåìó P
σ
N íàçûâàþò ñåìàíòè÷åñêè êîððåêòíîé, åñëè âñÿêàÿ
P
σ
N-âûâîäèìàÿ ôîðìóëà ÿâëÿåòñÿ îáùåçíà÷èìîé.
Ñèñòåìó P
σ
N íàçûâàþò ïðîòèâîðå÷èâîé, åñëè ñóùåñòâóåò ôîð-
ìóëà ßËÏ
σ
, âûâîäèìàÿ â P
σ
N âìåñòå ñî ñâîèì îòðèöàíèåì, è
íåïðîòèâîðå÷èâîé, åñëè òàêîé ôîðìóëû íå ñóùåñòâóåò.
! ÒÅÎÐÅÌÀ (î ñåìàíòè÷åñêîé êîððåêòíîñòè ñèñòåì P
σ
N). Âñÿêàÿ
P
σ
N-âûâîäèìàÿ ôîðìóëà ÿâëÿåòñÿ îáùåçíà÷èìîé.
Äîêàçàòåëüñòâî. Ñíà÷àëà äîêàæåì, ÷òî îòíîøåíèå
P
σ
N-âûâîäèìîñòè ñîãëàñîâàíî ñ îòíîøåíèåì ñåìàíòè÷åñêîãî ñëå-
äîâàíèÿ â ËÏ. Äåéñòâèòåëüíî, âî-ïåðâûõ, îòíîøåíèå
ËÏ
ðåô-
ëåêñèâíî è ìîíîòîííî. Âî-âòîðûõ, ñîãëàñíî ñâîéñòâàì ñåìàíòè-
÷åñêîãî ñëåäîâàíèÿ â ËÏ, âñå P
σ
N-ïðàâèëà ñîõðàíÿþò îòíîøåíèå
ËÏ
(ñì. § 3.6). Ñëåäîâàòåëüíî, â ñèëó ïðèíöèïà èíäóêöèè äëÿ
P
σ
N-âûâîäîâ (âî âòîðîé ôîðìå), îòíîøåíèå P
σ
N-âûâîäèìîñòè ñî-
ãëàñîâàíî ñ îòíîøåíèåì ñåìàíòè÷åñêîãî ñëåäîâàíèÿ â ëîãèêå ïðå-
äèêàòîâ:
(Ã) (F) (Ã
σ
PN
F → Ã
ËÏ
F).
209
Îòñþäà ïðè ïóñòîì à ïîëó÷àåì
(F) (
σ
PN
F →
F),
÷òî è òðåáîâàëîñü.
S Çàìå÷àíèå 1. Êàê óæå îòìå÷àëîñü, îòêàç îò îãðàíè÷åíèé â ïóí-
êòàõ (Ð
1
)–(Ð
4
) îïðåäåëåíèÿ PN-Δ-F-âûâîäà âåäåò ê ïîòåðå ñåìàí-
òè÷åñêîé êîððåêòíîñòè ñèñòåìû.
ÑËÅÄÑÒÂÈÅ. Âñÿêàÿ ïðåäèêàòíàÿ ñèñòåìà P
σ
N íåïðîòèâîðå-
÷èâà.
Äîêàçàòåëüñòâî. Ïðåäïîëîæèì, ÷òî ñèñòåìà P
σ
N ïðîòè-
âîðå÷èâà, è ïóñòü ôîðìóëà F òàêàÿ, ÷òî
σ
PN
F è
σ
PN
¬F. Òîãäà, ïî
òåîðåìå î ñåìàíòè÷åñêîé êîððåêòíîñòè ñèñòåìû P
σ
N, ôîðìóëû F
è ¬F îáå îáùåçíà÷èìû, ÷òî íåâîçìîæíî. Ñëåäîâàòåëüíî, ñèñòåìà
P
σ
N íåïðîòèâîðå÷èâà.
Ïðèâåäåííîå äîêàçàòåëüñòâî íåïðîòèâîðå÷èâî-
ñòè âñÿêîé ñèñòåìû P
σ
N, îïèðàþùååñÿ íà ñå-
ìàíòè÷åñêóþ êîððåêòíîñòü ýòîé ñèñòåìû, íîñèò
ñåìàíòè÷åñêèé õàðàêòåð.  ñâÿçè ñ ýòèì áîëåå
öåííûì ÿâëÿåòñÿ ñëåäóþùåå ñèíòàêñè÷åñêîå
äîêàçàòåëüñòâî íåïðîòèâîðå÷èâîñòè âñÿêîé ñèñòåìû P
σ
N.
! ÒÅÎÐÅÌÀ. Âñÿêàÿ ïðåäèêàòíàÿ ñèñòåìà P
σ
N íåïðîòèâîðå÷èâà.
Äîêàçàòåëüñòâî. Çàäàäèì èíäóêòèâíî îòîáðàæåíèå h
ìíîæåñòâà ôîðìóë ßËÏ
σ
âî ìíîæåñòâî ôîðìóë ßËÂ:
Áàçèñ èíäóêöèè. Êàêîâû áû íè áûëè n-ìåñòíûé ïðåäèêàòíûé
ñèìâîë
n
k
P
(n, k = 1, 2, …) è òåðìû ßËÏ
σ
t
1
, …, t
n
,
h(
n
k
P
(t
1
, …, t
n
)) = p
1
,
ãäå p
1
– ïðîïîçèöèîíàëüíàÿ ïåðåìåííàÿ.
Øàã èíäóêöèè. Ïóñòü À è  – ïðîèçâîëüíûå ôîðìóëû ßËÏ
σ
è
h(À), h(Â) îïðåäåëåíû. Òîãäà:
à) h(À ⊕ Â) = h(À) ⊕ h(Â), ãäå ⊕ åñòü ëþáàÿ èç ñâÿçîê &, ∨, ⊃;
á) h(¬À) = ¬h(À);
â) h(>õ À) = h(À);
ã) h(∃õ À) = h(À).
Ãîâîðÿ íåôîðìàëüíî, äëÿ âñÿêîé ôîðìóëû À ôîðìóëà h(À) ïî-
ëó÷àåòñÿ èç À «ñòèðàíèåì» êâàíòîðîâ è çàìåíîé êàæäîé ýëåìåí-
òàðíîé ôîðìóëû íà ïðîïîçèöèîíàëüíóþ ïåðåìåííóþ p
1
.
Синтаксическое
доказательство
непротиворечивости
системы PN
210
Ïðèìåð. h(
121
11 1 2 2 1 1 2
() (, ())
xP x x P c f x
∃⊃∀¬
) = p
1
⊃ ¬p
1
.
Òåïåðü äîêàæåì, ÷òî:
1) h(
()
x
t
A
) = h(À) äëÿ ëþáûõ ïåðåìåííîé õ, òåðìà t è ôîðìóëû À;
2) åñëè Ã
PN
À, òî h(Ã)
N
к
h(À) äëÿ ëþáîé ôîðìóëû À è ëþáîãî
ìíîæåñòâà à ôîðìóë ßËÏ
σ
, ãäå h(Ã) {h(F) | F ∈ Ã};
3) åñëè
PN
À, òî
N
ê
h(À) äëÿ ëþáîé ôîðìóëû À ßËÏ
σ
.
Äîêàçàòåëüñòâî óòâåðæäåíèÿ ï. 1 ïðîâåäåì èíäóêöèåé ïî ïîñò-
ðîåíèþ ôîðìóëû ßËÏ
σ
. Åñëè À – ýëåìåíòàðíàÿ ôîðìóëà, òî
()
x
t
A
–
òàêæå ýëåìåíòàðíàÿ ôîðìóëà. Ñëåäîâàòåëüíî, ñîãëàñíî îïðåäåëå-
íèþ îòîáðàæåíèÿ h (áàçèñ), h(
()
x
t
A
) = p
1
è h(À) = p
1
. Ïóñòü À è Â –
ïðîèçâîëüíûå ôîðìóëû ßËÏ
σ
è ïóñòü h(
()
x
t
A
) = h(À), h(
()
x
t
B
) = h(Â)
(ïðåäïîëîæåíèå èíäóêöèè). Òîãäà h(
()
x
t
AB
⊕
) = h(
()
x
t
A
⊕
()
x
t
B
) =
= h(
()
x
t
A
) ⊕ h(
()
x
t
B
) = h(À) ⊕ h(B) = h(À ⊕ B), ãäå ⊕ – ëþáàÿ èç
ñâÿçîê &, ∨, ⊃. Äëÿ ôîðìóëû ¬À ðàññóæäåíèå ïðîâîäèòñÿ àíàëî-
ãè÷íî.
Ïåðåéäåì ê ôîðìóëàì ñ âíåøíèì âõîæäåíèåì êâàíòîðà îáù-
íîñòè. Åñëè êâàíòîð áåðåòñÿ ïî òîé æå ïåðåìåííîé õ, âìåñòî êîòî-
ðîé ïîäñòàâëÿåòñÿ òåðì t, ò. å. ôîðìóëà èìååò âèä >õ À, òî
()
x
t
xA
∀
=
= >õ À, à çíà÷èò, h(
()
x
t
xA
∀
) = h(>õ À) = h(À). Åñëè êâàíòîð áåðåò-
ñÿ ïî êàêîé-íèáóäü ïåðåìåííîé ó, îòëè÷íîé îò õ, òî, ñîãëàñíî
îïðåäåëåíèþ ïîäñòàíîâêè òåðìà â ôîðìóëó,
()
x
t
yA
∀
= >ó
()
x
t
A
.
Òîãäà h(
()
x
t
yA
∀
) = h(>ó
()
x
t
A
) = h(
()
x
t
A
) = h(À).
Äëÿ êâàíòîðà ∃ ðàññóæäåíèå ïðîâîäèòñÿ àíàëîãè÷íî.
Äëÿ äîêàçàòåëüñòâà óòâåðæäåíèÿ 2 âîñïîëüçóåìñÿ ïðèíöèïîì
èíäóêöèè äëÿ PN-âûâîäîâ (âî âòîðîé ôîðìå). Îòíîøåíèå ρ çàäà-
äèì ñëåäóþùèì îáðàçîì: êàêîâû áû íè áûëè ôîðìóëà À è ìíîæå-
ñòâî ôîðìóë à ÿçûêà ßËÏ
σ
ÃρA
def
←⎯⎯→
h(Ã)
N
ê
h(À).
Ïîñêîëüêó îòíîøåíèå
N
ê
ðåôëåêñèâíî è ìîíîòîííî, òî ρ òàêæå
ðåôëåêñèâíî è ìîíîòîííî. Îñòàåòñÿ ïðîâåðèòü, ÷òî âñå PN-ïðà-