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

.. Îïðåäåëèì ìíîæåñòâà ΩOΓ = {hO, ki ∈ ΩΓ }, ΩΓ = {h⊗, ki ∈ ΩΓ },−+= {hp, ki ∈ ΩΓ |= {hp, ki ∈ ΩΓ | p ∈ Var}, ΩAtΩΓ = {h, ki ∈ ΩΓ }, ΩAtΓΓ+−OOAtAtp ∈ Var}, ΩAtΓ = ΩΓ ∪ ΩΓ , ΩΓ = ΩΓ ∪ ΩΓ . Ïîëîæèì In(α, β) = {γ ∈ ΩΓ |α < γ < β} ∪ {γ ∈ ΩΓ | β < γ < α}, Out(α, β) = ΩΓ − In(α, β) − {α, β}è Prec(α) = {γ ∈ ΩΓ | γ < α}. Äëÿ êàæäîãî âõîæäåíèÿ α ∈ ΩΓ îáîçíà⊗÷èì ÷åðåç δΓ (α) ðàçíîñòü |Prec(α) ∩ ΩOΓ | − |Prec(α) ∩ ΩΓ |.

Àíàëîãè÷íî⊗îáîçíà÷èì δΓ (α, β) = |In(α, β) ∩ ΩOΓ | − |In(α, β) ∩ ΩΓ |. Ôàêòè÷åñêè, âå-ëè÷èíà δΓ (α) ðàâíà ðàçíîñòè ìåæäó ñóììàðíûì ÷èñëîì çíà÷êîâ O è è ÷èñëîì ñâÿçîê ⊗ ñëåâà îò âõîæäåíèÿ α, à δΓ (α, β) ðàçíîñòè ìåæäóñîîòâåòñòâóþùèìè âåëè÷èíàìè äëÿ èíòåðâàëà ìåæäó α è β .Îïðåäåëåíèå 3.4.Íåîðèåíòèðîâàííûé ãðàô G = hΩΓ , Ei, ãäå E ⊂ΩΓ × ΩΓ ñèììåòðè÷íîå áèíàðíîå îòíîøåíèå, íàçûâàåòñÿ <Γ -ïëàíàðíûì , åñëè äëÿ ëþáûõ ð¼áåð (α1 , α2 ), (β1 , β2 ) ∈ E ëèáî In(α1 , α2 ) ⊆In(β1 , β2 ), ëèáî In(β1 , β2 ) ⊆ In(α1 , α2 ), ëèáî In(α1 , α2 ) ∩ In(β1 , β2 ) = ∅.Íåôîðìàëüíî ýòî îçíà÷àåò, ÷òî åñëè ýëåìåíòû ìíîæåñòâà ΩΓ ðàñïîëîæåíû íà îñè àáñöèññ â ïîðÿäêå <Γ , òî ð¼áðà ãðàôà G ìîæíî íàðèñîâàòüâ âåðõíåé ïîëóïëîñêîñòè áåç ïåðåñå÷åíèé.Ïðèìåð 3.6.Ïóñòü Γ = ((p1 ⊗ p2 ) O(p3 ⊗ p3 ))((p2 ⊗ p1 ) O p4 )p4 , òîãäàèçîáðàæ¼ííûé íà ðèñóíêå ãðàô G = hΩ, Ei ÿâëÿåòñÿ <Γ -ïëàíàðíûì.46 p1 ⊗ p2 O p2 ⊗ p3 p 3 ⊗ p1 O p 4 p4Îïðåäåëåíèå 3.5.Óïðîù¼ííîé ñåòüþ äîêàçàòåëüñòâà íàçûâàåòñÿ ïà-ðà N = hΩΓ , Ei, ãäå E ñèììåòðè÷íîå áèíàðíîå îòíîøåíèå, íàçûâàåìîåìíîæåñòâîì àêñèîìíûõ ñâÿçåé , óäîâëåòâîðÿþùàÿ ñëåäóþùèì óñëîâèÿì:⊗1.

|ΩOΓ | − |ΩΓ | = 2,2. E çàäà¼ò ðàçáèåíèå ìíîæåñòâà ΩAtΓ íà ïàðû, ïðè ýòîì â êàæäóþ ïàðóâõîäÿò ýëåìåíòû hp, ki è hp, li äëÿ íåêîòîðîé ïåðåìåííîé p ∈ Var.3. ∀hα, βi ∈ E (δΓ (α, β) = 1).4. N ÿâëÿåòñÿ <Γ -ïëàíàðíûì ãðàôîì.Ïðèìåð 3.7.Ïóñòü Γ = (p2 ⊗ p3 )p3 (p2 ⊗ p1 )p1 , òîãäà èçîáðàæ¼ííûé íàðèñóíêå ãðàô N = hΩΓ , Ei ÿâëÿåòñÿ óïðîù¼ííîé ñåòüþ äîêàçàòåëüñòâàäëÿ ñåêâåíöèè → Γ. Çàìåòèì, ÷òî ñåêâåíöèÿ → Γ âûâîäèìà â èñ÷èñëåíèè MCLL. p2 ⊗ p3 p3 p 2 ⊗ p1 p 1Ñëåäóþùàÿ òåîðåìà ñëåäóåò èç òåîðåìû 7.12 ðàáîòû [28].Òåîðåìà 6.Äëÿ âñÿêîé âûâîäèìîé â MCLL ñåêâåíöèè Γ ñóùåñòâóåòóïðîù¼ííàÿ ñåòü äîêàçàòåëüñòâà, òî åñòü ìîæíî íàéòè îòíîøåíèåAtE ∈ ΩAtΓ × ΩΓ , òàêîå ÷òî ãðàô N = hΩΓ , Ei áóäåò óïðîù¼ííîé ñåòüþäîêàçàòåëüñòâà.3.4Îöåíêè íà ÷èñëî âõîæäåíèé àòîìîâ â ñîâìåùàþùèé òèï äàííîì ðàçäåëå íà îñíîâå óïðîù¼ííûõ ñåòåé äîêàçàòåëüñòâà ìû äîêàæåì, ÷òî ïðè íåêîòîðûõ óñëîâèÿõ íà âõîæäåíèÿ ïåðåìåííîé p è å¼ îòðè47öàíèÿ â ñîâìåñòèìûå òèïû A è B ìîæíî îöåíèòü ñíèçó ÷èñëî âõîæäåíèéýòîé ïåðåìåííîé è å¼ îòðèöàíèÿ â ñîâìåùàþùèé òèï C .

 äàëüíåéøåìáóäåì îáîçíà÷àòü ÷èñëî âõîæäåíèé àòîìîâ p è p â ôîðìóëó A ÷åðåç |A|pè |A|p . Ïðè ýòîì ïðè ïîäñ÷¼òå |A|p âõîæäåíèÿ p íå ó÷èòûâàþòñÿ. Íàïîìíèì, ÷òî åñëè α íåêîòîðîå âõîæäåíèå àòîìà â ïîñëåäîâàòåëüíîñòüôîðìóë Γ, òî ÷åðåç δΓ (α) îáîçíà÷àåòñÿ ðàçíîñòü ìåæäó ñóììàðíûì ÷èñëîì âõîæäåíèé ïàðîâ è ðîìáîâ è ÷èñëîì òåíçîðîâ â ìíîæåñòâå ΩΓ ñëåâàîò α.Ïðèìåð 3.8.Ïóñòü A = (p1 ⊗ p2 ) O((p1 O p2 ) ⊗ p1 ), òîãäà |A|p1 = 2,|A|p1 = 1, |A|p2 = |A|p2 = 1. Åñëè α âõîæäåíèå àòîìà p2 â òèï A, òîδA (α) = 2.Äîêàæåì íåñêîëüêî âñïîìîãàòåëüíûõ óòâåðæäåíèé.Ëåììà 3.6.Äëÿ ëþáîé ôîðìóëû A ∈ Fm âåðíî, ÷òî d(A⊥ ) = −d(A).Äîêàçàòåëüñòâî. Èíäóêöèÿ ïî ïîñòðîåíèþ ôîðìóëû A.  ñëó÷àå A ∈At óòâåðæäåíèå âûïîëíÿåòñÿ.

Ïóñòü A = B ⊗ C , òîãäà A⊥ = C ⊥ O B ⊥è d(A⊥ ) = d(C ⊥ ) + 1 + d(B ⊥ ) = −(d(B) + d(C) − 1) = −d(A). Ñëó÷àéA = B O C ðàçáèðàåòñÿ àíàëîãè÷íî.Ëåììà 3.7.Äëÿ ëþáîé ôîðìóëû A ∈ Fm è ëþáîé ïåðåìåííîé p ∈ Varâûïîëíÿþòñÿ ðàâåíñòâà |A|p = |A⊥ |p è |A|p = |A⊥ |p .Äîêàçàòåëüñòâî. Èíäóêöèÿ ïî ïîñòðîåíèþ ôîðìóëû A.Ëåììà3.8.Ïóñòü A ∈ Fm ïðîèçâîëüíàÿ ôîðìóëà èñ÷èñëåíèÿMCLL, p ∈ Var ôîðìóëà, òàêàÿ ÷òî |A|p = 1 è α åäèíñòâåííîå âõîæäåíèå p â ôîðìóëó A.

Ïóñòü α0 åäèíñòâåííîå âõîæäåíèå pâ ôîðìóëó A⊥ , òîãäà δA⊥ (α0 ) = δA (α) − d(A).Äîêàçàòåëüñòâî. Èíäóêöèÿ ïî ïîñòðîåíèþ ôîðìóëû A. Åñëè A = p,òî δA⊥ (α0 ) = 1 è δA (α) − d(A) = 1 − 0 = 1, áàçà èíäóêöèè äîêàçàíà.Ïóñòü A = B ⊗ C , ñîîòâåòñòâåííî A⊥ = C ⊥ O B ⊥ , òîãäà âîçìîæíûäâà ïîäñëó÷àÿ â çàâèñèìîñòè îò òîãî, â êàêóþ èç ïîäôîðìóë âõîäèò48ïåðåìåííàÿ p (äëÿ ñîêðàùåíèÿ çàïèñè ìû îòîæäåñòâèì âõîæäåíèÿ p âA è â îäíó èç ïîäôîðìóë B è C ). Ïóñòü îíà âõîäèò â ïîäôîðìóëó B ,òîãäà δA (α) = δB (α) è δA⊥ (α0 ) = 1+d(C ⊥ )+1+(δB ⊥ (α0 )−1) = 1−d(C)+δB (α) − d(B) = −d(A) + δA (α), ÷òî è òðåáîâàëîñü.

Òåïåðü ïóñòü p âõîäèòâ ïîäôîðìóëó C , òîãäà δA (α) = δC (α) − 1 + d(B), ïðè ýòîì δA⊥ (α0 ) =δC ⊥ (α0 ) = δC (α) − d(C) = δA (α) − (d(B) + d(C) − 1) = δA (α) − d(A), ÷òîè áûëî íóæíî. Ñëó÷àé A = B O C ðàçáèðàåòñÿ àíàëîãè÷íî.Ëåììà 3.9.Ïóñòü A, B ∈ Fm ñîâìåñòèìûå ôîðìóëû, C èõ ñîâ-ìåùàþùàÿ ôîðìóëà.

Òîãäà âûïîëíÿþòñÿ ñëåäóþùèå óòâåðæäåíèÿ:1. Åñëè p ∈ Var ïåðåìåííàÿ, òàêàÿ ÷òî |A|p = |B|p = 1 è |A|p =|B|p = 0, à α è β âõîæäåíèÿ p â A è B ñîîòâåòñòâåííî, òî|C|p + |C|p > |δA (α) − δB (β)| + 1.2. Åñëè p ∈ Var ïåðåìåííàÿ, òàêàÿ ÷òî |A|p = |B|p = 0 è |A|p =|B|p = 1, à α è β âõîæäåíèÿ p â A è B ñîîòâåòñòâåííî, òî|C|p + |C|p > |δA (α) − δB (β)| + 1.Äîêàçàòåëüñòâî.

Äîñòàòî÷íî äîêàçàòü ïåðâûé ïóíêò ëåììû, âòîðîéäîêàçûâàåòñÿ àíàëîãè÷íî. Ïî îïðåäåëåíèþ ñîâìåñòèìîñòè ñåêâåíöèè→ A⊥ C è → B ⊥ C ÿâëÿþòñÿ âûâîäèìûìè. Îáîçíà÷èì ÷åðåç α0 è β 0åäèíñòâåííûå âõîæäåíèÿ àòîìà p â A⊥ è B ⊥ ñîîòâåòñòâåííî. Çàìåòèì, ÷òî â ñèëó ñîâìåñòèìîñòè ôîðìóë A è B è ëåììû 3.8 âûïîëíÿþòñÿ ðàâåíñòâà δA⊥ (α0 ) = δA (α) − d(A) = δA (α) − d(B) è ðàâåíñòâîδB ⊥ (β 0 ) = δB (β)−d(B), òàêèì îáðàçîì, δA⊥ (α0 )−δB ⊥ (β 0 ) = δA (α)−δB (β).Îáîçíà÷èì ýòó ðàçíîñòü ÷åðåç δ0 , áåç îãðàíè÷åíèÿ îáùíîñòè ìîæíî ñ÷èòàòü δ0 > 0.Ïóñòü γ íåêîòîðîå âõîæäåíèå àòîìà â ôîðìóëó C , îòîæäåñòâèì åãî ñ ñîîòâåòñòâóþùèìè âõîæäåíèÿìè ýòîãî æå àòîìà â ïîñëåäîâàòåëüíîñòè ôîðìóë A⊥ C è B ⊥ C . Çàìåòèì, ÷òî â ñèëó ñîâìåñòèìîñòèôîðìóë A è B âûïîëíÿåòñÿ ðàâåíñòâî δA⊥ C (γ) = d(A⊥ ) + 1 + δC (γ) =d(B ⊥ ) + 1 + δC (γ) = δB ⊥ C (γ).

Îáîçíà÷èì ýòó âåëè÷èíó ÷åðåç δ(γ).49Ïî òåîðåìå 6 äëÿ ñåêâåíöèé → A⊥ C è → B ⊥ C íàéäóòñÿ óïðîù¼ííûå ñåòè äîêàçàòåëüñòâà N1 è N2 ñ ìíîæåñòâàìè àêñèîìíûõ ñâÿçåé E1è E2 ñîîòâåòñòâåííî. Ïî îïðåäåëåíèþ óïðîù¼ííîé ñåòè äîêàçàòåëüñòâàíàéä¼òñÿ òàêàÿ ïîñëåäîâàòåëüíîñòü âõîæäåíèé α0 = α0 , α1 , . . . , α2n = β 0 ,â êîòîðîé íà íå÷¼òíûõ ìåñòàõ íàõîäÿòñÿ âõîæäåíèÿ àòîìà p â ôîðìóëó C , à íà ÷¼òíûõ àòîìà p â ôîðìóëó C èëè (â ñëó÷àå α0 è α2n ) âôîðìóëû A⊥ è B ⊥ è äëÿ êîòîðîé äëÿ âñåõ i < n âûïîëíÿþòñÿ óñëîâèÿ(α2i , α2i+1 ) ∈ E1 , (α2i+1 , α2i+2 ) ∈ E2 .

Çàìåòèì, ÷òî α0 < α1 è α2n < α2n−1â ñìûñëå ëèíåéíîãî ïîðÿäêà íà ñåêâåíöèÿõ → A⊥ C è → B ⊥ C . Îòñþäà ñëåäóåò, ÷òî δ(α1 ) = δ(α0 ) + 1 è δ(α2n−1 ) = δ(α2n ) + 1, ÷òî âëå÷¼òðàâåíñòâî |δ(α1 ) − δ(α2n−1 )| = δ0 .Çàìåòèì, ÷òî â ñèëó ïóíêòà 3 îïðåäåëåíèÿ óïðîù¼ííîé ñåòè äîêàçàòåëüñòâà äëÿ âñåõ i < 2n áóäåò âûïîëíåíî óñëîâèå |δ(αi )−δ(αi+1 )| = 1.Îòñþäà çàêëþ÷àåì, ÷òî |δ(α1 ) − δ(α2n−1 )| 6 2n − 2, òî åñòü 2n > δ0 + 2.Ïîñêîëüêó ïî ïîñòðîåíèþ ïîñëåäîâàòåëüíîñòè {αi | 0 6 i 6 2n} âñåâõîæäåíèÿ α1 , .

. . , α2n−1 ÿâëÿþòñÿ âõîæäåíèÿìè ëèáî àòîìà p, ëèáî àòîìà p â ôîðìóëó C , òî |C|p + |C|p > 2n − 1 > δ0 + 1 = |δA (α) − δB (β)| + 1.Ëåììà äîêàçàíà.Ïðèìåð 3.9.Ïóñòü A = (q ⊗ p) O r, B = (q O p) ⊗ r, òîãäà ôîðìóëû A èB ñîâìåñòèìû, è C = (q ⊗ p) O p O(p ⊗ r) èõ ñîâìåùàþùàÿ ôîðìóëà.Ïóñòü α è β âõîæäåíèÿ àòîìà p â ôîðìóëû A è B ñîîòâåòñòâåííî, α0è β 0 âõîæäåíèÿ àòîìà p â ôîðìóëû A⊥ è B ⊥ . Çàìåòèì, ÷òî δA (α) −δB (β) = δA⊥ (α0 ) − δB ⊥ (β 0 ) = 2, òîãäà ïî ëåììå 3.9 |C|p + |C|p > 3.rr⊗ pO pO qq⊗ q⊗ pO pO p⊗ rÐèñ. 3.1: Èëëþñòðàöèÿ äîêàçàòåëüñòâà ëåììû 3.9.50Îòíîøåíèÿ E1 è E2 èç äîêàçàòåëüñòâà ëåììû 3.9 ïîêàçàíû íà ðèñóíêå 3.1.

Ïóòü ïî îòíîøåíèþ E1 ∪ E2 èç α0 â β 0 îáîçíà÷åí óòîëù¼ííûìèëèíèÿìè.Ëåììà 3.10.Ïóñòü A, B ∈ Fm ñîâìåñòèìûå ôîðìóëû, à q ïå-ðåìåííàÿ, òàêàÿ ÷òî |A|q = |A|q = 1 è |B|q = |B|q = 0. Ïóñòüâõîæäåíèÿ α è β àòîìîâ q è q â ôîðìóëó A óäîâëåòâîðÿþò óñëîâèþ|δA (α) − δA (β)| =6 1.

Òîãäà äëÿ âñÿêîé ôîðìóëû C , êîòîðàÿ ÿâëÿåòñÿ ñîâìåùàþùåé äëÿ A è B , âûïîëíÿåòñÿ íåðàâåíñòâî |C|q + |C|q >|δA (α) − δA (β)| + 1.Äîêàçàòåëüñòâî. Îáîçíà÷èì ÷åðåç α0 è β 0 âõîæäåíèÿ q è q â ôîðìóëó A⊥ , ñîîòâåòñòâóþùèå âõîæäåíèÿì α è β . Òîãäà ïî ëåììå 3.8 èìååìδA⊥ (α0 ) − δA⊥ (β 0 ) = (δA (α) − d(A)) − (δA (β) − d(A)) = δA (α) − δA (β).Îáîçíà÷èì ýòó âåëè÷èíó ÷åðåç δ0 , òîãäà ïî óñëîâèþ ëåììû δ0 6= 1.Çàìåòèì, ÷òî â ñèëó óñëîâèÿ δ0 6= 1 âõîæäåíèÿ α0 è β 0 íå ìîãóò áûòü ñâÿçàíû àêñèîìíîé ñâÿçüþ. Ñëåäóÿ îáîçíà÷åíèÿì ëåììû 3.9è ðàññóæäàÿ òàê æå, êàê ïðè å¼ äîêàçàòåëüñòâå, ìû ïîëó÷èì, ÷òî íàéä¼òñÿ òàêàÿ ïîñëåäîâàòåëüíîñòü β1 , α1 , . .

. , βk , αk ∈ ΩAtC , ÷òî âñå βj ÿâëÿþòñÿ âõîæäåíèÿìè àòîìà q , à âñå αj âõîæäåíèÿìè àòîìà q , ïðèýòîì äëÿ âñåõ i 6 k âåðíî, ÷òî (βi , αi ) ∈ E2 , äëÿ âñåõ i < k âåðíî,÷òî (αi , βi+1 ) ∈ E1 , à òàêæå (α0 , β1 ) ∈ E1 è (αk , β 0 ) ∈ E1 . Çàìåòèì, ÷òîδ(β1 ) − δ(αk ) = δ(α0 ) − δ(β 0 ) = δ0 . Àíàëîãè÷íî ïðåäûäóùåé ëåììå ïîëó÷àåì, ÷òî |δ0 | < 2k − 1, îòêóäà è ïîëó÷àåòñÿ óòâåðæäåíèå ëåììû. Ëåììàäîêàçàíà.Ïðèìåð 3.10.Ïóñòü A = p O q O q O p, B = s O t O t O s, òîãäà ôîðìó-ëû A è B ñîâìåñòèìû, à C èõ ñîâìåùàþùàÿ ôîðìóëà. Îáîçíà÷èì ÷å-ðåç α è β âõîæäåíèÿ àòîìîâ p è p â ôîðìóëó A, òîãäà δA (α)−δA (β) = −3.Ïî ëåììå 3.10 âûïîëíÿåòñÿ íåðàâåíñòâî |C|p + |C|p > 4.

Àíàëîãè÷íûìîáðàçîì âåðíî íåðàâåíñòâî |C|s + |C|s > 4.Ìû áóäåì íàçûâàòü ôîðìóëó A ∈ Fm òîíêîé , åñëè äëÿ âñÿêîéïåðåìåííîé p ∈ Var âûïîëíÿþòñÿ óñëîâèÿ |A|p 6 1 è |A|p 6 1. Ïåðå51ìåííàÿ p íàçûâàåòñÿ íåéòðàëüíîé äëÿ A, åñëè |A|p = |A|p = 1. Åñëèïåðåìåííàÿ p íå ÿâëÿåòñÿ íåéòðàëüíîé äëÿ òîíêîé ôîðìóëû A, íî Añîäåðæèò îäèí èç àòîìîâ p è p, òî äàííûé àòîì áóäåì íàçûâàòü îäè-íî÷íûì. Ïàðà òîíêèõ ñîâìåñòèìûõ ôîðìóë A, B íàçûâàåòñÿ òîíêîé,åñëè äàííûå ôîðìóëû íå ñîäåðæàò îáùèõ íåéòðàëüíûõ ïåðåìåííûõ. Åñëè |A|π = 1, îáîçíà÷èì ÷åðåç γA (pi) âõîæäåíèå àòîìà π â ôîðìóëó A.Îáîçíà÷èì ÷åðåç D(A) ñóììóP(|δA (γA (p), γA (p))| + 1), ãäå p ïðîáåãàpåò âñå íåéòðàëüíûå äëÿ A ïåðåìåííûå, òàêèå ÷òî δA (γA (p), γA (p)) 6= 1.Åñëè A è B îáðàçóþò òîíêóþ ïàðó, îáîçíà÷èì ÷åðåç E(A, B) ñóììóP(|δA (γA (π)) − δB (γB (π))| + 1), ãäå ñóììèðîâàíèå âåä¼òñÿ ïî âñåì îäèπíî÷íûì àòîìàì π (â ñèëó ñîâìåñòèìîñòè ìíîæåñòâî îäèíî÷íûõ àòîìîâäëÿ A è B ñîâïàäàåò).