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

gLAWA   V.   iS^ISLENIE WYSKAZYWANIJ

   1.5. aKSIOMY I PRAWILA WYWODA iw. dLQ L@BYH FORMUL a, b, E SLEDU@]IE FORMULY
QWLQ@TSQ AKSIOMAMI iw.
aKSIOMA 1. a ! (b ! a).
aKSIOMA 2. (a ! (b ! c)) ! ((a ! b) ! (a ! c)).
aKSIOMA 3. (:b ! :a) ! ((:b ! a) ! b).
   eDINSTWENNYM PRAWILOM WYWODA iw QWLQETSQ ^ASTI^NAQ FUNKCIQ f WIDA:
                                       f(a
 a ! b) = f(a ! b
 a) = b:
   bUDEM EGO ZAPISYWATX W WIDE: a
 a ! b ` b.
   |TO PRAWILO WYWODA NAZYWA@T PRAWILOM OTDELENIQ (POSYLKI) ILI Modus ponens, SOKRA]EN-
NO MP.
   w DEJSTWITELXNOSTI, AKSIOM BESKONE^NOE MNOVESTWO, A WYE PRIWEDENY LIX SHEMY AKSIOM.
tAK NAPRIMER, QWLQETSQ AKSIOMOJ 1 FORMULA:
                                         (a ! b) ! (c ! (a ! b)).
  1.6. pRIMER WYWODIMOSTI W iw.
lEMMA 1. dLQ L@BOJ FORMULY a SPRAWEDLIWA WYWODIMOSTX                :


                                                 ` (a ! a)
dOKAZATELXSTWO. pOSTROIM WYWOD, OKAN^IWA@]IJSQ FORMULOJ (a ! a).
 1. (a ! ((a ! a) ! a)) ! ((a ! (a ! a)) ! (a ! a))          | aKSIOMA 2.
 2. a ! ((a ! a) ! a)                                        | aKSIOMA 1.
 3. (a ! (a ! a)) ! (a ! a)                                  | MP 2, 1.
 4. a ! (a ! a)                                              | aKSIOMA 1.
 5. (a ! a)                                                  | MP 4, 3.
    1.7. tEOREMA DEDUKCII. tEOREMA DEDUKCII, KAK BYLO OTME^ENO RANEE, USTANAWLIWAET
WAVNU@ SWQZX MEVDU PONQTIQMI WYWODIMOSTI I WYWODIMOSTI IZ GIPOTEZ. wO MNOGIH SLU^AQH ONA
SU]ESTWENNO OBLEG^AET DOKAZATELXSTWO WYWODIMOSTI TEH ILI INYH FORMUL.
tEOREMA 1. pUSTX ; | MNOVESTWO FORMUL, a I b KAKIE-TO FORMULY iw.
    eSLI ;, a ` b, TO ; ` (a ! b).
dOKAZATELXSTWO. tAK KAK b WYWODIMA IZ ; I a, TO SU]ESTWUET WYWOD b IZ ; I a. pUSTX
b1
 b2 
 : : :
 bn = b | WYWOD b IZ ; I a, TO ESTX FORMULA \TOGO WYWODA LIBO IZ ;, LIBO SOWPADAET S
a, LIBO POLU^ENA IZ PREDYDU]IH PRIMENENIEM PRAWILA WYWODA MP. iNDUKCIEJ PO i, 1  i  n,
POKAVEM, ^TO: ; ` (a ! bi ). pRI i = n \TO BUDET, W ^ASTNOSTI, ZAKL@^ENIE TEOREMY.
    pUSTX i = 1. dOKAVEM, ^TO ; ` (a ! b1). tAK KAK b1 | PERWAQ FORMULA WYWODA, TO ONA
NE MOVET BYTX POLU^ENA PRI POMO]I MP IZ PREDYDU]IH. tOGDA DLQ b1 WOZMOVNY SLEDU@]IE
SLU^AI:
    a) b1 | AKSIOMA
   b) b1 2 ;
   c) b1 = a.
   rASSMOTRIM KAVDYJ IZ \TIH SLU^AEW.
   a) sTROIM WYWOD DLQ (a ! b1).
    1. b1             | aKSIOMA.
    2. b1 ! (a ! b1 ) | aKSIOMA 1.
    3. a ! b1          | MP 1, 2.
    ` (a ! b1), SLEDOWATELXNO ; ` (a ! b1).
                                                    88