Logika id 517887 Nieznany

Logika

Materia ly pomocnicze do wyk ladu

dla pierwszego roku informatyki UW

Pawe l Urzyczyn

urzy@mimuw.edu.pl

25 sierpnia 2005

Wnioskowanie o prawdziwo´sci rozmaitych stwierdze´

n jest powszednim zaj

eciem matema-

tyk´

ow i nie tylko matematyk´

ow. Dlatego filozofowie i matematycy od dawna zajmowali

e systematyzacj

a metod wnioskowania i kryteri´

ow ich poprawno´sci. Oczywiscie ostatecz-

nym kryterium poprawno´sci rozumowania pozostaje zawsze zdrowy rozs

adek i przekonanie

o s luszno´sci wywodu. Logika, jako nauka o rozumowaniu, jest jednak wa˙znym i potrzebnym
narz

edziem, kt´

ore to przekonanie u latwia.

Szczeg´

oln

a rol

e w´sr´

od rozmaitych dzia l´

ow logiki zajmuje logika matematyczna, po´swi

econa

opisowi i analizie poprawno´sci wnioskowa´

n matematycznych. Jest to dyscyplina w pewnym

sensie paradoksalna: b

ac sama cz

e´sci

a matematyki, traktuje matematyk

e jako sw´

oj przed-

miot zainteresowania. Dla unikni

ecia

”

b l

ednego ko la” musimy wi

ec tutaj zauwa˙zy´

c, ˙ze

logika formalna nie opisuje rzeczywistych wywod´

ow matematyka, ale ich uproszczone mo-

dele, kt´

ore bez zastrze˙ze´

n mo˙zna uwa˙za´

c za zwyk le obiekty matematyczne. Mimo tego

ograniczenia, logika matematyczna dostarcza niezwykle wa˙znych wniosk´

ow o charakterze

filozoficznym i metamatematycznym.

Logika formalna by la kiedy´s ezoteryczn

a nauk

a z pogranicza filozofii i matematyki. P´

o´

zniej

okaza lo si

e jednak, ˙ze metody logiki formalnej znalaz ly wa˙zne zastosowania praktyczne,

dostarczaj

ac technik weryfikacji poprawno´sci program´

ow.

Jak stwierdzili´smy wy˙zej, logika matematyczna zajmuje si

e badaniem rozmaitych system´

formalnych, modeluj

acych rzeczywiste sposoby wnioskowania matematycznego. W ramach

tego wyk ladu zajmowa´

c si

e b

edziemy trzema takimi systemami. Najszerszy z nich to logika

pierwszego rz

edu, zwana te˙z rachunkiem predykat´

ow lub rachunkiem kwantyfikator´

ow . Dwa

wa˙zne fragmenty logiki pierwszego rz

edu, kt´

orym po´swi

ecimy wiele uwagi, to wnioskowanie

r´

owno´

sciowe i rachunek zda´

Struktury relacyjne

Definicja 1.1 Przez sygnatur

e rozumiemy pewien (zwykle sko´

nczony) zbi´

or symboli re-

lacyjnych i funkcyjnych, ka˙zdy z ustalon

a liczb

a argument´

ow. Sygnatur

e Σ przedstawi´

mo˙zna jako sum

Σ =

[

n∈N

∪

[

n∈N

R
n

gdzie Σ

jest zbiorem n-argumentowych symboli funkcyjnych, a Σ

R
n

jest zbiorem n-argu-

mentowych symboli relacyjnych. O symbolu f ∈ Σ

powiemy, ˙ze jego arno´

s´

c to liczba n

i napiszemy ar (f ) = n. Podobnie dla r ∈ Σ

R
n

. Elementy zbioru Σ

to symbole sta lych.

Natomiast elementy zbioru Σ

R
0

nazwiemy symbolami zdaniowymi .

Uwaga: Je˙zeli sygnatura jest sko´

nczona, to prawie wszystkie ze zbior´

ow Σ

i Σ

R
n

a puste.

Oczywi´scie n-argumentowe symbole funkcyjne pos lu˙z

a nam jako nazwy n-argumentowych

funkcji a n-argumentowe symbole b

a nazwami n-argumentowych relacji. Przypomnijmy,

˙ze n-argumentowa relacja w zbiorze A to dowolny podzbi´

or iloczynu kartezja´

nskiego A

Inaczej m´

owi

ac, jest to pewien zbi´

or krotek postaci ha

, . . . , a

i, gdzie a

, . . . , a

∈ A.

Krotk

e hai uto˙zsamiamy z elementem a, tj. uwa˙zamy, ˙ze A

to to samo co A. Natomiast

zbi´

or A

ma tylko jeden element, mianowicie pust

a krotk

e h i. S

a wi

ec tylko dwie relacje

zero-argumentowe: pusta i pe lna. Mo˙zemy je oznacza´

c odpowiednio przez 0 i 1.

Skoro zbi´

or A

ma tylko jeden element, to funkcja zeroargumentowa f : A

→ A przyj-

muje tylko jedn

a warto´s´

c. B

edziemy wi

ec ka˙zd

a tak

a funkcj

e nazywa´

c sta l

a i uto˙zsamia´

z odpowiednim elementem zbioru A.

Definicja 1.2 Struktura relacyjna albo model sygnatury Σ to niepusty zbi´

or (zwany dzie-

dzin

a lub no´

snikiem struktury) wraz z interpretacj

a symboli sygnaturowych jako funkcji

i relacji o odpowiedniej liczbie argument´

ow. Dok ladniej, je´sli Σ = {f

, . . . , f

, r

, . . . , r

to struktur

a relacyjn

a (modelem) nazywamy krotk

e postaci:

A = hA, f

, . . . , f

, r

, . . . , r

gdzie dla dowolnego i:

• f

: A

→ A, je´sli ar (f

) = k (w szczeg´

olno´sci f

∈ A, gdy k = 0);

• r

⊆ A

, gdy ar (r

) = k.

Definicja 1.3 Je´sli sygnatura Σ nie zawiera ˙zadnych symboli relacyjnych, to modele tej
sygnatury nazywamy algebrami .

Konwencje notacyjne: No´snik struktury A oznaczamy przez |A|. Cz

esto przyjmujemy

domy´slnie, ˙ze |A| = A, |B| = B itd., lub po prostu struktur

e i jej no´snik oznaczamy

tym samym symbolem. Cz

esto te˙z tak samo oznacza si

e symbol relacyjny (funkcyjny)

i odpowiadaj

a mu relacj

e (funkcj

e).

Przyk lad 1.4 Niech Σ = {+, •, 0, 1, ≤}, gdzie Σ

= {+, •}, Σ

= {0, 1}, oraz Σ

R
2

= {≤}.

Modelem dla sygnatury Σ jest oczywi´scie zbi´

or liczb rzeczywistych ze zwyk lymi dzia laniami

i porz

adkiem:

R = hR, +

, •

, 0

, 1

, ≤

Ten model zwykle zapiszemy po prostu tak:

R = hR, +, ·, 0, 1, ≤i.

Inne modele dla tej sygnatury to np. zbi´

or liczb naturalnych ze zwyk lymi dzia laniami i po-

adkiem oraz zbi´

or wszystkich podzbior´

ow R z dzia laniami mnogo´sciowymi i inkluzj

N = hN, +, ·, 0, 1, ≤i;

P = hP(R), ∪, ∩, ∅, R, ⊆i.

Ale modelem jest te˙z taka struktura:

A = hR, ·, f, π, 0, ∅i,

gdzie f (a, b) = 3 dla dowolnych liczb a, b (symbol “+” jest interpretowany jako mno˙zenie!).

Przyk lad 1.5 Modelami dla sygnatury Σ = {•, 1}, gdzie Σ

= {•} i Σ

= {1}, s

a na

przyk lad struktury hN, +, 0i i hN, ∗, 1i, oraz algebra s l´ow z konkatenacj

a i s lowem pustym:

h{a, b}

∗

, ·, εi.

Przyk lad 1.6 Graf zorientowany G = hV, Ei, gdzie V jest zbiorem wierzcho lk´

ow, nato-

miast E ⊆ V × V jest zbiorem kraw

edzi, jest modelem jednoelementowej sygnatury

Σ = Σ

R
2

= {r}.

Definicja 1.7 Podstruktura struktury A sygnatury Σ to taki niepusty podzbi´

or B ⊆ A,

kt´

ory jest zamkni

ety ze wzgl

edu na wszystkie operacje, tj. dla dowolnego n i dowolnego

f ∈ Σ

spe lnia warunek:

• Je´sli a

, . . . a

∈ B to f

, . . . , a

) ∈ B.

Taki podzbi´

or B jest oczywi´scie no´snikiem pewnej struktury

B = hB, f

, . . . , f

, r

, . . . , r

kt´

orej operacje i relacje s

a odpowiednimi obci

eciami operacji i relacji w A, tj. f

= f

oraz r

= r

∩ B

, dla wszystkich i, j. Tak

a struktur

e te˙z nazywamy podstruktur

a A,

i zwykle po prostu uto˙zsamiamy ze zbiorem B. Podstruktury algebr nazywamy oczywi´scie
podalgebrami .

Przyk lad 1.8

• Zbi´

or liczb naturalnych jest podalgebr

a algebry liczb rzeczywistych z dodawaniem

i mno˙zeniem, ale nie jest podalgebr

a algebry liczb rzeczywistych z dodawaniem,

mno˙zeniem i odejmowaniem.

• Rodzina z lo˙zona za wszystkich sko´

nczonych podzbior´

ow zbioru N i ich dope lnie´n

(nazywanych zbiorami kosko´

nczonymi ) jest podalgebr

a algebry hP(N), ∪, ∩, ∅, N, i.

Fakt 1.9

• Je´sli iloczyn jakiej´s rodziny podstruktur struktury A jest niepusty, to te˙z jest pod-

struktur

a struktury A.

• Je´sli w sygnaturze jest cho´

c jedna sta la, lub zbi´

or B ⊆ |A| jest niepusty, to ist-

nieje najmniejsza podstruktura struktury A zawieraj

aca B. Jest to iloczyn wszystkich

podstruktur zawieraj

acych B.

Dow´

od:

Latwe ´

cwiczenie.

Definicja 1.10 Najmniejsz

a podstruktur

e struktury A zawieraj

a zbi´

or B nazywamy

podstruktur

a generowan

a przez B. Je´sli jest to ca la struktura A, to m´

owimy, ˙ze B jest

zbiorem generator´

ow struktury A. Zwrot

”

Struktura A ma k generator´

ow” oznacza, ˙ze

istnieje zbi´

or generator´

ow mocy k.

Struktura (algebra) generowana przez zbi´

or pusty

nazywana jest struktur

a (algebr

a) Herbranda.

Przyk lad 1.11

• Podstruktura generowana w hR, +, ·, 0, 1, ≤i przez {−1} sk lada si

e ze wszystkich liczb

ca lkowitych, a generowana przez zbi´

or pusty — ze wszystkich liczb naturalnych. Nie

istnieje sko´

nczony zbi´

or generator´

ow dla hR, +, ·, 0, 1, ≤i.

• Struktura hN, 0, si, gdzie s(n) = n + 1, dla dowolnego n ∈ N, jest algebr

a Herbranda.

Fakt 1.12 Niech A = hA, f

, . . . , f

, r

, . . . , r

i, gdzie symbole f

, . . . , f

a odpowiednio

, . . . , k

-argumentowe, i niech B b

edzie podzbiorem A. Podstruktura generowana przez B

jest sum

a wst

epuj

acego ci

agu zbior´

ow B

, gdzie B

= B oraz B

n+1

= B

∪

n
i=1

→

Dow´

od:

Cwiczenie.

Homomorfizmy

Definicja 1.13 Homomorfizmem ze struktury A w stuktur

e B (tej samej sygnatury Σ)

jest ka˙zde przekszta lcenie h : A → B, kt´

ore zachowuje funkcje i relacje struktury A, tj.

• dla dowolnego f ∈ Σ

i dowolnych a

, . . . , a

∈ |A|, zachodzi h(f

, . . . , a

)) =

(h(a

), . . . , h(a

));

• dla dowolnego r ∈ Σ

R
n

i dowolnych a

, . . . , a

∈ |A|, je´sli ha

, . . . , a

i ∈ r

to tak˙ze

hh(a

), . . . , h(a

)i ∈ r

Homomorfizm jest silny, wtedy i tylko wtedy, gdy dodatkowo, dla dowolnego r ∈ Σ

R
n

spe lnia taki warunek:

• je´sli hh(a

), . . . , h(a

)i ∈ r

dla a

, . . . , a

∈ |A|, to istniej

a takie a

0
1

, . . . , a

0
n

∈ |A|, ˙ze

h(a

0
1

) = h(a

), . . . , h(a

0
n

) = h(a

), oraz ha

0
1

, . . . , a

0
n

i ∈ r

Na szcz

e´scie najcz

e´sciej interesuj

a nas homomorfizmy algebr, a oczywi´scie:

Fakt 1.14 Ka˙zdy homomorfizm algebr jest silny.

Definicja 1.15 Homomorfizm h : A

1−1

−→

B nazywamy izomorfizmem, je˙zeli przekszta lce-

nie odwrotne h

−1

: B

1−1

−→

A te˙z jest homomorfizmem. Piszemy wtedy A ≈ B.

Przyk lad 1.16

• Przekszta lcenie h : {0, 1}

∗

→ N, dane przez h(w) = |w|, jest homomorfizmem z alge-

bry h{0, 1}

∗

, ·, εi w algebr

e hN, +, 0i.

• Izomorfizm porz

adkowy zbior´

ow cz

e´sciowo uporz

adkowanych A i B to to samo co

izomorfizm struktur hA, ≤i i hB, ≤i.

• Reszta z dzielenia przez 3 jest silnym homomorfizmem graf´

ow na rysunku:

^^====

====

• Funkcja identyczno´sciowa jest homomorfizmem graf´

ow na drugim rysunku, ale nie

jest to homomorfizm silny ani izomorfizm.

^^====

====

^^====

====

Uwaga: Poj

ecie izomorfizmu, jak zawsze w matematyce, s lu˙zy do uto˙zsamienia ze sob

tych obiekt´

ow, kt´

ore s

a nierozr´

o˙znialne ze wzgl

edu na interesuj

ace nas w lasno´sci. W naszym

przypadku, stwierdzenie, ˙ze dwie struktury (algebry) s

a izomorficzne, oznacza, ˙ze operacje

i relacje s

a w nich okre´slone dok ladnie tak samo. Struktury izomorficzne mog

a si

e tylko

r´

o˙zni´

c od siebie no´snikami. W algebrze (i logice) takie struktury uwa˙za si

e za identyczne,

co pozwala np. na takie stwierdzenia jak

”

istnieje dok ladnie jedna taka algebra, ˙ze . . . ”

Fakt 1.17

• Z lo˙zenie homomorfizm´

ow jest homomorfizmem.

• Obraz podalgebry przy homomorfizmie jest podalgebr

a przeciwdziedziny.

• Homomorfizm jest izomorfizmem wtedy i tylko wtedy, gdy jest silnym homomorfizmem

i bijekcj

Dow´

od:

Latwe ´

cwiczenie.

Lemat 1.18 Je´

sli zbi´

or C generuje struktur

e A oraz h

, h

: A → B s

a homomorfizmami

spe lniaj

acymi warunek h

= h

, to h

= h

Dow´

od:

Latwo sprawdzi´

c, ˙ze zbi´

or D = {a ∈ A | h

(a) = h

(a)} jest podstruktur

struktury A. Z za lo˙zenia C ⊆ D, a wi

ec A = D, bo A jest najmniejsz

a podstruktur

zawieraj

a C.

Mora l 1.19 Homomorfizm jest jednoznacznie wyznaczony przez warto´

sci jakie przyjmuje

na generatorach. Wystarczy zna´

c te warto´

sci i ju˙z znamy homomorfizm. Uwaga: nie zawsze

istnieje homomorfizm przypisuj

acy generatorom ˙z

adane warto´

sci.

A zatem homomorfizm algebr jest izomorfizmem wtedy i tylko wtedy, gdy jest bijekcj

Kongruencje i ilorazy

Definicja 1.20 Relacja r´

ownowa˙zno´sci ∼ w zbiorze |A| jest kongruencj

a w A wtedy i tylko

wtedy, gdy dla dowolnego n i dowolnego f ∈ Σ

zachodzi warunek:

Je´sli a

∼ a

0
1

, . . . , a

∼ a

0
n

to f

, . . . , a

) ∼ f

0
1

, . . . , a

0
n

Przyk lad 1.21

• Relacja przystawania modulo 7 jest kongruencj

a w algebrze liczb ca lkowitych z do-

dawaniem i mno˙zeniem.

• Relacja

”

r´

o˙znica symetryczna zbior´

ow x i y jest sko´

nczona” jest kongruencj

a w alge-

brze hP(N), ∪, ∩, ∅, N, i.

Fakt 1.22 Iloczyn dowolnej niepustej rodziny kongruencji jest kongruencj

Dow´

od:

Latwy.

Przypomnijmy, ˙ze j

adrem przekszta lcenia f : A → B nazywamy relacj

e r´

ownowa˙zno´sci

ker(f ) = {ha, bi ∈ A × A | f (a) = f (b)}.

Fakt 1.23

adro dowolnego homomorfizmu jest kongruencj

Dow´

od:

Niech h : A → B b

edzie homomorfizmem i przypu´s´

cmy, ˙ze h(a

) = h(a

0
i

)

dla i = 1, . . . , n.

Jesli teraz f ∈ Σ

to: h(f

, . . . , a

)) = f

(h(a

), . . . , h(a

)) =

(h(a

0
1

), . . . , h(a

0
n

)) = h(f

0
1

, . . . , a

0
n

)).

Definicja 1.24 Niech ∼ b

edzie kongruencj

a w strukturze A = hA, f

, . . . , f

, r

, . . . , r

Struktura ilorazowa struktury A wyznaczona przez relacj

e ∼ to struktura

∼

= hA/

∼

, f

∼

, . . . , f

∼

, r

∼

, . . . , r

∼

gdzie operacje i relacje s

a zdefiniowane tak:

• Je´sli f

ma k argument´

ow, to f

∼

([a

]

∼

, . . . , [a

]

∼

) = [f

, . . . , a

)]

∼

• Je´sli r

ma k argument´

ow, to warunek h[a

]

∼

, . . . , [a

]

∼

i ∈ r

∼

zachodzi wtedy i tylko

wtedy, gdy istniej

a takie a

0
1

, . . . , a

0
k

, ˙ze a

∼ a

0
1

, . . . , a

∼ a

0
k

oraz ha

0
1

, . . . , a

0
k

i ∈ r

Uwaga: Poprawno´s´

c (jednoznaczno´s´

c) powy˙zszej definicji wynika natychmiast st

ad, ˙ze ∼

jest kongruencj

Fakt 1.25 Niech ∼ b

edzie kongruencj

a w A. W´

owczas przekszta lcenie κ : A

−→ A/

∼

okre´

slone przez κ(a) = [a]

∼

, jest silnym homomorfizmem.

Dow´

od:

Latwe ´

cwiczenie.

Homomorfizm κ nazywany bywa homomorfizmem kanonicznym. Relacja ∼ jest oczywi´scie
j

adrem tego homomorfizmu, sk

ad otrzymujemy:

Mora l 1.26 Kongruencje i j

adra homomorfizm´

ow to to samo.

Nastepuj

ace twierdzenie, zwane (pierwszym) twierdzeniem o homomorfizmie, to dalszy

krok w tym samym kierunku. Wraz z Faktem 1.25 stwierdza ono, ˙ze ilorazy danej struktury
to to samo, co jej obrazy przy silnych homomorfizmach.

Twierdzenie 1.27 Niech h : A

−→ B b

edzie silnym homomorfizmem, kt´

orego j

adrem jest

relacja ∼. Wtedy B jest izomorficzne z A/

∼

Dow´

od:

Izomorfizm i : A/

∼

→ B jest okre´slony r´

ownaniem i([a]

∼

) = h(a). Poniewa˙z

warunki a ∼ a

i h(a) = h(a

) s

a r´

ownowa˙zne, wi

ec i jest dobrze okre´slon

a funkcj

r´

o˙znowarto´sciow

a. Ta funkcja jest te˙z

”

na”, bo h jest

”

na”. Jest to homomorfizm, bo:

• Je´sli f ∈ Σ

, to i(f

∼

([a

]

∼

, . . . , [a

]

∼

)) = i([f

, . . . , a

)]

∼

) = h(f

, . . . , a

)) =

(h(a

), . . . , h(a

)) = f

(i([a

]

∼

), . . . , i([a

]

∼

)).

• Je´sli ar (r) = n oraz h[a

]

∼

, . . . , [a

]

∼

i ∈ r

∼

to ha

0
1

, . . . , a

0
n

i ∈ r

, dla pewnych

0
1

, . . . , a

0
m

spe lniaj

acych warunek a

∼ a

0
1

, . . . , a

∼ a

0
m

. Wtedy

hi([a

]

∼

), . . . , i([a

]

∼

)i = hh(a

), . . . , h(a

)i = hh(a

0
1

), . . . , h(a

0
n

)i ∈ r

bo h jest homomorfizmem.

Ponadto i jest silnym homomorfizmem, co wynika natychmiast st

ad, ˙ze h jest silnym ho-

momorfizmem, i ˙ze hi([a

]

∼

), . . . , i([a

]

∼

)i to to samo co hh(a

), . . . , h(a

)i. Z Faktu 1.17

wnioskujemy, ˙ze i jest izomorfizmem.

Poniewa˙z ka˙zdy homomorfizm algebr jest silny, wi

ec z Faktu 1.25 i Twierdzenia 1.27 wynika:

Mora l 1.28 Ilorazy i obrazy homomorficzne algebr to to samo.

Produkty

Definicja 1.29 Niech A

= hA

, f

, . . . , f

, r

, . . . , r

i, dla t ∈ T . Produktem rodziny

indeksowanej {A

}

t∈T

nazywamy struktur

t∈T

= h

t∈T

, f

, . . . , f

, r

, . . . , r

w kt´

orej operacje i relacje s

a zdefiniowane tak:

• Je´sli f

ma k argument´

ow, to f

(ξ

, . . . , ξ

)(t) = f

(ξ

(t), . . . , ξ

(t));

• Je´sli r

ma k argument´

ow, to hξ

, . . . , ξ

i ∈ r

zachodzi wtedy i tylko wtedy, gdy dla

wszystkich t ∈ T ma miejsce hξ

(t), . . . , ξ

(t)i ∈ r

Oczywi´scie, je´sli zbi´

or T jest dwuelementowy, na przyk lad T = {0, 1}, to zamiast

t∈T

piszemy po prostu A

× A

, a nale˙z

ace do produktu funkcje ξ : {0, 1} → A

∪ A

uto˙zsa-

miamy z parami uporz

adkowanymi hξ(0), ξ(1)i.

Je˙zeli natomiast wszystkie A

a identyczne z A, to zamiast

t∈T

A piszemy A

i m´

owimy

o strukturze pot

egowej.

Przyk lad 1.30 Struktura hP(N), ∪, ∩, ∅, N, i jest izomorficzna z pot

a h{0, 1}, ∨, ∧, 0, 1i

gdzie i ∨ j = max{i, j} oraz i ∧ j = min{i, j}.

Definicja 1.31 (Rzuty) Homomorfizm π

t∈T

−→ A

, okre´slony przez warunek

(ξ) = ξ(s), nazywamy rzutowaniem na wsp´

o lrz

edn

a s.

Termy

Jak powiedzieli´smy na pocz

atku, symbole nale˙z

ace do sygnatury maj

a nam s lu˙zy´

c jako

nazwy pewnych funkcji i relacji. Znaczenie tych nazw zale˙zy oczywi´scie od wybranego
modelu. W szczeg´

olno´sci symbole sta lych s

a nazwami ustalonych element´

ow modelu. Inne

elementy modelu te˙z mog

a by´

c nazwane, na przyk lad je´sli f ∈ Σ

i c ∈ Σ

to mo˙zemy

napisa´

c co´s takiego:

”

f (f (c, c), f (c, f (c, c)))”,

co w modelu A = hA, f, ci b

edzie oczywi´scie nazw

a elementu f(f(c, c), f(c, f(c, c))).

W ten spos´

ob mo˙zna jednak nazywa´

c tylko elementy podstruktury generowanej przez sta le.

Aby nazywa´

c dowolne elementy modelu potrzebujemy zmiennych. Ustalmy wi

ec pewien

zbi´

or symboli V , kt´

orego elementy (oznaczane x, y, . . .) b

edziemy nazywali zmiennymi in-

dywiduowymi , lub po prostu zmiennymi . Zwykle przyjmuje si

e, ˙ze V jest niesko´

nczonym

zbiorem przeliczalnym, wygodnie jest te˙z zak lada´

c, ˙ze jego elementy s

a ponumerowane, tj.

V = {x

: i ∈ N}. Okazjonalnie b

edziemy dopuszcza´

c zbiory zmiennych dowolnej mocy.

Definicja 2.1 Przez termy sygnatury Σ rozumiemy elementy najmniejszego zbioru napi-
s´

ow T

(ozn. te˙z po prostu przez T ) spe lniaj

acego warunki:

• V ⊆ T

;

• je´sli f ∈ Σ

oraz t

, . . . , t

∈ T

”

f (t

, . . . , t

)” ∈ T

Konwencje notacyjne: Niekt´

ore dwuargumentowe symbole funkcyjne, jak np.

”

+”,

”

∪”

a tradycyjnie pisane pomi

edzy argumentami. Dlatego i my zamiast formalnie poprawnego

”

+(2, 2)” zwykle napiszemy

”

2+2”.

Przyk lad 2.2 Wyra˙zenie

”

f (g(g(x

, f (c)), x

))” jest termem sygnatury Σ, gdzie g ∈ Σ

f ∈ Σ

oraz c ∈ Σ

. Wyra˙zenie

”

(0 + x

) • 1” jest termem sygnatury Σ, w kt´

orej +, • ∈ Σ

i 0, 1 ∈ Σ

esto wygodnie jest reprezentowa´

c termy za pomoc

a drzew sko´

nczonych, w kt´

orych li´scie

a etykietowane zmiennymi i sta lymi, a wierzcho lki wewn

etrzne symbolami funkcyjnymi.

Oczywi´scie stopie´

n wyj´sciowy wierzcho lka (liczba dzieci) musi si

e zgadza´

c z liczb

a argumen-

t´

ow u˙zytego symbolu funkcyjnego. Na przyk lad term f (g(g(x

, f (c)), x

)) przedstawiamy

jako:

yyy

Definicja 2.3 Dla dowolnego termu t, zbi´

or zmiennych wolnych termu t, oznaczany przez

F V (t), jest okre´slony przez indukcj

• F V (x) = {x}, gdy x jest zmienn

• F V (f (t

, . . . , t

)) = F V (t

) ∪ · · · ∪ F V (t

Je´sli X ⊆ V , to stosujemy takie oznaczenia:

• T

(X) = {t ∈ T

| F V (t) ⊆ X}

• T

(n) = T

({x

, . . . , x

})

Zauwa˙zmy, ˙ze F V (c) = ∅, gdy c jest symbolem sta lej (c ∈ Σ

Definicja 2.4 Struktura term´

ow sygnatury Σ, to dowolna taka struktura A, ˙ze:

• |A| = T

(X), dla pewnego X;

• f

, . . . , t

) =

”

f (t

, . . . , t

)”, dla dowolnego f ∈ Σ

;

Symbole relacyjne w strukturze term´

ow mog

a by´

c interpretowane dowolnie, istnieje wi

wiele takich struktur.

W przypadku sygnatur bez symboli relacyjnych, m´

owimy oczywi´scie o algebrach term´

ow .

Oczywi´scie istnieje wtedy tylko jedna algebra wszystkich term´

ow, oznaczana przez T

. Dla

dowolnego k mamy te˙z jednoznacznie wyznaczon

a algebr

e term´

ow k-argumentowych T

(k).

Wygodnie jest rozszerzy´

c pojecie algebry term´

ow na dowolne sygnatury. Zrobimy to tak:

algebra term´

ow T

(X) to taka struktura term´

ow o no´sniku T

(X), w kt´

orej wszystkie

relacje s

a. . . puste.

Fakt 2.5 Zbi´

or X ⊆ V jest zbiorem generator´

ow algebry T

(X).

Dow´

od:

Cwiczenie.

Warto´

sciowania i podstawienia

Oczywi´scie chcemy u˙zywa´

c term´

ow jako nazw obiekt´

ow indywiduowych (element´

ow jakie-

go´s modelu A). To znaczy, ˙ze chcemy ka˙zdemu termowi przypisa´

c jego warto´

s´

c w modelu A.

Definicja 2.6 Warto´

sciowaniem w danej strukturze A nazywamy dowolny homomor-

fizm v : T

→ A.

Latwo widzie´

c, ˙ze ka˙zde warto´sciowanie v jest jednoznacznie wyznaczone przez swoje ob-

ecie do zbioru zmiennych, tj. funkcj

e v|

: V → |A|. Wynika to z Mora lu 1.19. Co

ecej:

Fakt 2.7 Ka˙zda funkcja u : V → |A| jednoznacznie rozszerza si

e do pewnego warto´

sciowa-

nia v : T

→ A.

Dow´

od:

Dla dowolnego t ∈ T

zdefiniujemy v(t) przez indukcj

e ze wzgl

edu na d lugo´s´

c t:

a) v(x) = u(x), gdy x jest zmienn

b) v(f (t

, . . . , t

)) = f

(v(t

), . . . , v(t

)), gdy ar (f ) = n i t

, . . . , t

∈ T

Nietrudno sprawdzi´

c, ˙ze tak okre´slone przekszta lcenie jest homomorfizmem. (Zw laszcza

warunek dotycz

acy relacji jest latwy do sprawdzenia.)

Warto´sciowanie w A cz

esto definiuje si

e w la´snie jako funkcj

e u : V → A, a nast

epnie

rozszerza si

e do v : T

→ A za pomoc

a warunk´

ow (a) i (b) wyst

epuj

acych w dowodzie

Faktu 2.7. Piszemy wtedy v(t) = [[t]]

. Jak wida´

c, wychodzi na to samo, wi

ec zwykle

uto˙zsamia si

e u i v.

Je´sli znamy warto´sci zmiennych, to znamy warto´s´

c dowolnego termu. W istocie wa˙zne s

tylko te zmienne, kt´

ore w danym termie wyst

epuj

Fakt 2.8 Je´

sli v

, v

a takimi warto´

sciowaniami, ˙ze v

F V (t)

= v

F V (t)

, to v

(t) = v

(t).

Dow´

od:

Je´sli F V (t) = X to term t nale˙zy do algebry T (X) = T

(X) generowanej

przez X. Jest to oczywi´scie podalgebra algebry T

. Funkcje v

T (X)

i v

T (X)

a homomor-

fizmami z T

(X) do A, kt´

ore pokrywaj

a si

e na zbiorze generator´

ow X. Z Lematu 1.18

wynika, ˙ze pokrywaj

a si

e na ca lym T

(X), w szczeg´

olno´sci v

(t) = v

(t).

Mora l 2.9 Warto´

s´

c termu zale˙zy tylko od warto´

sci jego zmiennych wolnych.

Zauwa˙zmy, ˙ze je´sli term nie ma zmiennych wolnych, to jego warto´s´

c nie zale˙zy od warto´s-

ciowania i zamiast [[t]]

mo˙zna pisa´

c po prostu [[t]].

Oznaczenie: Przez v

oznaczamy warto´sciowanie, kt´

ore dla dowolnej zmiennej y spe lnia

takie warunki:

(y) =

gdy y = x;

v(y) w przeciwnym przypadku.

Oczywi´scie takie warto´sciowanie jest tylko jedno.

Podstawienia

Definicja 2.10 Warto´sciowanie w algebrze term´

ow nazywamy podstawieniem. Je´sli pod-

stawienie S jest takie, ˙ze S(x

) = t

, dla i = 1, . . . , n oraz S(y) = y dla wszystkich

zmiennych y 6∈ {x

, . . . , x

}, to cz

esto zamiast S(t) piszemy t[x

:= t

, . . . , x

:= t

] lub

t[t

, . . . , t

Uwaga: t[x := s, y := u] to zwykle nie to samo, co t[x := s][y := u].

O podstawieniu nale˙zy my´sle´

c jak o operacji syntaktycznej. Term S(t) powstaje z termu t

przez wstawienie termu S(x) na miejsce ka˙zdej zmiennej x.

Przyk lad: f (x, y)[x := f (y, x)] = f (f (y, x), y).

Lemat 2.11 Niech S b

edzie podstawieniem i niech v bedzie warto´

sciowaniem w pewnej

strukturze A. Przez v

oznaczmy takie warto´

sciowanie, ˙ze v

(x) = v(S(x)). W´

owczas, dla

dowolnego termu t, zachodzi r´

owno´

s´

c v(S(t)) = v

(t). W szczeg´

olno´

sci:

v(t[x := s]) = v

v(s)

(t).

Dow´

od:

Warto´sciowania v ◦ S i v

a homomorfizmami, kt´

ore pokrywaj

a si

e na gene-

ratorach. Zatem teza wynika z Lematu 1.18.

Wniosek 2.12 Niech F V (t) = {x

, . . . , x

} i niech y

, . . . , y

a r´

o˙znymi zmiennymi,

nie nale˙z

acymi do F V (t). Przyjmijmy t

= t[x

:= y

] . . . [x

:= y

]. Dla dowolnego v

istnieje takie w, ˙ze v(t) = w(t

Dow´

od:

Niech a

= v(x

), dla i = 1, . . . , n. Je´sli w(y

) = a

to z Lematu 2.11 wynika

r´

owno´s´

c w(t

) = w

. . .

(t) = v(t), bo warto´sciowania v i w

. . .

pokrywaj

a si

e dla

argument´

ow z F V (t).

Mora l na zako´

nczenie tej cz

e´sci jest taki: Je´sli warto´sci zmiennych przebiegaj

a jaki´s zbi´

or,

to warto´sci term´

ow tworz

a podalgebr

e generowan

a przez ten zbi´

or.

Fakt 2.13 Niech B b

edzie podalgebr

a generowana w A przez C. Wtedy nast

epuj

ace warunki

a r´

ownowa˙zne:

a) a ∈ B;

b) a = [[t]]

dla pewnego termu t i pewnego u : V → |A|, takiego, ˙ze

→

u (F V (t)) ⊆ C.

W szczeg´

olno´

sci, najmniejsz

a podalgebr

a algebry A (generowan

a przez zbi´

or pusty) jest

zbi´

or {[[t]] | t ∈ T (0)}, z lo˙zony z warto´

sci term´

ow sta lych.

Dow´

od:

Implikacj

e z (b) do (a) mo˙zna udowodni´

c przez latw

a indukcj

e ze wzgl

edu

na d lugo´s´

c termu t. Aby udowodni´

c implikacj

e z (a) do (b) musimy pokaza´

c, ˙ze zbi´

D = {[[t]]

| t ∈ T

oraz

→

u (F V (t)) ⊆ C}

jest podalgebr

a algebry A. Przypu´s´

cmy wi

ec, ˙ze f jest n-argumentowym symbolem funk-

cyjnym i ˙ze a

, . . . , a

∈ D. Zatem dla dowolnego i = 1, . . . , n mamy a

= [[t

]]

dla

pewnych term´

ow t

i pewnych warto´sciowa´

n u

, spe lniaj

acych

→

(F V (t

)) ⊆ C. Na mocy

Wniosku 2.12 mo˙zemy, bez straty og´

olno´sci za lo˙zy´

c, ˙ze zbiory F V (t

) s

a parami roz l

aczne.

ec istnieje takie warto´sciowanie u, ˙ze u|

F V (t

)

= u

F V (t

)

dla wszystkich i. Z Faktu 2.8

wynika, ˙ze [[t

]]

= a

, dla wszystkich i. A zatem f

, . . . , a

) = f

([[t

]]

, . . . , [[t

]]

) =

[[f (t

, . . . , t

)]]

∈ D i dobrze.

Klasy algebr

O klasach m´

owimy wtedy, gdy nie mo˙zemy m´

owi´

c o zbiorach, tj. gdy odpowiednie zbiory

nie istniej

a. Na przyk lad formu luj

ac og´

olne stwierdzenia o cia lach, wygodnie jest u˙zy´

skr´

otu my´slowego i powiedzie´

”

klasa wszystkich cia l”. Ch

etnie u˙zywamy te˙z wtedy notacji

”

= {A | A jest cia lem}” i piszemy

”

A ∈ F”gdy algebra A jest cia lem. Pami

etajmy jednak,

˙ze stosujemy t

e terminologi

e i takie oznaczenia tylko nieformalnie. W szczeg´

olno´sci klasy

nie s

a ju˙z elementami innych klas.

Umowa: Kiedy m´

owimy o klasie algebr K, to zawsze zak ladamy, ˙ze nale˙z

a do niej algebry

takiej samej sygnatury i ˙ze K jest zamkni

eta ze wzgl

edu na izomorfizmy: je´sli A ∈ K oraz

A ≈ B to B ∈ K. Algebry izomorficzne uwa˙zamy przecie˙z za nieodr´

o˙znialne.

Definicja 3.1 Gdy K jest klas

a algebr to H(K), S(K) i P (K) oznacza odpowiednio:

• klas

e wszystkich obraz´

ow homomorficznych algebr z klasy K;

• klas

e wszystkich podalgebr algebr z klasy K;

• klas

e wszystkich produkt´

ow algebr z klasy K.

Piszemy HSP (K) zamiast H(S(P (K))).

Lemat 3.2 Dla dowolnej klasy algebr K zachodz

a nast

epuj

ace inkluzje:

S(H(K)) ⊆ H(S(K))

P (H(K)) ⊆ H(P (K))

P (S(K)) ⊆ S(P (K))

Dow´

od:

Cwiczenie.

Wniosek 3.3 Dla dowolnych klas algebr K i L:

• K ⊆ HSP (K);

• HSP (HSP (K)) = HSP (K);

• Je´sli K ⊆ L to HSP (K) ⊆ HSP (L).

Dow´

od:

Cwiczenie.

Trzy charakterystyczne w lasno´sci wymienione we Wniosku 3.3 pozwalaj

a nam powiedzie´

˙ze HSP jest operacj

a domkni

ecia.

R´

owno´

sci

Napis postaci

”

= t

” (gdzie t

, t

∈ T ) nazywamy r´

ownaniem. R´

ownanie jest spe lnione

przez warto´sciowanie v w strukturze A gdy v(t

) = v(t

). Piszemy wtedy A, v |= t

= t

Je´sli ka˙zde warto´sciowanie w A spe lnia r´

ownanie, to m´

owimy, ˙ze jest ono prawdziwe w A

i piszemy A |= t

= t

. A je´sli tak jest dla ka˙zdej algebry z klasy K, to piszemy K |= t

= t

Je´sli E jest zbiorem r´

owna´

n, to notacja A |= E i K |= E oznacza, ˙ze warunek A |= e

(odpowiednio K |= e) zachodzi dla wszystkich r´

owna´

n e ∈ E.

Uwaga: Czasem m´

owi si

e, ˙ze algebra (klasa) “spe lnia” r´

ownanie, zamiast powiedzie´

c, ˙ze

to r´

ownanie jest prawdziwe w tej algebrze (klasie). Grozi to jednak nieporozumieniem, bo

przez “spe lnialno´s´

c” zwykle rozumiemy spe lnienie warunku przez pewne warto´sciowanie,

a nie przez ka˙zde.

Definicja 3.4 M´

owimy ˙ze klasa algebr K jest definiowalna r´

owno´

sciowo (jest rozmaito´

a), gdy istnieje taki zbi´

or r´

owna´

n E, ˙ze dla dowolnej algebry A:

A ∈ K

wtedy i tylko wtedy, gdy

A |= E.

Stosujemy wtedy notacj

e K = Mod(E).

Uwaga: Niech Eq(K) oznacza zbi´

or wszystkich r´

owna´

n prawdziwych we wszystkich alge-

brach klasy K. Oczywi´scie zachodz

a inkluzje K ⊆ Mod(Eq(K)) oraz E ⊆ Eq(Mod(E)).

Przyk lady klas definiowalnych r´

owno´

sciowo

W przyk ladach poni˙zej symbole +, · s

a zawsze dwuargumentowe, symbol − jest jednoar-

gumentowy a 0 i 1 oraz K i S to symbole sta lych.

Przyk lad 3.5 Algebr

e postaci hA, ·, 1i, w kt´

orej prawdziwe s

a r´

ownania

”

x · 1 = x”,

”

1 · x = x” ,

”

x · (y · z) = (x · y) · z”

nazywamy p´

o lgrup

a z jedno´

sci

a albo monoidem. Cz

esto zamiast

”

p´

o lgrupa z jedno´sci

a”

m´

owimy po prostu

”

p´

o lgrupa”. Przyk ladem p´

o lgrupy jest struktura s l´

ow hA

∗

, ·, εi. P´

o l-

grupa jest przemienna (inaczej abelowa) gdy jest w niej dodatkowo prawdziwe r´

ownanie

”

x · y = y · x”

Przyk lad 3.6 Je´sli hA, ·, 1i jest p´

o lgrup

a, w kt´

orej okre´slono dodatkow

a jednoargumen-

tow

a operacj

−1

o w lasno´sciach

x · x

−1

= 1,

−1

· x = 1,

to struktur

e hA, ·,

−1

, 1i nazywamy grup

a. Przyk ladem grupy jest struktura hF, ◦,

−1

, id

gdzie F jest zbiorem wszystkich bijekcyj z A do A.

Przyk lad 3.7 Pier´

scie´

n (przemienny z jedno´sci

a) to struktura A = hA, ·, +, −, 1, 0i, o ta-

kich w lasno´sciach:

• hA, +, −, 0i jest grup

a abelow

• hA, ·, 1i jest p´

o lgrup

a abelow

• A |= x · (y + z) = (x · y) + (x · z).

Przyk ladem pier´scienia jest zbi´

or R[x] wszystkich wielomian´ow o wsp´o lczynnikach rzeczy-

wistych.

Przyk lad 3.8 Pier´scie´

n A nazywamy cia lem, gdy ma co najmniej dwa elementy i dla

dowolnego niezerowego a ∈ |A| istnieje takie b ∈ |A|, ˙ze a · b = 1. Przyk ladem cia la
jest zbi´

or Z(x) wszystkich funkcji wymiernych o wsp´o lczynnikach ca lkowitych. Albo zbi´or

{0, 1, 2, 3, 4, 5, 6} z dzia laniami modulo 7.

Uwaga: W przeciwie´

nstwie do poprzednich przyk lad´

ow, klasa wszystkich cia l nie jest

definiowalna r´

owno´sciowo.

Przyk lad 3.9 Algebra kombinatoryczna to algebra hA, ·, K, Si, w kt´

orej prawdziwe s

a r´

ow-

nania:

• (K · x) · y = x;

• (((S · x) · y) · z) = (x · z) · (y · z).

Operacja · nazywana jest operacj

a aplikacji .

Cwiczenie*: W ka˙zdej algebrze kombinatorycznej prawdziwe jest r´

ownanie

((S · K) · K) · x = x.

Dlatego kombinator

(S · K) · K oznaczany jest przez I. Jak zdefiniowa´

c kombinator B

i kombinator 2, ˙zeby w ka˙zdej takiej algebrze prawdziwe by ly r´

ownania

((B · x) · y) · z = x · (y · z)

(2 · x) · y = x · (x · y)?

Kraty i algebry Boole’a

Poni˙zej, symbole u, t s

a zawsze dwuargumentowe, symbol − jest jednoargumentowy a 0

i 1 to symbole sta lych.

Definicja 4.1 Krat

a nazywamy algebr

e hB, u, ti, w kt´

orej s

a prawdziwe r´

ownania:

x t y = y t x

x u y = y u x

(x t y) t z = x t (y t z)

(x u y) u z = x u (y u z)

x u (x t y) = x

x t (x u y) = x.

Lemat 4.2 Je´

sli B = hB, u, ti jest krat

a, oraz a, b ∈ B, to

a t b = b wtedy i tylko wtedy, gdy a u b = a.

Dow´

od:

Je´sli a t b = b to a u b = a u (a t b) = a. Na odwr´

ot podobnie.

Fakt 4.3

1) Je´

sli B = hB, u, ti jest krat

a, to relacja ≤ okre´

slona warunkiem

a ≤ b

wtedy i tylko wtedy, gdy

a u b = a,

jest cz

e´

sciowym porz

adkiem i to takim, ˙ze a t b = sup{a, b} i a u b = inf{a, b}, dla

dowolnych a, b.

2) Je´

sli hB, ≤i jest zbiorem cz

e´

sciowo uporz

adkowanym, w kt´

orym ka˙zdy zbi´

or dwuele-

mentowy ma kres g´

orny i kres dolny, to B jest krat

a z operacjami a t b = sup{a, b}

i a u b = inf{a, b}.

Dla ch

etnych

Tak nazywamy termy nad t

a sygnatur

Dow´

od:

(1)

Relacja ≤ jest zwrotna, bo a = a u (a t (a u a)) = a u a, dla dowolnego

elementu a ∈ B. Jest przechodnia, bo je´sli a ≤ b i b ≤ c, to a u c = (a u b) u c = a u (b u c) =
a u b = a. Jest te˙z antysymetryczna, bo je´sli a ≤ b i b ≤ a, to a = a u b = b u a = b.

A wi

ec jest to cz

e´sciowy porz

adek. Poniewa˙z a u b = (a u a) u b = a u (a u b), wi

ec a u b ≤ a.

Podobnie a u b ≤ b, zatem iloczyn jest ograniczeniem dolnym dla a i b. Je´sli c jest jakim´s
innym ograniczeniem dolnym, tj. a u c = c i b u c = c, to (a u b) u c = a u (b u c) = a u c = c,
czyli c ≤ a u b. Wnioskujemy, ˙ze iloczyn jest kresem dolnym.

To, ˙ze suma jest kresem g´

ornym wynika w analogiczny spos´

ob z Lematu 4.2.

(2)

Latwe ´

cwiczenie.

Definicja 4.4 Krata jest dystrybutywna wtedy i tylko wtedy, gdy s

a w niej prawdziwe

r´

ownania:

a u (b t c) = (a u b) t (a u c);

a t (b u c) = (a t b) u (a t c).

Przyk lad 4.5 Krata wypuk lych podzbior´

ow p laszczyzny nie jest dystrybutywna.

Inny

przyk lad kraty, kt´

ora nie jest dystrybutywna, wida´

c na obrazku:

77p

^^===

===

ggOOOOOO

Istotnie: a t (b u c) = a t e = a, tymczasem (a t b) u (a t c) = d u c = c.

Definicja 4.6 Algebr

a Boole’a nazywamy algebr

e postaci hB, u, t, −, 0, 1i, gdy hB, u, ti

jest krat

a dystrybutywn

a oraz prawdziwe s

a r´

ownania:

0 u x = 0

0 t x = x

1 u x = x

1 t x = 1

x t −x = 1

x u −x = 0.

Dowoln

a algebr

e Boole’a, jak ka˙zd

a krat

e, mo˙zna uporz

adkowa´

c (Fakt 4.3), przyjmuj

ac, ˙ze

a ≤ b zachodzi wtedy i tylko wtedy, gdy a u b = a. Z Lematu 4.2 mamy oczywi´scie:

a ≤ b

wtedy i tylko wtedy, gdy

a t b = b.

ad natychmiast wynika, ˙ze w ka˙zdej algebrze Boole’a:

Cwiczenie: Dlaczego? Wskaz´

owka: jak jest okre´

slona suma w tej kracie?

• 1 jest elementem najwi

ekszym;

• 0 jest elementem najmniejszym,

ze wzgl

edu na uporz

adkowanie ≤.

Przyk lad 4.7 Oczywi´scie ka˙zdy zbi´

or postaci P(A) jest algebr

a Boole’a ze zwyk lymi ope-

racjami teoriomnogo´sciowymi. Podobnie ka˙zda podalgebra takiej algebry (inaczej cia lo
zbior´

ow ). W szczeg´

olno´sci rodzina wszystkich sko´

nczonych podzbior´

ow N i ich dope lnie´n

(tj. zbior´

ow kosko´

nczonych) tworzy algebr

e Boole’a. Ale najwa˙zniejszym przyk ladem al-

gebry Boole’a jest algebra dwuelementowa

= h{0, 1}, ∧, ∨, ¬, 0, 1i,

w kt´

orej i ∧ j = min(i, j), i ∨ j = max(i, j) oraz ¬i = 1 − i.

Przyk ladem kraty, kt´

ora nie jest algebr

a Boole’a (chocia˙z niewiele jej brakuje) jest al-

gebra H = hH, ∩, ∪, ¬, ∅, R

i, kt´

orej no´snik H to zbi´

or wszystkich otwartych podzbior´

p laszczyzny R

, a ¬A to wn

etrze dope lnienia zbioru A. W tej algebrze suma ¬A∪A zwykle

nie pokrywa ca lego R

, ale jej dope lnienie jest brzegowe (ma puste wn

etrze).

Zanim powr´

ocimy do zagadnienia r´

owno´sciowego definiowania klas algebr, zbierzemy teraz

kilka przydatnych w lasno´sci algebr Boole’a. Niech B = hB, u, t, −, 1, 0i b

edzie algebr

Boole’a.

Lemat 4.8 Dla dowolnych a, b ∈ B:

• a t b = 1 wtedy i tylko wtedy, gdy −a ≤ b;

• a u b = 0 wtedy i tylko wtedy, gdy −a ≥ b.

Dow´

od:

Za l´

o˙zmy, ˙ze a t b = 1. Wtedy b = b t 0 = b t (a u −a) = (b t a) u (b t −a) =

1u(bt−a) = bt−a, a wi

ec −a ≤ b. Na odwr´

ot, nier´

owno´s´

c −a ≤ b oznacza, ˙ze b = bt−a,

a zatem a t b = a t b t −a = a t −a t b = 1 t b = 1. W ten spos´

ob pokazali´smy pierwsz

e´s´

c tezy. Dow´

od drugiej jest podobny.

Wniosek 4.9 Dla dowolnego a ∈ B istnieje dok ladnie jedno b ∈ B, spe lniaj

ace warunki

a t b = 1 i a u b = 0. Jest to oczywi´

scie −a.

Wniosek 4.10 Dla dowolnych a, b ∈ B:

• −(−a) = a;

• −(a t b) = −a u −b;

• −(a u b) = −a t −b.

Dow´

od:

Wszystkie trzy warunki latwo wynikaj

a z Wniosku 4.9, bo na przyk lad (a u

b) t (−a t −b) = ((a t −a) u (b t −a)) t −b = (1 u (b t −a)) t −b = b t −a t −b = 1 t −a = 1
i podobnie (a u b) u (−a t −b) = 0. St

ad (−a t −b) musi by´

c dope lnieniem (a u b).

Czasem wygodnie jest zdefiniowa´

c w algebrze Boole’a jeszcze jedn

a operacj

a ⇒ b = −a t b

Lemat 4.11 Dla dowolnych a, b ∈ B:

• a ⇒ b = 1 wtedy i tylko wtedy, gdy a ≤ b.

Dow´

od:

Latwy.

Przechodzimy do definicji bardzo wa˙znego poj

ecia:

Definicja 4.12 Filtrem w algebrze B nazywamy niepusty podzbi´

or F zbioru B, spe lnia-

acy dla dowolnych a, b takie warunki:

• Je´sli a, b ∈ F to a u b ∈ F ;

• Je´sli a ∈ F i a ≤ b to b ∈ F .

Filtr F jest w la´

sciwy gdy F 6= B (lub r´

ownowa˙znie, gdy 0 6∈ F ). M´

owimy, ˙ze F jest filtrem

maksymalnym, gdy jest on maksymalny (ze wzgl

edu na inkluzj

e) w rodzinie wszystkich

filtr´

ow w la´sciwych. Inaczej m´

owi

ac, filtr maksymalny to taki w la´sciwy filtr F , ˙ze dla

dowolnego w la´sciwego filtru G, inkluzja F ⊆ G oznacza w istocie F = G.

O filtrze nale˙zy my´sle´

c jak o rodzinie element´

”

du˙zych”, tj. takich, kt´

ore ze wzgl

edu na

jakie´s kryterium mog

a by´

c uwa˙zane za bliskie elementowi najwi

ekszemu 1. Na przyk lad

rodzina kosko´

nczonych podzbior´

ow zbioru N jest filtrem w algebrze wszystkich podzbior´ow

tego zbioru. Ale w tej algebrze filtrem (i to maksymalnym) jest tak˙ze rodzina wszystkich
tych zbior´

ow, do kt´

orych nale˙zy liczba 13. Innym przyk ladem filtru (w algebrze P(R)) jest

rodzina wszystkich tych zbior´

ow, kt´

orych dope lnienia s

a miary zero.

Nietrudno zauwa˙zy´

c, ˙ze do ka˙zdego filtru musi nale˙ze´

c jedynka, i ˙ze zbi´

or {1} jest najmniej-

szym filtrem. Nast

epny lemat m´

owi o tym, sk

ad si

e bior

a filtry, a zw laszcza maksymalne.

Lemat 4.13

1) Je´

sli X ⊆ B ma tak

a w lasno´

s´

c, ˙ze ˙zaden sko´

nczony iloczyn element´

ow X nie jest

zerem

, to istnieje filtr w la´

sciwy zawieraj

acy X.

2) Je´

sli F jest filtrem i a 6∈ F , ale a u f 6= 0 dla dowolnego f ∈ F , to istnieje filtr

w la´

sciwy zawieraj

acy F ∪ {a}.

3) Je´

sli F jest filtrem w la´

sciwym, to istnieje filtr maksymalny zawieraj

acy F .

Dow´

od:

(1)

Rozpatrzmy zbi´

G = {b ∈ B | b ≥ d

u . . . u d

dla pewnego n i pewnych d

, . . . , d

∈ X}.

Oczywi´scie X ⊆ G, nietrudno te˙z sprawdzi´

c, ˙ze G jest filtrem.

(2)

Wystarczy zauwa˙zy´

c, ˙ze zbi´

or F ∪ {a} jest scentrowany. Dowolny sko´

nczony iloczyn

element´

ow F jest bowiem elementem F i jest r´

o˙zny od zera, bo skoro a 6∈ F , to F jest

w la´sciwy. A wi

ec sko´

nczone iloczyny element´

ow zbioru F ∪ {a} nale˙z

a do F lub maj

posta´

c f u a.

(3)

Rutynowe zastosowanie lematu Kuratowskiego-Zorna (´

cwiczenie).

Definicja 4.14 Filtr F jest pierwszy wtedy i tylko wtedy, gdy dla dowolnych a, b ∈ B
takich, ˙ze a t b ∈ F , zachodzi a ∈ F lub b ∈ F .

Filtr F jest ultrafiltrem wtedy i tylko wtedy, gdy dla dowolnego a ∈ B albo a ∈ F albo
−a ∈ F .

Lemat 4.15 Nast

epuj

ace warunki s

a r´

ownowa˙zne.

1) Filtr F jest maksymalny;

2) Filtr F jest pierwszy;

3) Filtr F jest ultrafiltrem.

Dow´

od:

(1)⇒(2)

Przypu´s´

cmy, ˙ze a t b ∈ F , ale a, b 6∈ F .

Je´sli f u a 6= 0 dla

dowolnego f ∈ F , to na mocy lematu 4.13(2), filtr F nie jest maksymalny. Podobnie dla b,
a wi

ec istniej

a takie f, g ∈ F , ˙ze f u a = g u b = 0. Zatem 0 = (f u a) t (g u b) =

(f t g) u (f t b) u (a t g) u (a t b) ∈ F , bo wszystkie cztery cz lony iloczynu nale˙z

a do

filtru F .

Taki zbi´

or nazywamy scentrowanym.

(2)⇒(3)

Oczywiste, bo a t −a = 1 ∈ F .

(3)⇒(1)

Przypu´s´

cmy, ˙ze F ⊆ G i G jest w la´sciwy. Je´sli teraz a ∈ G to a ∈ F , bo

w przeciwnym razie −a ∈ F ⊆ G, i by loby tak: 0 = a u −a ∈ G.

Uwaga: Istnieje silny zwi

azek pomi

edzy filtrami i kongruencjami. Latwo zauwa˙zy´

c, ˙ze dla

dowolnej kongruencji ∼, klasa [1]

∼

jest filtrem. Na odwr´

ot, ka˙zdy filtr F wyznacza tak

kongruencj

e ∼

a ∼

wtedy i tylko wtedy, gdy

a u f = b u f , dla pewnego f ∈ F .

Oczywi´scie F = [1]

∼

. Kongruencj

e ∼

mo˙zna te˙z zdefiniowa´

c za pomoc

a warunku:

a ∼

wtedy i tylko wtedy, gdy

(a u b) t (−a u −b) ∈ F .

Sprawdzenie tych w lasno´sci pozostawiamy dociekliwym jako ´

cwiczenie.

Teorie r´

owno´

sciowe

Definicja 5.1 Niech E b

edzie zbiorem r´

owna´

n. Relacj

e ∼

w zbiorze term´

ow T

definiu-

jemy jako najmniejsz

a relacj

e r´

ownowa˙zno´sci spe lniaj

a warunki:

• Je´sli

”

t = u” ∈ E to t ∼

• Je´sli t

∼

0
i

, dla i = 1, . . . , n to f (t

, . . . , t

) ∼

f (t

0
1

, . . . , t

0
n

) (tj. relacja ∼

jest

zamkni

eta ze wzgl

edu na dzia lania);

• Je´sli t ∼

u to S(t) ∼

S(u) dla dowolnego podstawienia S (tj. relacja ∼

jest

zamkni

eta ze wzgl

edu na podstawienia).

Je´sli t ∼

u to piszemy te˙z E `

∀

t = u. U˙zywamy tu specjalnie symbolu

”

∀

”, ˙zeby si

odr´

o˙znia l od zwyk lego

”

`”. Ale na razie to nie ma znaczenia.

Warunek t ∼

u mo˙zna wyrazi´

c w nast

epuj

acy spos´

ob. R´

owno´s´

”

t = u” mo˙zna udowodni´

wyprowadzaj

ac j

a z aksjomat´

ow r´

owno´

sciowych:

t = t

t = s

(dla “t = s” ∈ E)

za pomoc

a nastepujacych regu l wnioskowania r´

owno´

sciowego:

t = s

s = t

t = s, s = r

t = r

t = s

S(s) = S(t)

= s

, . . . , t

= s

f (t

, . . . , t

) = f (s

, . . . , s

)

R´

ownania zapisane nad kresk

a to przes lanki danej regu ly, a r´

ownanie pod kresk

a to jej

konkluzja. Przez wyprowadzenie (czyli dow´

od ) r´

ownania

”

t = u” nale˙zy rozumie´

c drzewo

etykietowane r´

ownaniami w ten spos´

ob, ˙ze:

• Etykiet

a korzenia jest

”

t = u”;

• Etykiet

a ka˙zdego li´scia jest jaki´s aksjomat;

• Etykieta ka˙zdego wierzcho lka wewn

etrznego jest konkluzj

a pewnej regu ly, kt´

orej

przes lanki s

a etykietami jego dzieci.

Przyk lad 5.2 Niech E bedzie zbiorem rowna´

n definiuj

acych kraty (Definicja 4.1). W´

ow-

czas E `

∀

x = x u x (czyli x ∼

x u x), a wyprowadzenie tej r´

owno´sci to takie drzewo:

x u (x t y) = x

x t (x u y) = x

x u (x t (x u x)) = x

x = x

x t (x u x) = x

kkkk

x = x u (x t (x u x))

x u (x t (x u x)) = x u x

mmmm

mmm

x = x u x

Zamiast rysowa´

c kraw

edzie drzewa, zwykle piszemy poziome kreski tam, gdzie w wypro-

wadzeniu zastosowano regu ly wnioskowania. A wi

ec nasze wyprowadzenie zapiszemy tak:

x u (x t y) = x

x u (x t (x u x)) = x
x = x u (x t (x u x))

x = x

x t (x u y) = x
x t (x u x) = x

x u (x t (x u x)) = x u x

x = x u x

Pozostawiamy czytelnikowi przyjemno´s´

c ustalenia, jakie regu ly zosta ly tu u˙zyte.

Twierdzenie 5.3 (o poprawno´

sci) Je´

sli t ∼

u to Mod(E) |= t = u (tj. A |= t = u

zachodzi zawsze gdy A |= E).

Je´sli um´

owimy si

e, ˙ze b

edziemy pisa´

c E |=

∀

t = u, gdy Mod(E) |= t = u, to powy˙zsze

twierdzenie przyjmuje nast

epuj

a posta´

Je´

sli E `

∀

t = u to E |=

∀

t = u.

Nale˙zy je rozumie´

c tak: wszystko to co mo˙zna wyprowadzi´

c z aksjomat´

ow r´

owno´sciowych E

jest prawd

a wsz

edzie tam, gdzie prawdziwe s

a te aksjomaty. A wi

ec wnioskowanie r´

owno´s-

ciowe jest poprawne.

Dow´

od:

Dow´

od twierdzenia o poprawno´sci przebiega przez indukcj

e ze wzgl

edu na de-

finicj

e relacji ∼

, co w istocie oznacza indukcj

e ze wzgl

edu na rozmiar wyprowadzenia

r´

ownania

”

t = u” (liczb

e wierzcho lk´

ow drzewa).

Krok bazowy to obserwacja, ˙ze wszystkie aksjomaty s

a prawdziwe w klasie Mod(E). Krok

indukcyjny polega na sprawdzeniu, ˙ze konkluzja ka˙zdej regu ly jest prawdziwa w Mod(E),
pod warunkiem, ˙ze prawdziwe s

a przes lanki. Na przyk lad, je´sli Mod(E) |= t = u, to tak˙ze

Mod(E) |= S(t) = S(u), dla dowolnego podstawienia S. Szczeg´

o ly pozostawiamy jako

cwiczenie.

Pe lno´

s´

c wnioskowania r´

owno´

sciowego

Nastepuj

aca obserwacja wynika wprost z definicji ∼

Fakt 5.4 Relacja ∼

jest kongruencj

a w algebrze term´

ow T

. (Jest to najmniejsza kon-

gruencja w T

, taka ˙ze t ∼

s dla wszystkich r´

owna´

n (t = s) ∈ E, kt´

ora jest zamkni

eta ze

wzgl

edu na podstawienia.)

Skoro mamy kongruencj

e, to mamy algebr

e ilorazow

a T

∼

, kt´

a dla uproszczenia ozna-

czamy przez T

. Podobnie, zamiast [t]

∼

piszemy [t]

Lemat 5.5 Je´

sli S jest podstawieniem, a v jest warto´

sciowaniem w T

spe lniaj

acym

warunek v(x) = [S(x)]

dla dowolnej zmiennej x, to dla dowolnego termu t mamy tak˙ze

v(t) = [S(t)]

Dow´

od:

Niech κ(t) = [t]

. Wtedy warto´sciowania v i κ ◦ S s

a homomorfizmami z T

do T

, kt´

ore pokrywaj

a si

e na zmiennych, tj. na generatorach. Zatem teza wynika

z Lematu 1.18.

Lemat 5.6 T

|= E

Dow´

od:

Niech

”

` = r” b

edzie r´

ownaniem z E i niech v b

edzie dowolnym warto´s-

ciowaniem w T /

. Wybierzmy podstawienie S tak, aby dla dowolnej zmiennej x zachodzi l

warunek S(x) ∈ v(x), czyli inaczej v(x) = [S(x)]

. Na mocy Lematu 1.18, warto´sciowanie v

jest identyczne ze z lo˙zeniem S i homomorfizmu kanonicznego, wi

ec v(t) = [S(t)]

zachodzi

dla dowolnego termu t.

Poniewa˙z E `

∀

` = r wi

ec tak˙ze E `

∀

S(`) = S(r), a st

ad tak˙ze v(`) = v(r), czyli

T /

, v |= ` = r. I o to chodzi.

Mora l 5.7 Ka˙zda teoria r´

owno´sciowa E ma model. Jest nim algebra ilorazowa T /

. Cza-

sami jednak ten model jest trywialny, tj. jednoelementowy. Dzieje si

e tak, gdy E `

∀

x = y

dla dw´

och r´

o˙znych zmiennych x, y. Wtedy nasza teoria r´

owno´sciowa ma tylko jednoele-

mentowe modele (dlaczego?).

Twierdzenie 5.8 (Birkhoffa o pe lno´

sci) Nast

epuj

ace warunki s

a r´

ownowa˙zne:

1) E |=

∀

t = u;

2) T

|= t = u;

3) E `

∀

t = u.

Dow´

od:

(1) ⇒ (2): Poniewa˙z T

∈ Mod(E) na mocy Lematu 5.6, wi

ec T

|= t = u.

(2) ⇒ (3): Niech v(x) = [x]

. Poniewa˙z T

|= t = u, wi

ec w szczeg´

olno´sci v(t) = v(u).

Korzystaj

ac z Lematu 5.5, otrzymujemy, ˙ze [t]

= v(t) = v(u) = [u]

. A wi

ec t ∼

czyli E `

∀

t = u.

(3) ⇒ (1): Twierdzenie 5.3 o poprawno´sci.

Przepisywanie term´

Zbi´

or aksjomat´

ow r´

owno´sciowych E, czytany z lewej do prawej, mo˙zna uwa˙za´

c za zbi´

regu l przekszta lcania term´

ow. ´

Sci´slej, zbi´

or E okre´sla pewn

a relacj

e →

w zbiorze term´

ow.

Definicja 5.9 Relacja →

to najmniejsza relacja w zbiorze term´

ow spe lniaj

aca nast

epu-

ace warunki:

1) Je´sli

”

` = r” jest w E to ` →

2) Je´sli t →

to S(t) →

S(t

) (tj. relacja →

jest zamkni

eta ze wzgl

edu na pod-

stawienia);

3) Je´sli t

→

0
i

, dla pewnego i ≤ n, to f (t

, . . . , t

) →

f (t

, . . . , t

i−1

, t

0
i

, t

i+1

, . . . , t

)

(tj. relacja →

jest zamkni

eta ze wzgl

edu na konteksty).

Relacja →

jest to relacja jednokrokowego przepisywania wyznaczona przez regu ly z E.

Nietrudno zauwa˙zy´

c, ˙ze t →

u zachodzi wtedy i tylko wtedy, gdy dla pewnego r´

ownania

”

` = r” ze zbioru E i dla pewnego podstawienia S:

• term t zawiera podterm postaci S(`), oraz

• term u powstaje z t przez wymian

e tego podtermu na term S(r).

Na przyk lad, je´sli do E nale˙zy r´

ownanie (K · x) · y = x, a term (K · ((K · x) · y)) · z oznaczymy

przez t, to mo˙zemy napisa´

c zar´

owno t →

(K · x) · y jak te˙z t →

(K · x) · z.

Definicja 5.10 Przez

oznaczamy najmniejsz

a relacj

e zwrotn

a i przechodni

a zawiera-

a →

(domkni

ecie przechodnie sumy relacji →

i relacji identyczno´sciowej). Symbol

←

↔

→

oznacza najmniejsz

a relacj

e r´

ownowa˙zno´sci zawieraj

a →

Lemat 5.11 Warunek t ←

↔

→

u zachodzi wtedy i tylko wtedy, gdy istnieje sko´

nczony ci

term´

ow t = t

, t

, . . . , t

= u, o tej w lasnosci, ˙ze dla ka˙zdego i ≤ n − 1, albo t

→

i+1

albo

i+1

→

Dow´

od:

Cwiczenie.

Uwaga*: M´

owimy, ˙ze relacja →

ma w lasno´

s´

c Churcha-Rossera, gdy t ←

↔

→

u implikuje t

dla pewnego u. Nie ka˙zdy system przepisywania term´

ow ma t

e w lasno´

s´

c. Na przyk lad taki: f (x) ⇒ c,

f (x) ⇒ d, gdzie c i d to dwie r´

o˙zne sta le. A oto mniej oczywisty przyk lad (tutaj ar (D) = 2, ar (C) = 1

i ar (a) = ar (e) = 0).

• D(x, x) ⇒ e;

• C(x) ⇒ D(x, C(x));

• a ⇒ C(a).

Wtedy C(a) →

D(a, C(a)) →

D(C(a), C(a)) →

e, ale tak˙ze C(a) →

C(C(a)) →

C(D(a, C(a))) →

C(D(C(a), C(a))) →

C(e) →

D(e, C(e)) →

D(e, D(e, C(e))) →

· · ·

Twierdzenie 5.12 Relacje ∼

i ←

↔

→

a identyczne.

Dow´

od:

Zauwa˙zmy, ˙ze relacja ∼

spe lnia warunki, o kt´

orych mowa w Definicji 5.9,

a wi

ec →

⊆ ∼

, bo →

jest najmniejsz

a relacj

a o tych w lasno´sciach. Ponadto ∼

jest

relacj

a r´

ownowa˙zno´sci, a najmniejsz

a relacj

a r´

ownowa˙zno´sci zawieraj

a →

jest ←

↔

→

ad relacja ←

↔

→

zawiera si

e w relacji ∼

Aby udowodni´

c inkluzj

e w przeciwn

a stron

e, na mocy Faktu 5.4, wystarczy pokaza´

c, ˙ze

relacja ←

↔

→

jest kongruencj

a w T

, zamkni

a ze wzgl

edu na podstawienia. To znaczy, ˙ze

wystarczy udowodni´

c nast

epuj

ace implikacje:

a) Je˙zeli t ←

↔

→

u to S(t) ←

↔

→

S(u).

b) Je˙zeli t

←

↔

→

0
i

, dla i = 1, . . . , n, to f (t

, . . . , t

) ←

↔

→

f (t

0
1

, . . . , t

0
n

Dla dowodu warunku (a) u˙zyjemy Lematu 5.11. Niech t = t

, t

, . . . , t

= u, gdzie dla

ka˙zdego i = 0, . . . , n − 1, albo t

→

i+1

albo t

i+1

→

Wtedy oczywi´scie tak˙ze

S(t

) →

S(t

i+1

) albo S(t

i+1

) →

S(t

), i w ten spos´

ob dostajemy S(t) ←

↔

→

S(u).

Aby pokaza´

c warunek (b), za l´

o˙zmy, ˙ze dla dowolnego i = 1, . . . , n istnieje taki ci

= t

0
i

, t

1
i

, t

2
i

, . . . , t

= t

0
i

, w kt´

orym t

j
i

→

j+1
i

lub t

j+1
i

→

j
i

zachodzi dla wszystkich

j = 0, . . . , k

− 1. Wtedy mo˙zemy skonstruowa´c ci

ag sko´

nczony

f (t

, . . . , t

) = f (t

0
1

, t

, . . . , t

), f (t

1
1

, t

, . . . , t

), . . .

. . . f (t

, t

, . . . , t

) = f (t

0
1

, t

0
2

, t

, . . . , t

), f (t

0
1

, t

1
2

, t

, . . . , t

), . . .

. . . f (t

0
1

, . . . , t

0
n−1

, t

) = f (t

0
1

, . . . , t

0
n

w kt´

orym kolejne wyrazy pozostaj

a w relacji →

lub relacji odwrotnej.

Bezpo´srednio z Twierdzenia 5.12 i twierdzenia Birkhoffa o pe lno´sci otrzymujemy:

Wniosek 5.13 Nast

epuj

ace warunki s

a r´

ownowa˙zne:

1) E |=

∀

t = u;

2) T

|= t = u;

3) E `

∀

t = u;

4) t ←

↔

→

Mora l 5.14 Je´sli w ka˙zdej algebrze z klasy Mod(E) prawdziwe jest r´

ownanie

”

t = u”, to

mo˙zna faktycznie przepisa´

c term t w term u, u˙zywaj

ac r´

owna´

n ze zbioru E jako (obustron-

nych) regu l przepisywania.

Algebry wolne

Definicja 5.15 Klasa algebr K jest trywialna wtedy i tylko wtedy, gdy wszystkie algebry
z tej klasy s

a jednoelementowe. W przeciwnym razie klasa K jest nietrywialna.

Poniewa˙z algebry jednoelementowe to dok ladnie te algebry, w kt´

orych prawdziwe jest r´

ow-

nanie

”

= x

”, wi

ec mamy nastepuj

acy oczywisty fakt:

Fakt 5.16 Klasa K jest trywialna wtedy i tylko wtedy, gdy K |= x

= x

Od tej pory zak ladamy, ˙ze klasy, o kt´

orych mowa, s

a nietrywialne.

Definicja 5.17 Algebra A ∈ K jest algebr

a woln

a w klasie K, o zbiorze wolnych genera-

tor´

ow X wtedy i tylko wtedy, gdy zbi´

or X ⊆ |A| generuje algebr

e A, oraz dla dowolnej

algebry B ∈ K, ka˙zde przekszta lcenie ζ : X → |B| rozszerza si

e (jednoznacznie) do homo-

morfizmu ζ : A → B.

Algebr

e woln

a w klasie K o pustym zbiorze wolnych generator´

ow nazywamy algebr

a po-

atkow

a w K.

Uwaga: S lowo

”

jednoznacznie” w Definicji 5.17 mo˙zna pomin

a´

c, bo na mocy Lematu 1.18

funkcj

e okre´slon

a na generatorach mo˙zna rozszerzy´

c do homomorfizmu co najwy˙zej na

jeden spos´

ob.

Zauwa˙zmy te˙z, ˙ze je´sli A jest pocz

atkowa w K, to dla dowolnej algebry B ∈ K istnieje

dok ladnie jeden homomorfizm z A do B.

Przyk lad 5.18

• Algebra s l´

ow h{a, b}

∗

, ·, εi jest algebr

a woln

a w klasie wszystkich p´

o lgrup (p´

o lgrup

woln

a), o dw´

och wolnych generatorach a i b.

• Algebra hN, ·, 1i nie jest p´o lgrup

a woln

a, jakkolwiek by nie wybiera´

c zbioru gene-

rator´

ow X. Je´sli bowiem n, m ∈ X oraz przyjmiemy ζ(m) = aa i ζ(n) = bb, to

poszukiwany przez nas homomorfizm ζ z N do {a, b}

∗

musia lby spe lnia´

c warunek

aabb = ζ(m · n) = ζ(n · m) = bbaa. Pozostaje wi

ec tylko taka mo˙zliwo´s´

c, ˙ze X

jest jednoelementowy. Ale oczywi´scie nasza algebra nie jest generowana przez ˙zaden
pojedynczy element.

• Algebra hN, s, 0i, gdzie s jest funkcj

a nast

epnika (s(n) = n + 1), jest algebr

a pocz

at-

kow

a w klasie wszystkich algebr swojej sygnatury.

• Algebra term´

ow T

jest wolna w klasie wszystkich algebr, a zbiorem generator´

ow jest

zbi´

or wszystkich zmiennych.

Fakt 5.19 Algebry wolne w tej samej klasie, o zbiorach wolnych generator´

ow tej samej

mocy, s

a izomorficzne.

Dow´

od:

Niech X i Y b

a zbiorami wolnych generator´

ow algebr wolnych A i B, i niech

ζ : X

1−1

−→

Y . Wtedy ζ rozszerza si

e do homomorfizmu ζ : A → B. Ale przekszta lcenie

odwrotne ζ

−1

te˙z rozszerza si

e do homomorfizmu ζ

−1

: B → A. Z lo˙zenia ζ ◦ ζ

−1

: B → B

oraz ζ

−1

◦ ζ : A → A pokrywaj

a si

e z przekszta lceniami identyczno´sciowymi na zbiorach

generator´

ow, zatem na mocy Lematu 1.18 s

a po prostu wzajemnie odwrotne. Oznacza to,

˙ze s

a izomorfizmami.

Fakt 5.20 Za l´

o˙zmy, ˙ze A jest algebr

a woln

a w klasie K o co najmniej k wolnych genera-

torach. Je´

sli A |= t = s i w r´

ownaniu

”

t = s” wyst

epuje tylko k zmiennych, to K |= t = s.

Dow´

od:

Przyjmijmy, ˙ze w r´

ownaniu

”

t = s” wyst

epuj

a tylko zmienne x

, . . . , x

. Niech

B ∈ K i niech v b

edzie warto´sciowaniem w B. Homomorfizm v mo˙zna przedstawi´

c jako

z lo˙zenie v = h ◦ w gdzie w(x

), . . . , w(x

) s

a wolnymi generatorami algebry A, a h jest

homomorfizmem rozszerzaj

acym przyporz

adkowanie w(x

) 7→ v(x

), dla i = 1, . . . , k. Skoro

w(t) = w(s), to tak˙ze v(t) = v(s). A wi

ec B, v |= t = s, dla dowolnego v.

Fakt 5.21 Algebra T

jest algebr

a woln

a w klasie Mod(E), o zbiorze wolnych genera-

tor´

ow mocy ℵ

. (A zatem jest te˙z algebr

a woln

a w ka˙zdej podklasie K ⊆ Mod(E), do kt´

orej

sama nale˙zy. Na przyk lad, gdy E = Eq(K).)

Dow´

od:

Latwo zgadn

a´

c, ˙ze zbi´

or X = {[x]

| x ∈ V } powinien by´c zbiorem wolnych

generator´

ow. Aby to sprawdzi´

c, przypu´s´

cmy, ˙ze ζ : X → |B| dla pewnego B ∈ Mod(E).

Niech v b

edzie warto´sciowaniem w algebrze B zadanym przez warunek v(x) = ζ([x]

Homomorfizm ζ definiujemy tak:

ζ([t]

) = v(t).

Definicja jest poprawna, bo dla t ∼

zachodzi B |= t = t

ec v(t) = v(t

). Nietrudno

za´s sprawdzi´

c, ˙ze ζ jest homomorfizmem.

Oczywi´scie zbi´

or generator´

ow algebry T

jest mocy ℵ

tylko dlatego, ˙ze przyj

eli´smy

za lo˙zenie o przeliczalno´sci zbioru zmiennych. Mo˙zna si

e jednak um´

owi´

c inaczej.

Fakt 5.22 Je´

sli zbi´

or zmiennych V jest mocy m, oraz T

∈ K ⊆ Mod(E), to T

jest algebr

a woln

a w klasie K, maj

a m wolnych generator´

ow. Podobnie, algebra T

(n)/

term´

ow n-argumentowych jest algebr

a woln

a o n wolnych generatorach.

Dow´

od:

Identyczny z dowodem Faktu 5.21

Twierdzenie Birkhoffa

Zacznijmy od nastepuj

acej prostej obserwacji:

Fakt 5.23 Je´

sli klasa K jest definiowalna r´

owno´

sciowo, to jest zamkni

eta ze wzgl

edu na pod-

algebry, obrazy homomorficzne i produkty, tj. zachodz

a inkluzje H(K) ⊆ K, S(K) ⊆ K oraz

P (K) ⊆ K.

Dow´

od:

Cwiczenie.

Znacznie mniej oczywiste jest to, ˙ze zachodzi tak˙ze twierdzenie odwrotne do Faktu 5.23.
Zamkni

eto´s´

c ze wzgl

edu na wymienione operacje jest warunkiem wystarczaj

acym na to,

aby dana klasa by la rozmaito´sci

a. Z Lematu 3.2 wynika, ˙ze w istocie chodzi tu o r´

owno´s´

HSP (K) = K. Otrzymujemy w ten spos´

ob czysto semantyczn

a charakteryzacj

e klas defi-

niowalnych r´

owno´sciowo, zwan

a twierdzeniem Birkhoffa.

Twierdzenie 5.24 (Twierdzenie Birkhoffa) Nast

epuj

ace warunki s

a r´

ownowa˙zne:

1) Klasa K jest definiowalna r´

owno´

sciowo;

2) Klasa K jest zamkni

eta ze wzgl

edu na podalgebry, obrazy homomorficzne i produkty;

3) HSP (K) = K.

Implikacja (1) ⇒ (2) stanowi tre´s´

c Faktu 5.23, a r´

ownowa˙zno´s´

c warunk´

ow (2) i (3) jest

latwym wnioskiem z Lematu 3.2. Pozostaje przed nami dow´

od najtrudniejszej implikacji

(2) ⇒ (1).

Lemat 5.25 Za l´

o˙zmy, ˙ze K jest nietrywialn

a klas

a spe lniaj

a warunek HSP (K) = K.

Wtedy klasa K ma algebry wolne o dowolnej niezerowej (sko´

nczonej lub niesko´

nczonej)

liczbie wolnych generator´

Dow´

od:

Poka˙zemy jak skonstruowa´

c algebr

e woln

a o zbiorze wolnych generator´

mocy ℵ

. Dla m 6= ℵ

dow´

od wymaga rozwa˙zania term´

ow nad zbiorem zmiennych mocy m,

ale przebiega w podobny spos´

ob.

Niech E = Eq(K). Rozpatrzmy nast

epuj

acy zbi´

or relacji:

Z = {ρ | ρ jest kongruencj

a w T

oraz T

∈ K}.

Na pocz

atek zauwa˙zmy, ˙ze Z 6= ∅. W tym celu we´

zmy dowolne wartosciowanie v w jakiej´s

algebrze A ∈ K. Jest to oczywi´scie homomorfizm, a jego zbi´

or warto´sci jest podalge-

a w A, izomorficzn

a z algebr

a ilorazow

a T

ker(v)

(Twierdzenie 1.27). Poniewa˙z klasa K

jest zamkni

eta ze wzgl

edu na podalgebry, wi

ec iloraz T

ker(v)

nale˙zy do K a j

adro ker(v)

jest elementem zbioru Z.

Skoro wi

ec rodzina Z jest niepusta, to jej iloczyn jest kongruencj

a w algebrze term´

ow.

Oznaczmy ten iloczyn przez ≈.

Niech teraz B =

ρ∈Z

. Algebra B nale˙zy do klasy K, bo K jest zamkni

eta ze wzgl

edu

na produkty. Zdefiniujemy przekszta lcenie h : T

≈

→ B warunkiem

h([t]

≈

)(ρ) = [t]

dla dowolnego ρ ∈ Z. To przekszta lcenie jest monomorfizmem (r´

o˙znowarto´sciowym homo-

morfizmem). W rzeczy samej, je´sli klasy [t]

≈

i [t

]

≈

a r´

o˙zne, to ht, t

i 6∈ ρ przynajmniej dla

jednej relacji ρ ∈ Z. Jako ´

cwiczenie pozostawiamy sprawdzenie, ˙ze h jest dobrze okre´slone

i ˙ze zachowuje operacje.

A zatem algebra ilorazowa T

≈

jest izomorficzna z pewn

a podalgebr

a algebry B i sama

te˙z nale˙zy do K. Inaczej m´

owi

ac, relacja ≈ jest (najmniejszym) elementem rodziny Z.

Relacja ≈ jest w istocie identyczna z relacj

a ∼

. Poka˙zemy najpierw inkluzj

e ∼

⊆ ≈.

Niech t ∼

u czyli E`

∀

t = u. St

ad K |= t = u, bo K |= E. Je´sli wi

ec ρ ∈ Z to tak˙ze

|= t = u, w szczeg´

olno´sci T

, κ |= t = u, gdzie κ jest warto´sciowaniem kanonicznym:

κ(s) = [s]

dla s ∈ T

. Ale to oznacza, ˙ze [t]

= [u]

czyli t ρ u. Tak jest dla wszystkich

ρ ∈ Z, a wi

ec t ≈ u.

Przypu´s´

cmy teraz, ˙ze t ≈ u. Dla wykazania, ˙ze t ∼

u wystarczy wiedzie´

c, ˙ze K |= t = u,

bo wtedy

”

t = u” ∈ E. Ale je´sli v jest warto´sciowaniem w jakiej´s algebrze B ∈ K, to

ker(v) ∈ Z, wi

ec skoro t ≈ u to te˙z (t, u) ∈ ker(v) czyli B, v |= t = u.

Konkluzja jest taka: Poniewa˙z ≈ to to samo co ∼

, wi

ec T

= T

≈

∈ K. Na mocy

Faktu 5.21 mamy poszukiwan

a algebr

e woln

Dow´

od twierdzenia Birkhoffa: Niech E = Eq(K). Poka˙zemy, ˙ze K = Mod(E). Inkluzja

z lewej do prawej jest oczywista. Niech wi

ec B ∈ Mod(E) b

edzie algebr

a o mocy m.

W klasie K istnieje algebra wolna A, o zbiorze wolnych generator´

ow G mocy m. Dowolna

bijekcja h : G

1−1

−→

|B| rozszerza si

e do homomorfizmu, kt´

ory jest oczywi´scie na |B|. A wi

nasza algebra jest obrazem homomorficznym algebry A. Klasa K jest zamkni

eta ze wzgl

edu

na obrazy homomorficzne, a st

ad B ∈ K.

Unifikacja

Definicja 6.1 Przez uk lad r´

owna´

n rozumiemy sko´

nczony ci

ag r´

owna´

Rozwi

azaniem r´

ownania

”

t = u” nazywamy dowolne podstawienie S, spe lniaj

ace warunek

S(t) = S(u). M´

owimy wtedy te˙z, ˙ze podstawienie S jest unifikatorem term´

ow t i s, lub ˙ze

je unifikuje. Rozwi

azanie uk ladu r´

owna´

n to takie podstawienie, kt´

ore jest rozwi

azaniem

wszystkich r´

owna´

n tego uk ladu.

Przyk lad 6.2 Za l´

o˙zmy, ˙ze ar (f ) = ar (g) = 2 oraz ar (c) = ar (d) = 0.

• Rozwi

azaniem r´

ownania f (g(x, y), x) = f (z, g(y, c)) jest na przyk lad podstawienie

S(x) = g(y, c), S(y) = y, S(z) = g(g(y, c), y).

• R´

ownanie f (g(y, c), y) = f (x, g(x, d)) nie ma rozwi

azania. Istotnie, gdyby S by lo

takim rozwi

azaniem, oraz S(x) = t, to term t musia lby by´

c postaci g(g(t, d), c), czyli

by lby d lu˙zszy sam od siebie.

• R´

ownanie f (x, f (y, c)) = f (g(y, c), x) te˙z nie ma rozwi

azania, ale z innego powodu.

Gdyby S by lo rozwi

azaniem, oraz S(y) = t, to termy g(t, c) i f (t, c) musia lyby by´

identyczne, a nie zgadzaj

a si

e ich symbole pocz

atkowe.

Zajmiemy si

e teraz algorytmicznym rozwi

azaniem problemu unifikacji , polegaj

acego na

ustaleniu, czy dany uk lad r´

owna´

n ma rozwi

azanie i jakie. Algorytm polega na upraszczaniu

danego uk ladu r´

owna´

n i jednoczesnym konstruowaniu rozwi

azania. W ka˙zdej fazie pracy

mamy wi

ec do czynienia z par

a postaci hE, Si, gdzie E jest uk ladem r´

owna´

n a S jest

podstawieniem. Rozpoczynamy od pary hE, idi, a naszym celem jest uzyskanie pary postaci
h∅, Si, gdzie S jest poszukiwanym rozwi

azaniem. Nasz algorytm polega na iterowaniu

operacji Θ, kt´

a zaraz zdefiniujemy.

Przyjmujemy tak

a notacj

e: Przez (t = u); E (odpowiednio: E; (t = u)) oznaczymy uk lad

powstaj

acy z E przez dodanie na pocz

atku (odpowiednio: na ko´

ncu) r´

ownania

”

t = u”.

Notacja E[x := t] oznacza uk lad powsta ly z E przez zastosowanie podstawienia [x := t] do
obu stron wszystkich r´

owna´

n. Podobnie uog´

olniamy inne oznaczenia, np. F V (E) oznacza

zbi´

or wszystkich zmiennych wyst

epuj

acych w uk ladzie E.

Definicja 6.3 Niech hE, Si b

edzie tak

a par

a, ˙ze E 6= ∅. Je´sli si

e uda, to okre´slimy now

par

e Θ(E, S) = hE

, S

i. Mamy kilka przypadk´

ow, w zale˙zno´sci od pierwszego r´

ownania

uk ladu E.

Przypadek 1: Uk lad E jest postaci (x = t); F , przy tym x 6∈ F V (t). W´

owczas E

F [x := t] oraz S

= [x := t] ◦ S, tj. S

(u) = S(u)[x := t] dla dowolnego termu u.

esto przyjmuje si

e, ˙ze uk lad r´

owna´

n to po prostu zbi´

or r´

owna´

n. Nam wygodniej przyj

a´

c, ˙ze r´

ownania

w uk ladzie s

a ponumerowane.

Przypadek 2: Uk lad E jest postaci (t = x); F , gdzie t nie jest zmienn

a i x 6∈ F V (t). Para

, S

i jest okre´slona tak samo jak w przypadku 1.

Przypadek 3: Uk lad E jest postaci (x = x); F . Wtedy E

= F oraz S

= S.

Przypadek 4: Uk lad E jest postaci (f (t

, . . . , t

) = f (u

, . . . , u

)); F , gdzie ar (f ) = k.

Wtedy E

= F ; (t

= u

); . . . ; (t

= u

) oraz S

= S.

Przypadek 5: Uk lad E jest postaci (x = t); F lub postaci (t = x); F , gdzie t nie jest
zmienn

a i x ∈ F V (t). Wtedy Θ(E, S) jest nieokre´slone.

Przypadek 6: Uk lad E jest postaci (f (t

, . . . , t

) = g(u

, . . . , u

)); F , gdzie f 6= g. Wtedy

Θ(E, S) te˙z jest nieokre´slone.

Latwo sprawdzi´

c, ˙ze przypadki 1–6 wyczerpuj

a wszystkie mo˙zliwo´sci, i ˙ze w przypadkach

5 i 6 pierwsze r´

ownanie (a zatem ca ly uk lad) nie ma rozwi

azania.

Twierdzenie 6.4 (Terminacja algorytmu) Dla dowolnych E i S istnieje takie n, ˙ze
Θ

(E, S) ma posta´

c h∅, P i lub jest nieokre´

slone.

Dow´

od:

Dla dowolnego E, przez #(E) oznaczymy par

e liczb hp, qi, gdzie:

• p to liczba zmiennych wyst

epuj

acych w E;

• q to suma d lugo´sci wszystkich term´

ow w E.

Przypu´s´

cmy, ˙ze Θ(E, S) = hE

, S

i i niech #(E) = hp, qi, oraz #(E

) = hp

, q

i. W przy-

padkach 1 i 2 mamy p

< p, a w przypadkach 3 i 4 zachodzi p

≤ p i q

< q. A wi

#(E

) ≺ #(E) w porz

adku leksykograficznym. Poniewa˙z jest to dobry porz

adek, wi

iteracja operacji Θ nie mo˙ze si

e ci

agn

a´

c w niesko´

nczono´s´

Trzeba jeszcze udowodni´

c, ˙ze nasz algorytm faktycznie robi to, czego od niego oczekujemy.

Ustalmy pewien uk lad E i przyjmijmy oznaczenie hE

, S

i = Θ

(E, id). W szczeg´

olno´sci

mamy E = E

i S = id. Na pocz

atek kilka latwych obserwacji.

Lemat 6.5

1. Je´

sli z ∈ F V (E

) to S

(z) = z.

2. Je´

sli z ∈ F V (S

(y)), to S

(z) = z. Zatem S

◦ S

= S

3. Je´

sli R jest rozwi

azaniem E

to jest te˙z rozwi

azaniem E

n+1

4. Je´

sli R jest takim podstawieniem, ˙ze R(x) = R(t), to R = R ◦ [x := t].

5. Je´

sli R jest rozwi

azaniem E

oraz R = R ◦ S

to R = R ◦ S

n+1

Dow´

od:

Dow´

od cz

e´sci (4) polega na prostym sprawdzeniu. Pozosta lych cz

e´sci dowodzi-

my przez latw

a indukcj

e ze wzgl

edu na n. Oczywi´scie mamy ka˙zdorazowo tyle przypadk´

ile ich jest w Definicji 6.3. Dla przyk ladu rozpatrzmy przypadek 1 w cz

e´sci (5). Wtedy

n+1

= [x := t] ◦ S

. Poniewa˙z R jest rozwi

azaniem E

ec R(x) = R(t). Z za lo˙zenia

indukcyjnego i cz

e´sci (4) mamy R = R ◦ S

= R ◦ [x := t] ◦ S

= R ◦ S

n+1

Twierdzenie 6.6 (Poprawno´

s´

c algorytmu)

1) Je´

sli Θ

(E, id) jest dla pewnego m nieokre´

slone, to uk lad E nie ma rozwi

azania.

2) Je´

sli Θ

(E, id) = h∅, Ri, to R jest rozwi

azaniem uk ladu E.

Dow´

od:

e´s´

c (1) wynika do´s´

c natychmiastowo z Lematu 6.5(3). Je´sli bowiem Θ

(E, id)

nie jest okre´slone, ale Θ

m−1

(E, id) = hE

m−1

, S

m−1

i jeszcze jest okre´slone, to znaczy, ˙ze

uk lad E

m−1

nie ma rozwi

azania. Ale z Lematu 6.5(3) wynika, ˙ze wtedy tak˙ze samo E nie

ma rozwi

azania. Zajmijmy si

e wi

ec cz

e´sci

a (2).

Przez indukcj

e ze wzgl

edu na r´

o˙znic

e m − n poka˙zemy, ˙ze dla n = 0, . . . , m:

• R jest rozwi

azaniem uk ladu E

;

• R = R ◦ S

Teza twierdzenia wynika z przypadku n = 0.

Oczywi´scie R jest rozwi

azaniem uk ladu pustego i na dodatek R = S

= S

◦ S

, na mocy

Lematu 6.5(2). St

ad wynika teza w przypadku pocz

atkowym, gdy n = m.

Przypu´s´

cmy, ˙ze R jest rozwi

azaniem E

n+1

, i ˙ze R = R ◦ S

n+1

Przypadek 1: Uk lad E

jest postaci (x = t); F , gdzie x 6∈ F V (t). Wtedy E

n+1

= F [x := t]

oraz S

n+1

= [x := t] ◦ S

Sprawdzamy, czy R(x) = R(t). Ot´

o˙z R(x) = R ◦ S

n+1

(x) = R ◦ [x := t] ◦ S

(x) = R(t), bo

x ∈ F V (E

) i na mocy Lematu 6.5(1) zachodzi S

(x) = x.

Sprawdzamy, czy R jest rozwi

azaniem uk ladu F . We´

zmy dowolne r´

ownanie

”

u = s” z tego

uk ladu. Z za lo˙zenia indukcyjnego mamy R(u[x := t]) = R(s[x := t]). Poniewa˙z ju˙z wiemy,

˙ze R(x) = R(t), wi

ec z Lematu 2.11 wnioskujemy, ˙ze R(u) = R

R(t)
x

(u) = R(u[x := t])

i analogicznie R(s) = R

R(t)
x

(s) = R(s[x := t]). A zatem R(u) = R(s).

Pozostaje wykaza´

c, ˙ze R = R ◦ S

. Wiemy jednak, ˙ze R = R ◦ S

n+1

= R ◦ [x := t] ◦ S

Ponadto z Lematu 6.5(4) mamy R ◦ [x := t] = R, bo R(x) = R(t). A wi

ec R = R ◦ S

Przypadek 2: Analogiczny.

Przypadek 3 i 4: Oczywiste, bo uk lady E

i E

n+1

maj

a te same rozwi

azania a podsta-

wienia S

i S

n+1

a takie same.

Tre´s´

c powy˙zszego twierdzenia mo˙zna wzmocni´

c. Rozwi

azanie znajdowane przez nasz algo-

rytm jest tzw. rozwi

azaniem g l´

ownym: ka˙zde inne rozwi

azanie mo˙zna z niego otrzyma´

c na

drodze podstawienia.

Fakt 6.7 Niech Θ

(E, id) = h∅, Ri i niech R

edzie rozwi

azaniem uk ladu E. Wtedy

= Q ◦ R dla pewnego podstawienia Q.

Dow´

od:

W istocie jako Q mo˙zna wybra´

c samo R

. Nale˙zy zauwa˙zy´

c na pocz

atku, ˙ze

= R

◦ id, a nast

epnie zastosowa´

c Lemat 6.5(5).

ezyk logiki predykat´

S lowo

”

predykat” oznacza wyra˙zenie opisuj

ace pewn

a w lasno´s´

c rozwa˙zanych obiekt´

ow.

System logiczny, kt´

orym b

edziemy si

e zajmowa´

c, jest nazywany logik

a (lub rachunkiem)

predykat´

ow (pierwszego rz

edu), bo wyst

epuj

a w nim symbole relacyjne, interpretowane

jako w lasno´sci przedmiot´

ow. W odniesieniu do logiki predykat´

ow u˙zywamy te˙z okre´slenia

”

rachunek kwantyfikator´

ow”.

Od tej pory umawiamy si

e, ˙ze je´sli m´

owimy o sygnaturze Σ, to symbol r´

owno´sci

”

=” nie

nale˙zy do Σ. Symbol

”

=” nie jest zwyk lym symbolem relacyjnym, ale jest traktowany na

specjalnych prawach.

Definicja 7.1 Formu ly atomowe sygnatury Σ s

a nast

epuj

ace:

• symbol

”

⊥” (na oznaczenie fa lszu);

• napisy postaci

”

r(t

, . . . , t

)”, gdzie r ∈ Σ

R
n

oraz t

, . . . , t

∈ T

;

• napisy postaci

”

= t

”, gdzie t

, t

∈ T

W szczeg´

olno´sci do formu l atomowych zaliczamy zeroargumentowe symbole relacyjne. Nazy-

wamy je symbolami zdaniowymi (lub zmiennymi zdaniowymi ). Uwaga: symbol

”

⊥” nie jest

zmienn

a zdaniow

a, ale sta l

a logiczn

Definicja 7.2 Formu ly sygnatury Σ definiujemy jako elementy najmniejszego zbioru F

(ozn. te˙z F ) spe lniaj

acego warunki:

• formu ly atomowe nale˙z

a do F

;

• je´sli ϕ, ψ ∈ F

to tak˙ze (ϕ → ψ) ∈ F

;

• je´sli ϕ ∈ F

i x ∈ V (x jest zmienn

a indywiduow

a) to tak˙ze (∀xϕ) ∈ F

W powy˙zszej definicji, dla prostoty dalszych rozwa˙za´

n, ograniczyli´smy si

e do implikacji

i fa lszu oraz kwantyfikatora og´

olnego ∀. Ale oczywi´scie na og´

o l pos lugujemy si

e te˙z innymi

sp´

ojnikami i kwantyfikatorem szczeg´

o lowym ∃ (nazywanym te˙z kwantyfikatorem egzysten-

cjalnym). Mo˙zemy je jednak wyrazi´

c za pomoc

a pozosta lych operator´

ow i uwa˙za´

c za skr´

oty

notacyjne. Przyjmujemy wi

ec, ˙ze:

Napis

(¬ϕ)

oznacza

(ϕ → ⊥);

(¬⊥);

(ϕ ∨ ψ)

((¬ϕ) → ψ);

(ϕ ∧ ψ)

(¬(ϕ → (¬ψ)));

(ϕ ↔ ψ)

((ϕ → ψ) ∧ (ψ → ϕ));

(∃xϕ)

¬(∀x¬ϕ).

Konwencje notacyjne: Niepotrzebne nawiasy pomijamy, stosuj

ac przy tym nast

epuj

ace

priorytety:

1. Kwantyfikatory i negacja;

2. Koniunkcja i alternatywa;

3. Implikacja.

Zatem na przyk lad:

• Wyra˙zenie

”

¬ϕ ∨ ψ → ϑ” oznacza (((¬ϕ) ∨ ψ) → ϑ);

• Napis

”

ϕ ∨ ψ ∧ ϑ” jest niepoprawny;

• Napis

”

∀xP (x) → R(x)” nale˙zy rozumie´c jako ((∀xP (x)) → R(x)) (a nie jako

(∀x(P (x) → R(x)))).

Uwaga:* Je´

sli po kwantyfikatorze stoi kropka, to oznacza ona lewy nawias, kt´

orego zasi

eg rozciaga si

e do

oporu w prawo (tj. do nast

epnego prawego nawiasu, lub do ko´

nca formu ly). Na przyk lad

”

∀x.P (x) → Q(x)”

oznacza

”

∀x(P (x) → Q(x))”. My jednak nie b

edziemy stosowa´

c tej konwencji.

Definicja 7.3 Zbi´

or zmiennych wolnych formu ly ϕ, oznaczany przez F V (ϕ), jest okre´slony

przez indukcj

• F V (r(t

, . . . , t

)) = F V (t

) ∪ · · · ∪ F V (t

);

• F V (t

= t

) = F V (t

) ∪ F V (t

);

• F V (⊥) = ∅;

• F V (ϕ → ψ) = F V (ϕ) ∪ F V (ψ).

• F V (∀xϕ) = F V (ϕ) − {x}.

Latwo sprawdzi´

c, ˙ze:

F V (ϕ ∧ ψ) = F V (ϕ ∨ ψ) = F V (ϕ) ∪ F V (ψ),

oraz

F V (∃xϕ) = F V (ϕ) − {x}.

Definicja 7.4 M´

owimy, ˙ze formu la jest otwarta, je´sli nie wyst

epuj

a w niej kwantyfikatory.

Natomiast formu la zamkni

eta (albo zdanie) to taka formu la ϕ, kt´

ora nie ma zmiennych

wolnych (tj. F V (ϕ) = ∅). Uwaga: niekt´

ore formu ly s

a jednocze´snie zamkni

ete i otwarte!

Zmienn

a x, wyst

epuj

a w kontek´scie

”

∀xϕ” nazywamy zwi

azan

a. (Dotyczy to te˙z zmien-

nej x w kontek´scie

”

∃xϕ”.)

Uwaga: ta sama zmienna mo˙ze wyst

epowa´

c w formule kilkakrotnie, zar´

owno jako wolna

jak i zwi

azana (i to r´

o˙znymi kwantyfikatorami), jak np. zmienna x w formule

”

∀x∃yP (x, y) → (Q(x) ∨ ∃xR(x))”.

(1)

Poniewa˙z napis ∀x ϕ czytamy

”

dla ka˙zdego x zachodzi ϕ”, jest intuicyjnie do´s´

c oczywiste,

˙ze np. znaczenie formu l ∀x P (x, z) i ∀y P (y, z) powinno by´

c takie samo. Istotnie, zaraz

e oka˙ze, ˙ze tak jest, i dlatego wygodnie jest uto˙zsamia´

c ze sob

a formu ly, r´

o˙zni

ace si

e od

siebie tylko zmiennymi zwi

azanymi. Takie uto˙zsamienie nazywamy alfa-konwersj

a. Dla

porz

adku wprowadzimy to poj

ecie w spos´

ob bardziej ´scis ly.

Definicja 7.5 Je´sli w jest dowolnym napisem, to przez w(x o y) oznaczymy napis, kt´

ory

otrzymujemy z w przez wymian

e wszystkich wyst

apie´

n x na y i odwrotnie. Na przyk lad

(∀x P (x, y, z))(x o y) = ∀y P (y, x, z).

Definicja 7.6 Relacja alfa-konwersji to najmniejsza relacja r´

ownowa˙zno´sci =

w zbiorze

formu l, spe lniaj

aca warunki:

• ∀x ϕ =

∀y ϕ(x o y), gdy y 6∈ F V (ϕ);

• Je´sli ϕ

to ∀x ϕ

∀x ϕ

;

• Je´sli ϕ

oraz ψ

to ϕ

→ ψ

Formu ly r´

ownowa˙zne ze wzgl

edu na alfa-konwersj

e to w la´snie formu ly

”

r´

o˙zni

ace si

e tylko

zmiennymi zwi

azanymi”. Od tej pory przyjmujemy nast

epuj

a umow

Je´

sli ϕ =

ψ to formu ly ϕ i ψ uwa˙zamy za identyczne.

Znaczenie formu l

Znaczeniem formu ly jest warto´s´

c logiczna

”

prawda” (1) lub

”

fa lsz” (0). Formu lom syg-

natury Σ mo˙zemy przypisywa´

c znaczenia w dowolnej strukturze tej sygnatury, zale˙znie od

wybranego warto´sciowania term´

ow. Przypomnijmy, ˙ze ka˙zde warto´sciowanie v : T

→ A

jest jednoznacznie wyznaczone przez swoje obci

ecie v|

: V → A. Dlatego zwykle m´

owimy

o warto´

sciowaniu zmiennych indywiduowych i uto˙zsamiamy v z v|

Je´sli v jest takim warto´sciowaniem w strukturze A, oraz a ∈ |A|, to przez v

oznaczamy

warto´sciowanie okre´slone tak:

(y) =

gdy y = x;

v(y), w przeciwnym przypadku.

Definicja 8.1 Warto´

s´

c formu ly ϕ w strukturze A przy warto´sciowaniu v oznaczamy przez

v(ϕ) i definiujemy przez indukcj

e (ze wzgl

edu na budow

e formu ly):

• v(⊥) = 0;

• v(r(t

, . . . , t

)) = 1, gdy hv(t

) . . . , v(t

)i ∈ r

;

• v(r(t

, . . . , t

)) = 0, w przeciwnym przypadku;

• v(t

= t

) = 1, gdy v(t

) = v(t

);

• v(t

= t

) = 0, w przeciwnym przypadku;

• v(ϕ → ψ) = 0, gdy v(ϕ) = 1 i v(ψ) = 0;

• v(ϕ → ψ) = 1, w przeciwnym przypadku.

• v(∀xϕ) = min{v

(ϕ) | a ∈ |A|}.

Zamiast v(ϕ) piszemy czasem [[ϕ]]

, a je´sli chcemy podkre´sli´

c, ˙ze chodzi o warto´sciowanie

w strukturze A to piszemy [[ϕ]]

A
v

Latwo widzie´

c, ˙ze v(ϕ → ψ) = max{v(ψ), 1 − v(ϕ)}, oraz ˙ze dla pozosta lych sp´

ojnik´

ow:

v(ϕ ∨ ψ) = max{v(ϕ), v(ψ)};

v(ϕ ∧ ψ) = min{v(ϕ), v(ψ)};

v(¬ϕ) = 1 − v(ϕ).

Natomiast dla kwantyfikatora szczeg´

o lowego otrzymujemy wz´

or:

v(∃xϕ) = max{v

(ϕ) : a ∈ |A|}.

Lemat 8.2 Niech ϕ b

edzie dowoln

a formu l

a. Je´

sli u, v : V → |A| s

a takimi warto´

sciowa-

niami, ˙ze u|

F V (ϕ)

= v|

F V (ϕ)

, to u(ϕ) = v(ϕ).

Dow´

od:

Dow´

od przebiega przez indukcj

e ze wzgl

edu na d lugo´s´

c formu ly. Przypadek

ϕ = ⊥ jest oczywisty. Je´sli ϕ = r(t

, . . . , t

) to za lo˙zenie u|

F V (ϕ)

= v|

F V (ϕ)

oznacza

w szczeg´

olno´sci, ˙ze u|

F V (t

)

= v|

F V (t

)

dla wszystkich t

. Zatem na mocy Faktu 2.8 mamy

v(t

) = u(t

), a st

ad latwo wynika, ˙ze v(r(t

, . . . , t

)) = u(r(t

, . . . , t

)). W ten sam spos´

post

epujemy w przypadku gdy ϕ jest r´

ownaniem.

Je´sli ϕ = ψ

→ ψ

to z za lo˙zenia indukcyjnego dla ψ

i ψ

otrzymujemy

u(ϕ) = max{u(ψ

), 1 − u(ψ

)} = max{v(ψ

), 1 − v(ψ

)} = v(ϕ).

Pozostaje przypadek, gdy formu la ϕ jest postaci ∀xψ. Z r´

owno´sci u|

F V (ϕ)

= v|

F V (ϕ)

, wynika

wtedy, ˙ze u

a
x

F V (ψ)

= v

F V (ψ)

, bo F V (ψ) ⊆ F V (ϕ) ∪ {x}. Z za lo˙zenia indukcyjnego dla ψ

dostajemy wi

ec u

a
x

(ψ) = v

(ψ) dla dowolnego a. Zatem

u(ϕ) = u(∀xψ) = min{u

a
x

(ψ) : a ∈ |A|} = min{v

(ψ) : a ∈ |A|} = v(ϕ).

Mora l z powy˙zszego jest oczywi´scie taki: warto´s´

c formu ly zale˙zy tylko od warto´sci jej

zmiennych wolnych. Na przyk lad warto´s´

c formu ly (1) nie zale˙zy od warto´sci y. Dlatego

gdy wiemy, ˙ze F V (ϕ) ⊆ {x

, . . . , x

}, to czasami zamiast ϕ piszemy ϕ(x

, . . . , x

), dla

zaznaczenia, jakie zmienne s

a tu istotne.

Poniewa˙z um´

owili´smy si

e, ˙ze alfa-r´

ownowa˙zne formu ly uwa˙zamy za identyczne, powinni´smy

e jeszcze przekona´

c, ˙ze alfa-konwersja nie zmienia warto´sci formu ly.

Lemat 8.3 Je´

sli ϕ =

ψ to v(ϕ) = v(ψ) przy dowolnym warto´

sciowaniu v.

Dow´

od: * Pozostawiaj

ac szczeg´

o ly najbardziej dociekliwym czytelnikom, zauwa˙zmy tylko, ˙ze wygodnie

jest pokaza´

c najpierw tak

a w lasno´

s´

c transpozycji zmiennych:

Je´

sli v

(x) = v

(y), v

(y) = v

(x) oraz v

(z) = v

(z) dla z 6= x, y, to v

(ϕ) = v

(ϕ(x o y)).

Dowodzimy tej w lasno´

sci przez indukcj

e ze wzgl

edu na d lugo´

s´

c formu ly ϕ.

Wynika z niej latwo, ˙ze

v(∀x ϕ) = v(∀y ϕ(x o y)) dla y 6∈ F V (ϕ).

Dalej post

epujemy przez indukcj

e ze wzgl

edu na definicj

relacji ϕ =

ψ.

Definicja 8.4 M´

owimy, ˙ze formu la ϕ jest spe lniona w A przez warto´sciowanie v, gdy

v(ϕ) = 1. Piszemy wtedy

A, v |= ϕ.

Je´sli F V (ϕ) ⊆ {x

, . . . , x

}, oraz v(x

) = a

, . . . , v(x

) = a

i ϕ jest spe lniona w A przez v

(czyli ϕ

, . . . , a

) = 1), to zamiast A, v |= ϕ piszemy te˙z

A, {a

, . . . , a

} |= ϕ, lub po prostu A, a

, . . . , a

|= ϕ,

gdy kolejno´s´

c argument´

ow jest oczywista. Podobnie, zamiast [[ϕ]]

mo˙zna wtedy napisa´

[[ϕ]]{a

, . . . , a

}. W szczeg´

olno´sci gdy formu la jest zamkni

eta, zamiast [[ϕ]]

piszemy

po prostu [[ϕ]].

Uwaga: Zamiast A, {a

, . . . , a

} |= ϕ czasem nieformalnie piszemy

A |= ϕ(a

, . . . , a

ale ten zapis w zasadzie nie jest poprawny. Pami

etajmy, ˙ze a

, . . . , a

a elementami modelu

(a nie cz

e´sci

a sk ladni), wi

”

ϕ(a

, . . . , a

)” nie oznacza ˙zadnej formu ly.

Definicja 8.5 Formu la jest spe lnialna (spe lnialna w A) je´sli jest spe lniona w pewnym
modelu (w modelu A) przez pewne warto´sciowanie. Zbi´

or formu l jest spe lnialny (w A)

je´sli wszystkie formu ly z tego zbioru s

a spe lnione przez to samo warto´sciowanie w pewnym

modelu (w modelu A).

Formu la ϕ jest prawdziwa w A (piszemy A |= ϕ), je˙zeli jest spe lniona w A przez wszystkie
warto´sciowania. Formu la ϕ jest prawdziwa (jest tautologi

a) je˙zeli jest prawdziwa w ka˙zdym

modelu A. Wtedy piszemy po prostu |= ϕ.

Przyk lad 8.6

• Formu la ∀x(y ≤ x) jest spe lniona w hN, ≤i dla v(y) = 0, ale nie jest spe lnialna

w modelu hR, ≤i.

• Formu la ∃x(¬r(x) ∧ r(x)) nie jest spe lnialna.

• Formu la ∃x(y ≤ x) jest prawdziwa w hR, ≤i.

• Formu la p(x) ∧ ∃y¬p(y) jest spe lnialna, ale nie jest w ˙zadnej strukturze prawdziwa.

Definicja 8.7 Niech Γ b

edzie zbiorem formu l. W´

owczas:

Piszemy

A, v |= Γ,

je˙zeli

A, v |= ϕ, dla dowolnego ϕ ∈ Γ;

”

A |= Γ,

”

A, v |= Γ, dla dowolnego v;

”

|= Γ,

”

A |= Γ, dla dowolnego A;

”

Γ |= ψ,

”

A, v |= ψ, dla dowolnych A, v, takich ˙ze A, v |= Γ;

”

Γ |=

∀

ψ,

”

A |= ψ, dla dowolnego A, takiego ˙ze A |= Γ.

Uwaga: Niech Γ

∀

= {∀γ | γ ∈ Γ}, gdzie ∀γ oznacza formu l

e otrzyman

a z γ przez

dopisanie z przodu tylu kwantyfikator´

ow og´

olnych, aby wszystkie zmienne w γ zosta ly

zwi

azane. Wtedy Γ |=

∀

ψ wtedy i tylko wtedy, gdy Γ

∀

|= ψ. W szczeg´

olno´sci stwierdzenia

Γ |=

∀

ψ i Γ |= ψ s

a r´

ownowa˙zne, gdy Γ jest zbiorem zda´

Operacja podstawienia

Przez t[x := s] oznaczali´smy term powsta ly z termu t przez podstawienie termu s w miejsce
wszystkich wyst

apie´

n zmiennej x.

W podobny spos´

ob mo˙zna latwo zdefiniowa´

c podstawienie termu w miejsce zmiennej do

formu ly otwartej. Podstawianie termu w miejsce zmiennej w formule z kwantyfikatorami
wymaga jednak pewnej ostro˙zno´sci. Po pierwsze, podstawienie powinno dotyczy´

c tylko

wolnych wyst

apie´

n zmiennych. Po drugie,

”

naiwne” podstawienie mo˙ze prowadzi´

c do u˙zy-

cia tej samej zmiennej w dw´

och znaczeniach.

Na przyk lad formu ly

”

∃y(y < x)” oraz

”

∃z(z < x)” s

a r´

ownowa˙zne. Tymczasem

”

naiwne” podstawienie y w miejsce x w obu

tych formu lach daje w wyniku odpowiednio

”

∃y(y < y)” i

”

∃z(z < y)”, a te dwie formu ly

znacz

a ca lkiem co innego. Przyczyn

a jest to, ˙ze w pierwszym przypadku zmienn

a y wsta-

wiono w zasi

eg kwantyfikatora ∃y. Jedno z mo˙zliwych rozwi

aza´

n tego problemu jest takie:

Przed dokonaniem podstawienia nale˙zy wymieni´

c zmienne zwi

azane, kt´

ore taki konflikt

mog lyby spowodowa´

c, na

”

nowe zmienne”. My przyjmiemy tym razem inne rozwi

azanie:

Podstawienie jest okre´slone tylko wtedy, gdy nie powoduje konfliktu nazw.

Definicja 8.8 Poni˙zsze warunki nale˙zy czyta´

c tak: Je´sli prawa strona jest okre´slona, to

lewa strona te˙z jest okre´slona.

• ⊥[x := s] = ⊥, gdy x 6∈ F V (ϕ);

• r(t

, . . . , t

)[x := s] = r(t

[x := s], . . . , t

[x := s]);

• (t

= t

)[x := s] =

”

[x := s] = t

[x := s]”;

• (ϕ → ψ)[x := s] = ϕ[x := s] → ψ[x := s];

• (∀x ϕ)[x := s] = ∀x ϕ;

• (∀y ϕ)[x := s] = ∀y ϕ[x := s], gdy y 6= x, oraz y 6∈ F V (s);

• W pozosta lych przypadkach podstawienie jest nieokre´slone.

Oczywi´scie istnieje zwi

azek mi

edzy podstawieniem i transpozycj

Lemat 8.9 Je´

sli y 6∈ F V (ϕ) i ϕ[x := y] jest okreslone, to ϕ[x := y] =

ϕ(x o y).

Mo˙zna teraz sprawdzi´

c (˙zmudny dow´

od opuszczamy), ˙ze podstawienie zachowuje alfa-

r´

ownowa˙zno´s´

Lemat 8.10 Je´

sli ϕ

to ϕ

[x := s] =

[x := s], o ile obie strony s

a okre´

slone.

Nast

epny lemat jest uog´

olnieniem Lematu 2.11 i wyra˙za semantyczny sens podstawienia:

warto´s´

c formu ly powstaj

acej przez podstawienie r´

owna jest warto´sci formu ly pocz

atkowej

przy warto´sciowaniu uwzgl

edniaj

acym warto´s´

c podstawianego termu.

Lemat 8.11

Je´

sli podstawienie ϕ[x := s] jest okre´

slone, to dla dowolnego warto´

sciowa-

nia v zachodzi r´

owno´

s´

c v(ϕ[x := s]) = v

v(s)

(ϕ).

Dow´

od:

Dla dowolnej formu ly atomowej r(t

, . . . , t

), warto´s´

c v(r(t

, . . . , t

)[x := s]) =

v(r(t

[x := s], . . . , t

[x := s]) jest r´

owna 1 wtedy i tylko wtedy, gdy wektor warto´sci

hv(t

[x := s]), . . . , v(t

[x := s])i nale˙zy do r

. Ale na mocy Lematu 2.11, dla dowol-

nego termu t zachodzi r´

owno´s´

c v(t[x := s]) = v

v(s)

(t). St

ad v(r(t

, . . . , t

)[x := s]) = 1

wtedy i tylko wtedy, gdy hv

v(s)

), . . . , v

v(s)

)i ∈ r

, czyli wtedy i tylko wtedy, gdy

v(s)

(r(t

, . . . , t

)) = 1. Przypadek r´

owno´sci jest podobny.

Dla ϕ = ψ → ϑ mamy takie r´

owno´sci: v(ϕ[x := s]) = v(ψ[x := s] → ϑ[x := s]) =

max{1 − v(ψ[x := s]), v(ϑ[x := s])} = max{1 − v

v(s)

(ψ), v

v(s)

(ϑ)} = v

v(s)

(ϕ).

Rozpatrzmy na koniec przypadek gdy ϕ rozpoczyna si

e od kwantyfikatora uniwersalnego.

Je´sli ϕ = ∀xψ, to v(ϕ[x := s]) = v(ϕ) = v

v(s)

(ϕ) z Lematu 8.2, bo v|

F V (ϕ)

= v

v(s)

F V (ϕ)

Je´sli ϕ = ∀yψ, gdzie x 6= y 6∈ F V (s) to korzystamy z za lo˙zenia indukcyjnego dla ψ i mamy:

v(ϕ[x:=s]) = v(∀yψ[x:=s]) = min{v

(ψ[x:=s]) | a ∈ |A|} = min{(v

)

(s)

(ψ) | a ∈ |A|} =

min{(v

)

v(s)
x

(ψ) | a ∈ |A|} = min{(v

v(s)

)

a
y

(ψ) | a ∈ |A|} = v

v(s)

(∀yψ) = v

v(s)

(ϕ). (Korzys-

tali´smy z tego, ˙ze v

(s) = v(s), bo y 6∈ F V (s).)

Jak dot

ad, stwierdzenia dotycz

ace podstawie´

n musieli´smy opatrywa´

c zastrze˙zeniami

”

o ile

podstawienie jest okre´slone”. Ale skoro uto˙zsamiamy alfa-r´

ownowa˙zne formu ly, to mo˙zemy

zapomnie´

c o zastrze˙zeniach. Mamy bowiem taki fakt:

Lemat 8.12 Niech ϕ b

edzie dowoln

a formu l

a i niech s b

edzie dowolnym termem. Istnieje

formu la ϕ

, dla kt´

orej podstawienie ϕ

[x := s] jest okre´

slone i taka, ˙ze ϕ =

Dow´

od:

Dow´

od jest przez indukcj

e ze wzgl

edu na d lugo´s´

c formu ly. Jedyny nieoczywisty

przypadek ma miejsce dla ϕ = ∀yψ, gdzie x 6= y ∈ F V (s). Dobierzmy zmienn

a z tak,

aby z 6∈ F V (ψ) oraz z 6∈ F V (s). Z za lo˙zenia indukcyjnego istnieje taka formu la ψ

, ˙ze

ψ(y o z) oraz podstawienie ψ

[x := s] jest okre´slone. A wi

ec wystarczy przyj

a´

= ∀zψ

Odt

ad zak ladamy, ˙ze podstawienie jest zawsze okre´slone, bo w razie potrzeby mo˙zemy

wymieni´

c ka˙zd

a zmienn

a zwi

azan

a na

”

now

a”. A wi

ec, na przyk lad:

• (∃z(z < x) → ∃x(x < y))[x := f (y)] =

”

∃z(z < f (y)) → ∃x(x < y)”;

• (∃y(y < x))[x := y] =

”

∃z(z < y)”.

Uwaga: Warto zauwa˙zy´

c analogi

e pomi

edzy zmiennymi wolnymi i zwi

azanymi w for-

mu lach oraz identyfikatorami lokalnymi i nielokalnymi w blokach i procedurach. Doko-
nanie operacji podstawienia w formule odpowiada przy tej analogii wywo laniu procedury
z parametrem przekazanym przez nazw

Logika formalna i jezyk polski

Systemy logiki formalnej s

a, jak ju˙z m´

owili´smy, tylko pewnymi modelami, czy te˙z przy-

bli˙zeniami rzeczywistych sposob´

ow wyra˙zania r´

o˙znych stwierdze´

n i wnioskowania o ich

poprawno´sci. Poziom dok ladno´sci takich przybli˙ze´

n mo˙ze by´

c wi

ekszy lub mniejszy. Wi

ek-

szy tam, gdzie mamy do czynienia z dobrze okre´slon

a teori

a matematyczn

a, lub j

ezykiem

programowania. Mniejszy wtedy, gdy u˙zywamy logiki do weryfikacji poprawno´sci stwier-
dze´

n j

ezyka potocznego, chocby takiego jak podr

ecznikowy przyk lad:

”

Janek idzie do

szko ly.” Oczywi´scie przypisanie temu stwierdzeniu warto´sci logicznej jest zgo la niemo˙zliwe,
nie wiemy bowiem, kt´

ory Janek do jakiej idzie szko ly i czy mo˙ze ju˙z doszed l? Wi

ecej sensu

ma zastosowanie logiki predykat´

ow do analizy np. takiego rozumowania:

Ka˙zdy cyrulik sewilski goli tych wszystkich m

e˙zczyzn w Sewilli, kt´

orzy si

e sami nie gol

Ale nie goli ˙zadnego z tych, kt´

orzy gol

a si

e sami.

A zatem w Sewilli nie ma ani jednego cyrulika.

W tym przypadku aparat logiki formalnej mo˙ze by´

c pomocny. Latwiej zrozumie´

c o co

chodzi, t lumacz

ac nasz problem na j

ezyk logiki predykat´

ow, i przedstawiaj

ac go jako py-

tanie o poprawno´s´

c pewnego stwierdzenia postaci Γ |= ϕ. Mo˙zna wi

ec zapyta´

c, czy

∀x(C(x) ∧ S(x) → ∀y(G(x, y) ↔ S(y) ∧ ¬G(y, y))) |= ¬∃x(C(x) ∧ S(x))?

Stwierdziwszy poprawno´s´

c powy˙zszego stwierdzenia, wywnioskujemy, ˙ze w Sewilli cyrulika

nie ma. I b

edzie to wniosek. . . b l

edny, bo cyrulik by´

c mo˙ze jest kobiet

W powy˙zszym przyk ladzie po prostu ´

zle ustalono logiczn

a interpretacj

e naszego zadania,

zapominaj

ac o jednym z jego istotnych element´

ow. B l

ad ten mo˙zna latwo naprawi´

c, co jest

zalecane jako ´

cwiczenie. Ale nie zawsze j

ezyk logiki formalnej wyra˙za ´sci´sle to samo, co

potoczny j

ezyk polski, a nawet j

ezyk w kt´

orym pisane s

a prace matematyczne. Zar´

owno

sk ladnia jak i semantyka tych j

ezyk´

ow rz

adzi si

e zupe lnie innymi prawami, i o tym nale˙zy

pami

eta´

c t lumacz

ac jeden na drugi.

Implikacja materialna i zwi

azek przyczynowo-skutkowy

Implikacja, o kt´

orej m´

owimy w logice klasycznej to tzw. implikacja materialna. Warto´s´

logiczna, kt´

a przypisujemy wyra˙zeniu

”

α → β” zale˙zy wy l

acznie od warto´sci logicznych

przypisanych jego cz

e´sciom sk ladowym α i β. Nie zale˙zy natomiast zupe lnie od tre´sci

tych wyra˙ze´

n, czy te˙z jakichkolwiek innych zwi

azk´

ow pomi

edzy α i β. W szczeg´

olno´sci,

wypowiedzi α i β mog

a m´

owi´

c o zaj´sciu jakich´s zdarze´

n i wtedy warto´s´

c logiczna implikacji

”

α → β” nie ma nic wsp´

olnego z ich ewentualnym nast

epstwem w czasie, lub te˙z z tym, ˙ze

jedno z tych zdarze´

n spowodowa lo drugie. W j

ezyku polskim stwierdzenie

”

je´

sli α to β”

oczywi´scie sugeruje taki zwi

azek, np. w zdaniu:

Je´

sli zasilanie jest w l

aczone, to terminal dzia la.

Tymczasem implikacja materialna nie zachodzi, o czym dobrze wiedz

a u˙zytkownicy termi-

nali. Co wi

ecej, w istocie materialn

a prawd

a jest stwierdzenie odwrotne:

Je´

sli terminal dzia la to zasilanie jest w l

aczone.

Natomiast zdanie

Terminal dzia la, poniewa˙z zasilanie jest w l

aczone,

stwierdza nie tylko zwi

azek przyczynowo-skutkowy, ale te˙z faktyczne zaj´scie wymienionych

zdarze´

n i w og´

ole nie ma odpowiednika w logice klasycznej.

Inne sp´

ojniki w mniejszym stopniu gro˙z

a podobnymi nieporozumieniami. Ale na przyk lad

sp´

ojnik

”

i” w j

ezyku polskim mo˙ze te˙z sugerowa´

c nast

epstwo czasowe

zdarze´

”

Poszed l

i zrobi l.” A wyra˙zenie

”

A, chyba ˙ze B” ma inny odcie´

n znaczeniowy ni˙z proste

”

A lub B”.

Przy tej okazji zwr´

o´

cmy uwag

e na to, ˙ze s lowo

”

albo” bywa czasem rozumiane w znaczeniu

alternatywy wykluczaj

acej. My jednak umawiamy si

e, ˙ze rozumiemy je tak samo jak

”

lub”.

Konfuzje sk ladniowe

Przy t lumaczeniu z j

ezyka polskiego na j

ezyk logiki formalnej i na odwr´

ot mozna latwo

pope lni´

c b l

ad nawet wtedy gdy nie powstaj

a problemy semantyczne. Sk ladnia tych j

ezyk´

jest oparta na innych zasadach. Na przyk lad te dwa zdania maj

a bardzo podobn

a budow

Ka˙zdy kot ma w

asy.

Pewien kot ma w

asy.

Ale ich t lumaczenia na j

ezyk rachunku predykat´

ow nie s

a ju˙z takie podobne:

∀x(Kot (x) → MaW

asy(x));

∃x(Kot (x) ∧ MaW

asy(x)).

W j

ezykach programowania jest podobnie, ale to ju˙z inna historia.

Zadziwiaj

aco cz

estym b l

edem jest w la´snie mylenie koniunkcji z implikacj

a w zasi

egu dzia-

lania kwantyfikatora. A oto inny przyk lad: Zdania

”

Liczba n jest parzysta”;

”

Liczba n jest dwukrotno´

sci

a pewnej liczby”

oznaczaj

a to samo. Zaprzeczeniem pierwszego z nich jest oczywi´scie zdanie

”

Liczba n nie jest parzysta”,

ale zaprzeczeniem drugiego nie jest zdanie

”

Liczba n nie jest dwukrotno´

sci

a pewnej liczby”,

otrzymane przecie˙z przez analogiczn

a operacj

”

podstawienia”. To zdanie rozumiemy bo-

wiem jako ∃x(¬n = 2x), a nie jako ¬∃x(n = 2x), mimo ˙ze negacja

”

nie” poprzedza w nim

s lowo

”

pewnej ”.

Innym popularnym b l

edem jest mylenie koniunkcji z alternatyw

a w przes lance implikacji,

zw laszcza gdy wyst

epuje tam negacja. Mamy bowiem sk lonno´s´

c do powtarzania s lowa “nie”

w obu cz lonach za lo˙zenia i nie razi nas zdanie

”

Kto nie ma biletu lub nie jest pracownikiem teatru, ten nie wejdzie na przedstawienie”.

Ale od tekstu matematycznego oczekujemy wi

ecej ´scis lo´sci i w takim tek´scie zdanie:

”

Je´

sli x nie jest r´

owne 2 lub nie jest r´

owne 3, to x

− 5x + 6 nie jest zerem.”

powinno by´

c uwa˙zane za b l

edne. Wielu takich b l

ed´

ow unikniemy, gdy przypomnimy sobie,

˙ze w j

ezyku polskim istniej

a takie s lowa jak

”

ani” i

”

˙zaden”.

Logika zdaniowa

Czasami do opisu pewnych zjawisk matematycznych nie jest potrzebny ca ly aparat logiki
predykat´

ow. Wystarczy cz

esto logika zdaniowa (nazywana te˙z rachunkiem zda´

n). Jest

to takie uproszczenie logiki predykat´

ow, w kt´

orym ignoruje si

”

przedmioty”, a rozwa˙za

jedynie wyra˙zenia orzekaj

ace (zdania). Oczywi´scie, w tej sytuacji kwantyfikatory indy-

widuowe staj

a si

e niepotrzebne, a rol

a logiki staje si

e badanie w jaki spos´

ob znaczenie

wyra˙ze´

n prostych wp lywa na znaczenie wyra˙ze´

n z lo˙zonych.

Logik

e zdaniow

a mo˙zna uwa˙za´

c za fragment logiki pierwszego rz

edu.

Definicja 10.1 Zdania otwarte dowolnej sygnatury Σ, sk ladaj

acej si

e wy l

acznie z symboli

zdaniowych, nazywamy formu lami zdaniowymi. Poj

ecie formu ly zdaniowej mo˙zna wi

ec tak

zdefiniowa´

c przez indukcj

• Symbole zdaniowe i ⊥ s

a formu lami zdaniowymi;

• Je´sli α i β s

a formu lami zdaniowymi to (α → β) jest formu l

a zdaniow

W tej sytuacji poj

ecie spe lnialnej i prawdziwej formu ly zdaniowej jest oczywi´scie okre´slone

zgodnie z Definicj

a 8.5, odwo luj

a si

e do struktur algebraicznych. Ale skoro sygnatura

sk lada si

e tylko z zeroargumentowych symboli relacyjnych, a my nie u˙zywamy zmiennych,

to w strukturze A = hA, p

A
1

, . . . , p

A
n

i interesuje nas tylko to, kt´

ora z zeroargumentowych

jest pusta (r´

owna 0) a kt´

ora pe lna (r´

owna 1). Natomiast sam zbi´

or A jest ca lkiem niewa˙zny.

Definicja 10.2 Przez warto´

sciowanie zdaniowe rozumiemy dowoln

a funkcj

e ρ, kt´

ora sym-

bolom zdaniowym przypisuje warto´sci logiczne 0 lub 1. Warto´

s´

c formu ly zdaniowej przy

warto´sciowaniu ρ okre´slamy przez indukcj

• [[⊥]]

= 0;

• [[p]]

= ρ(p), gdy p jest symbolem zdaniowym;

• [[α → β]]

= max{[[β]]

, 1 − [[α]]

Zamiast [[α]]

zwykle piszemy po prostu ρ(α).

Je´sli ρ(α) = 1 to piszemy te˙z ρ |= α. Je´sli Γ jest zbiorem formu l zdaniowych, oraz ρ |= γ
dla wszystkich γ ∈ Γ, to piszemy ρ |= Γ.

Symbole zdaniowe s

a cz

esto nazywane zmiennymi zdaniowymi . Jest to jednak zupe lnie inny

rodzaj zmiennych, ni˙z zmienne indwiduowe, wyst

epuj

ace w formu lach rachunku predyka-

t´

ow. R´

ownie˙z warto´sciowanie zdaniowe to troch

e co innego ni˙z warto´sciowanie term´

ow.

Fakt 10.3

• Je´sli Γ jest zbiorem formu l zdaniowych, a α jest formu l

a zdaniow

a, to Γ |= α zachodzi

wtedy i tylko wtedy, gdy ρ |= α, dla dowolnego warto´

sciowania zdaniowego ρ, takiego

˙ze ρ |= Γ. W szczeg´

olno´

sci:

• Formu la zdaniowa jest spe lnialna wtedy i tylko wtedy, gdy ρ(α) = 1 dla pewnego

warto´

sciowania zdaniowego ρ.

• Formu la zdaniowa jest prawdziwa wtedy i tylko wtedy, gdy ρ(α) = 1 dla ka˙zdego

warto´

sciowania zdaniowego ρ.

Widzimy wi

ec, ˙ze nasza interpretacja formu l zdaniowych jest zgodna z t

a, kt´

a znamy ze

szko ly.

Ale mo˙ze nie ca lkiem? ´

Cwiczenie: czy formu ly zdaniowe mo˙zna uwa˙za´

c za termy jakiej´

s sygnatury?

Czy warto´

sciowanie zdaniowe staje sie wtedy warto´

sciowaniem term´

ow w pewnej algebrze?

Tautologie rachunku zda´

Niech S b

edzie funkcj

a przypisujac

a symbolom zdaniowym pewne formu ly. Je´sli α jest

formu l

a zdaniow

a, to przez S(α) oznaczymy formu l

e otrzyman

a z α przez zamian

e ka˙zdego

wyst

apienia zmiennej zdaniowej p na formu l

e S(p). M´

owimy, ˙ze formu la S(α) jest instancj

schematu zdaniowego α. U˙zywamy oznaczenia S(Γ) = {S(β) | β ∈ Γ}.

Fakt 10.4 Je˙zeli Γ jest zbiorem formu l rachunku zda´

n i Γ |= α, to tak˙ze S(Γ) |= S(α).

W szczeg´

olno´

sci, je´

sli α jest tautologi

a to S(α) jest te˙z tautologi

Dow´

od:

Cwiczenie.

Fakt 10.5 Nast

epuj

ace formu ly (i wszystkie ich instancje) s

a tautologiami rachunku zda´

1. ⊥ → p;

2. p → (q → p);

3. (p → (q → r)) → ((p → q) → (p → r));

4. ((p → q) → p) → p;

5. p ∨ ¬p;

6. p → ¬¬p

¬¬p → p;

7. (p → q) → (¬q → ¬p)

(¬q → ¬p) → (p → q);

8. p → (p ∨ q),

q → (p ∨ q)

oraz

(p → r) → ((q → r) → (p ∨ q → r));

9. (p ∧ q) → p,

(p ∧ q) → q

oraz

(r → p) → ((r → q) → (r → (p ∧ q)));

10. ((p ∧ q) → r) ↔ (p → (q → r));

11. ¬(p ∨ q) ↔ (¬p ∧ ¬q);

12. ¬(p ∧ q) ↔ (¬p ∨ ¬q);

13. (p → q) ↔ (¬p ∨ q);

14. ((p ↔ q) ↔ r) ↔ (p ↔ (q ↔ r)).

Dow´

od:

Latwy.

Niekt´

ore z powy˙zszych formu l wskazuj

a na analogi

e pomi

edzy implikacj

a i uporz

adkowa-

niem (np. zawieraniem zbior´

ow). Implikacj

”

p → q” mo˙zna odczyta´

c tak:

”

warunek p

jest silniejszy (mniejszy lub r´

owny) od q”. Formu l

e (1) czytamy wtedy:

”

fa lsz jest najsil-

niejszym warunkiem (najmniejszym elementem)”. Formu ly (8) stwierdzaj

a, ˙ze alternatywa

p ∨ q jest najsilniejszym warunkiem, kt´

ory wynika zar´

owno z p jak i z q (czyli jest kresem

g´

ornym pary {p, q}, jak suma zbior´

ow). Formu ly (9) wyra˙zaj

a dualn

a w lasno´s´

c koniunkcji:

to jest kres dolny, czyli najs labszy warunek implikuj

acy oba argumenty. Prawa de Mor-

gana (11,12) wskazuj

a te˙z na analogie koniunkcja–iloczyn, alternatywa–suma, negacja–

dope lnienie. Ta ostatnia widoczna jest te˙z w prawach wy l

aczonego ´srodka (5), podw´

ojnej

negacji (6) i kontrapozycji (7).

O ile (9) wskazuje na analogi

e pomi

edzy koniunkcj

a i iloczynem mnogo´sciowym, o tyle

warto zauwa˙zy´

c, ˙ze koniunkcja ma te˙z w lasno´sci podobne do iloczynu kartezja´

nskiego.

Je´sli zbi´

or funkcji z A do B oznaczymy przez [A → B], to mamy (bardzo naturaln

r´

ownoliczno´s´

c [A×B → C] ∼ [A → [B → C]]. Podobie´

nstwo tego zwi

azku do formu ly (10)

nie jest wcale przypadkowe.

Formu la (13) wyra˙za implikacj

e z pomoc

a negacji i alternatywy i jest cz

esto bardzo przy-

datna, gdy np. chcemy przekszta lci´

c jak

a´s formu l

e do prostszej postaci.

Formu la (2) m´

owi, ˙ze dodatkowe za lo˙zenie mo˙zna zawsze zignorowa´

c. Formu la (3) (prawo

Frege) wyra˙za dystrybutywno´s´

c implikacji wzgl

edem siebie samej i mo˙ze by´

c odczytywana

tak: je´sli r wynika z q w kontek´scie p, to ten kontekst mo˙ze by´

c w l

aczony do za lo˙zenia i

konkluzji. Formu la (4) (prawo Peirce’a) wyra˙za przy pomocy samej implikacji zasadnicz

w lasno´s´

c logiki klasycznej: mo˙zliwo´s´

c rozumowania przez zaprzeczenie. Sens prawa Peirce’a

wida´

c najlepiej gdy q jest fa lszem, mamy wtedy prawo Claviusa: (¬p → p) → p.

Warto zauwa˙zy´

c, ˙ze formu ly w parach (6,7) nie s

a wcale tak symetryczne jak si

e wydaje na

pierwszy rzut oka. Na przyk lad, pierwsza z formu l (6) to w istocie p → ((p → ⊥) → ⊥).
Wiedz

ac, ˙ze p i p → ⊥, natychmiast zgadzamy si

e na ⊥. Intuicyjne uzasadnienie drugiej

formu ly jest za´s w istocie zwi

azane z prawem (5).

W lasno´sci

a, kt´

ora cz

esto uchodzi naszej uwagi, jest l

aczno´s´

c r´

ownowa˙zno´sci (14). W zwiaz-

ku z tym, wyra˙zenie α ↔ β ↔ γ mo˙zna z czystym sumieniem pisa´

c bez nawias´

ow. Zwr´

o´

cmy

jednak uwag

e na to, ˙ze oznacza ono zupe lnie co innego ni˙z stwierdzenie ˙ze α, β i γ s

a sobie

nawzajem r´

ownowa˙zne!

Powy˙zej pomini

eto bardziej oczywiste prawa: l

aczno´s´

c i przemienno´s´

c koniunkcji i alter-

natywy, ich wzajemn

a dystrybutywno´s´

c, przechodnio´s´

c i zwrotno´s´

c implikacji itp.

Posta´

c normalna formu l

Definicja 10.6 Ka˙zdy symbol zdaniowy i negacj

e symbolu zdaniowego nazywamy litera-

lem. M´

owimy, ˙ze formu la zdaniowa α jest w koniunkcyjnej postaci normalnej, gdy α jest

koniunkcj

a alternatyw litera l´

ow, tj.

α = (p

1
1

∨ · · · ∨ p

) ∧ · · · ∧ (p

1
r

∨ · · · ∨ p

(*)

gdzie r ≥ 1, k

≥ 1, dla i = 1, . . . r, a wszystkie p

i
j

a litera lami.

Formu lami r´

ownowa˙znymi nazywamy takie formu ly α i β, ˙ze r´

ownowa˙zno´s´

c α ↔ β jest

tautologi

Fakt 10.7 Dla ka˙zdej formu ly zdaniowej istnieje r´

ownowa˙zna jej formu la w koniunkcyjnej

postaci normalnej.

Dow´

od:

Dow´

od jest przez indukcj

e ze wzgl

edu na budow

e formu ly. Symbole zdaniowe

a oczywiscie w postaci normalnej. Postaci

a normaln

a dla formu ly ⊥ jest p ∧ ¬p. Je´sli α

jest w postaci (*), to ¬α mo˙zna przekszta lci´

c w koniunkcyjn

a posta´

c normaln

a stosuj

prawa de Morgana i prawa dystrybutywno´sci:

β ∨ (γ ∧ δ) ↔ (β ∨ γ) ∧ (β ∨ δ)

β ∨ (γ ∨ δ) ↔ (β ∨ γ) ∨ (β ∨ δ).

Podobnie post

epujemy z implikacj

, przekszta lcaj

ac j

a z pomoc

a prawa 10.5(13).

Tautologie rachunku predykat´

Wracamy teraz do logiki predykat´

ow. Nietrudno zauwa˙zy´

c, ˙ze Fakt 10.4 jest prawdziwy

tak˙ze wtedy gdy formu ly S(p) niekoniecznie s

a zdaniowe. Ka˙zda instancja tautologii zda-

niowej jest wi

ec tautologi

a rachunku predykat´

ow. Oczywi´scie jest wiele interesuj

acych

tautologii, w kt´

orych istotn

a rol

e odgrywaj

a kwantyfikatory.

Fakt 11.1 Dla dowolnych ϕ i ψ, nast

epuj

ace formu ly s

a tautologiami:

1. ∀x(ϕ → ψ) → (∀xϕ → ∀xψ);

2. ϕ → ∀yϕ, gdzie y 6∈ F V (ϕ);

3. ∀xϕ → ϕ[x := s].

Ta procedura jest dosy´

c pracoch lonna. Mo˙zna j

a nieco upro´

sci´

c, ale najgorszy przypadek i tak po-

zostanie wyk ladniczy.

Dow´

od:

(1)

Niech A b

edzie modelem i v niech b

edzie warto´sciowaniem w A. Je´sli

v(∀xϕ) = 0 lub v(∀x(ϕ → ψ)) = 0 to nasza formu la jest oczywi´scie spe lniona przez v.
Za l´

o˙zmy wi

ec, ˙ze v(∀x(ϕ → ψ)) = v(∀xϕ) = 1. Nale˙zy pokaza´

c, ˙ze v(∀xψ) = 1. We´

zmy

dowolne a ∈ |A|. Skoro v(∀xϕ) = 1, to musi by´

c v

(ϕ) = 1. Podobnie v

(ϕ → ψ) = 1. Ale

wtedy tak˙ze v

(ψ) = 1. Zatem v(∀xψ) = min{v

(ψ) | a ∈ |A|} = 1, i dobrze.

(2) Mo˙zna za lo˙zy´

c, ˙ze v(ϕ) = 1. Dla dowolnego a ∈ |A|, na mocy Lematu 8.2, mamy

r´

owno´s´

c v

(ϕ) = v(ϕ), bo F V (ϕ) = F V (∀yϕ). Zatem v(∀yϕ) = min{1} = 1.

(3) Na mocy Lematu 8.11, dla dowolnej struktury A i dowolnego warto´sciowania v zachodzi:

v(ϕ[x := s]) = v

v(s)

(ϕ) ≥ min{v

(ϕ) | a ∈ |A|} = v(∀xϕ).

Jak si

e niebawem oka˙ze, trzy tautologie, o kt´

orych mowa powy˙zej, wyra˙zaj

a podstawowe

w lasno´sci kwantyfikatora og´

olnego. Pierwsza z nich to prawo rozk ladu kwantyfikatora og´

ol-

nego (rozdzielno´s´

c ∀ wzgl

edem implikacji). Druga pozwala na dopisanie kwantyfikatora,

kt´

ory nie wi

a˙ze ˙zadnej zmiennej, a trzecia, zwana dictum de omni , m´

owi ˙ze uniwersalna

zasada obowi

azuje ka˙zdego.

Kolejne dwa wa˙zne przyk lady tautologii dotycz

a r´

owno´sci.

Fakt 11.2 Nast

epuj

ace formu ly (gdzie ϕ jest dowoln

a formu l

a) s

a tautologiami:

1. ∀x(x = x);

2. ∀x∀y(x = y → (ϕ[z := y] → ϕ[z := x])).

Dow´

od:

e´s´

c pierwsza jest oczywista, a cz

e´s´

c druga wynika z Lematu 8.11, bo dla

dowolnego warto´sciowania v, je´sli v(x) = v(y) to v(ϕ[z := y]) = v

v(y)

(ϕ) = v

v(x)

(ϕ) =

v(ϕ[z := x]).

Uwaga: Je´sli w drugiej cz

e´sci Faktu 11.2 jako ϕ wybierzemy formu l

”

z = u” to otrzymamy

∀x∀y(x = y → (y = u → x = u)).

Natomiast dla ϕ =

”

y = z” dostaniemy

∀x∀y(x = y → (y = y → y = x)).

Pierwsza z tych formu l wyra˙za przechodnio´s´

c r´

owno´sci, a druga jej symetri

Oczywi´scie dow´

od, ˙ze dana formu la jest tautologi

a polega na analizie jej spe lniania w dowol-

nych modelach. Natomiast wykazanie, ˙ze tak nie jest polega na podaniu odpowiedniego
kontrprzyk ladu. Takiego jak ten:

Przyk lad 11.3 Formu la (∀xp(x) → ∀xq(x)) → ∀x(p(x) → q(x)) nie jest tautologi

Rozpatrzmy bowiem model A = hN, p

, q

i, w kt´

orym:

• n ∈ p

, wtedy i tylko wtedy, gdy n jest parzyste;

• n ∈ q

, wtedy i tylko wtedy, gdy n jest nieparzyste;

Wtedy A 6|= ∀xp(x) wi

ec A |= ∀xp(x) → ∀xq(x).

Ale A 6|= ∀x(p(x) → q(x)), bo

A, 2 6|= p(x) → q(x). Rzeczywi´scie, 2 ∈ p

− q

Przyjrzyjmy si

e jeszcze kilku wa˙znym tautologiom.

Fakt 11.4 Nast

epuj

ace formu ly s

a tautologiami (dla dowolnych ϕ i ψ).

1. ∀x(ϕ → ψ) → (∃xϕ → ∃xψ);

2. ∃xϕ → ϕ, o ile x 6∈ F V (ϕ);

3. ϕ[x := s] → ∃xϕ;

4. ¬∀xϕ ↔ ∃x¬ϕ;

5. ¬∃xϕ ↔ ∀x¬ϕ;

6. ∀x(ϕ ∧ ψ) ↔ ∀xϕ ∧ ∀xψ;

7. ∃x(ϕ ∨ ψ) ↔ ∃xϕ ∨ ∃xψ;

8. ∀x(ϕ ∨ ψ) ↔ ϕ ∨ ∀xψ, o ile x 6∈ F V (ϕ);

9. ∃x(ϕ ∧ ψ) ↔ ϕ ∧ ∃xψ, o ile x 6∈ F V (ϕ);

10. ∀xϕ → ∃xϕ;

11. ∀x∀yϕ ↔ ∀y∀xϕ;

12. ∃x∃yϕ ↔ ∃y∃xϕ;

13. ∃x∀yϕ → ∀y∃xϕ;

Dow´

od:

Cwiczenie.

Formu ly (1)–(3) powy˙zej wyra˙zaj

a w lasno´sci kwantyfikatora szczeg´

o lowego i s

a odpowied-

nikami formu l z Faktu 11.1. Zauwa˙zmy, ˙ze zamiast rozdzielno´sci kwantyfikatora szczeg´

o lo-

wego, mamy tu jeszcze jedno prawo rozk ladu kwantyfikatora og´

olnego. Symetria pomi

edzy

∀ i ∃ nie jest wcale ca lkowita! Niemniej istnieje, co wyra˙zaj

a prawa de Morgana (4) i (5).

Kolejne dwie tautologie przypominaj

a o bliskim zwi

azku kwantyfikatora og´

olnego z ko-

niunkcj

a i kwantyfikatora szczeg´

o lowego z alternatyw

a. (Uwaga: zmienna x mo˙ze by´

wolna w ϕ i ψ.) Analogiczna rozdzielno´s´

c kwantyfikatora og´

olnego wzgl

edem alternaty-

wy (8) i kwantyfikatora szczeg´

o lowego wzgl

edem koniunkcji (9) nie zawsze jest prawd

a, ale

zachodzi pod warunkiem, ˙ze zmienna wi

azana kwantyfikatorem nie wyst

epuje w jednym

z cz lon´

ow formu ly. (Prawo (8) nazywane bywa prawem Grzegorczyka lub aksjomatem

Gabbaya.)

Formu la (10) jest odbiciem naszego za lo˙zenia o niepusto´sci ´swiata. Jest to tautologia,
poniewa˙z um´

owili´smy si

e, ˙ze rozwa˙zamy tylko niepuste struktury.

Prawa (11)–(13) charakteryzuj

a mo˙zliwo´sci permutowania kwantyfikator´

ow. Implikacja

odwrotna do (13) zazwyczaj nie jest tautologi

Stosuj

ac r´

ownowa˙zno´sci (4–9) mo˙zemy ka˙zd

a formu l

e sprowadzi´

c do postaci, w kt´

orej

wszystkie kwantyfikatory znajduj

a si

e na pocz

atku. M´

owimy, ˙ze formu la ϕ jest w prenek-

sowej postaci normalnej , gdy

ϕ = Q

. . . Q

ψ,

gdzie ka˙zde z Q

to ∀ lub ∃, a ψ jest formu l

a otwart

a. (Oczywi´scie n mo˙ze by´

c zerem.)

Fakt 11.5 Dla ka˙zdej formu ly pierwszego rz

edu istnieje r´

ownowa˙zna jej formu la w prenek-

sowej postaci normalnej.

Dow´

od:

Indukcja (´

cwiczenie).

Dowodzenie twierdze´

Sprawdzenie, czy dana formu la rachunku zda´

n jest tautologi

a, wymaga obliczenia jej

warto´sci dla 2

r´

o˙znych warto´sciowa´

n, gdzie n jest liczb

a zmiennych zdaniowych tej for-

mu ly. Dla rachunku predykat´

ow nie istnieje w og´

ole ˙zaden algorytm sprawdzania czy dana

formu la jest tautologi

a. W obu przypadkach s

a jednak metody dowodzenia pozwalaj

ace

na wyprowadzenie ka˙zdej prawdziwej formu ly z pomoc

a pewnego ustalonego systemu regu l

wnioskowania i aksjomat´

ow. Jeden z takich system´

ow opisany jest poni˙zej. (Zak ladamy,

˙ze ustalona jest sygnatura Σ, a formu ly r´

o˙zni

ace si

e tylko zmiennymi zwi

azanymi uwa˙zamy

za identyczne.) Aksjomatami naszego systemu s

a wszystkie formu ly postaci:

A1) ϕ → (ψ → ϕ);

A2) (ϕ → (ψ → ϑ)) → ((ϕ → ψ) → (ϕ → ϑ));

A3) ((ϕ → ψ) → ϕ) → ϕ;

A4) ⊥ → ϕ.

A5) ∀x(ϕ → ψ) → (∀xϕ → ∀xψ);

A6) ϕ → ∀yϕ, gdy y 6∈ F V (ϕ);

A7) ∀xϕ → ϕ[t/x];

A8) ∀x(x = x);

A9) ∀x∀y(x = y → ϕ[z := y] → ϕ[z := x]).

Powy˙zej, symbole ϕ, ψ i ϑ oznaczaj

a dowolne formu ly sygnatury Σ. A zatem nasz zbi´

aksjomat´

ow nie sk lada si

e z dziewi

eciu formu l, ale jest zbiorem niesko´

nczonym. (Niemniej,

jest to efektywny (lub obliczalny) zbi´

or aksjomat´

ow, bo istnieje latwe kryterium pozwala-

ace odr´

o˙zni´

c co jest aksjomatem a co nie jest.)

Przyjmujemy dwie regu ly wnioskowania. Pierwsz

a jest regu la odrywania (modus ponens),

zapisywana tak:

α, α → β

a drug

a regu la generalizacji , kt´

a zapisujemy tak:

∀xϕ

Regu ly nale˙zy rozumie´

c z grubsza w ten spos´

ob: je´sli formu ly nad kresk

a (przes lanki regu ly)

a ju˙z wyprowadzone, to mo˙zna wywnioskowa´

c formu l

e pod kresk

a (konkluzj

e). Z grubsza,

bo stosowanie regu ly generalizacji jest ograniczone (patrz ni˙zej).

Definicja 12.1 Dowodem formalnym lub wyprowadzeniem (w sensie Hilberta) formu ly ϕ
ze zbioru za lo˙ze´

n Γ nazywamy dowolny ci

ag formu l ϕ

, ϕ

, . . . , ϕ

, spe lniaj

acy nast

epuj

ace

warunki:

• ϕ

= ϕ;

• Dla ka˙zdego i ≤ n zachodzi jedna z czterech mo˙zliwo´sci:

– ϕ

jest aksjomatem;

– ϕ

∈ Γ;

– s

a takie `, j < i, ˙ze ϕ

= ϕ

→ ϕ

(tj. ϕ

jest otrzymana przez zastosowanie

modus ponens do formu l ϕ

i ϕ

);

– jest takie j < i, ˙ze ϕ

= ∀xϕ

, oraz x 6∈ F V (Γ) (tj. ϕ

jest otrzymana przez

generalizacj

e formu ly ϕ

Je´sli taki dow´

od istnieje, to piszemy Γ ` ϕ i m´

owimy, ˙ze ϕ mo˙zna udowodni´

c z za lo˙ze´

n Γ,

lub ˙ze ϕ jest (syntaktyczn

a) konsekwencj

a Γ. Je´sli ∅ ` ϕ to piszemy tylko ` ϕ i m´

owimy,

˙ze ϕ jest twierdzeniem rachunku predykat´

ow.

Jak wida´

c z powy˙zszej definicji, stosowanie regu ly generalizacji jest ograniczone do przy-

padku, gdy zmienna wi

azana kwantyfikatorem nie jest wolna w za lo˙zeniach ze zbioru Γ.

Dlatego regu l

e generalizacji nale˙zy ´sci´slej zapisa´

c tak:

∀xϕ

(x 6∈ F V (Γ))

Regu la generalizacji mo˙ze by´

c stosowana m.in. wtedy, gdy Γ nie ma zmiennych wolnych

(w szczeg´

olno´sci, gdy Γ = ∅).

Uwaga: Ten, kto nie chce uto˙zsamia´

c alfa-r´

ownowa˙znych formu l, musi nieco zmody-

fikowa´

c powy˙zszy system dowodzenia, poprzez pewne wzmocnienie regu ly generalizacji.

Na przyk lad takie:

ϕ(x o y)

∀xϕ

(y 6∈ F V (Γ))

Przyk lad 12.2

(1) Nast

epuj

acy ci

ag formu l (gdzie jako β mo˙zna przyj

a´

c jak

akolwiek formu l

e) jest dowo-

dem formu ly α → α (ze zbioru pustego).

1. (α → (β → α) → α) → ((α → (β → α)) → (α → α)) (aksjomat A2);

2. α → (β → α) → α (aksjomat A1);

3. (α → (β → α)) → (α → α) (odrywanie (2) od (1);

4. α → (β → α) (aksjomat A1);

5. α → α (odrywanie (4) od (3)).

(2) Nast

epuj

acy ci

ag formu l jest dowodem formu ly γ ze zbioru {α → β, β → γ, α}:

1. α → β (za lo˙zenie);

2. α (za lo˙zenie);

3. β (odrywanie (2) od (1));

4. β → γ (za lo˙zenie);

5. γ (odrywanie (3) od (4)).

(3) Nast

epuj

acy ci

ag formu l jest dowodem formu ly ∀x∀yP (x, y) → ∀xP (x, x):

1. ∀yP (x, y) → P (x, x) (aksjomat A7);

2. ∀x(∀yP (x, y) → P (x, x)) (generalizacja (1));

3. ∀x(∀yP (x, y) → P (x, x)) → (∀x∀yP (x, y) → ∀xP (x, x)) (aksjomat A5);

4. ∀x∀yP (x, y) → ∀xP (x, x) (odrywanie (2) od (3)).

Tradycyjna definicja hilbertowskiego dowodu formalnego jako ci

agu formu l jest cz

esto

wygodna i dlatego wci

a˙z popularna. Ale oczywi´scie ka˙zdy dow´

od w sensie Hilberta ukrywa

w sobie struktur

e drzewa. Na przyk lad dow´

od z Przyk ladu 12.2(3) mo˙zemy napisa´

c tak:

α → β

β → γ

Lemat 12.3 Przypu´

s´

cmy, ˙ze ci

ag formu l ϕ

, ϕ

, . . . , ϕ

jest dowodem formu ly ϕ

ze zbioru

za lo˙ze´

n Γ. Je´

sli x, y 6∈ F V (Γ), a na dodatek y 6∈ F V (ϕ

) dla i = 1, . . . , n, to ci

ag formu l

[x := y], ϕ

[x := y], . . . , ϕ

[x := y] jest dowodem formu ly ϕ

[x := y] z za lo˙ze´

n Γ.

Dow´

od:

Latwa indukcja ze wzgl

edu na n. W przypadku gdy w ostatnim kroku mamy

generalizacj

e ze wzgl

edu na z 6= x nale˙zy zauwa˙zy´

c, ˙ze (∀z ϕ

)[x := y] = ∀z ϕ

[x := y].

Przy generalizacji ze wzgl

edu na x korzystamy z tego, ˙ze ∀x ϕ

∀y ϕ

[x := y].

Lemat 12.4 (o os labianiu) Je´

sli Γ ` ϕ oraz Γ ⊆ Γ

to tak˙ze Γ

` ϕ.

Dow´

od:

Post

epujemy przez indukcj

e ze wzgl

edu na d lugo´s´

c dowodu formu ly ϕ z za-

lo˙ze´

n Γ. Jedyny nieoczywisty przypadek, to zastosowanie generalizacji. Mo˙ze si

e bowiem

zdarzy´

c, ˙ze ϕ

= ∀xϕ

gdzie x 6∈ F V (Γ) ale x ∈ F V (Γ

). Ale wtedy mo˙zemy skorzysta´

z Lematu 12.3 i skonstruowa´

c taki dow´

od, w kt´

orym zamiast formu ly ϕ

jest ϕ

[x := y],

a zmienna y nie nale˙zy do F V (Γ

). Mo˙zemy teraz generalizowa´

c i otrzymujemy formu l

∀y ϕ

[x := y] =

∀xϕ

Twierdzenie 12.5 (o poprawno´

sci) Je˙zeli Γ ` ϕ to Γ |= ϕ. W szczeg´

olno´

sci, ka˙zde

twierdzenie jest tautologi

Dow´

od:

Dow´

od przebiega przez indukcj

e ze wzgl

edu na d lugo´s´

c najkr´

otszego dowodu

formalnego formu ly ϕ ze zbioru Γ. Oczywi´scie Γ |= ϕ, dla ka˙zdego ϕ ∈ Γ. Z Fakt´

ow 10.5

i 10.4 natychmiast wynika, ˙ze aksjomaty (A1)–(A4) s

a tautologiami. Pozosta le aksjomaty

a tautologiami na mocy Faktu 11.1 i Faktu 11.2. Je´sli wi

ec dow´

od formu ly ϕ ma d lugo´s´

c 1,

to teza zachodzi. Je´sli dow´

od sk lada si

e z wi

ecej ni˙z jednego kroku, to ϕ otrzymano za

pomoc

a jednej z regu l dowodzenia.

Za l´

o˙zmy najpierw, ˙ze ostatni

a zastosowan

a regu l

a bylo modus ponens.

To znaczy, ˙ze

wcze´sniej w naszym dowodzie pojawi ly si

e pewna formu la ψ i formu la ψ → ϕ. Z za-

lo˙zenia indukcyjnego mamy Γ |= ψ i Γ |= ψ → ϕ. St

ad oczywi´scie wynika, ˙ze Γ |= ϕ.

(Ka˙zde warto´sciowanie spe lniaj

ace ψ i ψ → ϕ musi te˙z spe lnia´

c ϕ.)

Je˙zeli ostatnia by la regu la generalizacji, to ϕ jest postaci ∀xψ, gdzie x 6∈ F V (Γ). Z za-
lo˙zenia indukcyjnego Γ |= ψ. Chcemy pokaza´

c, ˙ze wtedy Γ |= ∀xψ. Niech wi

ec A, v |= Γ.

Wtedy tak˙ze A, v

|= Γ, przy dowolnym a ∈ |A|, bo x 6∈ F V (Γ). Zatem zawsze A, v

|= ψ,

ec v(∀xψ) = min{v

(ψ) : a ∈ |A|} = 1.

Konwencja notacyjna: napis Γ, ϕ oznacza zbi´

or Γ ∪ {ϕ}, podobnie zamiast {ϕ, β, γ} ` δ

piszemy ϕ, β, γ ` δ, itd.

Twierdzenie 12.6 (o dedukcji) Warunki Γ ` ϕ → ψ i Γ, ϕ ` ψ s

a r´

ownowa˙zne.

Dow´

od:

Implikacja z lewej do prawej jest oczywista: aby z Γ, ϕ otrzyma´

c ψ, nale˙zy

wyprowadzi´

c ϕ → ψ i oderwa´

c ϕ. Dow´

od implikacji odwrotnej przebiega przez indukcj

e ze

wzgl

edu na d lugo´s´

c dowodu formalnego formu ly ψ ze zbioru Γ, ϕ.

Je´sli ψ jest aksjomatem lub ψ ∈ Γ, to dow´

od formu ly ϕ → ψ jest otrzymany przez oder-

wanie ψ od aksjomatu ψ → (ϕ → ψ). Je´sli ψ = ϕ to korzystamy z tego, ˙ze ` ϕ → ϕ
(Przyk lad 12.2(1)) i tym bardziej Γ ` ϕ → ϕ.

Przypu´s´

cmy wi

ec, ˙ze ψ otrzymano przez odrywanie. Znaczy to, ˙ze Γ, ϕ ` ϑ → ψ i Γ, ϕ ` ϑ

dla pewnej formu ly ϑ, i ˙ze odpowiednie dowody s

a kr´

otsze. Z za lo˙zenia indukcyjnego

otrzymujemy, ˙ze formu ly ϕ → (ϑ → ψ) i ϕ → ϑ maj

a dowody ze zbioru Γ. Aby otrzyma´

dow´

od dla ϕ → ψ, nale˙zy te dwie formu ly kolejno oderwa´

c od aksjomatu (A2) w postaci

(ϕ → (ϑ → ψ)) → ((ϕ → ϑ) → (ϕ → ψ)).

Pozostaje przypadek, gdy dow´

od formu ly ψ ze zbioru Γ, ϕ ko´

nczy si

e generalizacj

a, tj gdy

ψ = ∀xϑ i mamy kr´

otszy dow´

od dla Γ, ϕ ` ϑ, a przy tym x 6∈ F V (Γ, ϕ), tj. x 6∈ F V (Γ)

i x 6∈ F V (ϕ). Z za lo˙zenia indukcyjnego mamy Γ ` ϕ → ϑ. Poniewa˙z x 6∈ F V (Γ), wi

z pomoc

a regu ly generalizacji otrzymamy Γ ` ∀x(ϕ → ϑ). U˙zyjemy nast

epnie aksjo-

matu (A5) i odrywania aby dosta´

c Γ ` ∀xϕ → ∀xϑ. St

ad z pomoc

a (A1) uzyskamy

Γ ` ϕ → (∀xϕ → ∀xϑ).

Poniewa˙z x 6∈ FV(ϕ), wi

ec formu la ϕ → ∀xϕ jest aksjo-

matem (A6), w szczeg´

olno´sci ma dow´

od z Γ. Pozostaje wykona´

c dwa odrywania od aks-

jomatu (A2) w postaci (ϕ → (∀xϕ → ∀xϑ)) → ((ϕ → ∀xϕ) → (ϕ → ∀xϑ)) i dostajemy
Γ ` ϕ → ∀xϑ.

Twierdzenie o dedukcji pozwala na latwe przekonanie si

e o istnieniu pewnych dowod´

bez ich wypisywania w ca lo´sci. Na przyk lad, latwo przekona´

c si

e o tym, ˙ze dla dowolnych

α, β i γ, formu la

(α → (β → γ)) → (β → (α → γ)),

jest twierdzeniem, sprawdzaj

ac tylko, ˙ze α → (β → γ), β, α ` γ. W podobny spos´

otrzymamy

Lemat 12.7 Je´

sli Γ ` ϕ → ψ oraz Γ ` ψ → ϑ to tak˙ze Γ ` ϕ → ϑ.

Dow´

od:

Najpierw pokazujemy, ˙ze ϕ → ψ, ψ → ϑ, ϕ ` ϑ, a potem trzy razy stosujemy

Twierdzenie 12.6.

Co mo ˙zna udowodni´

Naszym celem jest twierdzenie odwrotne do Twierdzenia 12.5, czyli twierdzenie o pe lno´sci.
Dow´

od tego twierdzenia wymaga pewnych przygotowa´

n. Musimy pokaza´

c, ˙ze w naszym

systemie wnioskowania potrafimy wyprowadzi´

c ca ly szereg rozmaitych formu l. Nast

epuj

aca

teraz seria lemat´

ow jest po´swi

econa temu zadaniu. Najpierw zrobimy pewn

a do´s´

c oczywist

obserwacj

e. B

edziemy z niej wielokrotnie korzysta´

Lemat 13.1

Je´

sli Γ ` α oraz ∆, α ` β to Γ, ∆ ` β.

Dow´

od:

Latwy. Ale trzeba u˙zy´

c Lematu 12.4.

Nast

epuj

acy lemat stwierdza, ˙ze najwa˙zniejsze w lasno´sci negacji s

a twierdzeniami naszego

systemu:

Lemat 13.2 Dla dowolnych formu l α i β:

1. α ` ¬¬α;

2. ¬α, α ` β;

3. ¬¬α ` α;

4. α → β, ¬α → β ` β.

Dow´

od:

(1) Poniewa˙z α, α → ⊥ ` ⊥, wi

ec z twierdzenia o dedukcji α ` (α → ⊥) → ⊥, czyli

w la´snie α ` ¬¬α.

(2) Poniewa˙z ¬α, α ` ⊥ (zob. (1)) oraz ⊥ ` β, wi

ec tak˙ze ¬α, α ` β.

(3) Korzystaj

ac z (2) otrzymamy ¬¬α, ¬α ` α, i z twierdzenia o dedukcji ¬¬α ` ¬α → α.

Prawo Peirce’a w postaci ((α → ⊥) → α) → α jest aksjomatem, a wi

ec przez odpowiednie

odrywanie dostajemy (3).

(4) Zauwa˙zmy na pocz

atek, ˙ze α → β, ¬α → β, β → ⊥ ` α → ⊥ (Lemat 12.7). Poniewa˙z

α → ⊥ to to samo co ¬α, i oczywi´scie α → β, ¬α → β, β → ⊥ ` ¬α → β, wi

latwo otrzymujemy α → β, ¬α → β, β → ⊥ ` β. Z twierdzenia o dedukcji otrzymamy
α → β, ¬α → β ` ¬¬β. Na mocy (3) wnioskujemy, ˙ze α → β, ¬α → β ` β.

Kolejne dwa lematy dotycz

a w lasno´sci koniunkcji i alternatywy, wyprowadzalnych w naszym

systemie dowodzenia. (Przypomnijmy, ˙ze α ∧ β = ¬(α → (¬β)) oraz α ∨ β = ¬α → β.)

Lemat 13.3 Dla dowolnych formu l α, β i γ:

1. α ∧ β ` α;

2. α, β ` α ∧ β;

3. α ∧ β ` β;

4. γ → α, γ → β ` γ → β ∧ α;

Dow´

od:

(1) Ten dow´

od poprowadzimy

”

od ko´

nca”, aby pokaza´

c metody jakimi mo˙zna

e pos lugiwa´

c dla konstrukcji wyprowadzenia. Mamy udowodni´

c, ˙ze α ∧ β ` α, czyli, ˙ze

(α → ¬β) → ⊥ ` α. Nie bardzo wiadomo jak si

e do tego zabra´

c, bo stosuj

ac modus ponens

do formu ly (α → ¬β) → ⊥ na pewno nie dostaniemy formu ly α. Ale wiemy, ˙ze wystarczy
udowodni´

c ¬¬α, czyli formu l

e (α → ⊥) → ⊥. Mamy te˙z twierdzenie o dedukcji, czyli

wystarczy je´sli otrzymamy to:

(α → ¬β) → ⊥, α → ⊥ ` ⊥.

(2)

Mamy szans

e wyprowadzi´

c ⊥, je´sli wyprowadzimy przes lank

e kt´

orego´s z za lo˙ze´

n. Spr´

obuj-

my wi

ec, czy uda si

e uzyska´

c to:

(α → ¬β) → ⊥, α → ⊥ ` α → ¬β.

(3)

Z twierdzenia o dedukcji wiemy, ˙ze wystarczy co´s takiego:

(α → ¬β) → ⊥, α → ⊥, α ` ¬β.

(4)

Ale to ju˙z jest latwe. Wystarczy si

e powo la´

c na Lemat 13.2(2). St

ad dostaniemy (3)

i dalej (2).

Uwaga: to co zrobili´smy, to nie by la konstrukcja dowodu w sensie Hilberta. To by lo tylko
uzasadnienie, ˙ze taki dow´

od mo˙zna skonstruowa´

(2) Poniewa˙z α, β, α → (β → ⊥) ` ⊥, wi

ec α, β ` (α → (β → ⊥)) → ⊥, a to jest w la´snie

to co trzeba.

(3) Poniewa˙z ¬β ` α → ¬β wi

ec (α → ¬β) → ⊥, ¬β ` ⊥, a st

ad α ∧ β ` ¬¬β, i pozostaje

skorzysta´

c z Lematu 13.2(3).

(4) Latwa konsekwencja cz

e´sci (2).

Lemat 13.4 Dla dowolnych formu l α, β i γ:

1. β ` α ∨ β;

2. α ` α ∨ β;

3. α → γ, β → γ ` α ∨ β → γ;

Dow´

od:

(1) i (2) Oczywiste, bo przecie˙z α ∨ β = ¬α → β.

(3) Mamy α → γ, β → γ, ¬α → β ` α → γ oraz α → γ, β → γ, ¬α → β ` ¬α → γ.
Z Lematu 13.2(4) wynika α → γ, β → γ, ¬α → β ` γ, i pozostaje zastosowa´

c twierdzenie

o dedukcji.

Lemat 13.5 Dla dowolnych formu l α, β, γ:

1. (α ∨ β) ∧ γ ` (α ∧ γ) ∨ (β ∧ γ);

2. (α ∧ γ) ∨ (β ∧ γ) ` (α ∨ β) ∧ γ;

3. (α ∧ β) ∨ γ ` (α ∨ γ) ∧ (β ∨ γ);

4. (α ∨ γ) ∧ (β ∨ γ) ` (α ∧ β) ∨ γ;

Dow´

od:

(1) Poniewa˙z α, γ ` α ∧ γ, wi

ec α, γ, α ∧ γ → ⊥ ` ⊥, czyli γ, α ∧ γ → ⊥ `

α → ⊥. St

ad γ, α ∧ γ → ⊥, (α → ⊥) → β ` β. Poniewa˙z oczywi´scie γ, . . . ` γ, wi

γ, α ∧ γ → ⊥, α ∨ β ` β ∧ γ, bo przecie˙z (α → ⊥) → β = α ∨ β. Z twierdzenia o dedukcji
γ, (α → ⊥) → β ` ¬(α ∧ γ) → (β ∧ γ), a poniewa˙z γ ∧ (α ∨ β) ` γ i γ ∧ (α ∨ β) ` α ∨ β
(Lemat 13.3(1, 3)), wi

ec ostatecznie γ ∧ (α ∨ β) ` (α ∧ γ) ∨ (β ∧ γ).

(2) Poniewa˙z α ` α ∨ β i γ ` γ, wi

ec α ∧ γ ` (α ∨ β) ∧ γ, z Lematu 13.3(1–2). Podobnie

β ∧ γ ` (α ∨ β) ∧ γ, wi

ec teza wynika z Lematu 13.4(3).

(3) Podobnie jak w (2) nale˙zy najpierw zauwa˙zy´

c, ˙ze γ ` (α ∨ γ) ∧ (β ∨ γ), bo γ ` (α ∨ γ)

i γ ` (β ∨ γ), oraz ˙ze α ∧ β ` (α ∨ γ) ∧ (β ∨ γ), bo α ∧ β ` (α ∨ γ) i α ∧ β ` (α ∨ γ).
Nast

epnie u˙zywamy Lematu 13.4(3).

(4) Poniewa˙z γ ∨ α = (γ → ⊥) → α, wi

ec γ ∨ α, ¬γ ` α. Podobnie γ ∨ β, ¬γ ` β, wi

γ ∨ α, γ ∨ β, ¬γ ` α ∧ β. St

ad tak˙ze α ∨ γ, β ∨ γ ` ¬γ → (α ∧ β). Zatem (α ∨ γ) ∧ (β ∨ γ) `

γ ∨ (α ∧ β).

Algebra Lindenbauma

Ustalmy pewien zbi´

or formu l Γ. Okre´slimy relacj

e ∼

w zbiorze wszystkich formu l:

α ∼

wtedy i tylko wtedy, gdy

Γ ` α ↔ β.

Latwo widzie´

c, ˙ze relacja ∼

jest relacj

a r´

ownowa˙zno´sci, bo wiemy ju˙z, ˙ze:

` α → α

oraz

α → β, β → γ ` α → γ

Ponadto relacja ∼

zachowuje sp´

ojniki logiczne ∨, ∧ i ¬:

Lemat 13.6 Je˙zeli α ∼

i β ∼

to:

1. ¬α ∼

¬α

;

2. α ∨ β ∼

∨ β

;

3. α ∧ β ∼

∧ β

;

Dow´

od:

Cwiczenie.

Powy˙zszy lemat pozwala na okre´slenie operacji ∪, ∩, − na klasach abstrakcji relacji ∼

Definiujemy je tak:

[α]

∼

∪ [β]

∼

= [α ∨ β]

∼

;

[α]

∼

∩ [β]

∼

= [α ∧ β]

∼

;

−[α]

∼

= [¬α]

∼

Lemat 13.6 gwarantuje poprawno´s´

c tych operacji (wynik nie zale˙zy od wyboru reprezen-

tant´

ow). Mo˙zemy te˙z okre´sli´

c relacj

e ≤ w zbiorze F

∼

[α]

∼

≤ [β]

∼

wtedy i tylko wtedy, gdy

Γ ` α → β.

Wskaz´

owka: najpierw nale˙zy pokaza´

c, ˙ze relacja ∼

zachowuje implikacj

Lemat 13.7 Relacja ≤ jest cz

e´

sciowym porz

adkiem w F

∼

, a dla dowolnych α i β:

• [α ∨ β]

∼

= sup{[α]

∼

, [β]

∼

};

• [α ∧ β]

∼

= inf{[α]

∼

, [β]

∼

Dow´

od:

Latwy wniosek z Lemat´

ow 13.3 i 13.4.

Lemat 13.8 Dla dowolnej formu ly α,

• α ∼

> wtedy i tylko wtedy, gdy Γ ` α. W szczeg´

olno´

sci α ∼

> dla α ∈ Γ.

• α ∼

⊥ wtedy i tylko wtedy, gdy Γ ` ¬α.

Dow´

od:

Latwy.

Fakt 13.9 Zbi´

or F

∼

, z lo˙zony ze wszystkich klas abstrakcji relacji ∼

, tworzy algebr

Boole’a z operacjami ∪, ∩, −, i sta lymi 0 = [⊥]

∼

oraz 1 = [>]

∼

Dow´

od:

Na mocy Lematu 13.7, algebra F

∼

jest krat

a. Dystrybutywno´s´

c wynika

z Lematu 13.5. Pozostaje sprawdzi´

c nast

epuj

ace cztery warunki:

1. α ∨ ⊥ ∼

α;

2. α ∧ > ∼

α;

3. α ∨ ¬α ∼

4. ¬α ∧ α ∼

⊥;

Warunki (1) i (2) wynikaj

a st

ad, ˙ze ⊥ i > s

a odpowiednio najmniejszym i najwi

ekszym ele-

mentem. Warunek (3) wynika z r´

owno´sci α ∨ ¬α = ¬α → ¬α, a warunek (4) z oczywistego

zwi

azku α, α → ⊥ ` ⊥.

Definicja 13.10 Algebr

e Boole’a L

= hF

∼

, ∪, ∩, −, 0, 1i, o kt´

orej mowa w Fak-

cie 13.9, nazywamy algebr

a Lindenbauma.

Twierdzenia o pe lno´

sci

Twierdzenie 14.1 (o pe lno´

sci rachunku zda´

n) Za l´

o˙zmy, ˙ze Γ jest zbiorem formu l

zdaniowych i niech α b

edzie formu l

a zdaniow

a. Je˙zeli Γ |= α to Γ ` α. W szczeg´

olno´

sci,

ka˙zda tautologia zdaniowa jest twierdzeniem.

Dow´

od:

Przypu´s´

cmy, ˙ze Γ 6` α. Oznacza to w szczeg´

olno´sci, ˙ze Γ, ¬α 6` ⊥, czyli, ˙ze

[¬α]

∼

6= 0. Na mocy Lematu 4.13, istnieje wi

ec taki filtr maksymalny F , ˙ze [¬α]

∼

∈ F .

Filtr F jest te˙z ultrafiltrem (Lemat 4.15), tj. dla dowolnej formu ly ϕ, jedna z klas [ϕ]

∼

lub [¬ϕ]

∼

musi nale˙ze´

c do F . Zauwa˙zmy jeszcze, ˙ze dla γ ∈ Γ mamy [γ]

∼

= 1 ∈ F .

Niech teraz w b

edzie takim warto´sciowaniem zdaniowym, ˙ze dla dowolnego symbolu zda-

niowego p

w(p) = 1

wtedy i tylko wtedy, gdy

[p]

∼

∈ F .

Udowodnimy, ˙ze dla dowolnej formu ly ϕ zachodzi

w(ϕ) = 1

wtedy i tylko wtedy, gdy

[ϕ]

∼

∈ F.

(5)

Post

epujemy przez indukcj

e ze wzgl

edu na budow

e formu ly ϕ. Oczywiste jest, ˙ze warunek (5)

zachodzi dla ⊥ i dla symboli zdaniowych. Niech wi

ec ϕ = ψ → ϑ.

Za l´

o˙zmy, ˙ze w(ψ → ϑ) = 1.

Wtedy albo w(ψ) = 0 albo w(ϑ) = 1.

W pierwszym

przypadku, z za lo˙zenia indukcyjnego [ψ]

∼

6∈ F , czyli [¬ψ]

∼

∈ F , bo F jest ultrafiltrem.

W drugim przypadku [ϑ]

∼

∈ F . Ale poniewa˙z zar´

owno [¬ψ]

∼

≤ [ψ → ϑ]

∼

jak te˙z i

[ϑ]

∼

≤ [ψ → ϑ]

∼

, wi

ec w obu przypadkach [ψ → ϑ]

∼

∈ F .

Na odwr´

ot, niech [ψ → ϑ]

∼

∈ F i niech w(ψ) = 1. Z za lo˙zenia indukcyjnego [ψ]

∼

∈ F ,

a wi

ec tak˙ze [ϑ]

∼

∈ F , bo [ψ]

∼

∩ [ψ → ϑ]

∼

≤ [ϑ]

∼

. Na mocy za lo˙zenia indukcyjnego

wnioskujemy, ˙ze w(ϑ) = 1.

Z warunku (5) wynika, ˙ze w(α) = 0, oraz w(γ) = 1 dla γ ∈ Γ. St

ad Γ 6|= α.

Pe lno´

s´

c rachunku predykat´

Dow´

od twierdzenia o pe lno´sci rachunku predykat´

ow jest nieco trudniejszy od rozwa˙zanego

poprzednio dowodu pe lno´sci rachunku zda´

n, chocia˙z zasadniczy tok rozumowania pozostaje

podobny. Znowu b

edzie mowa o algebrze Lindenbauma. Tym razem jednak nie szukamy

zerojedynkowego warto´sciowania zdaniowego, ale musimy skonstruowa´

c odpowiedni

a struk-

tur

e algebraiczn

a. Na dodatek, byle jaki filtr maksymalny tym razem niestety nie wystar-

czy. Potrzebny b

edzie filtr spe lniaj

acy do´s´

c wyrafinowane zachcianki i to stanowi zasad-

nicz

a trudno´s´

c techniczn

a. Mo˙zna j

a rozwi

aza´

c na dwa sposoby. Pierwszy jest bardziej

elegancki, bo czysto algebraiczny, i opiera si

e na twierdzeniu, kt´

ore tradycyjnie wbrew

gramatyce nazywane jest

”

lematem Rasiowa-Sikorski”.

Ten spos´

ob ma jednak pewn

wad

e: stosuje si

e tylko do przeliczalnych j

ezyk´

ow (sygnatura i zbi´

or zmiennych musz

a by´

przeliczalne). Drugi spos´

ob, zwany

”

metod

a sta lych Henkina” nie ma tego ograniczenia.

Definicja 14.2 Zbi´

or formu l Γ jest sprzeczny wtedy i tylko wtedy, gdy Γ ` ⊥.

Lemat 14.3 Je´

sli Γ ` ϕ to istnieje taki sko´

nczony podzbi´

or Γ

⊆ Γ, ˙ze Γ

` ϕ. W szczeg´

ol-

no´

sci, je´

sli Γ jest sprzeczny to ma sko´

nczony podzbi´

or, kt´

ory te˙z jest sprzeczny.

Dow´

od:

W wyprowadzeniu wyst

epuje tylko sko´

nczenie wiele formu l ze zbioru Γ. Reszta

jest niepotrzebna.

Lemat 14.4 Za l´

o˙zmy, ˙ze x 6∈ F V (Γ) i ˙ze sta la c nie wyst

epuje w formule ϕ ani w ˙zadnej

formule ze zbioru Γ. Je´

sli Γ ` ϕ[x := c], to Γ ` ∀xϕ.

Dow´

od:

Przez indukcj

e ze wzgl

edu na d lugo´s´

c wyprowadzenia Γ ` ϕ[x := c] pokazu-

jemy, ˙ze Γ ` ϕ. A teraz wystarczy zastosowa´

c regu l

e generalizacji.

Je´sli Σ jest dowoln

a sygnatur

a, a C jest zbiorem sta lych nie nale˙z

acych do Σ, to przez

Σ ∪ C oznaczymy sygnatur

e powstaj

a z Σ przez do l

aczenie sta lych z C do Σ.

Twierdzenie 14.5 (Lemat Henkina) Niech ∆ b

edzie dowolnym niesprzecznym zbiorem

formu l sygnatury Σ i niech x 6∈ F V (∆). Istnieje zbi´

or sta lych C i funkcja c : F

Σ∪C

1−1

−→ C,

o tej w lasno´

sci, ˙ze zbi´

or formu l

∆ ∪ {ϕ[x := c(ϕ)] → ∀xϕ | ϕ ∈ F

Σ∪C

}

jest niesprzeczny.

Dow´

od: *

Konstruujemy przez indukcj

e sygnatury Σ

, zbiory sta lych C

i przyporz

adkowania c

1−1

−→ C

w ten spos´

ob aby niesprzeczne by ly zbiory formu l:

∆

= ∆ ∪ {ϕ[x := c

(ϕ)] → ∀xϕ | ϕ ∈ F

Zaczynamy od Σ

= Σ. Dla jednostajno´

sci naszej konstrukcji przyjmijmy jeszcze C

−1

= ∅ i c

−1

= ∅. Gdy

n > 0 to przyjmujemy Σ

= Σ

n−1

∪ C

n−1

Dla dowolnego n okre´

slamy teraz C

i c

: F

1−1

−→ C

jakkolwiek, byle tylko zachodzi ly zawierania

n−1

⊆ C

i c

n−1

⊆ c

. (Trzeba po prostu wzi

a´

c odpowiednio du˙zo nowych sta lych). Nale˙zy teraz

wykaza´

c niesprzeczno´

s´

c zbioru ∆

Je´

sli zbi´

or ∆

jest sprzeczny to na mocy Lematu 14.3 ma sko´

nczony podzbi´

or sprzeczny. Wybierzmy

minimalny taki podzbi´

or Θ. Skoro sam zbi´

or ∆ jest niesprzeczny to Θ − ∆ 6= ∅ i mo˙zemy napisa´

Θ = Θ

∪ {ϕ[x := c

(ϕ)] → ∀xϕ}.

Zbi´

or Θ

jest niesprzeczny z minimalno´

sci Θ. Mamy teraz Θ

, ϕ[x := c

(ϕ)] → ∀xϕ ` ⊥, sk

ad wynika

` ¬(ϕ[x := c

(ϕ)] → ∀xϕ). Ale to oznacza, ˙ze Θ

` ϕ[x := c

(ϕ)] oraz Θ

` ¬∀xϕ.

Sta la c

(ϕ) nie wyst

epuje w ˙zadnej formule zbioru Θ

, ani te˙z w samej formule ϕ. Z lematu 14.4 wynika

ec sprzeczno´

s´

Ostatecznie okre´

slamy C =

S{C

| n ∈ N} oraz c =

S{c

| n ∈ N}. Niesprzeczno´s´c naszego zbioru formu l

wynika z Lematu 14.3: w przeciwnym razie kt´

ory´

s ze zbior´

ow ∆

by lby ju˙z sprzeczny.

Twierdzenie 14.6 (o pe lno´

sci rachunku predykat´

ow) Je˙zeli Γ |= φ to Γ ` φ.

Dow´

od:

Przypu´s´

cmy, ˙ze Γ 6` φ. To znaczy, ˙ze zbi´

or ∆ = Γ ∪ {¬φ} jest niesprzeczny.

Bez straty og´

olno´sci mo˙zemy za lo˙zy´

c, ˙ze istnieje niesko´

nczenie wiele zmiennych nie wys-

epuj

acych w Γ ani w ϕ. (W przeciwnym razie nale˙zy

”

przenumerowa´

c” zmienne, u˙zywaj

np. tylko tych o parzystych numerach.) Niech C b

edzie zbiorem sta lych, o kt´

orym mowa

w lemacie Henkina i niech c b

edzie odpowiedni

a funkcj

a. Tak samo jak w przypadku

zdaniowym, rozwa˙zamy algebr

e Lindenbauma L, tym razem jednak jest to algebra formu l

sygnatury Σ ∪ C. Poza tym definicja algebry L jest dok ladnie taka sama.

Wa˙zn

a w lasno´sci

a naszej algebry jest to, ˙ze kwantyfikatory og´

olne odpowiadaj

a kresom

dolnym. Dok ladniej, dla dowolnej formu ly ϕ zachodzi r´

owno´s´

[∀xϕ]

∼

= inf{[ϕ[x := t]]

∼

| t ∈ T

Σ∪C

(∗)

Istotnie, [∀xϕ]

∼

≤ [ϕ[x := t]

∼

, bo ` ∀xϕ → ϕ[x := t] (aksjomat A7).

Pozostaje

ec sprawdzi´

c, ˙ze [∀xϕ]

∼

jest najmniejszym ograniczeniem. Przypu´s´

cmy wi

ec, ˙ze dla

dowolnego t zachodzi Γ ` ζ → ϕ[x := t]. Wtedy w szczeg´

olno´sci Γ ` ζ → ϕ[x := y],

gdzie zmienna y nie wyst

epuje ani w ζ ani w ϕ ani w Γ (tak˙ze jako zmienna zwi

azana).

A zatem Γ, ζ ` ϕ[x := y] i stosuj

ac generalizacj

e dostajemy Γ, ζ ` ∀yϕ[x := y]. Korzystaj

z aksjomatu (A7) otrzymujemy Γ, ζ ` ϕ[x := y][y := x]. Ale y nie wyst

epuje gdzie nie

trzeba, wi

ec przy podstawieniu ϕ[x := y] nie uleg la zmianie ˙zadna zmienna zwi

azana.

Zmienna y nie pojawi la si

e te˙z w zasi

egu kwantyfikatora wi

a˙z

acego x.

Zatem kolejne

podstawienie ϕ[x := y][y := x] tak˙ze nie spowoduje wymiany zmiennych i w konsekwencji
otrzymamy ϕ[x := y][y := x] = ϕ. Ostatecznie [ζ]

∼

≤ [∀xϕ]

∼

Podobnie jak w dowodzie Twierdzenia 14.1 b

edzie nam teraz potrzebny filtr maksymalny F ,

do kt´

orego nale˙zy [¬φ]

∼

. Ale teraz to jeszcze za ma lo. Chcemy, aby w naszym filtrze by ly

te˙z wszystkie elementy postaci [ϕ[x := c(ϕ)] → ∀xϕ]

∼

dla ϕ ∈ F

Σ∪C

. Istnienie takiego

filtru wynika z lematu Henkina. Nietrudno bowiem zauwa˙zy´

c, ˙ze je´sli Γ ∪ Π jest zbiorem

niesprzecznym, to {[ϑ]

∼

| ϑ ∈ Π} jest scentrowanym podzbiorem algebry L.

Potrzebujemy teraz modelu A i warto´sciowania v, spe lniaj

acego wszystkie formu ly z na-

szego filtru F . Na pocz

atek rozpatrzmy struktur

e term´

ow T , w kt´

orej relacje s

a okre´slone

tak: Je´sli r jest k-argumentowym symbolem relacyjnym sygnatury Σ, to dla dowolnych
term´

ow t

, . . . , t

i ∈ r

wtedy i tylko wtedy, gdy

[r(t

, . . . , t

)]

∼

∈ F .

W strukturze T okre´slimy teraz relacj

e ≈ warunkiem:

t ≈ u

wtedy i tylko wtedy, gdy

[t = u]

∼

∈ F .

Ta relacja jest kongruencj

a w T . Wynika to z aksjomat´

ow (A8) i (A9). Mo˙zemy wi

utworzy´

c struktur

e ilorazow

a A = T /

≈

. I to jest w la´snie model, kt´

orego potrzebujemy.

W tym modelu okre´slimy warto´sciowanie kanoniczne v(t) = [t]

≈

. Naszym celem jest teraz

nast

epujaca r´

ownowa˙zno´s´

A, v |= ψ

wtedy i tylko wtedy, gdy

[ψ]

∼

∈ F.

(∗∗)

Dow´

od (∗∗) przebiega oczywi´scie przez indukcj

e ze wzgl

edu na ϕ i jest podobny do dowodu

r´

ownowa˙zno´sci (5) wyst

epuj

acej w dowodzie Twierdzenia 14.1. Jedyny istotnie nowy przy-

padek wyst

epuje wtedy gdy ψ = ∀xϕ.

Za l´

o˙zmy najpierw, ˙ze [∀xϕ]

∼

∈ F . Na mocy (∗) mamy wtedy [ϕ[x := t]]

∼

∈ F dla

wszystkich t. Z za lo˙zenia indukcyjnego A, v |= ϕ[x := t] dla dowolnego t. Ale v(ϕ[x := t]) =

v(t)

(ϕ) = v

[t]

≈

(ϕ), a ka˙zdy element A jest postaci [t]

≈

. St

ad A, v

|= ϕ dla wszystkich a ∈

A czyli A, v |= ∀xϕ.

Implikacja odwrotna jest kluczow

a cz

e´sci

a naszego dowodu. Przypu´s´

cmy, ˙ze A, v |= ∀xϕ.

To znaczy, ˙ze A, v |= ϕ[x := t] dla dowolnego termu t i z za lo˙zenia indukcyjnego mamy
[ϕ[x := t]]

∼

∈ F . W szczeg´

olno´sci [ϕ[x := c(ϕ)]]

∼

∈ F . Ale do filtru F nale˙zy te˙z klasa

[ϕ[x := c(ϕ)] → ∀xϕ]

∼

. St

ad [∀xϕ]

∼

te˙z musi nale˙ze´

c do filtru.

Z warunku (∗∗) wynika od razu, ˙ze A, v |= Γ oraz A, v |= ¬φ, w szczeg´

olno´sci A, v 6|= φ.

A zatem Γ 6|= φ.

Wniosek 14.7 Zbi´

or formu l Γ jest spe lnialny wtedy i tylko wtedy, gdy jest niesprzeczny.

Teoria modeli

Wniosek 15.1 (Dolne twierdzenie Skolema-L¨

owenheima) Je´

sli zbi´

or formu l Γ (w j

zyku przeliczalnym) jest spe lnialny to ma model przeliczalny.

Dow´

od:

Skoro Γ jest spe lnialny, to jest niesprzeczny, wi

ec Γ 6` ⊥. Powtarzaj

ac kon-

strukcj

e z dowodu Twierdzenia 14.6 otrzymamy struktur

e term´

ow A, spe lniaj

a Γ. Wa˙zne,

˙ze no´snik |A| = T

≈

jest zbiorem przeliczalnym.

Uwaga:

W przypadku j

ezyka nieprzeliczalnego, gdy zbi´

or wszystkich term´

ow jest mo-

cy m, mo˙zna uog´

olni´

c powy˙zszy wniosek tak: ka˙zdy spe lnialny zbi´

or formu l ma model

mocy co najwy˙zej m.

Twierdzenie Skolema-L¨

owenheima by lo kiedy´s nazywane

”

paradoksem Skolema-L¨

owenhei-

ma”, z powodu swoich zaskakuj

acych konsekwencji. Przyk ladowo, wiadomo, ˙ze liczb rzeczy-

wistych jest nieprzeliczalnie wiele. Na mocy dolnego twierdzenia Skolema-L¨

owenheima ist-

nieje jednak przeliczalna struktura hP, +, ·, 0, 1i spe lniaj

aca dok ladnie te same zdania co

zwyk le cia lo liczb rzeczywistych hR, +, ·, 0, 1i. Struktury te s

a wi

ec ca lkowicie nieodr´

o˙z-

nialne z punktu widzenia zwyk lej logiki predykat´

ow.

Jeszcze bardziej zaskakuj

ace jest istnienie przeliczalnego modelu dla teorii mnogo´sci, tj.

struktury przeliczalnej hS, , =i, w kt´

orej dwuargumentowa relacja spe lnia dok ladnie

wszystkie twierdzenia wynikaj

ace z aksjomat´

ow teorii mnogo´sci. W strukturze S prawdziwe

a np. zdania stwierdzaj

ace istnienie zbior´

ow nieprzeliczalnych!

Twierdzenie 15.2 (o zwarto´

sci) Je´

sli Γ |= ϕ to istnieje taki sko´

nczony podzbi´

or Γ

⊆ Γ,

˙ze Γ

|= ϕ. W szczeg´

olno´

sci, je´

sli ka˙zdy sko´

nczony podzbi´

or zbioru Γ jest spe lnialny, to Γ

jest spe lnialny.

Dow´

od:

Natychmiastowa konsekwencja twierdzenia o pe lno´sci i Lematu 14.3.

Klasycznym zastosowaniem twierdzenia o zwarto´sci jest nast

epuj

ace twierdzenie:

Fakt 15.3 Je´

sli Γ ma dowolnie du˙ze modele sko´

nczone to ma model niesko´

nczony.

Dow´

od:

Niech {y

: i ∈ N} b

a r´

o˙znymi zmiennymi, nie wyst

epuj

acymi wolno w for-

mu lach z Γ. Rozpatrzmy zbi´

or formu l ∆ = {

”

¬(y

= y

)” | i 6= j}.

Je´sli Γ

⊆ Γ ∪ ∆ jest zbiorem sko´

nczonym to istnieje takie j, ˙ze dla i ≥ j, zmienne y

nie wyst

epuj

a w Γ

. Istniej

a takie A, v, ˙ze A, v |= Γ oraz |A| ma co najmniej j r´

o˙znych

element´

ow a

, . . . , a

j−1

. Niech v

edzie takim warto´sciowaniem, ˙ze v

) = a

dla i < j

oraz v

(x) = v(x) dla innych zmiennych x. Wtedy oczywi´scie A, v

|= Γ

Zatem ka˙zdy sko´

nczony podzbi´

or zbioru Γ ∪ ∆ jest spe lnialny. Z twierdzenia o zwarto´sci

tak˙ze zbi´

or Γ∪∆ jest spe lnialny. Ale ca ly zbi´

or Γ∪∆ mo˙ze by´

c jednocze´snie spe lniony tylko

w niesko´

nczonym modelu: je˙zeli bowiem A, v |= ∆, to wszystkie elementy v(y

) musz

a by´

r´

o˙zne.

Wniosek 15.4 Nie istnieje taki zbi´

or zda´

n Γ, ˙ze dla dowolnego modelu A:

A |= Γ

wtedy i tylko wtedy, gdy

|A| jest sko´

nczone.

Dow´

od:

Prosta konsekwencja Faktu 15.3

A zatem nie mo˙zna zdefiniowa´

c poj

ecia sko´

nczono´sci przy pomocy formu l pierwszego rz

edu.

Twierdzenie 15.5 (Twierdzenie Skolema-L¨

owenheima)

Je´

sli zbi´

or formu l Γ (w przeliczalnym j

ezyku) ma model niesko´

nczony to ma modele dowol-

nej mocy niesko´

nczonej.

Dow´

od:

Podobny do dowodu Faktu 15.3. Niech m ≥ ℵ

. Dodajemy do j

ezyka zbi´

or Y

nowych zmiennych (lub sta lych) o mocy m i rozszerzamy zbi´

or Γ o aksjomaty

”

¬(y = y

)”

dla wszystkich r´

o˙znych y, y

∈ Y . Z twierdzenia o zwarto´sci wynika

istnienie modelu mocy

co najmniej m. Co wi

ecej, nasz rozszerzony zbi´

or ma wy l

acznie takie modele. Z dolnego

twierdzenia Skolema-L¨

owenheima (por. uwaga po Tw. 15.1) wnioskujemy, ˙ze istnieje model

mocy r´

ownej m.

Ciekawym przyk ladem zastosowania twierdzenia o zwarto´sci jest twierdzenie Kfoury’ego-
Parka, kt´

ore przedstawimy na przyk ladzie (dla unikni

ecia d lugich definicji). Rozpatrzmy

nast

epuj

acy prosty while-program P (x) z jedn

a zmienn

a wej´sciow

a x:

begin y := c; while x 6= y do y := f (y) end

Niech A = hA, f

, c

i b

edzie dowolnym modelem sygnatury {f, c}. Dla warto´sci wej´sciowej

a ∈ A rozpatrzmy obliczenie P (a) programu P . Nietrudno zauwa˙zy´

c, ˙ze obliczenie P (a)

nie zatrzymuje si

e wtedy i tylko wtedy, gdy A, a |= ∆, gdzie ∆ sk lada si

e ze wszystkich

formu l postaci ¬(x = f (f (· · · (c) · · · )))).

Szukamy takiego zbioru zda´

n Γ aby dla dowolnej interpretacji A = hA, f

, c

i zachodzi lo

wynikanie:

Je´sli

A |= Γ

to obliczenie P (a) zatrzymuje si

e dla dowolnego a ∈ |A|.

Przypu´s´

cmy, ˙ze Γ jest zbiorem zda´

n o tej w lasno´sci. W´

owczas zbi´

or formu l

Γ ∪ {

”

¬(x = f

(c))” | n ∈ N}

jest zbiorem niespe lnialnym. (Oczywi´scie f

orym

symbol f wyst

epuje n razy.)

Na mocy twierdzenia o zwarto´sci istnieje sko´

nczony podzbi´

or niespe lnialny. Istnieje wi

takie n, ˙ze dla dowolnego modelu A spe lniaj

acego Γ, i ka˙zdego elementu a ∈ |A| zachodzi

jedna z r´

owno´sci a = c, a = f

), . . . , a = f

(· · · f

) · · · )), gdzie liczba iteracji

funkcji f

jest co najwy˙zej r´

owna n.

I to si

e nazywa g´

ornym twierdzeniem Skolema-L¨

owenheima.

A zatem ka˙zdy warunek wystarczaj

acy na to aby while-program by l totalny, tj. zawsze

e zatrzymywa l, w istocie okre´sla tak˙ze pewne ograniczenie g´

orne na liczb

e krok´

ow tego

programu. Nie spos´

ob wi

ec skonstruowa´

c zbioru formu l rachunku predykat´

ow, kt´

orego

spe lnienie by loby warunkiem koniecznym i wystarczaj

acym na zatrzymywanie si

e danego

while-programu, przy dowolnej interpretacji wyst

epuj

acych w nim symboli funkcyjnych.

Dowolno´s´

c interpretacji, o kt´

orej mowa powy˙zej, jest istotna.

Je´sli si

e ograniczy´

c na

przyk lad do standardowego modelu arytmetyki , tj. struktury N = hN, +, ·, 0, si (gdzie
s oznacza funkcj

e nastepnika) to mamy nast

epuj

ace

Twierdzenie 15.6 (tw. G¨

odla o reprezentacji) Dla dowolnego while-programu P (x),

w kt´

orym wyst

epuj

a tylko symbole funkcyjne +, ·, 0, s i symbol r´

owno´

sci, istnieje taka for-

mu la ϕ, ˙ze

N , n |= ϕ

wtedy i tylko wtedy, gdy obliczenie P (n) zatrzymuje si

e w N

Konflikt pomi

edzy tre´sci

a Twierdzenia 15.6 i twierdzenia Kfoury’ego i Parka jest pozorny.

Okazuje si

e, ˙ze w j

ezyku rachunku predykat´

ow nie mo˙zna zdefiniowa´

c jednoznacznie stan-

dardowego modelu arytmetyki.

Fakt 15.7 Istnieje niestandardowy model arytmetyki, tj. przeliczalna struktura

M = hM, ⊕, ⊗, 0, Si,

o takich w lasno´

sciach:

• dla dowolnego zdania ϕ, warunki N |= ϕ i M |= ϕ s

a r´

ownowa˙zne;

• struktury N i M nie s

a izomorficzne.

Dow´

od:

Niech Th(N ) oznacza zbi´

or wszystkich zda´

n prawdziwych w modelu N i niech

∆ sk lada si

e ze wszystkich formu l postaci x 6= s(s(. . . s(0) . . .)). Nietrudno pokaza´

c, ˙ze

ka˙zdy sko´

nczony podzbi´

or zbioru Th(N )∪∆ jest spe lnialny w modelu N przez dostatecznie

du˙z

a warto´s´

c x. Zatem ca lo´s´

c jest spe lnialna w pewnym modelu M przez pewne warto´s-

ciowanie v. Wtedy M spe lnia te same zdania co N , ale element v(x) nie ma odpowiednika
w modelu N , bo ka˙zdy element N mo˙zna otrzyma´

c z zera za pomoc

a nastepnika.

Arytmetyka Peano

Skoro nie mo˙zna zdefiniowa´

c jednoznacznie modelu standardowego, mo˙ze mo˙zna chocia˙z,

za pomoc

a odpowiednich aksjomat´

ow, scharakteryzowa´

c zdania kt´

ore s

a w nim prawdziwe?

Przez PA (od

”

Peano Arithmetics”) oznaczymy zbi´

or aksjomat´

ow z lo˙zony z formu l:

• ∀x¬(s(x) = 0)

• ∀x∀y (s(x) = s(y) → x = y);

• ∀x (x + 0 = x);

• ∀x∀y (x + s(y) = s(x + y));

• ∀x (x · 0 = 0);

• ∀x∀y (x · s(y) = (x · y) + x);

• ∀x (ϕ(x) → ϕ(s(x))) → (ϕ(0) → ∀x ϕ(x)),

gdzie ϕ(x) mo˙ze by´

c dowoln

a formu l

a. Pierwsze dwa aksjomaty m´

owi

a, ˙ze zero nie jest

nast

epnikiem ˙zadnej liczby i ˙ze operacja nast

epnika jest r´

o˙znowarto´sciowa (to gwaran-

tuje niesko´

nczono´s´

c). Kolejne dwa aksjomaty stanowi

a indukcyjn

a definicj

e dodawania,

a nast

epne dwa — indukcyjn

a definicj

e mno˙zenia. Na ko´

ncu mamy nie pojedy´

nczy ak-

sjomat, ale schemat aksjomatu, nazywany schematem indukcji . Zatem zbi´

or aksjomat´

Peano jest w istocie niesko´

nczony. Ale zbi´

or ten jest efektywny, tj. mo˙zna mechanicznie

ustali´

c co jest aksjomatem a co nie jest.

Oczywi´scie standardowy model arytmetyki jest modelem arytmetyki Peano:

N |= PA.

Inaczej m´

owi

ac, wszystkie konsekwencje aksjomat´

ow Peano (twierdzenia teorii PA) s

prawdziwe w standardowym modelu. A na odwr´

ot? Kiedy´s przypuszczano, ˙ze PA jest

teori

a zupe ln

a, tj. ˙ze ka˙zde zdanie prawdziwe w N jest twierdzeniem arytmetyki Peano.

Przypuszczenie to okaza lo sie fa lszywe dzieki odkryciu dokonanemu przez G¨

odla, a mia-

nowicie dzi

eki metodzie arytmetyzacji (numeracji G¨

odla). Wszystkie symbole j

ezyka aryt-

metyki numerujemy na przyk lad tak:

Symbol:

⊥

→

∀

(

)

. . .

Numer:

. . .

Ka˙zdemu ci

agowi znak´

ow, w tym ka˙zdej formule, dowodowi itp., mo˙zna teraz przypisa´

kod liczbowy. Je´sli przez #a oznaczymy numer znaku a, to kodem napisu

”

. . . a

” jest

liczba

Kod (a

. . . a

) = 2

· · · p

Teoria T jest zupe lna, wtedy i tylko wtedy, gdy dla dowolnego zdania ϕ (w j

ezyku tej teorii) zachodzi

albo T |= ϕ albo T |= ¬ϕ. Zbi´

or zda´

n prawdziwych w ustalonym modelu jest oczywi´

scie zawsze teori

zupe ln

gdzie p

oznacza n-t

a liczb

e pierwsz

a. Odkrycie G¨

odla oparte jest na obserwacji, ˙ze w las-

no´sci formu l arytmetyki mog

a by´

c wyra˙zane w j

ezyku samej arytmetyki jako teorioliczbowe

w lasno´sci kod´

ow. Zamiast np. m´

owi´

c o w lasno´sciach formu ly

”

∀x

((x

+ x

= 0) → ⊥)”,

mo˙zna m´

owi´

c o w lasno´sciach jej kodu, tj. liczby

Kod (∀x

((x

+ x

= 0) → ⊥)) = 2

Niech symbol n oznacza term s

(0). Oczywi´scie znaczeniem termu n w N jest liczba n.

Mo˙zna teraz np. napisa´

c tak

a formu l

e F (x) o jednej zmiennej wolnej x, ˙ze dla dowolnego

n ∈ N zachodzi r´ownowa˙zno´s´c

N |= F (n), wtedy i tylko wtedy, gdy n jest numerem formu ly o jednej zmiennej wolnej.

Oczywi´scie wiele rozmaitych w lasno´sci syntaktycznych mo˙zemy wyrazi´

c w podobny spos´

ob.

Przydatna jest np. formu la T (x, y) o takiej w lasno´sci:

N |= T (n, m), wtedy i tylko wtedy, gdy

• m jest numerem pewnej formu ly ζ(x) o jednej zmiennej wolnej,

• n jest numerem zdania ζ(m).

W skr´

ocie zapiszemy to tak:

N |= T (n, m), wtedy i tylko wtedy, gdy n jest numerem zdania ϕ

(m).

Nie ka˙zda w lasno´s´

c formu l mo˙ze jednak by´

c wyra˙zona w jezyku arytmetyki.

Twierdzenie 15.8 (tw. Tarskiego o niewyra ˙zalno´

sci prawdy) Nie istnieje formu la

wyra˙zaj

aca prawdziwo´

s´

c formu l w standardowym modelu, tj. taka formu la P (x), ˙ze

N |= P (n) wtedy i tylko wtedy, gdy n jest numerem zdania prawdziwego w N .

Dow´

od:

Dow´

od twierdzenia polega na wyra˙zeniu znanego paradoksu k lamcy

w j

ezyku

arytmetyki. Rozpatrzmy nastepuj

a formu l

T (x) ≡ ∃y (T (y, x) ∧ ¬P (y)).

W´

owczas N |= T (n) wtedy i tylko wtedy, gdy

• n jest numerem pewnej formu ly ζ(x) o jednej zmiennej wolnej,

• zdanie ζ(n) jest fa lszywe w N .

Istotnym problemem technicznym jest konieczno´

s´

c kodowania ci

ag´

ow liczb o nieznanej z g´

ory d lugo´

sci.

U˙zywa si

e w tym celu tzw. chi´

nskiego twierdzenia o resztach.

Stwierdzenie

”

To zdanie jest fa lszywe” nie mo˙ze by´

c ani prawdziwe ani fa lszywe.

Mniej ´sci´sle, ale pro´sciej:

N |= T (n) wtedy i tylko wtedy, gdy N |= ¬ϕ

(n).

Formu la T (x) te˙z ma numer, powiedzmy, ˙ze T (x) = ϕ

(x). A zatem mo˙zemy napisa´

N |= T (k) wtedy i tylko wtedy, gdy N |= ¬ϕ

(k).

Mo˙zemy to napisac z czystym sumieniem, bo warunek

• k jest numerem pewnej formu ly ζ(x) o jednej zmiennej wolnej,

jest oczywi´scie spe lniony. Ale przecie˙z ϕ

(k) to w la´snie formu la T (k). A zatem:

N |= T (k) wtedy i tylko wtedy, gdy N |= ¬T (k).

No jasne: zdanie T (k) stwierdza

”

Ja jestem fa lszywe!” Ze znanym skutkiem . . .

Twierdzenie G¨

odla o niezupe lno´sci arytmetyki otrzymamy po nieznacznej modyfikacji po-

wy˙zszego rozumowania.

Zamiast niemo˙zliwego do zdefiniowania pojecia prawdy, u˙zy-

jemy wyra˙zalnej w lasno´sci

”

mie´

c dow´

od w arytmetyce Peano”. Otrzymamy w ten spos´

zdanie Z, kt´

ore m´

owi:

”

Ja nie mam dowodu! ”.

Uwaga: Twierdzenie Tarskiego podpowiada rozstrzygni

ecie paradoksu k lamcy: Problem

le˙zy w niewyra˙zalno´sci poj

ecia “zdania prawdziwego”, tak˙ze w j

ezyku polskim. A skoro

pytamy o w lasno´s´

c, kt´

orej nie umiemy zdefiniowa´

c, to nie dziwmy si

e, ˙ze nie ma odpowiedzi.

Twierdzenie 15.9 (G¨

odla o niezupe lno´

sci) Istnieje takie zdanie Z w j

ezyku arytmetyki,

˙ze P A 6` Z i P A 6` ¬Z.

Dow´

od:

Post

epujemy jak w poprzednim dowodzie, u˙zywaj

ac formu ly P

(x) o w lasno´sci

N |= P

(n) wtedy i tylko wtedy, gdy n jest numerem zdania, kt´

ore ma dow´

od w PA.

Otrzymamy w ko´

ncu tak

a konkluzj

e: N |= T (k) wtedy i tylko wtedy, gdy PA 6` T (k).

Przyjmuj

ac Z = T (k), wnioskujemy, ˙ze ani Z ani ¬Z nie mo˙ze mie´

c dowodu w PA.

Za lo˙zenie P A ` Z prowadzi do sprzeczno´sci, bo je´sli P A ` Z to N |= Z. Ale za lo˙zenie
P A ` ¬Z te˙z prowadzi do sprzeczno´sci, bo mieliby´smy z jednej strony N |= ¬Z, a z drugiej
N |= Z. Uwaga: nietrudno zauwa˙zy´c, ˙ze N |= Z.

Istota twierdzenia G¨

odla polega nie na tym, ˙ze akurat PA jest niezupe lna. Je´sli zbi´

aksjomat´

ow PA rozszerzymy do innego efektywnego (!) zbioru aksjomat´

ow prawdziwych

w N to nadal b

edzie istnia lo zdanie niezale˙zne od tych aksjomat´

ow. Dow´

od pozostanie

prawie bez zmian. A wi

ec nie tylko PA, ale w og´

ole ka˙zda efektywnie zadana teoria musi

byc niezupe lna (je´sli tylko jest dostatecznie silna na to, aby da lo sie w niej zinterpretowa´

poj

ecia arytmetyczne).

Niech m b

edzie numerem zdania

”

0 = s(0)” i niech Con oznacza zdanie ¬P

(m). Zdanie to

wyra˙za niesprzeczno´s´

c arytmetyki Peano. Rozumowanie podobne do u˙zytego w dowodzie

Twierdzenia 15.9 mo˙zna. . . sformalizowa´

c w j

ezyku arytmetyki. Otrzymamy konkluzj

PA ` Con → Z,

gdzie Z jest zdaniem z Twierdzenia 15.9. W konsekwencji otrzymujemy:

Wniosek 15.10 PA 6` Con.

Niesprzeczno´sci arytmetyki Peano nie mo˙zna udowodni´

c na gruncie samej arytmetyki

Peano (chyba, ˙ze sama PA jest sprzeczna). Ta sama konkluzja dotyczy ka˙zdej dostatecznie
silnej teorii.

Rachunek sekwent´

Systemy dowodzenia twierdze´

n w stylu Hilberta maj

a pewne zasadnicze wady, zwi

azane

z tym, ˙ze g l´

ownym narz

edziem w dowodach jest regu la odrywania.

Po pierwsze, aby

wyprowadzi´

c nawet prost

a formu l

e, trzeba si

e pos lugiwa´

c formu lami znacznie d lu˙zszymi.

Po drugie, je´sli chcemy wyprowadzi´

c formu l

e ϕ z pomoc

a regu ly modus ponens

ϑ → ϕ, ϑ

to musimy odgadn

a´

c odpowiedni

a formu l

e ϑ, a nie mamy ˙zadnych wskaz´

owek co do jej

kszta ltu. Dlatego systemy w stylu Hilberta nie bardzo nadaj

a si

e do zastosowa´

n praktycz-

nych.

Rachunek sekwent´

ow, wprowadzony przez Gentzena, to inna metoda wyprowadzania twier-

dze´

n rachunku zda´

n lub rachunku predykat´

ow. Definicje s

a tu mo˙ze troch

e bardziej skom-

plikowane, ale za to otrzymujemy system, kt´

ory prawie nie ma wy˙zej wymienionych wad.

Sekwentem nazywamy napis postaci

”

, . . . , α

` β

, . . . , β

”, gdzie α

i β

a formu lami.

Zar´

owno m jak n mo˙ze by´

c zerem. Piszemy Γ, α lub α, Γ na oznaczenie ci

agu powsta lego

z Γ przez dopisanie α z ty lu lub z przodu. Za aksjomaty rachunku sekwent´

ow przyjmujemy

sekwenty postaci:

⊥ `

oraz

α ` α,

gdzie α jest dowoln

a formu l

a. (Czasem mog

a by´

c przyjmowane jeszcze dodatkowe aksjo-

maty, o czym za chwil

e. Inne definicje pozostaj

a wtedy bez zmian.) Regu ly rachunku

sekwent´

ow pozwalaj

a z jednego lub dw´

och sekwent´

ow-przes lanek wyprowadzi´

c sekwent-

konkluzj

Regu ly przedstawione w tabeli tworz

a system dowodzenia sekwent´

ow w rachunku predy-

kat´

ow. Tym razem nie korzystamy z mo˙zliwo´sci definiowania jednych sp´

ojnik´

ow przez

inne.

Warto bowiem zobaczy´

c w jaki spos´

ob regu ly rachunku sekwent´

ow zwi

azane s

z podstawowymi w lasno´sciami poszczeg´

olnych operacji logicznych.

Uwaga: (1) Regu ly rachunku sekwent´

ow mo˙zna znacznie upro´sci´

c, je´sli zamiast ci

ag´

formu l u˙zywa si

e zbior´

ow, tj. zaniedbuje si

e kolejno´s´

c formu l w ci

agu i ich powt´

orzenia.

Wtedy regu ly wymiany i skracania staj

a si

e niepotrzebne.

(2) Nasze regu ly dla kwantyfikator´

ow s

a sformu lowane w taki spos´

ob, aby nie by lo potrzebne

uto˙zsamianie ze sob

a alfa-r´

ownowa˙znych formu l. Przy za lo˙zeniu alfa-konwersji regu ly (P∀)

i (L∃) mo˙zna napisa´

c tak:

(P∀)

Γ ` ϕ, Σ

Γ ` ∀xϕ, Σ

(x 6∈ F V (Γ ∪ Σ))

(L∃)

Γ, ϕ ` Σ

Γ, ∃xϕ ` Σ

(x 6∈ F V (Γ ∪ Σ))

Definicja 16.1 Wyprowadzeniem sekwentu Γ ` Σ (lub dowodem formalnym w sensie
Gentzena) nazywamy drzewo

etykietowane sekwentami, kt´

ore ma nast

epuj

ace w lasno´sci:

• Korze´

n ma etykiet

e Γ ` Σ;

• Etykiety li´sci s

a aksjomatami;

• Etykiety pozosta lych wierzcho lk´

ow s

a otrzymane z etykiet ich nast

epnik´

ow (syn´

ow)

za pomoc

a regu l wnioskowania.

Uwaga: Jak powiedziano wy˙zej, kolejno´s´

c i powt´

orzenia formu l w sekwencie s

a istotne.

W praktyce jednak czasami pomijamy kroki dowodu polegaj

ace na zastosowaniu regu l

wymiany i skracania (stosujemy je domy´slnie), por. Przyk lad 16.2(3).

Przyk lad 16.2 (1) Dow´

od sekwentu ` ((p → q) → p) → p:

p ` p

(PO)

p ` q, p

(PI)

` p → q, p

p ` p

(LI)

(p → q) → p ` p

(PI)

` ((p → q) → p) → p

Tym razem nale˙zy sobie wyobra˙za´

c, ˙ze drzewo ma korze´

n na dole a li´

scie na g´

orze.

Os labianie:

Γ ` Σ

Γ, α ` Σ

(LO)

Γ ` Σ

Γ ` α, Σ

(PO)

Wymiana:

Γ, ϕ, ψ, ∆ ` Σ

Γ, ψ, ϕ, ∆ ` Σ

(LW)

Γ ` ∆, ϕ, ψ, Σ

Γ ` ∆, ψ, ϕ, Σ

(PW)

Skracanie:

Γ, ϕ, ϕ ` Σ

Γ, ϕ ` Σ

(LS)

Γ ` ϕ, ϕ, Σ

Γ ` ϕ, Σ

(PS)

Negacja:

Γ ` α, Σ

Γ, ¬α ` Σ

(LN)

Γ, α ` Σ

Γ ` ¬α, Σ

(PN)

Koniunkcja:

Γ, α ` Σ

Γ, α ∧ β ` Σ

(LK)

Γ, β ` Σ

Γ, α ∧ β ` Σ

Γ ` α, Σ

Γ ` β, Σ

Γ ` α ∧ β, Σ

(PK)

Alternatywa:

Γ, α ` Σ

Γ, β ` Σ

Γ, α ∨ β ` Σ

(LA)

Γ ` α, Σ

Γ ` α ∨ β, Σ

(PA)

Γ ` β, Σ

Γ ` α ∨ β, Σ

Implikacja:

Γ ` α, Σ

Γ, β ` Σ

Γ, α → β ` Σ

(LI)

Γ, α ` β, Σ

Γ ` α → β, Σ

(PI)

Kwantyfikator og´

olny:

Γ, ϕ[x:=t] ` Σ

Γ, ∀xϕ ` Σ

(L∀)

Γ ` ϕ[x:=y], Σ

Γ ` ∀xϕ, Σ

(P∀)

Kwantyfikator szczeg´

o lowy:

Γ, ϕ[x:=y] ` Σ

Γ, ∃xϕ ` Σ

(L∃)

Γ ` ϕ[x:=t], Σ

Γ ` ∃xϕ, Σ

(P∃)

ecie:

Γ ` α, Σ

Γ, α ` Σ

Γ ` Σ

(Ciach!)

Regu ly (P∀) i (L∃) maj

a nast

epuj

ace ograniczenie: zmienna y nie mo˙ze wyst

epowa´

c wolno

w ˙zadnej formule nale˙z

acej do Γ ∪ Σ.

(2) Dow´

od sekwentu p ∨ ¬p:

p ` p

(PN)

` ¬p, p

(PA)

` p ∨ ¬p, p

(PW)

` p, p ∨ ¬p

(PA)

` p ∨ ¬p, p ∨ ¬p

(PS)

` p ∨ ¬p

(3) Ten sam dow´

od zapisany w uproszczony spos´

ob (domy´slna wymiana i skracanie):

p ` p

(PN)

` ¬p, p

(PA)

` p ∨ ¬p, p

(PW + PA + PS)

` p ∨ ¬p

(4) Dow´

od sekwentu ∀xP (x) ` ¬∃x(P (x) → ⊥). Kilka razy domy´slnie u˙zyto regu ly (LW).

(LI)

P (x) ` P (x)

⊥ `

⊥, P (x) `

(LO)

(L∀)

P (x), P (x) → ⊥ `

(L∃)

∀xP (x), P (x) → ⊥ `

(PN)

∀xP (x), ∃x(P (x) → ⊥) `

∀xP (x) ` ¬∃x(P (x) → ⊥)

Uwaga: Poniewa˙z mamy do dyspozycji regu ly os labiania, wi

ec regu ly (PK), (LA), (LI)

oraz regu la ci

ecia mog

a by´

c r´

ownie dobrze wybrane tak:

Γ ` α, Σ

∆ ` β, Π

Γ, ∆ ` α ∧ β, Σ, Π

(PK1)

Γ, α ` Σ

∆, β ` Π

Γ, ∆, α ∨ β ` Σ, Π

(LA1)

Γ ` α, Σ

∆, β ` Π

Γ, ∆, α → β ` Σ, Π

(LI1)

Γ ` α, Σ

∆, α ` Π

Γ, ∆ ` Σ, Π

(Ciach1)

Natomiast inna mo˙zliwa posta´

c regu l (LK) i (PA) jest taka:

Γ, α, β ` Σ

Γ, α ∧ β ` Σ

(LK1)

Γ ` α, β, Σ

Γ ` α ∨ β, Σ

(PA1)

Rachunek sekwent´

ow Gentzena jest r´

ownowa˙zny systemowi dowodzenia w stylu Hilberta.

Twierdzenie 16.3 Nast

epuj

ace warunki s

a r´

ownowa˙zne:

1. Sekwent Γ ` β

, . . . , β

ma dow´

od w sensie Gentzena;

2. Formu la β

∨ · · · ∨ β

ma dow´

od w sensie Hilberta ze zbioru za lo˙ze´

n Γ;

3. Γ |= β

∨ · · · ∨ β

A zatem formu la α jest tautologi

a wtedy i tylko wtedy, gdy sekwent

”

` α” ma dow´

w sensie Gentzena.

Dow´

od:

(Szkic) Skorzystamy oczywi´scie z twierdzenia o pe lno´sci dla systemu Hilberta.

Mamy st

ad implikacj

e (3) ⇒ (2). Implikacja (1) ⇒ (3) jest latwa: wystarczy sprawdzi´

kolejno poprawno´s´

c wszystkich regu l. Dow´

od implikacji (2) ⇒ (1) te˙z nie jest trudny, bo

mamy do dyspozycji regu l

e ci

ecia. Na przyk lad maj

ac Γ ` α i Γ ` α → β, mo˙zna otrzyma´

Γ ` β w nast

epuj

acy spos´

ob:

(Ciach)

(PO)

Γ ` α → β

Γ ` α → β, β

(LI )

Γ ` α

β ` β

(LO )

Γ, β ` β

(LO )

Γ, α → β ` β

Γ ` β

W dowodzie powy˙zszego twierdzenia istotnie korzystali´smy z regu ly ci

ecia. Okazuje si

jednak, ˙ze ci

ecie nie jest niezb

edne. I w la´snie o to chodzi.

Twierdzenie 16.4 (o eliminacji ci

ecia) Ka˙zdy sekwent, kt´

ory ma dow´

od w rachunku

sekwent´

ow, ma te˙z taki dow´

od, kt´

ory nie u˙zywa regu ly ci

ecia.

G l´

owna zaleta dowod´

ow bez ci

ecia wynika z nast

epuj

acej w lasno´

sci podformu l: wszystkie

formu ly wyst

epuj

ace w przes lance dowolnej regu ly (poza ci

eciem) s

a podformu lami formu l

wyst

epuj

acych w konkluzji. Dlatego np. w dowodzie sekwentu

` α mamy do czynienia

tylko z podformu lami formu ly α. Dla danej formu ly α, latwiej wi

ec znale´

z´

c dow´

od w sensie

Gentzena ni˙z dow´

od w sensie Hilberta. Dlatego systemy zbli˙zone do rachunku sekwent´

a stosowane w praktyce.

Uwaga: Poj

ecie podformu ly danej formu ly, w przypadku formu l rachunku zda´

n oznacza

po prostu tak

a cz

e´s´

c danej formu ly, kt´

ora sama jest poprawnie zbudowan

a formu l

a. Zatem

ka˙zda formu la rachunku zda´

n ma tylko sko´

nczenie wiele podformu l. W przypadku formu l

z kwantyfikatorami jest niestety inaczej: za podformu l

e formu ly ∀xϕ musimy uwa˙za´

c ka˙zd

formu l

e postaci ϕ[x:=t], gdzie t jest dowolnym termem. Formu la z kwantyfikatorami ma

ec niesko´

nczenie wiele podformu l.

Z w lasno´sci podformu l wynika w lasno´s´

c konserwatywno´

sci logiki nad swoimi fragmentami:

je´sli formu la, w kt´

orej nie wyst

epuje jaki´s sp´

ojnik jest tautologi

a, to jej wyprowadzenie nie

wymaga regu l zwi

azanych z tym sp´

ojnikiem.

Klauzule Horna i regu la rezolucji

Klauzul

a nazywamy sekwent postaci p

, . . . , p

` q

, . . . , q

, gdzie p

, . . . , p

, q

, . . . , q

zmiennymi zdaniowymi, i m, n ≥ 0. Klauzul

a Horna nazywamy klauzul

e, dla kt´

orej m = 1.

Przypu´s´

cmy teraz, ˙ze mamy do czynienia tylko z klauzulami, ale za to opr´

ocz standard-

owych aksjomat´

⊥ `

oraz

α ` α,

mamy jeszcze jakie´s aksjomaty dodatkowe. Wtedy Twierdzenie 16.4 nie jest ju˙z prawdziwe,
ale mamy jego nast

epuj

a wersj

Twierdzenie 17.1 (o rezolucji) Ka˙zda klauzula, kt´

ora ma dow´

od w systemie Gentzena,

rozszerzonym o pewne klauzule jako aksjomaty, ma te˙z taki dow´

od u˙zywaj

acy tylko regu l

os labiania i regu ly ci

ecia, stosowanej zawsze tak, ˙ze lewa przes lanka jest aksjomatem:

, . . . , p

` s

, . . . , s

, q,

q, q

, . . . , q

` r

, . . . , r

, . . . , p

, q

, . . . , q

` s

, . . . , s

, r

, . . . , r

Regu la ci

ecia, ograniczona jak w Twierdzeniu 17.1, nosi nazw

e regu ly rezolucji . Jej

”

t lu-

maczenie” na styl Hilberta mo˙ze by´

c zapisane tak:

¬p

∨ · · · ∨ ¬p

∨ s

∨ · · · ∨ s

∨ q,

¬q ∨ ¬q

∨ · · · ∨ ¬q

∨ r

∨ . . . ∨ r

¬p

∨ · · · ∨ ¬p

∨ ¬q

∨ · · · ∨ ¬q

∨ s

∨ · · · ∨ s

∨ r

∨ · · · ∨ r

W uproszczeniu:

L ∨ q,

¬q ∨ P

L ∨ P

Je´sli rozwa˙zane s

a tylko klauzule Horna to regu la rezolucji jest stosowana w postaci:

, . . . , p

` q,

q, q

, . . . , q

` r

, . . . , p

, q

, . . . , q

` r

Zadanie, kt´

ore chcemy rozwi

azywa´

c, jest nast

epuj

ace: przyjmuj

ac pewne klauzule Horna

jako nowe aksjomaty, chcemy wywnioskowa´

c klauzul

e postaci ` p. Przyk ladowo: wiemy,

˙ze drapie˙zniki (D) maj

a w

asy (W ), i ˙ze ten kto ma w

asy i ogon (O) jest kotem (K). Mamy

drapie˙znika z ogonem i pytamy czy to jest kot.

Naszymi aksjomatami s

a wi

ec cztery klauzule Horna:

• W, O ` K;

• D ` W ;

• ` D;

• ` O.

Mo˙zna z nich latwo wyprowadzi´

c klauzul

e ` K. Jednak proces wyszukiwania potrzebnej

informacji jest lepiej widoczny, gdy zamiast dowodzi´

c ` K dodamy do aksjomat´

ow klauzul

”

K ` ” i spr´

obujemy wyprowadzi´

c sprzeczno´s´

c, tj klauzul

”

` ”. Mo˙zna to zrobi´c tak:

` O

` D

D ` W

W, O ` K

K `

W, O `

D, O `

O `

Zauwa˙zmy, ˙ze je´sli zamienimy w powy˙zszym dowodzie klauzule postaci Γ ` na Γ ` K to
otrzymamy dow´

”

wprost” klauzuli ` K.

Sekwent postaci

”

p ` ” nazywamy klauzul

a celu. Klauzul

e celu wraz z danymi aksjomatami

nazywamy programem logicznym. W naszym przyk ladzie mamy do czynienia z programem,
kt´

ory w cz

esto spotykanej notacji by lby zapisany jako pi

e´

c klauzul. S

a to dwie

”

regu ly”:

K :− W, O.

W :− D.

dwa

”

fakty”:

O :− .

D :− .

oraz cel:

:− K?

Wykonanie programu polega na sprowadzeniu pytania o K do pytania o W, O i ostatecznie
do fakt´

ow O i D. Interpreter j

ezyka programowania udzieli wtedy odpowiedzi

”

tak”. Nie

zawsze to musi by´

c natychmiastowe: w przypadku programu

A :− B.

C :− A.

C :− D.

D :− .

:− C?

pr´

oba sprowadzenia pytania o C do pytania o A nie prowadzi do sukcesu i konieczny jest

nawr´

ot. W og´

olno´sci mo˙ze by´

c gorzej: interpreter mo˙ze wpa´s´

c w p

etl

e i nie znale´

z´

c dowodu

cho´

c on istnieje. M´

owimy wtedy o niezgodno´sci interpretacji

”

procedurowej” programu

z jego interpretacj

”

logiczn

a”. Problem ten wyst

api na przyk lad dla programu:

A :− C.

C :− A.

C :− D.

D :− .

:− C?

Programowanie w logice

Programy logiczne w kt´

orych wyst

epuj

a tylko zmienne zdaniowe, maj

a umiarkowane zasto-

sowania. (Ostatecznie, kot jaki jest, ka˙zdy widzi.) Nale˙zy wi

ec metod

e rezolucji rozszerzy´

na j

ezyk rachunku predykat´

ow. Klauzule Horna to teraz sekwenty postaci A

, . . . , A

` B,

gdzie A

oraz B s

a formu lami atomowymi, a klauzula celu ma posta´

c C(x

, . . . , x

) ` ,

gdzie C ∈ Σ

R
k

. Wyprowadzenie sprzeczno´sci z takiej klauzuli celu, to tyle co dow´

od for-

mu ly ∃x

, . . . , x

C(x

, . . . , x

). W istocie dow´

od ten jest konstruktywny, tj. polega na

znalezieniu konkretnych term´

ow t

, . . . , t

, dla kt´

orych sekwent ` C(t

, . . . , t

) ma dow´

od.

Regu l

e rezolucji w postaci odpowiedniej dla logiki pierwszego rz

edu mo˙zna zapisa´

c tak:

, . . . , A

` B

C, C

, . . . , C

` D

S(A

), . . . , S(A

), S(C

), . . . , S(C

) ` S(D)

gdzie S jest takim podstawieniem, ˙ze S(B) = S(C). A zatem regu la rezolucji l

aczy w sobie

elementy regu ly ci

ecia i operacji podstawienia.

Program logiczny, jak poprzednio, sk lada si

e z regu l i fakt´

ow, oraz klauzuli celu, np:

• matka(Zofia, Helena) :− .

• matka(Helena, Barbara) :− .

• babka(x, y) :− matka(x, z),matka(z, y).

• :− babka(x, Barbara)?

Ustalenie, ˙ze Zofia jest babk

a Barbary polega na zastosowaniu rezolucji z u˙zyciem pod-

stawienia S(y) =Barbara; S(z) = Helena; S(z) = Zofia. Wynikiem dzia lania programu
jest sta la

”

Zofia”.

Inny przyk lad:

• silnia(0, 1) :− .

• silnia(n + 1, x) :− silnia(n, y), x = y ∗ (n + 1).

• :− silnia(4, x)?

Programy logiczne mog

a by´

c u˙zywane do rozwi

azywania takich samych zada´

n jak programy

imperatywne. R´

o˙znica polega na tym, ˙ze program logiczny nie okre´sla w pe lni czynno´sci

jakie maj

a by´

c wykonane dla znalezienia wyniku, a raczej podaje specyfikacj

e oczekiwanych

zwi

azk´

ow pomi

edzy wej´sciem i wyj´sciem, pozostawiaj

ac szczeg´

o ly interpreterowi.

Przyk lad 17.2 Zadanie polega na takim pokolorowaniu mapy, aby s

asiednie obszary mia-

ly r´

o˙zne kolory. Mapa jest taka:

+------------+------------+-------+
| A

B | C

+-----+-----+

| D

+------+

| E

F |

+-----+-----+

+------------+------------+-------+

Program w jednym z dialekt´

ow j

ezyka Prolog wygl

ada tak:

domains

kolor=symbol

predicates

mapa(kolor,kolor,kolor,kolor,kolor,kolor)
ok(kolor,kolor)
inne(kolor,kolor)

clauses

mapa(A,B,C,D,E,F) :- ok(A,B),ok(A,D),ok(A,E),ok(B,C),ok(B,D),

ok(B,F),ok(C,F),ok(D,E),ok(D,F),ok(E,F).

inne(czerwone,zielone).
inne(czerwone,niebieskie).

inne(zielone,niebieskie).
ok(X,Y) :-

inne(X,Y).

ok(X,Y) :- inne(Y,X).

Goal: mapa(A,B,C,D,E,F)

Rozwi

azania znalezione przez program:

A=czerwone, B=zielone, C=niebieskie, D=niebieskie, E=zielone, F=czerwone
A=czerwone, B=niebieskie, C=zielone, D=zielone, E=niebieskie, F=czerwone
A=zielone, B=niebieskie, C=czerwone, D=czerwone, E=niebieskie, F=zielone
A=zielone, B=czerwone, C=niebieskie, D=niebieskie, E=czerwone, F=zielone
A=niebieskie, B=czerwone, C=zielone, D=zielone, E=czerwone, F=niebieskie
A=niebieskie, B=zielone, C=czerwone, D=czerwone, E=zielone, F=niebieskie
6 Solutions

Podzi

ekowania

Za liczne uwagi, kt´

ore pomog ly usun

a´

c z tych notatek rozmaite b l

edy, dzi

ekuj

e Paniom Eli

epskiej i Magdzie Michalskiej oraz Panom Micha lowi Brzozowskiemu, Piotrowi Dittwaldowi,

Markowi Dopierze, Aleksandrowi Jankowskiemu, Micha lowi Jaszczykowi, Lukaszowi Kalbarczy-
kowi, Adamowi Kawie, Paw lowi K

epce, Krzysztofowi Kulewskiemu, Olkowi Na l

eczy´

nskiemu,

Filipowi Noworycie, Krzysztofowi Nozderko, Miko lajowi Radwanowi, S lawomirowi Sadziakowi,
Przemkowi Strzelczykowi, Bartoszowi Su lkowskiemu, Jankowi Urba´

nskiemu, Piotrowi Wojtale-

wiczowi, a tak˙ze prof. Piotrowi Zakrzewskiemu.

Ostatnia zmiana 25 sierpnia 2005 o godzinie 12: 20.

Wyszukiwarka

Podobne podstrony:
metodologia z logika id 295026 Nieznany
LOGIKA 6 id 271991 Nieznany
logika 7 id 271993 Nieznany
AK1 L 09 Logika id 53611 Nieznany (2)
def logika id 760893 Nieznany
logika1 id 272292 Nieznany
metodologia z logika id 295026 Nieznany
LOGIKA wyklad 5 id 272234 Nieznany
logika egzamin id 272077 Nieznany
logika KOLOS gr 3 id 272135 Nieznany
logika notatki 1 id 272149 Nieznany
LOGIKA KRASZEWSKI id 272137 Nieznany
logika KOLOS gr 3 id 272133 Nieznany
Logika test UJK 2 id 272176 Nieznany
logika KOLOS gr 1 id 272134 Nieznany
logika grupa2 id 272082 Nieznany
LOGIKA SCIAGA id 272164 Nieznany
LOGIKA wyklad 2 id 272229 Nieznany
logika ii cw id 272129 Nieznany

więcej podobnych podstron