112750

1.    Spójniki wiążą swe argumenty wedhig następującej kolejności: negacja, potem równorzędnie koniunkcja i alternatywa, implikacja i na końcu równoważność.

2.    Zewnętrzne nawiasy opuszczamy.

3.    Opuszczamy te nawiasy, których opuszczenie nie powoduje wieloznaczności w jednoznacznym sposobie odczytania formuły (wiąże się to z umowami z punktów 1. i

2.).

PRZYKŁAD. Na zastosowanie umowy.

Zgodnie z definicją formulami są: ((pi->p2)-H(p2->P:ó->(pi->P3))); ((piAp2>-»pi). Na podstawie powyższej umowy możemy napisać obie formuły tak jak są one zapisane na liście aksjomatów.

Po trzecie aksjomatów naszego systemu jest tylko skończenie wiele, ale za to musimy przyjąć regułę podstawiania w systemie. Można zastosować zabieg, polegający na tym, że możemy przyjąć nieskończony zbiór aksjomatów, ale wypisanych w postaci schematów aksjomatów. Schematy te wyglądają tak samo jak nasze aksjomaty z tym, że na miejscach zmiennych zdaniowych występują metazmienne. Pod każdy taki schemat podpada nieskończenie wiele aksjomatów. Na przykład pod schemat: A->(B->A) podpada nasz aksjomat [3] jak i na przykład formula: pAq->((r->r)->pAq). W takim przypadku można zrezygnować z reguły podstawiania i system będzie miał tylko jedną regułę - regułę odrywania.

Po czwarte komentarza wymagają reguły inferencji. W KRZ mamy dwie reguły. Na mocy RO mając implikację i jej poprzednik, można dołączyć następnik tej implikacji. Reguła podstawiania pozwala uzyskać formułę, która jest wynikiem podstawienia równoczesnego za niektóre flub wszystkie) zmienne zdaniowe występujące w formule dowolnych wyrażeń poprawnie zbudowanych. Każda reguła inferencji jest pewnego rodzaju efektywnym przepisem, który pozwala na wykonanie pewnej ściśle określonej operacji na zbiorze wyrażeń danych.

TWIERDZENIE SF := Formułę A nazywamy twierdzeniem określonego SF wtw istnieje dowód A w SF._

-.-

DOWOD A W SF := Skończony ciąg formuł <A|.....A„> nazywamy dowodem A w

systemie formalnym SF wtw spełnia następujące warunki:_

•    A„ = A,

•    Każda formuła A* [gdzie l£ i £ n) jest albo aksjomatem, albo została uzyskana z formuł wcześniejszym w tym ciągu za pomocą którejś z reguł mlerencyjnych SF.

Zbiór wszystkich twierdzeń KRZ oznaczmy symbolem Dow_Krz.

PRZYKŁAD.

Formuła p->p jest twierdzeniem KRZ [symb: p->pe DowkrzI-

Następujący ciąg formuł jest jej dowodem: < (p-»(p-»q))-»(p->q). (p->(p-»p))-»(p->p).

p—>(q—>p). p->(p->p), p->p>.