Rachunek zdań w postaci założeniowej

• Jest też nazywany systemem dedukcji naturalnej, gdyż na pewien sposób naśladuje intuicyjny sposób dedukowania.

• Został opracowany niezależnie przez dwóch logików: Gerard Gentzen i Stanisław Jaśkowski.

• W przeciwieństwie do rachunku aksjomatycznego, nie zawiera żadnych aksjomatów - jedynie reguły:

1. reguły dołączania nowych wierszy do dowodu (pierwotne i wtórne)

2. reguły konstruowania dowodu

reguły pierwotne

• reguła odrywania (RO) - jeżeli uznana została za prawdziwą pewna i implikacja i jej poprzednik również został uznany za prawdziwy, to można też uznać za prawdziwy (dołączyć do dowodu) jej następnik

• reguła dołączania koniunkcji (DK) - jeżeli za prawdziwe (należące do dowodu) uznane zostały dwie formuły, to można też uznać za prawdziwą (dołączyć do dowodu) ich koniunkcję

• reguła opuszczania koniunkcji (OK) - jeżeli za prawdziwą uznana została pewna koniunkcja, to należy każdą z jej formuł uznać oddzielnie za prawdziwą

• reguła dołączania alternatywy (DA) - jeżeli za prawdziwą uznana została jakaś formuła, to za prawdziwą należy uznać także alternatywę tej formuły z dowolną inną

• reguła opuszczania alternatywy (OA) - jeżeli za prawdziwą uznana została jakaś alternatywa, a za fałszywy - jeden z jej członów, to za prawdziwy uznać należy drugi z członów tej alternatywy

∼

• reguła dołączania równoważności (DR) - jeżeli za prawdziwą uznana została pewna implikacja, a jej odwrotność również została uznana za prawdziwą, to za prawdziwą uznać można równoważność pomiędzy formułami, będącymi członami powyższych implikacji

• reguła opuszczania równoważności (OR) - jeżeli za prawdziwą uznana została pewna równoważność, to za prawdziwe należy także uznać oddzielne, obustronne implikacje, których członami są formuły, będące członami powyższej równoważności

• reguła opuszczania negacji (ON) - jeżeli za prawdziwą uznana została negacja negacji jakiejś formuły, to za prawdziwą uznać należy także samą tę formułę

reguły konstruowania dowodów

Jeżeli twierdzenie ma postać implikacji, to dowód może mieć charakter dowodu wprost lub dowodu nie wprost.

• dowód wprost polega na: wypisaniu wszystkich założeń implikacji, a następnie wypisaniu wyrażeń, na przyjęcie których pozwalają reguły pierwotne dołączania; dowód uznaje się za zakończony, gdy wypisany zostanie ostateczny następnik implikacji

- bezkoniunkcyjny sylogizm hipotetyczny

1. założenie
   

2. założenie
   

3. założenie
   

4. RO (1, 3)
   

5. RO (2, 4)
   

Dowód miał trwać do chwili, gdy pojawiło się r, które było ostatecznym następnikiem.

• dowód nie wprost polega na: wypisaniu wszystkich założeń implikacji, wypisaniu negacji ostatecznego następnika (założenie dowodu nie wprost), a dalej: wypisaniu wyrażeń, na przyjęcie których pozwalają reguły pierwotne dołączania; dowód uznaje się za zakończony, gdy wśród wypisanych wyrażeń pojawi się sprzeczność

(∼p→q)→(∼q→p)

1. założenie
   

2. założenie
   

3. założenie dowodu nie wprost
   

4. RO (1, 3)
   

Należy zauważyć sprzeczność (2, 4) - dowód zakończony.

• Jeżeli twierdzenie nie ma postaci implikacji, to należy założyć negację całego twierdzenia, a następnie wypisać wyrażenia, na przyjęcie których pozwalają reguły pierwotne dołączania; dowód uznaje się za zakończony, gdy wśród wypisanych wyrażeń pojawi się sprzeczność

1. założenie
   

2. ON (1)
   

3. OK (2)
   

4. OK (2)
   

5. OK (4)
   

6. RO (3, 5)
   

7. OK (4)
   

Należy zauważyć sprzeczność (6, 7) - dowód zakończony.

Po zakończeniu dowodu można dodać wtórne reguły dołączania nowych wierszy do dowodu. Dla

będzie to: