104307

Ponadto udowodnić musimy jako twierdzenia teorii:

Istnienie: Vxi... Vx„ 3y <j>(xi, ..., x„,y) - istnieje wynik operacji f (jeżeli działamy na coś funkcją, to dostajemy coś innego)

Jednoznaczność (jedyność): Vxi... Vx„ Vy Vy* {[cp(xi, ..., x_n, y) a <p(xi, ...,x^y’)] =*y=y’} - istnieje dokładnie jeden wynik operacji f

Ewentualnie? Vxi... Vx„ [f(xi,..., x_n) = <* f(xj,..., x„)], gdzie t jest termem języka.

Stałe indywiduowe można rozpatrywać jako 0-argumentowe symbole funkcyjne.

Przykłady złych definicji

1.    Niech /(x) = ^l/_x

Vx Vy [/(x) = y <=>_df x • y = 1]

x/0, y/0: f(0) = f(0) <=> 0 • f(0) = 1, więc 0=1 (zdanie udowodnione w starym języku -niespełnienie warunku nietwórczości).

~ Vx 3y x • y = 1, ponieważ ~ 3y 0 • y = 1.

2.    Niech f(x) = Vx

Vx Vy [f(x) = y <=>_df y • y = x]

Wiadomo, że 1 • 1 = 1 i (-1) • (— 1) = 1. x/l, y/1: f (1) = 1 x/l, y/-l: f(l) = - 1

Więc 1 = - 1 - sprzeczność powstała w wyniku niespełnienia warunku jednoznaczności. Niespełnienie warunku istnienia w R - nie dla każdej liczby rzeczywistej istnieje Vx.

Niech U - uniwersum. Niech zmienne A, B, C przebiegają podzbiory U, a x, y, z elementy U.

1. VAVB VC{AuB = C <=>* Vx [xeC <=> (xe A v x€ B)]>

2. VA VB VC {A n B = C Vx [xeC <=> (xe A a x€ B)]}

3.    VA VB VC {A - B = C <=*_df Vx [x€C <=> (x€ Aa~xg B)]}

Dowodzimy istnienia i jednoznaczności.

1.

Istnienie: VA VB 3C Vx [xe C <=> (x€ A v \e B)]

Dowód Niecił A, B - ustalone zbiory. Na mocy ograniczonego schematu wyróżniania 3Z Vx {xe Z «=> [xe U a (xe A v xe B)]}. Oznaczmy przez C zbiór taki, że Vx (x€ C <=» [x€ U a (x€ A v xe B)]} (*). Chcemy udowodnić, że Vx [xe C <=> (xe A v xe B)]. Niech x będzie ustalonym elementem U.

(=>): załóżmy, że xeC. Wówczas, na mocy (*), xe A v xe B.

(<=): załóżmy, że xe A v xe B. Ponadto xe U. Zatem xeC. □

Jednoznaczność: VA VB VC VC' ({Vx [xe C <=> (xe Avxe B)] a Vx [xe C’ «(xeAv xe B)]} =>C = C’)

Dowód. Niech A, B, C, C' będą podzbiorami zbioru U takimi, że:

(I)    Vx [x€ C <=> (x€ A V X€ B)]

(II)    Vx [xe C' <=> (xe A v xe B)]

Chcemy pokazać, że Vx (xeC <=> xe C’).

Ustalmy x takie, że xe U. FAE:

xeC

xe A v x€ B (na mocy I) xeC’ (na mocy II)

Zatem Vx (xe C <=^ xe C'). Na mocy zasady ekstensjonalności C = C'. □