KIF07

dołączyć do dowodu wyrażenie W powstające z W przez zastąpienie zmiennej a wszędzie, gdzie jest ona wolna, nazwą nieokreśloną nic występującą dotąd w żadnym wierszu dowodu.

(DV'> tefpb dołączania małego kwantyftkalora: jeśli do dowodu należy wyrażenie W, to wolno dołączyć do dowodu wyrażenie postaci \/ a W’, w którym W powstaje z W przez konsekwentne zastąpienie pewnej nazwy nieokreślonej lub pewnej zmiennej (wszędzie, gdzie jest ona wolna) zmienną a, pod warunkiem jednak, że zmienna a nie jest wolna w założeniach dowodu.

Warunek nałożony na regułę 0\/' uzasadniamy następująco. Jeśli do dowodu należą na przykład wyrażenia V oraz \J xQ(x), to dołączywszy kolejno wyrażenia ■/*(*•) oraz Q (*•) przesądzalibyśmy o istnieniu przedmiotu mającego zarazem własność P i własność Q; tymczasem wyrażenia V xP(x) i V xQ(x) wcale tego nic gwarantują — własności P i Q mogą się wykluczać. Dlatego korzystając w dowodzie po raz drugi (i dalszy) z reguły O \/' trzeba użyć nowej nazwy nieokreślonej: y*, r*. itd.

Uzasadnij potrzebę przestrzegania warunków stosowalności reguł D A'. D V'-

84. Przykładem dowodu wprost w systemie założeniowym rachunku kwantyfikatorów jest podany niżej dowód twierdzenia :

xP(x)-» V 1-

(założenie) (założenie I

(OV': 2)

(OA'^: »

(RO: J. ^4!

(DV'^{: 51}

(J) A x[P(x)-*Q(x)]

(2)    \/xP(x)

(3)    />(*•)

(5)    W)

(6)    V ^xQ(x)

ttm

Zbuduj założeniowe dowody wprost podanych niżej tautologii kwantyfikatorowych.

(a)

(b) A    a <?(*)]-*lA xP(x)a A *«*)]■

(c)    [AxP(x)a A *C(*)1“* Ax[P(x)aC(x)J.

(d)    V *F<*) a C(*)]-*IV*^) a V *GW]

85. Udowodniwszy pewne twierdzenie, można je dołączyć jako nowy wiersz do dowodu dowolnego innego twierdzenia. Na przykład, mając dowód twierdzenia:

(TJ    P(x)-*\/xP(x)

korzystamy zeń w dowodzie twierdzenia:

~\J xP{x)~* /\x~P(x) w następujący sposób:

(I) ~ V xP(x)    (założenie)

(2)    P(x)->\JxP(x)

(3)    ~P(x)

(4)    Ax~P{x)

(Ti)

(RRZ: 2, 1)

PA': 3)

(RRZ jest skrótem wyrażenia „reguła rachunku zdań“; w tym wypadku jest nią reguła wtórna oparta na prawie modus tollcndo tollens).

(A) Udowodnij twierdzenie Tj oraz twierdzenie:

(T.)

A xP(xy+p(x).

(B) Korzystając z twierdzeń Tj, T, udowodnij następujące twierdzenia:

(a)    ~\/xP(x)^\/x~P(x).

(b)    A x~P(#-*~ A xP(x).

86. Przykładem dowodu niewprost w systemie założeniowym rac liunku kwantyfikatorów jest podany niżej dowód

69