Об отношении совместимости в исчислении Ламбека и в его варианте с операциями замещения, страница 12

Îòñþäà ïîëåììå 5.4 ïîëó÷àåì òðåáóåìîå.Ëåììà 5.5.Åñëè HDL ` A → B , òî JAK = JBK.Äîêàçàòåëüñòâî. Èíäóêöèÿ ïî âûâîäó â èñ÷èñëåíèè HDL.Ñëåäñòâèå 5.2.Åñëè HDLk ` A → B , òî JAK = JBK.Èç äîêàçàííîé ëåììû íåìåäëåííî âûòåêàåò, ÷òî ðàâåíñòâî JAK =JBK ÿâëÿåòñÿ íåîáõîäèìûì óñëîâèåì ñîâìåñòèìîñòè òèïîâ A è B êàê71â èñ÷èñëåíèè HDL, òàê è â ëþáîì èç èñ÷èñëåíèé HDLk .

Îñòàâøàÿñÿ÷àñòü ãëàâû áóäåò ïîñâÿùåíà äîêàçàòåëüñòâó åãî äîñòàòî÷íîñòè, òî åñòüñëåäóþùåé òåîðåìû:Òåîðåìà 10.5.2Èç óñëîâèÿ A ∼k B ñëåäóåò, ÷òî JAK = JBK.Äîêàçàòåëüñòâî êðèòåðèÿ ñîâìåñòèìîñòèÄàííûé ðàçäåë ïîñâÿù¼í äîêàçàòåëüñòâó äîñòàòî÷íîãî óñëîâèÿ ñîâìåñòèìîñòè è, êàê ñëåäñòâèå, êðèòåðèÿ ñîâìåñòèìîñòè. Âíà÷àëå ïðèâåä¼ìñïèñîê ñåêâåíöèé, íà âûâîäèìîñòü êîòîðûõ ìû áóäåì îïèðàòüñÿ â äàëüíåéøåì. Ïðè ýòîì â êàæäîì èç ñëó÷àåâ ìû ñ÷èòàåì, ÷òî ñîðòà òèïîâ Aè B òàêîâû, ÷òî âñå âõîäÿùèå â ñåêâåíöèþ òèïû îïðåäåëåíû.Ëåììà 5.6.Ñëåäóþùèå ñåêâåíöèè ÿâëÿþòñÿ âûâîäèìûìè â èñ÷èñëå-íèè HDLk :1. (A/B) · B → A; B · (B \ A) → A,2. A → (A · B)/B; A → B \(B · A),3. A · (B/C) → (A · B)/C; (C \ B) · A → C \(B · A),4.

B j (B ↓j A) → A äëÿ ëþáîãî j 6 s(B);(A ↑j B) j B → A äëÿ ëþáîãî j 6 s(A) − s(B) + 1,5. A · J → (A · B) ↑s(A)+1 B; J · A → (B · A) ↑1 B ,6. A · B → (A · J) s(A)+1 B; A · B → (J · B) 1 A,7. A · I → A; I · A → A.Äîêàçàòåëüñòâî. Âî âñåõ ïóíêòàõ ëåììû ïðèâåä¼ì âûâîä òîëüêî äëÿïåðâîãî óòâåðæäåíèÿ, âòîðîå äîêàçûâàåòñÿ àíàëîãè÷íî.1.A/B → A/B(A/B) · B → A2.A·B →A·BA → (A · B)/B723.A · (B/C) · C → AA · (B/C) → (A · B)/C4.B ↓j A → B ↓j AB j (B ↓j A) → A5.(A · J) s(A)+1 B → A · BA · J → (A · B) ↑s(A)+1 B6. ßâëÿåòñÿ îäíîé èç àêñèîì èñ÷èñëåíèÿ HDL.7. ßâëÿåòñÿ îäíîé èç àêñèîì èñ÷èñëåíèÿ HDL. ñëåäóþùåé ëåììå ïðèâîäÿòñÿ ïðèìåðû ¾íåéòðàëüíûõ ïî óìíîæåíèþ¿ ýëåìåíòîâ c òî÷êè çðåíèÿ îòíîøåíèÿ ∼.Ëåììà 5.7.Äëÿ ïðîèçâîëüíûõ òèïîâ A, B ∈ Tpk âåðíû óòâåðæäåíèÿA · (B/B) ∼ A · (B \ B) ∼ (B/B) · A ∼ (B \ B) · A ∼ A.Äîêàçàòåëüñòâî.

Ñîâìåñòèìîñòü òèïîâ A è A · (B/B) âûòåêàåò èç âûâîäèìîñòè ñåêâåíöèé A → (A · (B/B))/(B/B) è A · (B/B) → (A ·(B/B))/(B/B). Ïåðâàÿ èç ýòèõ ñåêâåíöèé ñëåäóåò èç ïóíêòà 2 ëåììû5.6, âûâîä âòîðîé ïðèâåä¼í íèæå. Çàìåòèì, ÷òî ïîñêîëüêó s(B/B) = 0,òî ïðè ëþáîì k èç óñëîâèé A ∈ Tpk è B ∈ Tpk âñåãäà ñëåäóåò, ÷òîA · (B/B) ∈ Tpk . Àíàëîãè÷íî äîêàçûâàåòñÿ ñîâìåñòèìîñòü òèïîâ A è(B \ B) · A. Ñîâìåñòèìîñòü òèïîâ A è A · (B \ B) ñëåäóåò èç âûâîäèìîñòèñåêâåíöèé A → (A·(B \ B))/(B \ B) è A·(B \ B) → (A·(B \ B))/(B \ B).Ïåðâàÿ èç äàííûõ ñåêâåíöèé ñëåäóåò èç ïóíêòà 2 ëåììû 5.6, âòîðàÿ äîêàçûâàåòñÿ àíàëîãè÷íî ñåêâåíöèè A · (B/B) → (A · (B/B))/(B/B).73(B/B) · (B/B) → (B/B) · (B/B)B/B → B/B(B/B) · (B/B) · B → (B/B) · B(B/B) · B → B(B/B) · (B/B) · B → BA→A(B/B) · (B/B) → B/BA · (B/B) · (B/B) → A · (B/B)A · (B/B) → (A · (B/B))/(B/B)Ïóñòü A íåêîòîðûé òèï èñ÷èñëåíèÿ HDL, à i öåëîå ïîëîæèòåëüíîå ÷èñëî, ÷åðåç Ai áóäåì îáîçíà÷àòü òèï A. .

· A}. Áóäåì ñ÷èòàòü,| · .{zi ðàç÷òî A = I äëÿ ëþáîãî òèïà A.0Ñëåäóþùàÿ ëåììà ïîêàçûâàåò, ÷òî ïåðåñòàíîâêà ñîìíîæèòåëåéïðè êîíêàòåíàöèè íå âëèÿåò íà ñîâìåñòèìîñòü, à òàêæå ¾íåîòëè÷èìîñòü¿ ëåâîãî è ïðàâîãî äåëåíèÿ ñ òî÷êè çðåíèÿ îòíîøåíèÿ ñîâìåñòèìîñòè.Ëåììà 5.8.1. Äëÿ ëþáîãî òèïà A ∈ Tpk , òàêîãî ÷òî s(A) = 0, âûïîëíÿåòñÿóñëîâèå A · J ∼ J · A.2. Äëÿ ëþáîãî òèïà A ∈ Tpk , òàêîãî ÷òî s(A) < k , âûïîëíÿåòñÿóñëîâèå A · J ∼ J · A.3. Äëÿ ëþáîãî òèïà A ∈ Tpk , òàêîãî ÷òî s(A) = 0, è ïðîèçâîëüíîãîòèïà B ∈ Tpk âûïîëíÿåòñÿ óñëîâèå A · B ∼ B · A.4.

Äëÿ ëþáûõ òèïîâ A, B ∈ Tpk , òàêèõ ÷òî ê òîìó æå A · B ∈ Tpk ,âûïîëíÿåòñÿ óñëîâèå A · B ∼ B · A.5. Äëÿ ëþáûõ òèïîâ A, B ∈ Tpk , òàêèõ ÷òî ê òîìó æå A/B ∈ Tpk ,âûïîëíÿåòñÿ óñëîâèå A/B ∼ B \ A.6. Äëÿ ëþáûõ òèïîâ A, B, C∈ Tpk , òàêèõ ÷òî ê òîìó æå(A/B)/C ∈ Tpk , âûïîëíÿåòñÿ óñëîâèå (A/B)/C ∼ (A/C)/B .Äîêàçàòåëüñòâî.741. Ïîñêîëüêó s(A) = 0, òî ïî ïóíêòó 5 ëåììû 5.6 èìååì A · J ∼ (A ·A) ↑1 A ∼ J · A, ÷òî è òðåáîâàëîñü.2. Èç ïóíêòà 1 ëåììû 5.6, ïðèìåí¼ííîé s(A) ðàç, ñëåäóåò, ÷òî(A/J s(A) )·J s(A) ∼ A, òîãäà ïîëó÷àåì, ÷òî A·J ∼ (A/J s(A) )·J s(A) ·J ↔(A/J s(A) ) · J · J s(A) .

Ïîñêîëüêó s(A/J s(A) ) = 0, òî ïî ïóíêòó 1 ïîëó÷àåì, ÷òî (A/J s(A) ) · J · J s(A) ∼ J · (A/J s(A) ) · J s(A) ∼ J · A. Ñîåäèíÿÿäîêàçàííûå öåïî÷êè, ïîëó÷àåì òðåáóåìîå.3. Ïîñêîëüêó s(A) = 0, òî ïî ïóíêòó 6 ëåììû 5.6 âåðíû óòâåðæäåíèÿA · B ∼ (A · J) 1 B è (J · A) 1 B ∼ B · A. Êðîìå òîãî, ïî ïóíêòó1 íàñòîÿùåé ëåììû âåðíî, ÷òî A · J ∼ J · A, îáúåäèíÿÿ äàííûåñîîòíîøåíèÿ è èñïîëüçóÿ ëåììó 5.2, ïîëó÷àåì òðåáóåìîå.4. Áåç îãðàíè÷åíèÿ îáùíîñòè ìîæíî ñ÷èòàòü, ÷òî s(A) > 0, òîãäà ïîëó÷àåì, ÷òî A · B ∼ (A/J s(A) ) · J s(A) · B . Èñïîëüçóÿ ïóíêòû 2 è 3òåêóùåé ëåììû è ó÷èòûâàÿ, ÷òî s(A/J s(A) ) = 0, èìååì (A/J s(A) ) ·J s(A) · B ∼ (A/J s(A) ) · J s(A)−1 · B · J ∼ . .

. ∼ (A/J s(A) ) · B · J s(A) ∼B · (A/J s(A) ) · J s(A) ∼ B · A, ÷òî è òðåáîâàëîñü.5. Âûòåêàåò èç öåïî÷êè ñîîòíîøåíèé A/B ∼ (B · (B \ A))/B ∼((B \ A) · B)/B ∼ (B \ A) · (B/B) ∼ B \ A. Ïåðâîå ñîîòíîøåíèåñëåäóåò èç ïóíêòà 1 ëåììû 5.6 è ëåììû 5.2, òðåòüå ñîîòíîøåíèåâûòåêàåò èç ïóíêòà 3 ëåììû 5.6, âòîðîå èç ïóíêòà 4 äîêàçûâàåìîéëåììû, à ÷åòâ¼ðòîå èç ëåììû 5.7.6.

Èç óñëîâèÿ (A/B)/C ∈ Tpk âûòåêàåò íåðàâåíñòâî s(C) 6 s(A/B),îòêóäà ñëåäóåò, ÷òî s(B) + s(C) 6 s(A) 6 k , òàêèì îáðàçîììîæíî çàêëþ÷èòü, ÷òî C · B ∈ Tpk . Èç âûâîäèìîñòè ñåêâåíöèè(A/B)/C → A/(C · B) âûòåêàåò ñîîòíîøåíèå (A/B)/C ∼ A/(C · B).Àíàëîãè÷íî äîêàçûâàåòñÿ ñîîòíîøåíèå (A/C)/B ∼ A/(B · C). Ïðèìåíÿÿ ïóíêò 2 äàííîé ëåììû è ëåììó 5.2, ïîëó÷àåì ñîîòíîøåíèåA/(C · B) ∼ A/(B · C). Îáúåäèíÿÿ òðè äîêàçàííûõ ñîîòíîøåíèÿ, ïîòðàíçèòèâíîñòè îòíîøåíèÿ ñîâìåñòèìîñòè ïîëó÷àåì òðåáóåìîå.75Ñëåäóþùàÿ ëåììà ïîêàçûâàåò, ÷òî ñ òî÷êè çðåíèÿ îòíîøåíèÿ ñîâìåñòèìîñòè íèæíèé èíäåêñ ïðè ñâÿçêàõ j , ↓j , ↑j íå èìååò çíà÷åíèÿ.Ëåììà 5.9.1.

Äëÿ ëþáûõ òèïîâ A, B ∈ Tpk , òàêèõ ÷òî s(A)+s(B) 6 k+1, è ëþáûõ èíäåêñîâ i, j , òàêèõ ÷òî ñîîòâåòñòâóþùèå òèïû îïðåäåëåíû,èìååò ìåñòî ñîîòíîøåíèå A i B ∼ A j B .2. Äëÿ ëþáûõ òèïîâ A, B ∈ Tpk , òàêèõ ÷òî s(A) > s(B), è ëþáûõ èíäåêñîâ i, j , òàêèõ ÷òî ñîîòâåòñòâóþùèå òèïû îïðåäåëåíû, èìååòìåñòî ñîîòíîøåíèå A ↑i B ∼ A ↑j B .3. Äëÿ ëþáûõ òèïîâ A, B ∈ Tpk , òàêèõ ÷òî s(B) > 1 è s(A) >s(B)−1, è ëþáûõ èíäåêñîâ i, j , òàêèõ ÷òî ñîîòâåòñòâóþùèå òèïûîïðåäåëåíû, èìååò ìåñòî ñîîòíîøåíèå B ↓i A ∼ B ↓j A.Äîêàçàòåëüñòâî.1. Ïîñêîëüêó s(A) + s(B) 6 k + 1, òî òèï A l B îïðåäåë¼í äëÿ âñåõl 6 s(A). Ïóñòü áåç îãðàíè÷åíèÿ îáùíîñòè i < j 6 s(A).

ÒîãäàA i B ∼ (J j · (J j \ A)) i B ∼ (J j i B) · (J j \ A) ∼ J i−1 · B · J j−i ·(J j \ A) ∼ J j−1 · B · (J j \ A) ∼ (J j−1 · J · (J j \ A)) j B ∼ A j B ,÷òî è òðåáîâàëîñü. Ïåðâîå è øåñòîå ñîîòíîøåíèÿ ñëåäóþò èç ïóíêòà1, à òðåòüå èç ïóíêòà 6 ëåììû 5.6. Âòîðîå è ïÿòîå ñîîòíîøåíèÿâûòåêàþò èç ëåììû 4.3, ÷åòâ¼ðòîå ñîîòíîøåíèå äîêàçàíî â ëåììå5.8.2. Ïîñêîëüêó s(A) > s(B), òî òèï A ↑l B îïðåäåë¼í äëÿ âñåõ l 6 s(A) −s(B) + 1.

Òîãäà èìååì A ↑i B ∼ ((A ↑j B) j B) ↑i B ∼ ((A ↑j B) iB) ↑i B ∼ A ↑j B , ÷òî è òðåáîâàëîñü. Ïåðâîå ñîîòíîøåíèå äîêàçàíîâ ïóíêòå 6 ëåììû 5.6, âòîðîå âûòåêàåò èç ïåðâîãî ïóíêòà íàñòîÿùåéëåììû, à òðåòüå äîêàçàíî â ïóíêòå 5 ëåììû 5.6.3. Ïîñêîëüêó s(A) > s(B) − 1 > 0, òî òèï B ↓l A îïðåäåë¼í äëÿ âñåõl 6 s(B). Òîãäà èìååì B ↓i A ∼ B ↓i (B j (B ↓j A)) ∼ B ↓i (B i(B ↓j A)) ∼ B ↓j A, ÷òî è òðåáîâàëîñü. Ïåðâîå ñîîòíîøåíèå äîêàçàíî76â ïóíêòå 6 ëåììû 5.6, âòîðîå âûòåêàåò èç ïåðâîãî ïóíêòà íàñòîÿùåéëåììû, à òðåòüå äîêàçàíî â ïóíêòå 5 ëåììû 5.6.Ñëåäóþùàÿ ëåììà è ñëåäñòâèå ïîñëå íå¼ ïîçâîëÿþò èçó÷àòü îòíîøåíèå ñîâìåñòèìîñòè òîëüêî äëÿ òèïîâ, íå ñîäåðæàùèõ ¾ðàçðûâíûõ¿ñâÿçîê j , ↓j , ↑j .Îïðåäåëåíèå 5.3.Òèï A ∈ Tpk íàçûâàåòñÿ íåïðåðûâíûì, åñëè îí íåñîäåðæèò ñâÿçîê ↑j , ↓j , j äëÿ ëþáîãî j .Ëåììà 5.10.1.

Äëÿ ëþáûõ òèïîâ A, B ∈ Tpk , òàêèõ ÷òî ê òîìó æå A ↑j B ∈ Tpk ,âûïîëíÿåòñÿ ñîîòíîøåíèå A ↑j B ∼ (A/B) · J .2. Äëÿ ëþáûõ òèïîâ A, B ∈ Tpk , òàêèõ ÷òî ê òîìó æå B ↓j A ∈ Tpk ,âûïîëíÿåòñÿ ñîîòíîøåíèå B ↓j A ∼ A/(B/J).3. Äëÿ ëþáûõ òèïîâ A, B ∈ Tpk , òàêèõ ÷òî ê òîìó æå Aj B ∈ Tpk ,âûïîëíÿåòñÿ ñîîòíîøåíèå A j B ∼ (A/J) · B .Äîêàçàòåëüñòâî.1. Óñëîâèå A ↑j B ∈ Tpk âëå÷¼ò âûïîëíåíèå íåðàâåíñòâ s(B) 6 s(A) ès(A)−s(B)+1 6 k , òîãäà (A/B)·J ∈ Tpk . Ïîñêîëüêó âñå êîððåêòíûåòèïû âèäà A ↑j B ñîâìåñòèìû äðóã ñ äðóãîì, äîñòàòî÷íî äîêàçàòüóòâåðæäåíèå äëÿ êàêîãî-òî îäíîãî çíà÷åíèÿ j , âîçüì¼ì j = s(A) −s(B) + 1 = s(A/B) + 1.

Òîãäà óòâåðæäåíèå ñëåäóåò èç âûâîäèìîñòèñåêâåíöèè (A/B) · J → A ↑(s(A/B)+1) B :A/B → A/B(A/B) · B → A((A/B) · J) s(A/B)+1 B → A(A/B) · J → A ↑(s(A/B)+1) B2. Óñëîâèå B ↓j A ∈ Tpk âëå÷¼ò âûïîëíåíèå íåðàâåíñòâ s(B) > 1 ès(A) > s(B) − 1, îòêóäà ñëåäóåò, ÷òî A/(B/J) ∈ Tpk . Ïîñêîëüêó77âñå êîððåêòíûå òèïû âèäà A ↓j B ñîâìåñòèìû äðóã ñ äðóãîì, äîñòàòî÷íî äîêàçàòü óòâåðæäåíèå äëÿ êàêîãî-òî îäíîãî çíà÷åíèÿ j ,âîçüì¼ì j = 1.

Òîãäà ïî ïóíêòó 5 ëåììû 5.8 è ëåììå 5.2 èìååìA/(B/J) ∼ A/(J \ B), à ïî ïóíêòó 1 ëåììû 5.6 èìååì B ∼ J ·(J \ B).Äîêàæåì âûâîäèìîñòü ñåêâåíöèè A/(J \ B) → (J · (J \ B)) ↓1 A.A/(J \ B) → A/(J \ B)(A/(J \ B)) · (J \ B) → A(J · (J \ B)) 1 (A/(J \ B)) → AA/(J \ B) → (J · (J \ B)) ↓1 AÎòñþäà ïî òðàíçèòèâíîñòè îòíîøåíèÿ ñîâìåñòèìîñòè ïîëó÷àåì òðåáóåìîå.3. Èç óñëîâèÿ Aj B ∈ Tpk ñëåäóåò, ÷òî s(A) > 1 è s(A)−1+s(B) 6 k ,ïîýòîìó (A/J) · B ∈ Tpk .