Semantyka logiczna 12. 10. 2010r
Metalogika: Teorie pierwszego rzędu.
Teorie:
w znaczeniu intuicyjnym;
w znaczeniu logicznym (sformalizowane)
Na terenie logiki teorią lub systemem dedukcyjnym nazywamy dowolny zbiór formuł X spełniający warunek:
X=Cn(X)
Elemenety zbioru X nazywamy tezami lub
Z przyjętego określenia oraz definicji operacji Cn wynika, że
Dla dowolnej teorii X i dowolnej formuły A z języka teorii X zachodzi następująca zależność:
A e X (czyli A jest teza X) wtw A posiada dowód na gruncie teorii X.
A zatem w skład teorii X wchodzą wszystkie i tylko takie formuły, które są w niej dowodliwe:
Jeżeli A e X, to A ma dowód na gruncie X (tzn. każda teza danej teorii ma w niej dowód):
Intuicyjnie, teoria (w sensie logicznym) to system, w którym wszystko co było możliwe do rozstrzygnięcia zostało rozstrzygnięte. W teorii zbiór tez osiąga „stan nasycenia”.
Dygresja. Ponieważ operacja Cn jest zwrotna, tj. X _c Cn(X) więc warunkowi definiującemu teorię nadaje się niekiedy postać inkluzji: Cn(X) _c X (żąda on aby wszystkie formuły, które dają się udowodnić na gruncie X znajdowały się w X).
Teorie w znaczeniu logicznym:
Aksjomatyzowane:
- skończone
- nieskończone
Nieaksjomatyzowane
Wśród teorii wyróżnia się teorie aksjomatyzowane, tj. takie, które dają się przedstawić jako zbiory tych i tylko tych formuł, które można udowodnić w oparciu o pewne wybrane formuły - aksjomaty. Teorie aksjomatyzowalne są aksjomatyzowalne skończenie i nieskończenie.
Dygresja. Teoretycznie rzecz ujmując, aksjomaty można dobierać dowolnie. W praktyce jednak dąży się do tego aby teoria oddając intuicje formalizowanego problemu, nie miała pewnych niepożadanych własności. W przypadku teorii formalnych (takich jak artymetyka liczb naturalnych), wymaga się zwykle, aby zbiór aksjomatów był rekurencyjnie przeliczalny.
[rekurencyjnie przeliczalny - w prosty sposób, mechaniczny, potrafili odróżnić formuły, które są aksjomatami, od tych które nie są aksjomatami].
Ze względu na język, w którym teoria zostala sformułowana, teorie (w sensie logicznym) dzielimy na:
Teorie w znaczeniu logicznym:
rzędu zerowego (KRZ)
rzędu pierwszego (KRP)
rzędu drugiego (kwantyfikatory mogą wiązać litery predykatowe)
...
Przypomnienie:
Jeżeli X jest zbiorem formuł jakiegoś języka pierwszego rzędu oraz spełnia warunek:
X = Cn(Arp u X)
mówimy, że X jest teorią pierwszego rzędu, lub teorią elementarną.
Przypomnienie: CnL(X) = Cn(Arp u X)
Def 3. Teorią pierwszego rzędu. Zbiór formuł X nazywamy teorią pierwszego rzędu wtw X jest zbiorem formuł dowolnego języka formuł pierwszego rzędu oraz spełnia warunek:
X = CnL(X).
Elementy zbioru X nazywamy twierdzeniami/tezami tej teorii.
Najmniejszą teorią w dowolnym języku pierwszego rzędu J jest zbiór CnL( (/) ), czyli zbiór wszystkich tez KRP zapisanych w języku J. Ponieważ KRP jest nieskończenie aksjomatyzowalny, każda teoria oparta o KRP jest również nieskończenie aksjomatyzowalna.
Dygresja. Teoria pierwszego rzędu może być też oparta na innej niż klasyczna logice. Zamiast Arp będzie wówczas występował zbiór aksjomatów „bazowej” logiki.
Zbiór aksjomatów dowolnej teorii pierwszego rzędu możemy podzielić na dwie części:
aksjomaty logiczne, czyli aksjomaty KRP (charakteryzujące stałe logiczne: spójniki, kwantyfikatory i ewentualnie znak identyczności).
Aksjomaty pozalogiczne (specyficzne), czyli takie, które charakteryzują terminy specyficzne rozważanej teorii.
Niech X będzie teorią elementarną aksjomatyzowalną, zaś S jej aksjomatami specyficznymi.
Wówczas:
A jest teorią X wtw A posiada dowód w oparciu o zbiór Arp u S.
Symbolicznie A e X wtw A e CnL(S)
Tak więc:
KRP = CnL( (/) ) (=Cn(Arp))
KRPI = CnL(Aid)
KRPI posiada specyficzne aksjomaty związane z stałą logiczną - znakiem identyczności ( = ).
Aid = Aksjomaty identyczności.
_
Przypomnienie: A e CnL(X) wtw A e CnL(X).
Na mocy tego twierdzenia aksjomaty dowolnej teorii pierwszego rzedu, w szczególności aksjomaty pozalogiczne, można zapisywać w postaci formuł otwartych (tj. zawierających zmienne wolne), jak i zdań (tj. bez zmiennych wolnych). W obu przypadkach uzyska się teorię o dokładnie tych samych tezach. [można nie zapisywać kwantyfikatorów generalnych, na mocy tego twierdzenia].
Dygresja: Mówiąc dalej aksjomaty mamy na myśli aksjomaty pozalogiczne.
Batóg: s. 96 - 107.
Teoria mniejszości ( TM ). Jest ona nadbudowana nad KRPI.
Słownik języka TM oprócz zmiennych indywiduowych, spójników, kwantyfikatorów i nawiasów zawiera tylko dwa predykaty: = (znak identyczności), < (znak mniejszości).
[zwykle „=” zalicza się do stałych logicznych]
Termami TM są tylko zmienne indywiduowe.
Formułami atomowymi języka TM są wyrażenia postaci: xi = xj oraz xi < xj.
Zbiór formuł FMTM jest najmniejszym zbiorem takim, że:
(a) Każda formuła atomowa jest jego elementem;
(b) Jeżeli A, B e FMTM oraz xi jest zmienną indywiduowe, to:
~(A), (A) ^ (B), (A) v (B), (A) → (B), (A) ↔ (B), \-/xi(A), 3xi(A) e FMTM
[aksjomaty specyficzne w tej teorii ze znakiem mniejszości]
zbiór aksjomatów TM zawiera:
(a) Aksjomaty logiczne:
zbiór Arp, mówiąc dokładniej wszystkie formuły języka TM, które są reprezentowane przez schematy tworzące ów zbiór.
Zbiór Aid:
I1. x =x
I2. x = y → y=x
I3. X = y ^ y = z → x =z
I4. X = y ^ x < z → y < z
I5. X = y ^ z < x → z < y
[formuły otwarte = pominięte kwantyfikatory generalne]
(b) Aksjomaty pozalogiczne (Amn):
M1. X < y → ~(y < x) [asymetria]
M2. x < y ^ y < z → x < z [przechodniość]
M3. ~(x = y) → x < y v y < x [spójność] [x=y v x < y v y < x]
M4. x < y → 3z(x < z ^ z < y) [gęstość]
M5. ~3x\-/y(y = x v x < y) [nieistnienie elementu najmniejszego]
M6. ~3x\-/y(y = x v y < x) [nieistnienie elementu największego]
Dygresja. Aksjomaty M1 - M6 określają relację mniejszości jako gęsty porządek liniowy bez elementu najmniejszego i bez elementu największego. Jest to pełna aksjomatyka TM. Spełniają ją np. liczby rzeczywiste. Oczywiście można zrezygnować z pewnych aksjomatów, np. M4 [ale nie M1 - M3].
Z aksjomatów tych wyprowadza się dalsze twierdzenia teorii posługując siię przyjętymi regułami inferencyjnymi.
TM = CnL(Aid u Amn)
Dla przykładu dowód następującego twierdzenia:
T1. \-/x3y(y < x) [dla każdego elementu istnieje element od niego mniejszy]
Ax11 [KRP - dictum de singulum - A(x) → 3xA(x)]
1; reg. Transpozycji
M5
2,3 RO
M3
M3 → (~(y < x) → y = x v x < y) [teza KRP]
5, 6 RO
7 RG
\-/y(7) → [Teza KRP (pr. Rozkładu \-/ wzgl. → )]
8, 9 RO
10 Reg. Transpozycji
11 RO
teza KRP (pr. De morgana)
12, 13 RO
14 RG
Arytmetyka liczb naturalnych Peano (PA). Jest ona nadbudowana nad KRPI.
Słownik języka PA oprócz zmiennych indywiduowych (ZI), spójników, kwantyfikatorów i nawiasów zwiera:
predykat identyczności: =
stałe nazwowe: 0 (zero)
symbole funkcyjne: s, +, *
(s jest symbolem funkcyjnym 1-argumentowym interpretowanym jako następnik; oznacza on funkcje określoną wzorem S(x) = x+1; znaki + i * są symbolami funkcyjnymi 2 - argumentowymi, interpretowanymi jako „plus” i „razy”).
Zbiór termów TMPA jest najmniejszymi zbiorem, takim że:
(a) ZI u {0} _c TMPA
(b) jeżeli t e TMPA, to s(t) e TMPA np. s(y); s(0)
(c)jeżeli t1, t2 e TMPA, to (t1 + t2), (t1 * t2) e TMPA np. x+y; x+0; x*y; x*0.
Formułami atomowymi języka PA są wyrażenia postaci t1 = t2, gdzie t1, t2 e TMPA. [np. z = s(y); x+y = x*z]
Zbiór formuł FMPA jest najmniejszym zbiorem takim,że:
(a) każda formuła atomowa jest jego elementem
(b) jeżeli A,B e FMPA oraz xi jest zmienną indywiduową, to:
~(A), (A)^(B), (A)v(B), (A) → (B), (A) ↔ (B), \-/xi(A), 3xi(A) e FMPA
Zbiór aksjomatów PA zawiera:
Aksjomaty logiczne:
Zbiór Arp; mówiąc dokładniej wszystkie formuły języka PA, które są reprezentowane przez schematy tworzące ów zbiór.
Zbiór Ais (ax. Identyczności)
I1. x=x
I2. x=y → y=x
I3. x=y ^ y=z → x=z
I4. x=y → s(x)=s(y)
I5. x=y → z +x = z+y
I6. x=y → x+z=y+z
I7. x=y → z*x = z*y
I8. x=y → x*z=y*z
[cztery ostatnie to ax. Ekstensjonalne].
Dygresja. Zauważmy, że jeśli x jest zmienną wolną w formule A, t jest dowolnym termem podstawialnym do A w miejsce x i A jest tezą, to również A(x/t) jest tezą. Istotnie załóżmy, że A(x) jest tezą. Dalej rozumujemy następująco:
A(x)
\-/xA(x) [na mocy RG]
\-/xA(x) → A(x/t) [dictum de omni]
A(x/t) [na mocy RO]
stąd aksjomaty dla identyczności można zapisać używając - zamiast zmiennych - liter oznaczających dowolne termy (np. t, t1, t2, t3, …, tn)
Aksjomaty pozalogiczne (Aln):
N1. s(x) = s(y) → x=y [różnowartościowość następnika]
[x =/= y → s(x) =/= s(y) ]
N2. ~(0 = s(x)) [0 jest liczbą najmniejszą, tj. nie jest następnikiem]
N3. x + 0 = x [N3 i N4 to indukcyjna def. Dodawania]
N4. x + s(y) = s(x+y)
N5. x*0 = 0 [N5 i N6 to indukcyjna def. Mnożenia]
N6. x*s(y) = x*y+x
N7. {A(0) ^ \-/x[A(x) → A(s(x))]} → \-/xA(x) [zasada indukcji matematycznej]
[N7 - zasada indukcji matematycznej: „A(0)” powstaje z formuły A(x) gdy pod x podstawimy 0. A(s(x)) powstaje przez podstawienie pod x - s(x).]
z aksjomatów tych wyprowadza się dalsze twierdzenia teorii posługując się przyjętymi regułami inferencyjnymi [RO i RG].
PA = CnL(Aid u Aln)
Dygresja. Wzór N7 to schemat nieskończenie wielu aksjomatów podobnie zbudowanych. Sens N7 jest można wyjaśnic następująco: Jeżel
liczba 0 ma pewną własność (opisaną przez formułę A)
oraz
zawsze jeśli jakaś liczba ma tę własność, to musi ją mieć też liczba następna,
to każda liczba naturalna ma tę własność.
A zatem, jeśli formuła A opisuje jakąś własność dotyczącą liczb naturalnych to na mocy aksjomatu N7 zastosowanego do A, wystarczy udowodnić „wewnątrz arytmetyki” formułe A(x/0) (tzw. pierwszy krok indukcji) oraz formułę \-/x[A(x) → A(x/s(x))] (tzw. drugi krok indukcji), by orzec że \-/xA(x) jest tezą PA.
(aksjomaty bez N7 tworzą tzw. arytmetykę Robinsona - w literaturze zapisuje się jako Q)
Dygresja. Z przyjętych aksjomatów wynika, że każda liczba ma dokładnie jeden następnik. Majjąc liczbę 0, możemy zdefiniować kolejne liczby naturalne, przyjmując 1 =s(0), 2 = s(s(0)), ogólnie n = s(...s(0)...)
Przykład. Przykładem dowodu wykorzystującego N7 jest dowód formuły:
\-/x(0+x=x).
Szkic dowodu: Zauważmy, że:
0 + 0 = 0 jest wnioskiem z N3
0 + x = x → 0 + s(x) = s(x) jest twierdzeniem, bo:
0 + x = x → s(0+x) = s(x) jest wnioskiem z I4, a
0 + s(x) = s(0+x) jest wnioskiem z N4.
Zatem przez RG otrzymujemy:
\-/x(0 + x = x → 0 + s(x) = s(x))
Stąd na mocy N7 i RO otrzymujemy:
\-/x(0 + x = x)
co kończy dowód.