KIF06

82. Podobnie jak w rachunku zdań. tak i w rachunku kwanty-fikatorów budowanym metodą aksjomatyczną można rozmaicie dobierać aksjomaty i reguły dowodzenia; w szczególności, wzbogacając aksjomatykę o dostatecznie wiele twierdzeń swoiście kwantyfikatorowych można ograniczyć układ reguł dowodzenia do reguł rachunku zdań. Można również przyjąć zarówno aksjomaty, jak i reguły swoiste dla kwantyfikatorów. Przykładem takiego ujęcia jest system, którego aksjomatykę stanowi zbiór wszystkich twierdzeń rachunku zdań i ich podstawień wzbogacony o następujące dwa twierdzenia swoiście kwantyfikatorowe:

(A*l) f\xP(x)-*P(y)    (dictum de omni).

(A*2) /\x[p-+P(x)]a[p-+ f\xP(x)] (jedno z praw przenoszenia kwantyfikatorów; p reprezentuje dowolną formułę zdaniową nie zawierającą zmiennej wolnej x).

Regułami dowodzenia w tym systemie są: RO, RP' (Zob. zadanie 78) oraz:

(RP") Reguła podstawiania dla wyrażeń funkcyjnych: jeśli do dowodu należy wyrażenie W zawierające wyraźcnk funkcyjne /, to wolno dołączyć do dowodu wyrażenie W powstające z W przez zastąpienie (konsekwentne) wyrażenia f wyrażeniem g, w którym występują jako zmienne wolne wszystkie te 2micnnc, które są wolne w /; obowiązuje jednak warunek, że żadna zmienne wolna w g nie stanie się związana w W'.

(D/\") Reguła dołączania dużego kwantyfikatora do tez: jriii do dowodu należy wyrażenie IP, to wolno dołączyć do dowodu wyrażenie f\a\P.

(RZZ) Reguła zamiany zmiennych z\ iązanych: jeśli do dowodu należy wyrażenie [\aW, to wolno dołączyć do dowode wyrażenie [\bW', o ile W powstaje z W przez zają-pienie (konsekwentne) zmiennej wolnej a zmiena b; obowiązuje jednak warunek, że zmienna 6 nie występuje w W.

(A)    Podaj przykłady stosowania reguł RP”. D/\”, RZZ do aksjomatów tego systemu.

(B)    Uzasadnij na przykładach potrzebę przestrzegania warunków stosowalności reguł RP” i RZZ.

(C)    Uzasadnij w sposób intuicyjny, źe żadna spośród reguł RP”. D/\", RZZ nic prowadzi nigdy od tautologii do schematów nictautologicznych.

(D)    Zdefiniuj mały kwantyfikator za pomocą dużego kwanty-fikatora i funktora negacji.

83. Rachunek kwantyfikatorów można też zbudować metodą założeniową. Konstrukcja ta polega na dołączeniu do reguł¹ założeniowego systemu rachunku zdań odpowiednio dobranych reguł kw antyfikatorowych. Zasady budowy dowodów założeniowych są takie same. jak w rachunku zdań (zob. zadania 33-38). Pierwotne reguły kwantyńkatorowę są dość skomplikowane. Poniżej podajemy je w postaci, w jakiej służyć mogą wyłącznic dowodzeniu formuł, w których wszystkie zmienne są równokształtne.

(O A') Reguło opuszczania dużego kwantyfikatora: jeśli do dowodu należy wyrażenie postaci f\aW_t to wolno dołączyć do dowodu wyrażenie W' powstające z W przez zastąpienie zmiennej a wszędzie, gdzie jest ona wołna, dowolną zmienną lub nazwą nieokreśloną¹⁹. (D AO Reguła dołączania dużego k wantyfikatora: jeśli do dowodu należy wyrażenie W, to wolno dołączyć-do dowodu wyrażenie postaci f\aW, pod warunkiem jednak, że że zmienna a nie jest wolna w założeniach dowodu. (O V') Reguła opuszczania małego kwanty fika lora: jeśli do dow odu należy wyrażenie postaci \/ a W, to wolno

67

1

Mogą to być reguły r¹rwotne łub wszelkie reguły rachunku rdAł,

'¹ Nazwy nieokreślone, oznaczane symbolami /•, z¹.....reprezeo-

tąlą bliżej nie określone przedmioty rozważanego rodzaju, których istnienie gwarantuje dana formuła.