104317

LOGKA

Reguły inferencji systemu S:

1. reguła podstawiania - podstawiając w dowolnej formule, która jest tezą systemu, za któryś z jej symboli zdaniowych (wszędzie tam, gdzie ten symbol występuje) inny symbol zdaniowy lub formulę, otrzymuje się tezę systemu;

F

symbolicznie: _F(z/F)

2. reaula odrywania - jeśli formula implikacyjna i jej poprzednik są tezami systemu, to również następnik tej formuły jest tezą systemu;

symbolicznie:

Dowodzenie twierdzeń pochodnych systemu S można zilustrować wykazując, że tezą tego systemu jest formula;

• P->P

W akąomacie 1 podstawiamy formulę.—p' za „q" i „p” za „r", otrzymujemy:

(P -* —P) -> K~~P -»P) -»(P -* P)1

Poprzednik otrzymanej implikacji jest aksjomatem A4 systemu S. Na mocy reguły odrywania otrzymujemy, że tezą tego systemu jest również formula:

<—P —»■ P) —> (P -* P)

I ta formula jest implikacją, której poprzednik stanowi aksjomat A5. Na mocy reguły odrywania:

P->P

Zostało udowodnione, że formula .p -> p" jest tezą systemu S.