RACHUNEK PREDYKATÓW 6
Trzy przedstawione poniżej systemy aksjomatyczne KRP są równoważne, tj.
posiadają ten sam zbiór twierdzeń (czyli formuł dowodliwych w systemie).
(I) Dla dowolnych formuł A, B, C rachunku predykatów oraz dowolnych liter
predykatowych P i Q aksjomatami są formuły postaci:
(1) A (B A)
(2) (A (B C)) ((A B) (A C))
(3) (A B) (<" B <"A)
(4) '"P(u) P(u / v)
u
(5) P '"P(u) pod warunkiem, że u nie jest zmienną wolną w P
u
(6) '"[P(u) Q(u)] ['"P(u) '"Q(u)]
uu u
Reguły wnioskowania:
reguła odrywania (RO)
reguła dołączania kwantyfikatora ogólnego (D'" )
(II) Aksjomatykę stanowi zbiór wszystkich aksjomatów pewnego
zaksjomatyzowanego systemu rachunku zdań, w których za zmienne
zdaniowe podstawia się odpowiednio formuły zdaniowe rachunku
predykatów. Reguły wnioskowania  jak w systemie (III).
(III) Aksjomatykę stanowi zbiór wszystkich twierdzeń rachunku zdań, w
których za zmienne zdaniowe podstawia się odpowiednio formuły
zdaniowe rachunku predykatów. Reguły wnioskowania:
reguła odrywania (RO)
A B
A
B
reguła podstawiania (RP)
A
A(u / ą)
( A(u / ą)  prawidłowe podstawienie termu ą za zmienną u w formule A).
reguła opuszczania kwantyfikatora ogólnego w następniku (O'" N)
A '"B
u
A B
1
RACHUNEK PREDYKATÓW 6
reguła dołączania kwantyfikatora ogólnego w następniku (D'" N)
A B pod warunkiem, że
zmienna u nie jest
A '"B
u zmienną wolną w A.
reguła opuszczania kwantyfikatora szczegółowego w poprzedniku
(O(" P)
(" A B
u
A B
reguła dołączania kwantyfikatora szczegółowego w poprzedniku
(D(" P)
pod warunkiem, że
A B
zmienna u nie jest
(" A B
zmienną wolną w B.
u
reguła uogólniania (RU)
A
'"A
u
ZADANIE
Udowodnij poniższe formuły w systemie (III).
(T1) '"A A
x
(T2) '"A A(x / ą)
x
(T3) A (" A
x
(T4) A(x / ą) (" A
x
(T5) '"A (" A
xx
(T6) '"A "! A o ile x nie jest zmienną wolną w A
x
(T7) ("A "! A o ile x nie jest zmienną wolną w A
x
o ile y nie jest zmienną wolną w A oraz
(T8) '"A "!'"A(x / y)
xy y jest podstawialne za x w A
o ile y nie jest zmienną wolną w A oraz
(T9) ("A "!("A(x / y)
xy
y jest podstawialne za x w A
(T10) '"'"A "! '"'"A
x y y x
(T11) ("(" A "! ("("A
x y y x
(T12) ("'"A '"("A
x y y x
(T13) (" <" A <" '"A
xx
2