RACHUNEK PREDYKATÓW 5
A(x / ą)  oznacza wynik podstawienia termu ą za zmienną x w wyra\
eniu A.
Prawidłowe podstawienie termu do wyra\
enia prawdziwego powinno zawsze
dawać wyra\
enie prawdziwe. Gwarancją tego jest spełnienie trzech warunków:
(1) Podstawiamy wyłącznie za zmienne wolne.
(2) Podstawiamy konsekwentnie, tj. w ka\
dym miejscu, gdzie występuje
dana zmienna wolna podstawiamy ten sam term.
(3) śadna zmienna wolna termu, który podstawiamy, nie mo\
e zostać
związana w wyniku podstawienia.
Jeśli A(x/ą) jest prawidłowym podstawieniem, to mówimy te\
, \
e term ą jest
podstawialny za zmienną x w wyra\
eniu A.
KRP, podobnie jak KRZ, mo\
na przedstawić w formie systemu zało\
eniowego
(lub aksjomatycznego). Pojęcie dowodu (wprost i nie wprost) pozostaje takie
samo. Natomiast za reguły wnioskowania przyjmiemy wszystkie reguły pierwotne
i wtórne systemu zało\
eniowego rachunku zdań (w odpowiednio rozszerzonej
interpretacji) oraz swoiste reguły pierwotne dla rachunku kwantyfikatorów: reguły
dołączania i opuszczania kwantyfikatora ogólnego i szczegółowego.
W poni\
szych regułach A oznacza dowolną formułę zdaniową języka rachunku
predykatów, ą  dowolny term, a  dowolną stałą nazwową, zaś A(u / ą) 
prawidłowe podstawienie.
(O'" ) reguła opuszczania kwantyfikatora ogólnego:
'"
'"
'"
'"A
u
A(u/ ą)
Jeśli do dowodu nale\
y formuła zdaniowa skwantyfikowana ogólnie, to wolno
dołączyć do dowodu dowolne prawidłowe podstawienie tej formuły zdaniowej (a
w szczególności  tę samą formułę zdaniową).
(D'" ) reguła dołączania kwantyfikatora ogólnego:
'"
'"
'"
pod warunkiem, \
e zmienna u
A
nie jest wolna w zało\
eniach
'" A
dowodu, ani nie jest indeksem.
u
Jeśli do dowodu nale\
y formuła zdaniowa A, to wolno dołączyć do dowodu tę
formułę skwantyfikowaną ogólnie (pod podanym wy\
ej warunkiem).
(D(" ) reguła dołączania kwantyfikatora szczegółowego:
("
("
("
A(u/ ą)
pod warunkiem, \
e zmienna u
nie jest indeksem.
(" A
u
Jeśli do dowodu nale\
y formuła zdaniowa A lub jej prawidłowe podstawienie, to
wolno dołączyć do dowodu tę formułę skwantyfikowaną szczegółowo (pod
podanym wy\
ej warunkiem).
1
RACHUNEK PREDYKATÓW 5
(O(" ) reguła opuszczania kwantyfikatora szczegółowego:
("
("
("
(" A(u)
pod warunkiem, \
e nazwa a
u
(a)
nie występowała dotąd w
A(u/ a)
\
adnym wierszu dowodu..
Jeśli do dowodu nale\
y formuła zdaniowa A(u) (o jednej tylko zmiennej wolnej u)
skwantyfikowana szczegółowo (względem tej zmiennej), to wolno dołączyć do
dowodu dowolne prawidłowe podstawienie stałej nazwowej za tę zmienną w
danej formule zdaniowej (pod podanym wy\
ej warunkiem).
(" A(u,u1,& ,un) pod warunkiem, \
e nazwa
u
(b)
au ,& ,un nie występowała dotąd
1
A(u/ au ,& ,un,u1,& ,un)
1
w \
adnym wierszu dowodu..
Jeśli do dowodu nale\
y formuła zdaniowa A(u,u1,& ,un) (w której wszystkimi
zmiennymi wolnymi są u,u1,& ,un ) skwantyfikowana szczegółowo (względem
zmiennej u), to wolno dołączyć do dowodu dowolne prawidłowe podstawienie
stałej nazwowej au ,& ,un (zdeterminowanej przez zmienne u1,& ,un jako indeksy)
1
za tę zmienną w danej formule zdaniowej (pod podanym wy\
ej warunkiem).
Uwaga 1: Podstawiana według tej reguły stała nazwowa oznacza tu pewien
(bli\
ej nieokreślony) przedmiot, dla którego prawdziwy jest wniosek tej reguły, o
ile tylko prawdziwa jest jej przesłanka.
Uwaga 2: Rolę podstawianej tu nazwy mo\
e równie\
pełnić zmienna (pod
podanym wy\
ej warunkiem).
ZADANIE 1
Przeprowadz
dowody zało\
eniowe następujących formuł:
(1) '"[P(x) Q(x)] ['"P(x) '"Q(x)]
x x x
(2) '"[P(x) Q(x)] [("P(x) ("Q(x)]
x x x
(3) '"'" R(x,y) "!'"'" R(x,y)
x y y x
(4) ("'" R(x,y) '"("R(x,y)
x y y x
(5) '" <" P(x) <" ("P(x) (nie wprost)
x x
(6) <" ("P(x) '" <" P(x) (dictum de singulo)
x x
(7) <" ("P(x) (" <" P(x) (dictum de singulo)
x x
(8) '" <" P(x) <" '"P(x) (dictum de omni)
x x
2
RACHUNEK PREDYKATÓW 5
ZADANIE 2
Sprawdz
, czy poni\
sze ciągi formuł są poprawnymi dowodami:
(I) dla formuły '"[P(x) Q(x)] [P(x) '"Q(x)]
x x
(1) '"[P(x) Q(x)] (zał.)
x
(2) P(x) (zał.)
(3) P(x) Q(x) (O'" 1)
'"
'"
'"
(4) Q(x) (RO 2,3)
(5) '"Q(x) (D'" 4)
'"
'"
'"
x
(II) dla formuły [("P(x) '"(" <" P(x)] ("[P(x) '" <" P(x)]
x x x
(1) ("P(x) '"(" <" P(x) (zał.)
x x
(2) ("P(x) (OK 1)
x
(3) (" <" P(x) (OK 1)
x
(4) P(a) (O(" 2)
("
("
("
(5) <" P(a) (O(" 3)
("
("
("
(6) P(a) '" <" P(a) (DK 4,5)
(7) ("[P(x) '" <" P(x)] (D(" 6)
("
("
("
x
3