Sekwenty.pdf

(28 KB) Pobierz
Przykladowe dowody w rachunku sekwentow
Konrad Zdanowski
18 stycznia 2004
Skrotowe nazwy regul:
1. Oslabienie, lewo{ i prawostronne:
O L
i O P .
2. Wprowadzenie negacji, lewo{ i prawostronne:
N L
i N P .
3. Wprowadzenie implikacji, lewo{ i prawostronne:
N L
i N P .
4. Wprowadzenie kwantykatora ogolnego, lewo{ i prawostronne:8 L i8 P .
5. Wprowadzenie kwantykatora egzystencjalnego, lewo{ i prawostronne:
9 L
i9 P .
6. Regula ci ecia:
RC .
Jesli nie jest podane, do ktorego sekwentu zastosowano dan a regule
wnioskowania
aby
otrzymac
sekwent X,
to
jest
to
sekwent,
ktory
bezposrednio poprzedza sekwent X.
Dla reguly
I L
przyjmuj e nast epuj ace oznaczenia, ktore wykorzystam w
opisie dowodow:
!;' ; !
(') ); !
Przyklady dowodow:
A)9x(P(x)):P(x)))9x:P(x)
1. P(a)!P(a),
aksjomat
2.!P(a);:P(a),
N P
3.!P(a);9x:P(x), 9 P
1
896868614.001.png
4.:P(a);P(a)!,
N L
z 1
5.:P(a)!:P(a),
N P
6.:P(a)!9x:P(x), 9 P
7. (P(a)):P(a))!9x:P(x),
I P
z 3 i 6 dla =;, =f9x:P(x)g,
' = P(a), =:P(a)
8.8x(P(x)):P(x))!9x:P(x), 8 L
9.!8x(P(x)):P(x)))9x:P(x),
I P
B)8x(P(x))R(x)))(9xP(x))9xR(x))
1. P(a)!P(a),
aksjomat
2. R(a)!R(a),
aksjomat
3. P(a);R(a)!R(a),
O L
4. P(a)!P(a);R(a),
O P
z 1
5. (P(a))R(a));P(a)!R(a),
I L
z 3 i 4 dla =fP(a)g,
=fR(a)g, ' = P(a), = R(a)
6. (P(a))R(a));P(a)!9xR(x), 9 P
7.8x(P(x))R(x));P(a)!9xR(x), 8 P
8.8x(P(x))R(x));9xP(x)!9xR(x), 9 L
9.8x(P(x))R(x))!(9xP(x))9xR(x)),
I P
10.!8x(P(x))R(x)))(9xP(x))9xR(x)),
I P
C)8x9z(P(z))R(x)))(8zP(z))8xR(x))
1. P(a)!P(a),
aksjomat
2. R(b)!R(b),
aksjomat
3. P(a)!P(a);R(b),
O P
4. P(a);R(b)!R(b),
O L
2
5. (P(a))R(b));P(a)!R(b),
I L
z 3 i 4 dla zbiorow jak w punkcie
B)
6. (P(a))R(b));8zP(z)!R(b), 8 L
7.9z(P(z))R(b));8zP(z)!R(b), 9 L
8.8x9z(P(z))R(x));8zP(z)!R(b), 8 L
9.8x9z(P(z))R(x));8zP(z)!8xR(x), 8 P
10.8x9z(P(z))R(x))!8zP(z))8xR(x),
I P
11.!8x9z(P(z))R(x)))(8zP(z))8xR(x)),
I P
Zastanawiaj ac si e nad znalezieniem dowodu w rachunku sekwentow dla
danej formuly ' proponuj e jako zasad e heurystyczn e przyj ac zastanowienie
si e jaka regula byla zastosowana w dowodzie jako ostatnia. W ten sposob
mozna skonstruowac dowod zaczynaj ac od formul znajduj acych si e na koncu
dowodu.
3

Plik z chomika:

Inne pliki z tego folderu:

Inne foldery tego chomika:

Zgłoś jeśli naruszono regulamin