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

                                   x 1. qZYK I AKSIOMY IS^ISLENIQ WYSKAZYWANIJ. tEOREMA DEDUKCII

oPREDELENIE 1. wYWODOM TEORII T NAZYWAETSQ WSQKAQ KONE^NAQ POSLEDOWATELXNOSTX FOR                    -
MUL \TOJ TEORII, KAVDAQ IZ KOTORYH QWLQETSQ LIBO AKSIOMOJ, LIBO POLU^ENA IZ PREDYDU]IH
FORMUL PO ODNOMU IZ PRAWIL WYWODA.
   fORMULA a NAZYWAETSQ WYWODIMOJ FORMULOJ (TEOREMOJ) TEORII T, ESLI SU]ESTWUET WY-
WOD, OKAN^IWA@]IJSQ \TOJ FORMULOJ. wYWOD \TOT NAZYWAETSQ WYWODOM (DOKAZATELXSTWOM)
FORMULY (TEOREMY) a. dLQ WYWODIMOJ FORMULY a PRINQTO OBOZNA^ENIE ` a.
  1.3. wYWODIMOSTX IZ MNOVESTWA FORMUL.
oPREDELENIE 1. kONE^NAQ POSLEDOWATELXNOSTX FORMUL NAZYWAETSQ WYWODOM IZ MNOVESTWA
FORMUL ;, ESLI KAVDAQ FORMULA \TOJ POSLEDOWATELXNOSTI QWLQETSQ LIBO AKSIOMOJ, LIBO PRI-
NADLEVIT ;, LIBO POLU^ENA IZ PREDYDU]IH FORMUL PRIMENENIEM ODNOGO IZ PRAWIL WYWODA.
   fORMULA a NAZYWAETSQ WYWODIMOJ IZ MNOVESTWA FORMUL ;, ESLI SU]ESTWUET WYWOD IZ ;,
OKAN^IWA@]IJSQ FORMULOJ a. oBOZNA^AETSQ ; ` a. fORMULY IZ ; NAZYWA@TSQ GIPOTEZAMI.
   pONQTNO, ^TO ESLI ; = ?, TO W DEJSTWITELXNOSTI a | WYWODIMAQ FORMULA. pRI \TOM WMESTO
ZAPISI ? ` a PIUT ` a.
   oTMETIM, ^TO MEVDU PONQTIQMI WYWODIMOSTI I WYWODIMOSTI IZ GIPOTEZ SU]ESTWUET TESNAQ
SWQZX, KOTORAQ WYRAVAETSQ TEOREMOJ DEDUKCII. oNA BUDET W DALXNEJEM DOKAZANA.
tEOREMA 1. pONQTIE WYWODIMOSTI IZ GIPOTEZ OBLADAET SLEDU@]IMI SWOJSTWAMI 1{3.
   1.   ; I  ` a, TO ; ` a.
   2. ; ` a TOGDA I TOLXKO TOGDA KOGDA W ; SU]ESTWUET KONE^NOE PODMNOVESTWO , DLQ
KOTOROGO  ` a.
   3. eSLI ; ` b DLQ L@BOJ FORMULY b IZ  I  ` a, TO ; ` a.


dOKAZATELXSTWO. 1. o^EWIDNO.
   2. eSLI W ; SU]ESTWUET PODMNOVESTWO (NE OBQZATELXNO KONE^NOE) , DLQ KOTOROGO  ` a, TO
PO SWOJSTWU 1, ; ` a.
   pUSTX TEPERX ; ` a. tOGDA SU]ESTWUET WYWOD IZ ;, OKAN^IWA@]IJSQ a:
                                             a1 
 : : :
 an 
 a.
   oBOZNA^IM ^EREZ  MNOVESTWO FORMUL IZ \TOGO WYWODA, PRINADLEVA]IH ;. pONQTNO, ^TO
 ` a,   ; I  | KONE^NOE.
   3. pUSTX a1
 a2
 : : :
 an 
 a | WYWOD a IZ  I PUSTX a01
 a02 
 : : :
 a0s | FORMULY \TOGO WYWODA,
PRINADLEVA]IE . pO USLOWI@ ONI WYWODIMY IZ ;. zAPIEM IH SOOTWETSTWU@]IE WYWODY IZ ;:
                                        b11
 b12 
 : : :
 b1k1 
 a01
                                        b21
 b22 
 : : :
 b2k2 
 a02
                                        : : :: : :: : :: : :: : :: : :: : :
                                        bs1
 bs2
 : : :
 bsks 
 a0s :
wSTAWIW W WYWOD a IZ  WMESTO FORMUL a01 
 a02 
 : : :
 a0s IH SOOTWETSTWU@]IE WYWODY IZ ;, POLU^IM
WYWOD FORMULY a IZ ;.
   1.4. qZYK iw. aLFAWIT iw SOSTOIT IZ SLEDU@]IH SIMWOLOW.
  1. fA1
 A2
 : : :g | S^ETNOE MNOVESTWO BUKW.
  2. :, ! | SWQZKI (LOGI^ESKIE SIMWOLY).
  3. ), ( | WSPOMOGATELXNYE SIMWOLY (PRAWAQ I LEWAQ SKOBKI).
oPREDELENIE 1 (FORMULY). 1. wSE BUKWY ALFAWITA iw QWLQ@TSQ FORMULAMI.
 2. eSLI a I b | FORMULY, TO :a I (a ! b) TAKVE QWLQ@TSQ FORMULAMI.


 3. dRUGIH FORMUL, KROME UKAZANNYH W PUNKTAH 1{2 NET.


  w DALXNEJEM USLOWIMSQ WNENIE SKOBKI W FORMULAH OPUSKATX.
                                                       87