Reguła. Stosując dowolną dyrektywę prawdotwórczą do zespołu tez prawdziwych otrzymujemy w wyniku zawszę tezę prawdziwą

2.1.8.10. Wyjaśnienie. Przez „interpretację merytoryczną” systemu sformalizowanego rozumiemy podanie takiej dyrektywy, która:

1) Nadaje każdemu wyrażeniu pierwotnemu odnośnego języka sformalizowanego interpretację merytoryczną i to taką, że w tej interpretacji każda (ewentualna) teza pierwotna odnośnego systemu sformalizowanego staje się:

a) Tezą przyjętą na danym etapie rozwoju nauki za prawdziwą;

lub

b) Hipotezą przyjętą na danym etapie rozwoju nauki;

2) Przekształca każdą dyrektywę językową danego systemu sformalizowanego w dyrektywę znaczeniotwórczą;

oraz

3) Przekształca każdą dyrektywę wnioskowania danego systemu sformalizowanego w dyrektywę prawdotwórczą.

2.1.8.11. Wyjaśnienie. Przez „formalizację” systemu zaksjomatyzowanego rozumiemy przekształcenie danego systemu zaksjomatyzowanego w system sformalizowany.

Na pierwszy rzut oka - żaden system sformalizowany nie nadaje się do badania rzeczywistości materialnej. Fakt, ze język sformalizowany nie zawiera ani jednego wyrażenia merytorycznego, teoria sformalizowana zaś nie zawiera żadnej tezy prawdziwej, dyskwalifikuje, zdawałoby się – wszelki system sformalizowany, jako narzędzie badania. Dzięki jednak metodzie interpretacyjnej, to jest dzięki stosowaniu interpretacji merytorycznej, można niekiedy użyć niektórych - systemów sformalizowanych do badania rzeczywistości materialnej. Niekiedy jeden i ten sam - system sformalizowany ma więcej niż jedną interpretację merytoryczną (poznamy takie systemy w części 3), wówczas system taki pozwala na jednoczesne badanie, więcej niż jednego fragmentu rzeczywistości.

2.1.8.20. Wyjaśnienie. Mówimy, że dany system sformalizowany jest przepełniony, zamiast mówić, że każda jakoby-teza należąca do języka sformalizowanego danego systemu należy też do odnośnej teorii sformalizowanej.

Pojęcie przepełnienia pierwszy sprecyzował logik polski Stanisław Jaśkowski. Jak wiemy, każdy system sformalizowany jest systemem sprzężonym wyrażeń formalnych, wobec czego zespół dyrektyw wnioskowania ma charakter selektora czy filtru, który pewne tylko jakoby-tezy przepuszcza z języka sformalizowanego do teorii sformalizowanej. System przepełniony - to taki i tylko taki system, w którym wzmiankowany filtr nie działa skutecznie i przepuszcza wszelkie jakoby-tezy z języka sformalizowanego do teorii sformalizowanej. Budowanie, więc systemów przepełnionych jest zbędne, są one wszystkie bezwartościowe. Gdy budujemy jakiś system sformalizowany, co do którego zachodzą wątpliwości, czy nie jest on przepełniony, należy zbudować dowód nieprzepełnienia tego systemu. Związek między przepełnieniem z jednej strony a sprzecznością logiczną (i antynomiami) z drugiej – wykraczają poza zakres tematyczny niniejszej książki.

2.1.8.30. Wyjaśnienie. Przez „metajęzyk” rozumiemy taki i tylko taki język, w którym wypowiadamy się:

1) O pewnym innym języku czy innych językach lub

2) O pewnym języku sformalizowanym czy też językach sformalizowanych.

Przykład. Weźmy pod uwagę gramatykę języka rosyjskiego napisaną po polsku. W gramatyce tej występuje metajęzyk, na który składa się: (1) fragment graficznego języka polskiego, wystarczający do sformułowania reguł gramatycznych rosyjskiego języka graficznego oraz (2) odpowiednie nazwy przykładowo dobranych wyrażeń rosyjskich (nazwy te powstają przez ujęcie wyrażenia rosyjskiego w cudzysłów lub wprost wydrukowanie go kursywą, zależnie od przyjętych zwyczajów).

Weźmy pod uwagę jakikolwiek system sformalizowany; zawszę mamy tu do czynienia z metajęzykiem: każda - bowiem dyrektywa językowa i każda dyrektywa wnioskowania napisana jest w metajęzyku (rolę metajęzyka spełnia tu zwykle jakiś naturalny język graficzny czy też jego fragment, niekiedy jednak metajęzykiem może być jakiś język mieszany czy nawet sztuczny). W definicjach wielu systemów sformalizowanych występuje znany nam skrót „=Df”; tezy pierwotne i tezy wtórne niejednego systemu sformalizowanego poprzedzamy znanym już nam skrótem

„⊢”. Oba te skróty należą do metajęzyka.

Każda teoria ma swój przedmiot badania, na przykład przedmiotem badania planimetrii jest płaszczyzna (ściślej - każda płaszczyzna jest przedmiotem badania planimetrii). Przedmiotem badania arytmetyki liczb naturalnych są liczby naturalne itd. Nie wynika z tego, żeby każda rzecz czy każdy zespół rzeczy miał swoją teorię, której jest przedmiotem. Liczne doświadczenia z dziejów nauki zdają się wskazywać, że każda teoria może być przedmiotem innej teorii.

Doświadczenia te wskazują nam w każdym razie na istnienie takich teorii, których przedmiotem badania są teorie.

2.1.8.31. Wyjaśnienie. Mówimy krótko „metateoria”, zamiast mówić teoria mająca za przedmiot badania:

1) Jakąś teorię czy jakieś teorie;

lub

2) Jakiś system zaksjomatyzowany czy systemy zaksjomatyzowane;

lub

3) Jakiś system sformalizowany czy jakieś systemy sformalizowane.

2.1.8.32.Wyjaśnienie. Mówimy krótko „metasystem zaksjomatyzowany” zamiast mówić, „system zaksjomatyzowany taki, że zawarta w nim teoria jest metateorią”.

2.1.8.33. Wyjaśnienie. Mówimy krótko „metasystem sformalizowany”, zamiast mówić „system sformalizowany mający taką interpretację merytoryczną, w której odnośna teoria sformalizowana staje się metateorią”.

Piśmiennictwo: Greniewski H. G.2.1.

2.1.9.BLASKI I NĘDZE SYSTEMÓW SFORMALIZOWANYCH

Zachodzi znaczne podobieństwo między pojęciem systemu zaksjomatyzowanego a pojęciem systemu sformalizowanego. Oprócz podobieństwa występują jednak i różnice. Budowanie wyrażeń języka systemu zaksjomatyzowanego nie jest obiektywnie unormowane i wobec tego nie jest bezsporne. Budowanie wyrażeń języka systemu sformalizowanego (tj. języka sformalizowanego) jest natomiast obiektywnie unormowane przez dyrektywy językowe), a więc powinno być (przy dostatecznie starannej redakcji - dyrektyw językowych) bezsporne.

Budowanie (dowodzenie) tez w systemie zaksjomatyzowanym nie jest obiektywnie unormowane, a więc nie jest bezsporne. Poza tym w niejednym już systemie zaksjomatyzowanym zbudowano, jak pisaliśmy już, antynomie. Natomiast budowanie (dowodzenie, selekcjonowanie) jakoby-tez w systemie sformalizowanym jest obiektywnie unormowane (przez dyrektywy wnioskowania), a więc powinno być (przy dostatecznie starannej redakcji dyrektyw) bezsporne.

W sprawie doniosłości systemów sformalizowanych przytoczymy pogląd logika i matematyka polskiego Andrzeja Mostowskiego. ”Dowodzenie twierdzeń matematycznych uchodziło z dawien dawna za czynność umysłową, i to nawet za jedną z najtrudniejszych i najsubtelniejszych. W teoriach sformalizowanych zastąpiliśmy jednak tę czynność umysłową przez mechaniczne stosowanie reguł wnioskowania. Teoretycznie rzecz biorąc, można by w nauce sformalizowanej dowodzić twierdzeń zupełnie bezmyślnie, próbując tylko stosować (na wszelkie możliwe sposoby) reguły wnioskowania do aksjomatów, twierdzeń już udowodnionych...

… Inaczej mówiąc, dla każdej teorii sformalizowanej można wyobrazić sobie maszynę, która kolejno wypisuje twierdzenia tej teorii i to tak, że po dłuższym lub krótszym funkcjonowaniu wypisze każde z góry dane twierdzenie.

Droga ta praktycznie nie daje się zrealizować przynajmniej w chwili obecnej, gdyż dowody sformalizowane są tak długie, że nie starczyłoby życia ludzkiego, by dojść w ten sposób do twierdzeń ciekawych... rola intuicji w dowodach twierdzeń (w teoriach sformalizowanych) nie jest bynajmniej istotna: sprowadza się ona do tego, żeby wśród chaosu wszelkich możliwych kroków dowodowych znaleźć takie ich następstwo, które względnie szybko doprowadzi do celu”²⁶.

Pojęcie systemu sformalizowanego jest niewątpliwie wysoce interesujące. Fakt zbudowania (niejednego już) systemu sformalizowanego jest faktem naukowo doniosłym. Stworzenie

26 Mostowski, M.5.1, s.231 - 232.

systemów sformalizowanych otworzyło przed nauką nowe perspektywy rozwojowe i zarazem było początkowo źródłem... wielkich - a jak się później okazało - nieuzasadnionych złudzeń.

Wydawało się w pewnym (niedawnym zresztą) okresie pierwszego trzydziestolecia XX wieku, że całą wiedzę logiczną i matematyczną da się ująć - jako merytoryczną interpretację pewnej (niewielkiej stosunkowo) liczby systemów sformalizowanych. Wielką zasługą austriackiego logika Kurta Gödla jest, że w 1931 roku pogląd ten obalił w sposób ścisły. Wyniku tego (wchodzącego w skład metateorii systemów sformalizowanych) nie możemy w elementarnym wykładzie w sposób wyczerpujący zreferować (w literaturze polskiej wynik Gödla został systematycznie wyłożony w cytowanej już książce Andrzeja Mostowskiego). Praca Gödla jest trudna do zrozumienia. Jej ostateczny rezultaty poprzedzone są czterdziestoma sześcioma definicjami i kilkoma ważnymi twierdzeniami, które trzeba sobie przyswoić. W pracy tej pokazano zdumiewający dla ówczesnych logików rezultat badań nad metodą aksjomatyczną i formalizacją, według których metody te związane są nierozłącznie z pewnym ograniczeniem, sprawiającym, iż nie można wykazać wewnętrznej, logicznej niesprzeczności wielu złożonych systemów dedukcyjnych – bez zastosowania tak skomplikowanych środków dowodowych, że ich własna niesprzeczność wewnętrzna jest równie wątpliwa, jak niesprzeczność owych systemów. Konsekwencją tego wyniku, było stwierdzenie, że system dedukcyjny niesprzeczny, to system, w którym nie da się udowodnić jednocześnie pewnego zdania i jego zaprzeczenia. Tak więc - odkrycie Gödla zniweczyło zakorzenione głęboko przeświadczenie i zburzyło nadzieje, towarzyszące wcześniejszym badaniom nad podstawami matematyki. Ale wyniki tej pracy nie okazały się wyłącznie negatywne, otworzyły one drogę do pionierskiej problematyki, a mianowicie teorii obliczalności i teorii algorytmów, problematyki kluczowej dla informatyki.

Niesprzeczność systemu dedukcyjnego, pociąga za sobą własność rozstrzygalności w tym systemie. Rozstrzygalność, jak się dalej okazało, jest równoznaczna z istnieniem algorytmu.

Alan Turing, opublikował w 1934 roku swoją prawdopodobnie najważniejszą pracę matematyczną „On Computable Numbers”. To właśnie w tej pracy wprowadził Turing abstrakcyjną maszynę, która była w stanie wykonywać zaprogramowaną matematyczną sekwencję operacji, czyli tak zwany algorytm. Następnie w roku 1936, Turing opracował tak zwaną uniwersalną maszynę Turinga (patrz podrozdział 3.8.4), która w zależności od instrukcji zapisanej na taśmie, miała wykonywać dowolny algorytm. Obok Turinga do rozwoju nowej dziedziny teorii algorytmów przyczynili się Alonso Church, wykorzystując notację nazwaną rachunkiem 𝜆 do zdefiniowania algorytmu. W późniejszym okresie pokazano, że obie definicje algorytmu, to jest Turinga i Churcha, są równoważne. Powiązanie nieformalnego pojęcia algorytmu z precyzyjną definicją z wykorzystaniem maszyny Turinga nazwano tezą Churcha-Turinga.

Mimo przesadnych nadziei i błędnego filozoficznie podejścia do systemów sformalizowanych powstał kierunek zwany formalizmem. Pojęcie systemu sformalizowanego jest - jak już wspomnieliśmy - wysoce interesujące; dodajmy jeszcze, że w pewnym zakresie jest ono więcej niż pożyteczne; na przykład, gdy chodzi o wykład pewnych najprostszych teorii logiki, gdy chodzi o zasady budowy komputerów, systemów operacyjnych, języków programowania, systemów baz danych, itp.

Piśmiennictwo: Greniewski H. G.2.1. , Kisielewicz A. K.1.1.,, Mostowski A. M.5.1.,Turing A. T.6.1.