Дискретная математика. Кулабухов С.Ю. - 121 стр.

                                                                     x 5. tEORII PERWOGO PORQDKA

    pOLXZUQSX OBY^NYMI PONQTIQMI WYPOLNIMOSTI I ISTINNOSTI, LEGKO POKAZATX, ^TO DLQ PRO-
IZWOLXNYH FORMUL a I b TEORII 1-GO PORQDKA 
   1. eSLI NA DANNOJ OBLASTI INTERPRETACII ISTINNY FORMULY a I a ! b, TO ISTINNA I FORMU-
      LA b.
   2. a ISTINNO NA DANNOJ OBLASTI INTERPRETACII TOGDA I TOLXKO TOGDA, KOGDA ISTINNO 8xi a.
    |TO OZNA^AET, ^TO WSQKAQ WYWODIMAQ W  FORMULA BUDET ISTINNOJ NA MODELI \TOJ TEORII.
oBY^NO PRI POSTROENII TEORII 1-GO PORQDKA , FORMALIZU@]EJ NEKOTORU@ SODERVATELXNU@
TEORI@, SOBSTWENNYE AKSIOMY WYBIRA@TSQ TAK, ^TOBY MNOVESTWO LOGI^ESKIH SLEDSTWIJ WSEH
AKSIOM  SOWPADALO SO MNOVESTWOM WSEH WYWODIMYH W  FORMUL.
pRIMER 1. wSQKAQ POLUGRUPPA QWLQETSQ MODELX@ FORMALXNOJ TEORII POLUGRUPP, POSTROENNOJ
W PRIMERE 5.3.1.
pRIMER 2. mNOVESTWO WSEH TO^EK I PRQMYH PROIZWOLXNOJ PLOSKOSTI QWLQETSQ MODELX@ GEOMET-
RII eWKLIDA (PLANIMETRII).
   5.5. nEPROTIWORE^IWOSTX, POLNOTA I NERAZREIMOSTX IS^ISLENIJ PREDIKATOW
PERWOGO PORQDKA. nIVESLEDU@]U@ TEOREMU NAZYWA@T TEOREMOJ gEDELQ O POLNOTE IS^ISLE-
NIQ PREDIKATOW.
tEOREMA 1. wO WSQKOM IS^ISLENII PREDIKATOW 1-GO PORQDKA TEOREMAMI QWLQ@TSQ TE I TOLXKO
TE FORMULY, KOTORYE LOGI^ESKI OB]EZNA^IMY.
    dANNAQ TEOREMA PRIWODITSQ BEZ DOKAZATELXSTWA.
tEOREMA 2. wSQKOE IS^ISLENIE PREDIKATOW 1-GO PORQDKA NEPROTIWORE^IWO.
dOKAZATELXSTWO. oBOZNA^IM ^EREZ h(a) FORMULU, KOTORAQ POLU^AETSQ IZ a UDALENIEM WSEH KWAN-
TOROW I TERMOW WMESTE S SOOTWETSTWU@]IMI SKOBKAMI, ZAPQTYMI, PREDMETNYMI PEREMENNYMI I
PREDMETNYMI POSTOQNNYMI. tAKIM OBRAZOM, h(a) QWLQETSQ FORMULOJ ALGEBRY WYSKAZYWANIJ.
    lEGKO WIDNO, ^TO OPERATOR h, PRIMENENNYJ K LOGI^ESKIM AKSIOMAM PROIZWOLXNOGO IS^ISLENIQ
PREDIKATOW DAET TAWTOLOGII. tAKVE PROWERQETSQ, ^TO ESLI h(a) I h(a ! b) QWLQ@TSQ TAWTOLOGIQ-
MI, TO I h(b) TAKVE TAWTOLOGIQ. tAK KAK h(a) = h(8xi a), TO ESLI h(a) | TAWTOLOGIQ, TO I h(8xi a)
TAKVE TAWTOLOGIQ. wSE \TO OZNA^AET, ^TO ESLI a ESTX WYWODIMAQ W IS^ISLENII PREDIKATOW FORMU-
LA, TO h(a) | TAWTOLOGIQ. zNA^IT, ESLI BY W IS^ISLENII PREDIKATOW SU]ESTWOWALA BY FORMULA b
TAKAQ, ^TO ` b I ` :b, TO h(b) I h(:b) = :h(b) BYLI BY TAWTOLOGIQMI, ^TO NEWOZMOVNO.
tEOREMA 3. wSQKOE IS^ISLENIE PREDIKATOW PERWOGO PORQDKA QWLQETSQ NERAZREIMOJ TEORIEJ.
    tEOREMA TAKVE PRIWODITSQ BEZ DOKAZATELXSTWA I IZ NEE SLEDUET, ^TO TAK KAK KAVDAQ TEORIQ
1-GO PORQDKA SODERVIT NEKOTOROE IS^ISLENIE PREDIKATOW W KA^ESTWE PODTEORII, TO L@BAQ TEORIQ
1-GO PORQDKA NERAZREIMA, TO ESTX NE SU]ESTWUET ALGORITMA, KOTORYJ POZWOLQL BY DLQ KAVDOJ
FORMULY \TOJ TEORII OPREDELQTX QWLQETSQ \TA FORMULA WYWODIMOJ ILI NET.
   5.6. fORMALXNAQ ARIFMETIKA. nARQDU S GEOMETRIEJ ARIFMETIKA NAIBOLEE NEPOSRED-
STWENNO INTUITIWNAQ OBLASTX MATEMATIKI. pO\TOMU WPOLNE ESTESTWENNO IMENNO S ARIFMETIKI
NA^ATX POPYTKU FORMALIZACII I STROGOGO OBOSNOWANIQ MATEMATIKI. pERWOE, POLUAKSIOMATI^ES-
KOE POSTROENIE ARIFMETIKI BYLO PREDLOVENO dEDEKINDOM I pEANO NEZAWISIMO. |TI AKSIOMY
IZWESTNY POD NAZWANIEM \SISTEMY AKSIOM pEANO".
aKSIOMY pEANO.
 P1. 0 ESTX NATURALXNOE ^ISLO.
 P2. dLQ L@BOGO NATURALXNOGO ^ISLA x SU]ESTWUET ^ISLO x0 NEPOSREDSTWENNO SLEDU@]EE ZA x.
 P3. dLQ L@BOGO NATURALXNOGO ^ISLA x, 0 6= x0.

                                              121