Лекции В.А. Захарова, страница 37

Ðàññìîòðèì ýòó òðàññó tr .Äëÿ êàæäîãî i, i ≥ 0, ïîëîæèìBi = {ψ : ψ ∈ FLSubϕ1 , tr |i |= ψ .}Ñîãëàñíî óòâåðæäåíèþ 4, âñå ïîñòðîåííûå ìíîæåñòâà Biÿâëÿþòñÿ ñîãëàñîâàííûìè.Ïîêàæåì, ÷òî ïîñëåäîâàòåëüíîñòü ïàð(tr [0], B0 ), (tr [1], B1 ), (tr [2], B2 ), . . . , (tr [n], Bn ), (tr [n+1], Bn+1 ), .

. .îáðàçóåò èñêîìûé ðàäóæíûé ìàðøðóò â ãðàôå Γϕ1 .ÒÀÁËÈ×ÍÛÉ ÌÅÒÎÄ ÂÅÐÈÔÈÊÀÖÈÈÄåéñòâèòåëüíî,1. Äëÿ ëþáîãî n, n ≥ 0, âåðíî tr [n] −→ tr [n + 1], ïîñêîëüêó tr ìàðøðóò â LTS M .2. Äëÿ ëþáîãî n, n ≥ 0 è äëÿ ëþáîé ôîðìóëûâåðíîXψ ∈ Bn ⇐⇒ ψ ∈ Bn+1ψ ∈ XSubϕ1 ,XïîñêîëüêóXψ ∈ Bn ⇐⇒ tr |n |= Xψ ⇐⇒ tr |n+1 |= ψ ⇐⇒ ψ ∈ Bn+1 .3. tr [0] ∈ S0 (ò. ê. tr íà÷àëüíàÿ òðàññà â M ) è ϕ1 ∈/ B0 (ò. ê.tr |0 6|= ϕ1 ).Çíà÷èò, ïîñëåäîâàòåëüíîñòü(tr [0], B0 ), (tr [1], B1 ), (tr [2], B2 ), . . . , (tr [n], Bn ), (tr [n+1], Bn+1 ), .

. .ÿâëÿåòñÿ ìàðøðóòîì â ãðàôå Γϕ1 ,M , èñõîäÿùèì èç íóæíîéâåðøèíû.ÒÀÁËÈ×ÍÛÉ ÌÅÒÎÄ ÂÅÐÈÔÈÊÀÖÈÈ4. Îñòàëîñü ïîêàçàòü, ÷òî ìàðøðóò(tr [0], B0 ), (tr [1], B1 ), (tr [2], B2 ), . . . , (tr [n], Bn ), (tr [n+1], Bn+1 ), . . .ÿâëÿåòñÿ ðàäóæíûì.Ðàññìîòðèì ïðîèçâîëüíîå ÷èñëî n, n ≥ 0 è ïðîèçâîëüíóþôîðìóëó ψi ∈ URSubϕ1 . Ïîêàæåì, ÷òî ñóùåñòâóåò òàêîåk, k ≥ 0, ÷òî âåðøèíà (tr [n + k], Bn+k ) îêðàøåíà â öâåò i .ÒÀÁËÈ×ÍÛÉ ÌÅÒÎÄ ÂÅÐÈÔÈÊÀÖÈÈÎãðàíè÷èìñÿ ðàññìîòðåíèåì Until-ôîðìóëû ψi = χ0 Uχ2 .(Äëÿ ôîðìóë âèäà ψi = χ0 Rχ2 äîêàçàòåëüñòâî ïðîâåäèòåñàìîñòîÿòåëüíî. )1. Åñëè tr |n 6|= X(χ1 Uχ2 ), òî X(χ1 Uχ2 ) ∈/ Bn , è,ñëåäîâàòåëüíî, âåðøèíà (tr [n], Bn ) îêðàøåíà â öâåò j .2.

À åñëè tr |n |= X(χ1 Uχ2 ), òî tr |n+1 |= χ1 Uχ2 . Òîãäàñóùåñòâóåò òàêîå k, k ≥ 1, ÷òî tr |n+k |= χ2 . Ïîýòîìóχ2 ∈ Bn+k , è âåðøèíà (tr [n + k], Bn+k ) îêðàøåíà â öâåò j .Òàêèì îáðàçîì, âåðøèíû öâåòà j âñòðå÷àþòñÿ â íàøåììàðøðóòå áåñêîíå÷íî ÷àñòî. Ïîñêîëüêó ψi áûëà ïðîèçâîëüíîé(Until-Release)-ôîðìóëîé, ýòî îçíà÷àåò, ÷òî íàø ìàðøðóò âãðàôå Γϕ1 ,M ÿâëÿåòñÿ ðàäóæíûì.ÀËÃÎÐÈÒÌ ÂÅÐÈÔÈÊÀÖÈÈ ÌÎÄÅËÅÉÏÐÎÃÐÀÌÌÍî êàê ïðîâåðèòü, ÷òî èç çàäàííîé âåðøèíû â ãðàôå Γϕ1 ,Míå èñõîäèò íè îäíîãî ðàäóæíîãî ìàðøðóòà?Îðèåíòèðîâàííûé ãðàô Γ íàçûâàåòñÿ ñèëüíî ñâÿçíûì , åñëèäëÿ ëþáîé ïàðû âåðøèí v è u â ãðàôå Γ ñóùåñòâóåò ìàðøðóòèç v â u è ìàðøðóò èç u â v .Âñÿêèé ìàêñèìàëüíûé ñèëüíî ñâÿçíûé ïîäãðàô ãðàôà Γíàçûâàåòñÿ êîìïîíåíòîé ñèëüíîé ñâÿçíîñòè .Êîìïîíåíòó ñèëüíîé ñâÿçíîñòè ãðàôà (ñèñòåìû Õèíòèêêè)Γϕ1 ,M áóäåì íàçûâàòü ðàäóæíîé, åñëè â íåé ñîäåðæàòñÿâåðøèíû âñåõ öâåòîâ.ÀËÃÎÐÈÒÌ ÂÅÐÈÔÈÊÀÖÈÈ ÌÎÄÅËÅÉÏÐÎÃÐÀÌÌÒåîðåìà.Èç âåðøèíû v â ãðàôå Γϕ1 ,M èñõîäèò ðàäóæíûé ìàðøðóò òîãäàè òîëüêî òîãäà, êîãäà ñóùåñòâóåò ìàðøðóò , âåäóùèé èçâåðøèíû v õîòÿ áû â îäíó èç âåðøèí õîòÿ áû îäíîé ðàäóæíîéêîìïîíåíòû ñèëüíîé ñâÿçíîñòè.Äîêàçàòåëüñòâî.Ñàìîñòîÿòåëüíî.

Çäåñü âñå î÷åâèäíî.ÀËÃÎÐÈÒÌ ÂÅÐÈÔÈÊÀÖÈÈ ÌÎÄÅËÅÉÏÐÎÃÐÀÌÌôîðìóëà PLTL ϕ è LTSM = hAP, S, S0 , −→, ρi.Èñõîäíûå äàííûå:1. Ïîñòðîèòü ðàâíîñèëüíóþ ïîçèòèâíóþ ôîðìó ϕ1 .2. Ïîñòðîèòü ñèñòåìó Õèíòèêêè Γϕ1 ,M .3. Âûäåëèòü ìíîæåñòâî ïîäôîðìóë URSubϕ1 è ðàñêðàñèòüâåðøèíû ãðàôà Γϕ1 ,M .4.

Âûäåëèòü ðàäóæíûå êîìïîíåíòû ñèëüíîé ñâÿçíîñòè âãðàôå Γϕ1 ,M .5. Âûäåëèòü ìíîæåñòâî V 0 âñåõ âåðøèí ãðàôà Γϕ1 ,M , èçêîòîðûõ äîñòèæèìû ðàäóæíûå êîìïîíåíòû ñèëüíîéñâÿçíîñòè.6. Âûäåëèòü ìíîæåñòâî V 00 âñåõ âåðøèí (s0 , B0 ), äëÿ êîòîðîéâûïîëíÿåòñÿ s0 ∈ S0 , ϕ1 ∈/ B0 .0007. Âû÷èñëèòü V = V ∩ V .Ðåçóëüòàò:M |= ϕ ⇐⇒ V = ∅.ÀËÃÎÐÈÒÌ ÂÅÐÈÔÈÊÀÖÈÈ ÌÎÄÅËÅÉÏÐÎÃÐÀÌÌÏðèìåð.ϕ = p UqLTS M :'s1'- iξ(s1 ) = {p} 6&s0$s2?i$ξ(s2 ) = {q}%yξ(s0 ) = {p}'s3&- iξ(s3 ) = {p} 6&$s4?iξ(s4 ) = {p}%%ÀËÃÎÐÈÒÌ ÂÅÐÈÔÈÊÀÖÈÈ ÌÎÄÅËÅÉÏÐÎÃÐÀÌÌÏðèìåð.ϕ = F(p Uq)1.

Ïîçèòèâíàÿ ôîðìà ϕ1 = p UqFLSubϕ1 = {p, ¬p, q, ¬q, p Uq, X(p Uq)};XSubϕ1 = {X(p Uq)};URSubϕ1 = {p Uq}.ÀËÃÎÐÈÒÌ ÂÅÐÈÔÈÊÀÖÈÈ2. Ñòðîèì ñèñòåìó Õèíòèêêè Γϕ1 ,M{p, ¬q}- ?is1's2's1'- i6{p, ¬q,ϕ1 , Xϕ1 }s0{p, ¬q}is0{p, ¬q,ϕ1 , Xϕ1 }6%s2?i$${¬p, q}ϕ1 , Xϕ1 }i?s4is3&- i6{p, ¬q} {p, ¬q}- is36%{p, ¬q}ϕ1 , Xϕ1 }&i{¬p, q}ϕ1 , Xϕ1 }s4?{p, ¬q}i%ÀËÃÎÐÈÒÌ ÂÅÐÈÔÈÊÀÖÈÈ3. Ðàñêðàøèâàåì âåðøèíû ñèñòåìûΓ ϕ1 ,M{p, ¬q}- ?ys1's2's1'- i6{p, ¬q,ϕ1 , Xϕ1 }s0{p, ¬q}ys0{p, ¬q,ϕ1 , Xϕ1 }6%s2?y$${¬p, q}ϕ1 , Xϕ1 }i?s4is3&- i6{p, ¬q} {p, ¬q}- ys36%{p, ¬q}ϕ1 , Xϕ1 }&y{¬p, q}ϕ1 , Xϕ1 }s4?{p, ¬q}y%ÀËÃÎÐÈÒÌ ÂÅÐÈÔÈÊÀÖÈÈ4. Âûäåëÿåì ðàäóæíûå êîìïîíåíòûñèëüíîéñâÿçíîñòè{p, ¬q}- ?ys1's2's1'- i6{p, ¬q,ϕ1 , Xϕ1 }s0{p, ¬q}ys0{p, ¬q,ϕ1 , Xϕ1 }6%s2?y$${¬p, q}ϕ1 , Xϕ1 }i?s4is3&- i6{p, ¬q} {p, ¬q}- ys36%{p, ¬q}ϕ1 , Xϕ1 }&y{¬p, q}ϕ1 , Xϕ1 }s4?{p, ¬q}y%ÀËÃÎÐÈÒÌ ÂÅÐÈÔÈÊÀÖÈÈ5.

Âûäåëÿåì âåðøèíû èç êîòîðûõäîñòèæèìûðàäóæíûå êîìïîíåíòû{p, ¬q}- ?is1's2's1'- y6{p, ¬q,ϕ1 , Xϕ1 }s0{p, ¬q}ys0{p, ¬q,ϕ1 , Xϕ1 }6%s2?y$${¬p, q}ϕ1 , Xϕ1 }y?s4is3&- i6{p, ¬q} {p, ¬q}- ys36%{p, ¬q}ϕ1 , Xϕ1 }&y{¬p, q}ϕ1 , Xϕ1 }s4?{p, ¬q}y%ÀËÃÎÐÈÒÌ ÂÅÐÈÔÈÊÀÖÈÈ6. Èùåì âåðøèíó (s0 , B) íà êîòîðîéîïðîâåðãàåòñÿϕ1{p, ¬q}- ?is1's2's1'- y6{p, ¬q,ϕ1 , Xϕ1 }y{¬p, q}6%s2?y$${¬p, q}ϕ1 , Xϕ1 }s0s0yy{p, ¬q}{p, ¬q,ϕ1 , Xϕ1 }?s4is3&- i6{p, ¬q} {p, ¬q}ϕ1 , Xϕ1 }&{p, ¬q}- ys36%ϕ1 , Xϕ1 }s4?{p, ¬q}y%ÀËÃÎÐÈÒÌ ÂÅÐÈÔÈÊÀÖÈÈ ÌÎÄÅËÅÉÏÐÎÃÐÀÌÌÎïèñàííûé çäåñü ïîäõîä ê âåðèôèêàöèè ðàñïðåäåëåííûõïðîãðàìì ðåàëèçîâàí â ïðîãðàììíî-èíñòðóìåíòàëüíîé ñèñòåìåâåðèôèêàöèè SPIN .Ìîäåëè ïàðàëëåëüíûõ âçàèìîäåéñòâóþùèõ ïðîöåññîâîïèñûâàþòñÿ íà ÿçûêå PROMELA (Process Meta Language),ñíàáæàþòñÿ òåìïîðàëüíûìè ñïåöèôèêàöèÿìè (PLTLôîðìóëàìè), à çàòåì âûïîëíèìîñòü ýòèõ ôîðìóë ïðîâåðÿåòñÿñèñòåìîé âåðèôèêàöèè SPIN . ñèñòåìå SPIN ïðèìåíÿåòñÿ òàáëè÷íûé àëãîðèòìâåðèôèêàöèè ìîäåëåé ðàñïðåäåëåííûõ ïðîãðàìì.

Äëÿïîâûøåíèÿ åãî ýôôåêòèâíîñòè èñïîëüçóåòñÿ ðÿä ïðèåìîâ:Iïðîâåðêà ìîäåëè ¾íà ëåòó¿;Iðåäóêöèè ÷àñòè÷íûõ ïîðÿäêîâ;Iñèìâîëüíîå ïðåäñòàâëåíèå äàííûõ è äð.ÊÎÍÅÖ ËÅÊÖÈÈ 22Îñíîâûìàòåìàòè÷åñêîéëîãèêèèëîãè÷åñêîãîïðîãðàììèðîâàíèÿËÅÊÒÎÐ: Â.À. ÇàõàðîâËåêöèÿ 23.Êàê óñòðîåíà ìàòåìàòèêà.Èñ÷èñëåíèå ïðåäèêàòîâïåðâîãî ïîðÿäêà.Àêñèîìàòè÷åñêèå òåîðèè.Ýëåìåíòàðíàÿ ãåîìåòðèÿ.Òåîðèÿ ìíîæåñòâÖåðìåëîÔðåíêåëÿ.Àðèôìåòèêà Ïåàíî.Òåîðåìà Ãåäåëÿ î íåïîëíîòå.ìîäàëüíûåëîãèêèyèíòóèöèîíèñòñêàÿëîãèêàyI@@òåîðèÿäîêàçàòåëüñòâ6yäðóãèåëîãè÷åñêèåîïåðàöèè@äðóãàÿ@ñåìàíòèêàëîãè÷åñêèõ@@ñâÿçîêäðóãèåôîðìûëîãè÷åñêîãîâûâîäà@@y äðóãèå êâàíòîðûëîãèêèâûñøèõ ïîðÿäêîâ@ i ñïåöèàëüíûå èíòåðïðåòàöèè- yÊËÀÑÑÈ×ÅÑÊÀßËÎÃÈÊÀàêñèîìàòè÷åñêèåòåîðèèÊàê óñòðîåíà ìàòåìàòèêàÌàòåìàòèêà ýòî ñïåöèôè÷åñêàÿ íàóêà.Îíà íå îòíîñèòñÿ ê ÷èñëó åñòåñòâåííûõ íàóê (ôèçèêà,áîòàíèêà, ãåîëîãèÿ, è ïð.), ò.

ê. îíà íå èìååò äåëà íè ñïðèðîäíûìè ÿâëåíèÿìè, íè ñ ýìïèðè÷åñêèìè çíàíèÿìè.Îíà íå îòíîñèòñÿ ê ÷èñëó ãóìàíèòàðíûõ íàóê (ôèëîñîôèÿ,èñòîðèÿ, ïîëèòîëîãèÿ è ïð. áîëòîëîãèÿ), ò. ê îíà íå çàíèìàåòñÿíè ëþäñêîé äåÿòåëüíîñòüþ, íè ëþäñêèìè âîççðåíèÿìè.Îíà çàíèìàåòñÿ ñîçäàíèåì, ðàçâèòèåì è èçó÷åíèåììàòåìàòè÷åñêèõ òåîðèé óìîçðèòåëüíûõ êîíñòðóêöèé,êîòîðûå ñòðîÿòñÿ ïî ñòðîãèì îáúåêòèâíûì çàêîíàìôîðìàëüíîé ëîãèêè .Êàê óñòðîåíà ìàòåìàòèêàÑòàíèñëàâ Ëåì ñðàâíèâàëìàòåìàòèêó ñ áåçóìíûì ïîðòíûì,êîòîðûé øüåò îäåæäó äëÿíåâåäîìûõ ñóùåñòâ.Ïîðòíîãî íå áåñïîêîèò, êîìóïðèäåòñÿ âïîðó åãî îäåæäà.Îí ëèøü õî÷åò, ÷òîáû ïëàòüåáûëî ñøèòî ïðî÷íî.Êàê óñòðîåíà ìàòåìàòèêàÑ ÷åãî íà÷èíàåòñÿ ðàññêàç î êàæäîì ðàçäåëå ìàòåìàòèêè?IIIIÂíà÷àëå óñëàâëèâàþòñÿ î ñèñòåìå îáîçíà÷åíèé,îïðåäåëÿþò ÿçûê, íà êîòîðîì áóäóò çàïèñûâàòüìàòåìàòè÷åñêèå óòâåðæäåíèÿ (îïðåäåëÿåòñÿ ñèíòàêñèñìàòåìàòè÷åñêîãî ÿçûêà ).Çàòåì ïðèõîäÿò ê ñîãëàøåíèþ îá îñíîâîïîëàãàþùèõñâîéñòâàõ, çàêîíàõ, êîòîðûì äîëæíû óäîâëåòâîðÿòüèíòåðåñóþùèå íàñ îïåðàöèè è îòíîøåíèÿ íàäâîîáðàæàåìûìè îáúåêòàìè (ôîðìóëèðóþòñÿ àêñèîìûìàòåìàòè÷åñêîé òåîðèè ).Äàëåå äîãîâàðèâàþòñÿ î òîì, êàêèå ñðåäñòâà îáîñíîâàíèÿèñòèííîñòè ìàòåìàòè÷åñêèõ óòâåðæäåíèé ñ÷èòàþòñÿäîïóñòèìûìè (îïðåäåëÿåòñÿ àïïàðàò ëîãè÷åñêîãî âûâîäà ).È ïîñëå ýòîãî ïðèñòóïàþò ê ïîëó÷åíèþ ëîãè÷åñêèîáîñíîâàííûõ óòâåðæäåíèé ñôîðìóëèðîâàííîéìàòåìàòè÷åñêîé òåîðèè (âûâîä òåîðåì ).Âîò òàê ñòðîÿòñÿ ôîðìàëüíûå àêñèîìàòè÷åñêèå òåîðèè .Êëàññè÷åñêîå èñ÷èñëåíèå ïðåäèêàòîâÊàê ìîæíî àêñèîìàòèçèðîâàòü òåîðèþ îáùåçíà÷èìûõóòâåðæäåíèé (ôîðìóë)? Íàïðèìåð, òàê:ÀÊÑÈÎÌÛ.1.

Ax1. ϕ1 → (ϕ2 → ϕ1 ),2. Ax2. (ϕ1 → (ϕ2 → ϕ3 )) → ((ϕ1 → ϕ2 ) → (ϕ1 → ϕ3 )),3. Ax3. (ϕ1 & ϕ2 ) → ϕ1 ,4. Ax4. (ϕ1 & ϕ2 ) → ϕ2 ,5. Ax5. ϕ1 → (ϕ2 → (ϕ1 & ϕ2 )),6. Ax6. ϕ1 → (ϕ1 ∨ ϕ2 ),7. Ax7. ϕ2 → (ϕ1 ∨ ϕ2 ),8. Ax8. (ϕ1 → ϕ0 ) → ((ϕ2 → ϕ0 ) → ((ϕ1 ∨ ϕ2 ) → ϕ0 )),9. Ax9. ϕ1 → (¬ϕ1 → ϕ0 ),10. Ax10. ϕ1 ∨ ¬ϕ1 ,Êëàññè÷åñêîå èñ÷èñëåíèå ïðåäèêàòîâÀÊÑÈÎÌÛ.1.

Ax11. ∀X ϕ(X ) → ϕ(t),2. Ax12. ϕ(t) → ∃X ϕ(X ),3. Ax13. ∀X (ϕ1 → ϕ2 (X )) → (ϕ1 → ∀X ϕ2 (X )),4. Ax14. ∀X (ϕ1 (X ) → ϕ2 ) → (∃X ϕ1 (X ) → ϕ2 ).ÏÐÀÂÈËÀ ÂÛÂÎÄÀ.1. Ïðàâèëî îòäåëåíèÿ (modus ponens)2. Ïðàâèëî îáîáùåíèÿϕ∀X ϕϕ, ϕ → ψ,ψÊëàññè÷åñêîå èñ÷èñëåíèå ïðåäèêàòîâËÎÃÈ×ÅÑÊÈÉ ÂÛÂÎÄ.Ïóñòü çàäàíî íåêîòîðîå ìíîæåñòâî ôîðìóë (ãèïîòåç) Γ .Òîãäà ëîãè÷åñêèì âûâîäîì èç ìíîæåñòâà ãèïîòåç Γíàçûâàåòñÿ êîíå÷íàÿ ïîñëåäîâàòåëüíîñòü ôîðìóëϕ1 , ϕ2 , . . .

, ϕn ,â êîòîðîé êàæäàÿ ôîðìóëà ϕi óäîâëåòâîðÿåò îäíîìó èçñëåäóþùèõ óñëîâèé:1. ëèáî ϕi ÿâëÿåòñÿ àêñèîìîé,2. ëèáî ϕi ÿâëÿåòñÿ ãèïîòåçîé, ò. å. ϕi ∈ Γ ,3. ëèáî ϕi ïîëó÷àåòñÿ èç ïðåäøåñòâóþùèõ ôîðìóë ýòîéïîñëåäîâàòåëüíîñòè ïî ïðàâèëó îòäåëåíèÿ èëè ïî ïðàâèëóîáîáùåíèÿ. ýòîì ñëó÷àå ôîðìóëà ϕn íàçûâàåòñÿ âûâîäèìîé èçìíîæåñòâà Γ , è ýòîò ôàêò îáîçíà÷àåòñÿ Γ ` ϕnÔîðìóëà ϕ íàçûâàåòñÿ òåîðåìîé , åñëè ∅ ` ϕ , è ýòîò ôàêòîáîçíà÷àåòñÿ ` ϕ .Êëàññè÷åñêîå èñ÷èñëåíèå ïðåäèêàòîâÈñ÷èñëåíèå ïðåäèêàòîâ ñ ðàâåíñòâîì.Ââåäåì ñïåöèàëüíûé äâóõìåñòíûé ïðåäèêàòíûé ñèìâîë = èäîáàâèì ê àêñèîìàì ÊÈÏ ñëåäóþùèå àêñèîìû ðàâåíñòâà:1.

Ax15. ∀X (X = X ),2. Ax16 ∀X , Y (X = Y → (ϕ(X , X ) → ϕ(X , Y ))).Ïîëó÷åííóþ ñèñòåìó àêñèîì íàçûâàþò êëàññè÷åñêèìèñ÷èñëåíèåì ïðåäèêàòîâ ñ ðàâåíñòâîì ÊÈÏ= .Àëãåáðàè÷åñêàÿ ñèñòåìà I íàçûâàåòñÿ íîðìàëüíîéèíòåðïðåòàöèåé , åñëè äëÿ ëþáîé ïàðû ðàçëè÷íûõ ïðåäìåòîâd1 , d2 èç îáëàñòè èíòåðïðåòàöèè DI âåðíî ñîîòíîøåíèåI 6|= d1 = d2 .Àêñèîìàòè÷åñêèå òåîðèè ïåðâîãî ïîðÿäêàÝëåìåíòàðíàÿ àêñèîìàòè÷åñêàÿ òåîðèÿ îáðàçóåòñÿ èçèñ÷èñëåíèÿ ïðåäèêàòîâ ñ ðàâåíñòâîì çà ñ÷åòIîãðàíè÷åíèÿ ñèãíàòóðû ÿçûêà ëîãèêè ïðåäèêàòîâôèêñèðîâàííûì êîíå÷íûì íàáîðîì êîíñòàíò,ôóíêöèîíàëüíûõ è ïðåäèêàòíûõ ñèìâîëîâ, îáîçíà÷àþùèõáàçîâûå îáúåêòû, îïåðàöèè è îòíîøåíèÿ òåîðèè,Iäîáàâëåíèÿ ê ìíîæåñòâó àêñèîì èñ÷èñëåíèÿ ïðåäèêàòîâñïåöèàëüíûõ (íåëîãè÷åñêèõ) àêñèîì, îïèñûâàþùèõáàçîâûå ïðèíöèïû òåîðèè.Òàêèì îáðàçîì îáðàçóþòñÿ ýëåìåíòàðíàÿ òåîðèÿ ðàâåíñòâà,ýëåìåíòàðíàÿ òåîðèÿ ãðóïï, ýëåìåíòàðíàÿ òåîðèÿ ïîëåé,ýëåìåíòàðíàÿ ãåîìåòðèÿ, ýëåìåíòàðíàÿ àðèôìåòèêà,ýëåìåíòàðíàÿ òåîðèÿ ìíîæåñòâ, è äð.Ôîðìóëû ϕ , ëîãè÷åñêè âûâîäèìûå èç àêñèîì ýëåìåíòàðíîéàêñèîìàòè÷åñêîé òåîðèè T , íàçûâàþòñÿ òåîðåìàìè òåîðèè Tè îáîçíà÷àþòñÿ çàïèñüþ T ` ϕ .Àêñèîìàòè÷åñêèå òåîðèè ïåðâîãî ïîðÿäêàÝëåìåíòàðíàÿ àêñèîìàòè÷åñêàÿ òåîðèÿ T íàçûâàåòñÿIíåïðîòèâîðå÷èâîé , åñëè íå âñå ôîðìóëû ÿâëÿþòñÿòåîðåìàìè òåîðèè T , ò.

å. ñóùåñòâóåò òàêàÿ ôîðìóëà ϕ ,äëÿ êîòîðîé T 6` ϕ ;Iïîëíîé , åñëè äëÿ âñÿêîé çàìêíóòîé ôîðìóëû ëèáî îíàñàìà, ëèáî åå îòðèöàíèå ÿâëÿåòñÿ òåîðåìîé òåîðèè T , ò. å.äëÿ ëþáîé ôîðìóëû ϕ ëèáî T ` ϕ , ëèáî T ` ¬ϕ ;Iêàòåãîðè÷íîé , åñëè ëþáûå äâå íîðìàëüíûå ìîäåëèòåîðèè T èçîìîðôíû, ò. å. äëÿ ëþáîé ïàðû íîðìàëüíûõèíòåðïðåòàöèé I1 , I2 âåðíîI1 |= T è I2 |= T =⇒ I1 ∼= I2 ;Iðàçðåøèìîé , åñëè ñóùåñòâóåò àëãîðèòì, ïðîâåðÿþùèé,ÿâëÿåòñÿ ëè ïðîèçâîëüíàÿ ôîðìóëà òåîðåìîé òåîðèè T .Óòâåðæäåíèå.Âñÿêàÿ ïîëíàÿ êîíå÷íî àêñèîìàòèçèðóåìàÿ òåîðèÿ ðàçðåøèìà.Àêñèîìàòè÷åñêîå óñòðîéñòâî ãåîìåòðèèÂïåðâûå ïîïûòêó àêñèîìàòèçèðîâàòü ãåîìåòðèþ ïðåäïðèíÿëÅâêëèä (3 â.