Untitled Scanned 08

Początek tego skrótowo przedstawionego dowodu można tu nazwać informacją dowodową. Mówi ona mniej więcej tyle: bierzemy aksjomat (tezę) I i podstawiamy w nim formułę [p -* {q -» r)] -> [(/? -► q) *{p -► r)] za p i równocześnie formułę q -> r za q\ w wyniku tych podstawień uzyskujemy implikację, której poprzednikiem jest aksjomat 2 zaś następnikiem napisana poniżej formuła (1); do implikacji tej i aksjomatu 2 można zastosować regułę odrywania, w wyniku czego otrzymamy (1).

Podwójny dwukropek dzieli taką informację dowodową na dwie części, z których pierwsza informuje, jakie wykonujemy podstawienia i do czego, druga zaś opisuje wynik tych podstawień i wskazuje, że stosuje się regułę odrywania.

Druga informacja dowodowa [poniżej formuły (1)] mówi tutaj mniej więcej, co następuje: bierzemy aksjomat 2 i podstawiamy w nim q -* r za p, p-*(q — r) za q, (p -> q) -> (p -* r) za r, przy czym wszystkie te podstawienia wykonujemy jednocześnie; w rezultacie otrzymujemy implikację, której poprzednikiem jest formuła (1); po zastosowaniu do tej implikacji i do (1) reguły odrywania otrzymujemy implikację, której poprzednik powstaje z aksjomatu l przez podstawienie q-* r za p i równocześnie p za q\ poprzednik ten jest tezą, więc znów można stosować odrywanie; jego wynikiem będzie już dowodzona teza 15.

Krótkość lego drugiego zapisu dowodu twierdzenia 15 uzyskaliśmy głównie dzięki posługiwaniu się numerami tez a nic samymi tezami oraz dzięki stosowaniu podstawień równocześnie za kilka zmiennych. 'I'cn drugi punkt wymaga pewnego wyjaśnienia. Reguła podstawiania mówi bowiem o podstawianiu tylko za jedną zmienną zdaniową. Z tego względu w podanym na początku pełnym dowodzie prawa 15 stosowane były podstawienia tylko za jedną zmienną. Łatwo jednak zdać sobie sprawę, że równoczesne podstawianie za kilka zmiennych prowadzi tylko do takich rezultatów, które można też osiągnąć przez wielokrotne stosowanie operacji podstawianiu za jedną zmienną. Trzeba tylko pamiętać o potrzebie wykonania w pewnych przypadkach podstawień pomocniczych. Z tego względu równoczesne podstawienia będziemy stosowali dalej bez żadnych ograniczeń.

W informacjach dowodowych stosujemy strzałkę podwójną => (różną od -»), aby uniknąć potrzeby wprowadzania do tych informacji dodatkowych znaków technicznych. Strzałka ta oznacza zawsze implikację niejako gotową do odrywania. Nigdy nic jest ona częścią żadnej formuły podstawianej za jakąś zmienną.

W następnych paragrafach tego rozdziału udowodnimy cały szereg praw rachunku zdań, które bądź są doniosłe same w sobie, bądź będą wykorzystywane w dalszych rozdziałach.