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

                                                                  x 5. tEORII PERWOGO PORQDKA

   5.7. pRIMERY WYWODOW W FORMALXNOJ ARIFMETIKE S. pOKAVEM, ^TO W L@BOJ TEORII
PERWOGO PORQDKA IMEET MESTO SLEDU@]EE PRAWILO INDIWIDUALIZACII.
tEOREMA 1. w L@BOJ TEORII 1-GO PORQDKA ESLI TERM t SWOBODEN DLQ PEREMENNOJ x W FORMU-
LE a(x), TO 8xa(x) ` a(t).
dOKAZATELXSTWO. rASSMOTRIM POSLEDOWATELXNOSTX FORMUL:
     1. 8xa(x)         | GIPOTEZA,
     2. 8xa(x) ! a(t) | AKSIOMA A4,
    3. a(t)           | MP 1,2
   |TA POSLEDOWATELXNOSTX QWLQETSQ WYWODOM FORMULY a(t) IZ GIPOTEZY 8xa(x).
tEOREMA 2. w FORMALXNOJ ARIFMETIKE S FORMULA t = r ! t0 = r0 QWLQETSQ WYWODIMOJ, GDE t
I r | PROIZWOLXNYE TERMY.
dOKAZATELXSTWO. pOSTROIM WYWOD \TOJ FORMULY.
     1. x1 = x2 ! x01 = x02          | AKSIOMA S2,
     2. 8x2 (x1 = x2 ! x1 = x2 )
                         0       0   | PRAWILO Gen K P. 1,
     3. 8x1 8x2(x1 = x2 ! x01 = x02) | PRAWILO Gen K P. 2,
     4. 8x2 (t = x2 ! t0 = x02 )     | PRAWILO INDIWIDUALIZACII K P. 3,
     5. t = r ! t = r
                  0   0              | PRAWILO INDIWIDUALIZACII K P. 4.
   pOQSNITE SAMOSTOQTELXNO PRAWOMERNOSTX PRIMENENIQ W \TOM WYWODE PRAWILA INDIWIDUALIZA-
CII.
   |TA TEOREMA I ANALOGI^NYE EJ POKAZYWA@T PO^EMU AKSIOMY S1{S8 FORMALXNOJ ARIFMETIKI
QWLQ@TSQ KONKRETNYMI FORMULAMI, A NE SHEMAMI AKSIOM.
   5.8. tEOREMA gEDELQ O NEPOLNOTE FORMALXNOJ ARIFMETIKI S. w SWQZI S OBNARU-
VENIEM NA RUBEVE XIX I XX WEKOW RAZLI^NYH PARADOKSOW W OSNOWANIQH MATEMATIKI BYLI PRED-
PRINQTY ZNA^ITELXNYE USILIQ PO IH USTRANENI@ I DOKAZATELXSTWU NEPROTIWORE^IWOSTI KLASSI-
^ESKOJ MATEMATIKI. oDIN IZ PUTEJ W \TOM NAPRAWLENII RAZRABATYWALSQ NEMECKIM MATEMATIKOM
d. gILXBERTOM. oSNOWANNOE IM TE^ENIE W OBOSNOWANII MATEMATIKI POLU^ILO NAZWANIE FORMA-
LIZMA. bOLXAQ ROLX W \TIH ISSLEDOWANIQH OTWODILASX FORMALXNOJ ARIFMETIKE, TAK KAK DOKA-
ZATELXSTWO NEPROTIWORE^IWOSTI ZNA^ITELXNOJ ^ASTI KLASSI^ESKOJ MATEMATIKI MOVET BYTX SWE-
DENA K PROBLEME NEPROTIWORE^IWOSTI ARIFMETIKI NATURALXNYH ^ISEL. pOSLE NEKOTORYH ^ASTI^-
NYH USPEHOW GILXBERTOWSKOJ KOLY W DOKAZATELXSTWE NEPROTIWORE^IWOSTI ARIFMETIKI NADEVDY
NA POLU^ENIE VELAEMOGO DOSTIVENIQ BYLI UNI^TOVENY REZULXTATOM, POLU^ENNYM W 1931 GODU
k. gEDELEM. oN UTWERVDAET NEWOZMOVNOSTX DOKAZATELXSTWA NEPROTIWORE^IWOSTI FORMALXNOJ TE-
ORII, WKL@^A@]EJ FORMALXNU@ ARIFMETIKU, KONSTRUKTIWNYMI METODAMI, FORMALIZUEMYMI W
SAMOJ TEORII.
   pRIWEDEM FORMULIROWKI SOOTWETSTWU@]IH TEOREM.
   fORMULA TEORII 1-GO PORQDKA NAZYWAETSQ ZAMKNUTOJ, ESLI ONA NE SODERVIT SWOBODNYH PERE-
MENNYH.
oPREDELENIE 1. eSLI ZAMKNUTAQ FORMULA a TEORII 1-GO PORQDKA  OBLADAET SLEDU@]IM SWOJ-
STWOM: a NEWYWODIMO W  I :a NEWYWODIMO W  , TO a NAZYWAETSQ NERAZREIMYM PREDLOVENIEM
TEORII  .
   sLEDU@]U@ TEOREMU DOKAZAL k. gEDELX W 1931 G.
tEOREMA 1. eSLI FORMALXNAQ ARIFMETIKA S NEPROTIWORE^IWA, TO W NEJ SU]ESTWUET PO KRAJ-
NEJ MERE ODNO NERAZREIMOJ PREDLOVENIE.
   wOZNIKAET IDEQ: ESLI NELXZQ WYWESTI NI \TO PREDLOVENIE, NI EGO OTRICANIE, TO, MOVET BYTX,
DOBAWIW EGO K AKSIOMAM, POLU^IM TEORI@, NE SODERVA]U@ NERAZREIMYH PREDLOVENIJ? oDNAKO,
\TO TOVE NI^EGO NE DAST. |TO SLEDUET IZ NIVESLEDU@]EJ TEOREMY, TAKVE DOKAZANNOJ gEDELEM,
DLQ FORMULIROWKI KOTOROJ DADIM SNA^ALA SLEDU@]EE
                                            123