09.pdf

4. SYSTEMY SFORMALIZOWANE

IARYTMETYKA

4.1. POJĘCIESYSTEMU SFORMALIZOWANEGO

Dążnośćdojasnościwypowiedziipewnościtwierdzeńjestcelem

naukiodsamychjejpoczątków.Ponadwątpliwośćceletewnajwyż-

szym stopniu udało się osiągnąć naukom dedukcyjnym. Odpowiedź

napytanie,jaknależypostępować,abywmożliwienajwyższymstop-

niuzrealizowaćtenideał,jakwwypadkuwszystkichinnychnauk,tak

iwwypadkulogiki imatematyki, dajemetodologia naukdedukcyj-

nych,awszczególnościmetodologiamatematyki 80 Swojąszczególną

pozycjęnaukidedukcyjnezawdzięczająwynalezieniusystemudeduk-

cyjnego.

Aksjomatyczneujęcieteoriiniejestczymśnowym.Historycznie

pierwszym systemem aksjomatycznym była geometria matematyka

greckiego Euklidesa (ok. 365– ok. 300 p.n.e.). Stanowiła ona pod-

sumowanietrzystulatdziałalnościmatematyków greckichizarazem

fundamentdalszego rozwojumatematyki. SamEuklidespozostawał

jeszczepodwyraźnymwpływemPlatona,założycielaAkademiiiuwa-

żał,żenaukaniemanicwspólnegozpraktyką.ZaPlatonemuznawał

też metodę aksjomatyczną za właściwą dla matematyki. Konstruk-

cjaksiąg Elementów ,rozpoczynanieoddeﬁnicjipojęćswoistychoraz

właściwych postulatów i aksjomatów wyraźnie wskazuje na wpływ

Arystotelesa i jego metodologii wyłożonej w Analitykach wtórych .

80 Por. Tarski [1994], s.123–124; a na temat związków z terminami „metalo-

gika”, „metamatematyka” i podobne zob. s. 147 oraz przypisy. Termin „meta-

matematyka” został wprowadzony przez D. Hilberta na oznaczenie badań nad

systemami sformalizowanymi. Najważniejszymi zagadnieniami metamatematyki

są: niesprzeczność,zupełność i rozstrzygalnośćteorii.

230

4. SYSTEMY SFORMALIZOWANEI ARYTMETYKA

Przezprawie2200lat,doXIXw.,jegowykładgeometrii, Elementy ,

byłypowszechnieużywanympodręcznikiem 81 . Dlamatematykówinie

tylko dla nich, były wzorem. Stanowiły paradygmat matematyki 82 .

DlaEuklidesageometriamiałabyćnaukąopisującąrealnąprzestrzeń.

Jej aksjomaty były traktowane jako prawdy intuicyjnie oczywiste,

którychnawetniepowinnosiędowodzićczyuzasadniać.Byłato„la

science de la v´erit´e” (Poincar´e). Jej twierdzenia oceniane zaś były

wkategoriach prawdyifałszu 83 . Istotnypostępnastąpiłdopieropo

1890 r., gdy postać systemu aksjomatycznego uzyskały arytmetyka,

dzięki pracom włoskiego matematyka Peano 84 igeometria,cobyło

osiągnięciemHilberta 85 .

Pojęcie systemu aksjomatycznego podlegałozmianom 86 . Na sa-

mym początku aksjomaty były zdaniami uznanymi za intuicyjnie

oczywiste. Zawierały one pojęcia pierwotne , czyli pojęcia niezdeﬁ-

niowane.Miałyonebyćintuicyjniejasne.Znaczeniatychpojęćbyły

charakteryzowaneprzezaksjomaty.Współczesnerozumieniesystemu

aksjomatycznego określa się jako system sformalizowany .Pierwsze

próbyformalizacjipodjąłFrege.Jegopodstawowedziełologiczne Be-

griﬀsschrift,einederarithmetischennachgebildeteFormelsprachedes

reinenDenkens (1879)zawierałopierwszywdziejachsformalizowany

system aksjomatyczny, jakim był implikacyjno-negacyjny rachunek

81 Liczbą wydańitłumaczeń Elementy ustępujątylko Biblii .

82 Matematyka była wzorem nauki dla racjonalizmu kartezjańskiego. Wspo-

mnijmy tutaj choćby prace ﬁlozoﬁczne pisane more geometrico jak np. najważ-

niejszytraktatB.Spinozy Ethicaordinegeometricodemonstrata .„Takmatema-

tycznej postaci ﬁlozoﬁanie miałaani przed Spinozą, ani ponim”. –zob. Tatar-

kiewicz[1970],t.II,s.71.

83 Zmiana poglądów nastąpiła w związku z powstaniem systemów geometrii

nieeuklidesowych. Od tego czasu geometria przestała być nauką«empiryczną» i

stałasięnaukąabstrakcyjną.

84 Mamytunauwadzepracęzbiorową,którejredaktoremigłównymautorem

jestPeano, Formulairedemath´ematiques ,Torino1895-1908.Dodajmyjeszcze,że

zasługąPeanojeststworzeniebardzowygodnejiprzejrzystejsymbolikilogicznej

imatematycznej,którazniewielkimi zmianami–wprowadzonymigłównieprzez

Russella –przetrwaładodziś.

85 Mamytunauwadzejegosłynnedzieło GrundlagenderGeometrie ,Leipzig-

-Berlin,1899.

86 Wsprawiemetodologicznegopunktuwidzeniazob.Ajdukiewicz[1960].

4.1. POJĘCIE SYSTEMU SFORMALIZOWANEGO

231

zdań.

Jeśli w początkach aksjomatyzacja sprowadzała się w zasadzie

do wskazania pewnych zdań-pewników nie wymagających dowodze-

nia,pozostawiającresztęintuicjipoprawności,towspółcześnieintu-

icyjność została wyeliminowana całkowicie, jedyne co potrzebne to

umiejętność rozróżniania napisów jako równokształtnych, bądź nie-

równokształtnych.

Pierwszymetapemformalizacjiteoriibędziewięc formalizacjaję-

zyka tejteorii.Teoriematematyczneformułowanesązwyklewjęzyku

naturalnym.Korzystasięzjegosłownictwa,uzupełniającjejedynie

o specyﬁczne terminy, które są zwykle tworzone według jego norm

słowotwórczych.Dotegodochodząwygodnesymbole,umożliwiające

krótkiiprzejrzystyzapis.Wyrażeniabudujesięzgodniezzasadami

gramatycznymi.Ocenapoprawnościjęzykowejnależydokompetencji

użytkownikategojęzykajakojęzykacodziennego.Wwypadkujęzyka

sformalizowanego zadanyjest słownik poprzezwskazaniewszystkich

itylko«wyrazów»,symbolipodstawowych,a gramatyka opisanajest

«przepisami», regułami na tworzenie wyrażeń poprawnie zbudowa-

nych : ciąg elementów słownika jest poprawnie zbudowanym wyra-

żeniem danego języka wtedy i tylko, gdy jest utworzony zgodnie z

tymiregułami. 87 Regułysątegorodzaju,żeichstosowaniewymaga

tylkoumiejętnościidentyﬁkacjiwyrażeńrównokształtnych.Zzasady

słownikskładasięzeznaków stałych logicznych , symboli nazwowych

(stałychizmiennych) , literpredykatowych , literfunkcyjnych oraz na-

wiasów jakoznakówinterpunkcyjnych.Wsłownikuwyróżniasię stałe

specyﬁczneteorii ,czylisymbolenapojęciapierwotneformalizowanej

teorii.Regułygramatycznesąróżnieopisywane.Badasięróżnegra-

matykiformalne.

Fakt,żesystemmacharakterformalnyiżerozwijającgoignoru-

jemyznaczeniewyrażeńnieoznacza,żewypowiedzimatematycznesą

pozbawione treści. „Jeśli ktoś przy konstruowaniu nauki zachowuje

siętak,jakgdybynierozumiałznaczeniaterminówtejnauki,tonie

jest to jednoznaczne z odmawianiem tym terminom jakiegokolwiek

87 Gdy kontekst wskazuje, że chodzi o wyrażenie poprawnie zbudowane i jest

jasneojakijęzykchodzi,mówisiępoprostuowyrażeniu.

232

4. SYSTEMY SFORMALIZOWANEI ARYTMETYKA

sensu. Zdarza się, co prawda, że budującpewną teorię dedukcyjną,

nieprzypisujemyjejterminomokreślonegoznaczeniaiodnosimysię

do nich jak do symboli zmiennych. [ ... ] Ale sytuacja tego rodzaju

[ ... ]zdarzasiętylko,gdydysponujemykilkomamodelamiczyinter-

pretacjamidlasystemuaksjomatycznegotejnauki,awięcjeślimamy

szereg możliwości przypisania konkretnego znaczenia terminom wy-

stępującymwtejnauce,ale[ ... ]żadnejztychmożliwościniechcemy

wyróżnić. Taki natomiast system formalny, dla którego nie potraﬁ-

libyśmy podać ani jednego modelu, przypuszczalnie nikogo by nie

interesował 88 .”

Opisującjęzyk,wzbiorzewyrażeńwydzielasięzdania.Spośród

zdańwyróżniasię aksjomaty ,którebezdowoduprzyjmowanesąjako

twierdzenia danego systemu. Nie wymaga się, by zdania te były in-

tuicyjnie oczywiste, jak to miało miejsce w wypadku niesformalizo-

wanegosystemuaksjomatycznego. Aksjomatyspecyﬁczne toteaksjo-

maty,którewyróżniajądanysystemsformalizowany spośródinnych

systemówsformalizowanych.Sąoneodpowiednikamiaksjomatównie-

sformalizowanegosystemuaksjomatycznego.Pozostałeaksjomatysą

aksjomatamiprzyjętegosystemulogiki.

Określeniezasadiregułdowodzeniajestnastępnymetapemfor-

malizacjiteorii.Intuicjapoprawnościrozumowańzostajezastąpiona

przez reguły wyprowadzania twierdzeń. Dowód formalny to zwykle

skończony ciągformułdanegojęzyka,któresąbądź(specyﬁcznymi)

aksjomatami rozważanej teorii, bądź tezami przyjętej logiki, bądź

dająsięznichwyprowadzićzapomocąprzyjętychregułdowodzenia.

Zdanie, dla którego istnieje dowód formalny to twierdzenie .Aksjo-

matylogiczneiregułydowodzeniato aparatlogiczny systemusforma-

lizowanego. Dla stwierdzenia poprawności dowodu wystarcza umie-

jętnośćidentyﬁkowaniawyrażeńrównokształtnych,czyliwyrażeńnie

różniącychsiękształtem.

Odrzucając z teorii sformalizowanej jej aksjomaty specyﬁczne

otrzymujemy pewien formalny system logiczny. W systemie tym

mamyaksjomatyiregułydowodzenia.Możemywięctę«resztę»trak-

tować jak system sformalizowany. W naturalny sposób nasuwa się

88 Zob.Tarski[1994],s.135.

4.1. POJĘCIE SYSTEMU SFORMALIZOWANEGO

233

pytanie, czy taki system pozwala udowodnić wszystkie i tylko tezy

logiczne.Natopytaniedajeodpowiedźjednoznajważniejszychtwier-

dzeńlogikimatematycznejudowodnioneprzezK.G¨odlaw1930r.Od-

powiedźta jestpozytywnaw wypadkuteorii elementarnych. Teorie

elementarne tozaś takie teorie, któreniezawierają zmiennych wyż-

szych typów , czyli zmiennych,których wartościami mogą byćprzed-

miotyniebędąceindywiduami,jakzbioryindywiduów,relacjewzbio-

rzeindywiduów,relacjewklasiezbiorówindywiduówitd.

W teorii sformalizowanej wyraźnie wskazane są również reguły

deﬁniowania 89 . Intuicjapoprawnoścideﬁnicjizostajezastąpionaprzez

regułyformalne.Pojęciapierwotnescharakteryzowanesąprzezaksjo-

maty,wszystkieinnepojęciawprowadzanesąnadrodzedeﬁnicji.

Możliwość formalizacji systemu ma znaczenie teoretyczne, w

szczególności dla metamatematycznych badań systemów aksjoma-

tycznych.Dlatychcelówwystarczazwyklesamopisformalizacji.W

praktyce z zasady nie spotykamy się z wykładem w pełni sformali-

zowanych teorii,conajwyżej–itozwyklejakoilustracja–zjakimś

fragmentem.Powodemtegojestniezwykłarozwlekłośćinieczytelność

dlazwykłegoczytelnikatakwyłożonejteorii 90 .

Mającjakąśteorię(zbiórwszystkichitylkozdańprawdziwychw

określonej dziedzinie) możemy pytać się, czy teoria ta daje się zak-

sjomatyzować,czyjest aksjomatyzowalna .Czymożliwejestwybranie

spośród jej zdań takich, z których dadzą się udowodnić wszystkie i

tylkopozostałezdaniaprawdziwe?Okazałosię–dowiódłtegoG¨odel

– że bogatsze teorie (te które zawierają arytmetykę liczb natural-

nych)niesąaksjomatyzowalne.Biorącjakikolwiekzestawzdańtaki,

żemożnarozstrzygnąć,czydanezdaniejestaksjomatemniezbudu-

jemy systemu, którego zbiór twierdzeń byłby równy zbiorowi zdań

prawdziwychteorii.

Teoriasformalizowanataka,żedladowolnegozdania(formułynie

zawierającejzmiennychwolnnych)sformułowanegowjęzykutejteo-

riiono,bądźjegonegacjajesttwierdzeniemteoriito teoria zupełna .

89 Jakjużwcześniej byłaotymmowa,formalizacjadeﬁniowaniajestosiągnię-

ciemStanisławaLeśniewskiego.

90 Por.przypisnas.140,Tarski[1994].

Plik z chomika:

Inne pliki z tego folderu:

Inne foldery tego chomika: