Formalizmy

Wśród wielu przyjemności, frajd i uciech jakimi usłane było i jest moje dotychczasowe życie, poczesne miejsce zajmuje praca w pewnej, nie istniejącej już firmie na B, gdzie za więcej niż godziwe pieniądze, z jednym tylko wyznaczonym celem - stworzyć coś olśniewającego - mogłem oddawać się przez parę miesięcy studiom i eksperymentom, za które nikt inny by mi nigdy nie zapłacił złamanego grosza. Oczywiście wszystko w nadziei że, ów szczytny cel zostanie osiągnięty.
Zagadnienia z jakimi walczyłem w owym czasie (pomijając wewnątrzkorporacyjną politykę, ową nieodłączną, mroczną towarzyszkę wszelkich dzieleń skór na niedźwiedziach) to software'owe systemy agentowe, protokoły komunikacyjne i socjalne owych agentów i przede wszystkim różnorakie wykorzystanie ontologii formalnych do komunikacji między agentami, organizacji ich społecznego życia i bazy dla ich rozumowania o świecie jaki im, biednym niewolnikom, chcieliśmy stworzyć.
Pojęcie ontologie formalne, nie jest do końca formalne i może znaczyć wiele rzeczy. Ogólnie jednak są to pewne teorie wyrażone w jakimś sformalizowanym języku plus pewne reguły wnioskowania. Ontologiczną częścią (tym co istnieje z punktu widzenia owych teorii) są stałe, predykaty, funkcje itp. Przy ich użyciu za pomocą stosownych operatorów logicznych i predykatów pochodzących z języka w którym zapisujemy ontologie (który dla niej samej staje się metajęzykiem) możemy opisać prawa świata którego formalną reprezentację konstruujemy. Na ogół czynimy to w ten sposób by zamodelować jakiś fragment istniejącego świata (zawodowiec w swoim żargonie powiedziałby, że dokonujemy konceptualizacji owego fragmentu), jakiejś konkretnej dziedziny, aktywności czy czegoś w tym rodzaju. Potem dzięki możliwościom formalnego wnioskowania, możemy w pewien sposób mechanizować rozumowania w naszej teorii - czy to by uzyskać rygorystyczne dowody pewnych własności owego świata, czy to po to, by mogła naszej konceptualizacji używać maszyna lub maszyny.
Zabawy z ontologiami formalnymi w świecie komputerów to względnie nowa rzecz. Wiązało się z nimi w czasach (historia nieustannie przyspiesza skoro o czymś co miało miejsce sześć lub siedem la temu mówimy "w owych czasach") wielkie, częściowo tylko spełnione nadzieje. Wokół tej idei osnuta była cała koncepcja "semantic web" promowana przez Berner's Lee i W3 Consortium, języki do modelowania ontologii jak DAML lub OIL, projekty jak SUO , czy w końcu technologie związane z serwisami internetowymi jak UDDI. Nie wspomnę już o dawniejszych i fantastycznych rozmachem pomysłach z kręgu sztucznej inteligencji w rodzaju Cyc.
Oczywiście nic tu nie jest naprawdę nowe. Formalizacja wnioskowań znana była już Arystotelesowi, który zostawił kodyfikację sylogizmów (fragmentu logiki zaledwie)- ziarnko z którego po stuleciach i perturbacjach wyrosła współczesna logika symboliczna.
Euklides dokonał formalnej konceptualizalizacji intuicji przestrzennych i praktycznej wiedzy mierniczej tworząc swój system geometrii. Gdyby go zapisać w sformalizowanym języku (co uczynił np. Hilbert) mielibyśmy nowoczesną formalną teorię matematyczną - z pewnego punktu widzenia więc ontologię formalną.
Patrząc na geometrię - najstarszą tak porządnie rozwiniętą naukę formalną - można dostrzec zawiłości związane z modelowaniem rzeczywistości w języku. Np. byty które egzystują w świecie geometrii Euklidesa to punkty i proste. Nie mające odnośnika w rzeczywistości którą geometria stara się z pewnego punktu widzenia opisać, żadnych odnośników. Możemy scierpieć dzisiaj, bogatsi o bez mała dwa tysiące lat rozwoju matematyki, że są to byty abstrakcyjne - ale rozwiązując zadanie geometryczne i tak będziemy bazgrać na papierze figury. Co więcej, pojęcie punktu, choć łatwo przystaniemy na to, że jest to dobra i zręcznie dobrana intuicja - dręczy nas w różnych tam paradoksach Zenona z Elei, odbija się czkawką w piętrowych konstrukcjach continuum itp. Alfred Tarski - współtwórca Teorii Modeli (a jakże), działu matematyki (właściwie metamatematyki) który relację między matematyczną rzeczywistością i jej formalizmem bada stworzył np. system geometrii, gdzie bytem pierwotnym nie był punkt ale kula i dla takiego systemu podał aksjomatykę. W takim systemie nie istnieją z kolei punkty - tylko ciała rozciągłe. Dziś niektórzy naukowcy próbujący nauczyć komputery rozumowań na temat przestrzeni sięgają po ową geometrię jako ontologię przestrzeni.
Odkrycia współczesnej fizyki i teorie próbujące je wyjaśnić też coraz częściej sięgają po geometrię w której pojęcie punktu traci sens. Tak jest np. z geometrią nieprzemienną Connesa modnym, trudnym i ważnym ostatnio działem matematyki, z którą również pewna grupa fizyków teoretyków wiąże wielkie nadzieje.
Formalizacja to także docenione narzędzie w rękach filozofów usiłujących przedrzeć się przez pułapki i śliskości języka naturalnego. Miast używać tego niedoskonałego narzędzia, rekonstruują pojęcia i relacje między nimi w postaci formalnej. Czy badając ten swój sformalizowany twór oglądają to o czym myśleli ? Znajdują w nim rzeczy nowe i zaskakujące? Teoretycznie powinni. Przecież geometria Euklidesa pozostaje żywa interesująca i zaskakująca do dzisiaj mimo osczędności pojęć i aksjomatyki.
Takiego "uformalnienia" pewnych rozważań na gruncie epistemologii fenomenalistycznej dokonał Rudolf Carnap w 1928 roku w pracy Der logische Aufbau Der Welt idąc w ślady Bertranda Russela i jego Our Knowledge of External World. To spojrzenie jest z kolei punktem wyjścia do ciekawej próby rekonstrukcji pojawienia się logiki, abstrakcyjnej myśli i w końcu nauki z czysto biologicznych predyspozycji którą podjął Willard Van Orman Quine w książce pod polskim tytułem Od bodźca do nauki. Właśnie zacząłem ją czytać i to ona sprowokowała mnie do dzisiejszego postu i wspominek z firmy na B.