Wyjaśnienie. Przez formalizację danego wyrażenia merytorycznego rozumiemy:

1) Pozbawienie tego wyrażenia niepustego rozumienia (wprowadzenie strony znaczeniowej pustej na miejsce niepustej);

lub

2) Podstawienie za to wyrażenie merytoryczne wyrażenia formalnego.

2.1.6.10. Wyjaśnienie. Przez „interpretację merytoryczną danego wyrażenia formalnego”

rozumiemy:

1) Wprowadzenie do tego wyrażenia strony znaczeniowej niepustej na miejsce pustej lub

2) Podstawienie wyrażenia merytorycznego za to wyrażenie formalne.

2.1.6.11. Wyjaśnienie. Przez „interpretację formalną danego wyrażenia formalnego” rozumiemy podstawienie za to wyrażenie wyrażenia formalnego.

2.1.6.20. Reguła. Tłumaczenie nie jest czynnością formalną. Uzasadnienie: Dokonanie tłumaczenia wymaga znajomości strony znaczeniowej dwu wyrażeń merytorycznych (wyjaśnienia 2.1.6.00 oraz 2.1.6.00).

2.1.6.21. Reguła. Formalizacja jest czynnością formalną (wyjaśnienia 2.1.6.01 oraz 2.1.6.00).

2.1.6.22. Reguła. Interpretacja merytoryczna nie jest czynnością formalną. Uzasadnienie:

Dokonanie interpretacji merytorycznej wymaga znajomości rozumienia nadawanego wyrażeniu formalnemu lub rozumienia wyrażenia merytorycznego podstawionego za wyrażenie formalne (wyjaśnienia 2.1.6.10 oraz 2.1.6.00).

2.1.6.23. Reguła. Interpretacja formalna jest czynnością formalną (wyjaśnienia 2.1.6.11 oraz 2.1.6.00).

Przy posługiwaniu się powyższymi wyjaśnieniami i regułami okazuje się pomocna tabela 2.1.6.30.

Dla lepszego zrozumienia wyliczonych wyżej czynności podamy jeszcze pewien przykład. Do przykładu tego będą nam potrzebne cztery wyrażenia, mianowicie dwa wyrażenia merytoryczne i dwa wyrażenia formalne. Oba wyrażenia merytoryczne będą przy tym równoznaczne lecz nierównokształtne; będą to dwie nazwy jednostkowe pewnego wybitnego logika rzymskiego - nazwa spolszczona „𝐵𝑜𝑒𝑐𝑗𝑢𝑠𝑧” i nazwa łacińska ,,𝐵𝑜𝑒𝑡𝑖𝑢𝑠". Oba wyrażenia formalne są jakoby-nazwami jednostkowymi: „𝐴𝑤𝑖𝑎𝑠𝑧” oraz „𝐵𝑒𝑤𝑖𝑎𝑠𝑧”. Zastosujmy teraz reguły z tabeli 2.1.6.30 do niniejszego przykładu:

Ad. 1. „Boetiusz” tłumaczenie „Boetius” lub odwrotnie (czynność nieformalna);

Ad. 2. „Boeciusz” formalizacja „Awiasz” lub „Boetius” formalizacja „Bewiasz” (czynność formalna);

Ad. 3. „Awiasz” interpretacja merytoryczna „Boeciusz”

lub „Bewiasz” interpretacja merytoryczna „Boetius” (czynność nieformalna);

Ad. 4. „Awiasz” interpretacja formalna „Bewiasz lub odwrotnie” (czynność formalna).

Poznaliśmy ostatnio cztery czynności wykonywane zawsze równocześnie na jednym wyrażeniu.

Każda z tych czynności daje zawsze - jako wynik jedno wyrażenie. Poznamy ponadto analogiczne czynności, z których każda wykonywana jest za każdym razem na jakimś zespole czy systemie wyrażeń i jako wynik daje zawsze zespół czy system wyrażeń.

Te cztery nowe czynności, to:

1) Tłumaczenie tekstu (z języka na język);

2) Formalizacja (systemu zaksjomatyzowanego);

3) Interpretacja merytoryczna (systemu wyrażeń formalnych);

4) Interpretacja formalna (systemu wyrażeń formalnych).

Tłumaczenie tekstu - to czynność dla naszych celów mniej interesująca, pozostałe trzy czynności poznamy wkrótce, przedtem jednak musimy poznać ważniejsze odmiany systemów wyrażeń formalnych.

2.1.6.40. Wyjaśnienie. Przez „system wyrażeń formalnych” rozumiemy każdy i tylko taki zespół złożony wyłącznie z wyrażeń formalnych, który zbudowany jest w sposób następujący:

1) Podana jest lista wyrażeń pierwotnych, czyli zbudowanych przed rozpoczęciem budowania systemu;

2) Podane są (w jakimś języku naturalnym) dyrektywy budowania nowych wyrażeń za pomocą wyrażeń zaliczonych już do systemu;

3) Dyrektywy te są wykonalne, to znaczy z wyrażeń pierwotnych można zbudować chociaż jedno wyrażenie nie będące wyrażeniem pierwotnym;

4) Każda czynność przewidziana w którejkolwiek z dyrektyw jest czynnością formalną.

2.1.6.41.Wyjaśnienie. Przez „wyrażenie wtórne” (danego systemu) rozumiemy każde i tylko takie wyrażenie formalne, które można zbudować za pomocą dyrektyw (tegoż systemu) lub przez zdefiniowanie, a które nie jest (w danym systemie) wyrażeniem pierwotnym.

2.1.6.42. Wyjaśnienie. Przez „jednorodny system wyrażeń formalnych” rozumiemy każdy i tylko taki system wyrażeń formalnych, w którym ani na liście wyrażeń pierwotnych, ani w tekście dyrektyw nie wprowadzamy żadnego podziału wyrażeń należących do systemu na różne rodzaje (poza podziałem na wyrażenia pierwotne i wtórne).

W związku z wyjaśnieniem 2.1.6.40 zauważymy teraz, że do zbudowania jakiegokolwiek systemu wyrażeń formalnych niezbędne jest rozumienie pewnych wyrażeń merytorycznych (tych mianowicie, z których zbudowane są dyrektywy); mimo to rozbudowa takiego systemu odbywa się przez wykonywanie wyłącznie czynności formalnych. W związku natomiast z wyjaśnieniem 2.1.6.41 - zauważymy, że żaden system wyrażeń formalnych, w którym będziemy odróżniać na przykład jakoby-zdania od jakoby-nazw, nie będzie systemem jednorodnym;

natomiast jednorodny system wyrażeń formalnych może się składać wyłącznie z jakoby-zdań czy też, na przykład, wyłącznie z jakoby-nazw. Przykład. Każdy język programowania (np. język C – patrz rozdział 1.5.), jest systemem wyrażeń formalnych.

Piśmiennictwo: Greniewski H. G.2.1.

2.1.7.POJĘCIE SYSTEMU SFORMALIZOWANEGO

2.1.7.00. Wyjaśnienie. „Przez sprzężony system wyrażeń formalnych” rozumiemy każdą i tylko taką parę uporządkowaną zespołów wyrażeń, która spełnia wszystkie warunki następujące:

1) Zespół pierwszy jest systemem wyrażeń formalnych (jednorodnym lub niejednorodnym);

2) Każde wyrażenie należące do zespołu drugiego pierwszego, ale niekoniecznie na odwrót;

3) Zespół drugi - ma chociaż jedną dyrektywę budowania wyrażeń zaliczanych do tego zespołu, każda z tych dyrektyw jest wykonalna i każda opisuje sposób budowania wyrażeń zespołu drugiego w oparciu o wyrażenia już zaliczone do zespołu pierwszego lub drugiego.

Jak widać z powyższego wyjaśnienia, w każdym systemie sprzężonym mamy do czynienia z - dwoma zespołami wyrażeń: pierwszy z nich jest zwykłym systemem wyrażeń formalnych (może

on być jednorodny lub niejednorodny), drugi zaś jest wynikiem selekcjonowania wyrażeń zespołu pierwszego. Dyrektywy budowania wyrażeń zespołu drugiego są swojego rodzaju selektorem, który pewne wyrażenia już zaliczone do pierwszego zespołu (ale zwykle nie wszystkie), „wybiera” z zespołu pierwszego i zalicza do zespołu drugiego. Można by też przyrównać rolę dyrektyw zespołu drugiego do filtru, który tylko niektóre wyrażenia zaliczone do zespołu pierwszego „przepuszcza” do zespołu drugiego.

Zauważmy jeszcze, ze wyjaśnienie 2.1.7.00 – nie stawia systemowi sprzężonemu wymagania, aby drugi z obu zespołów miał swoją odrębną listę wyrażeń pierwotnych. Jednakże trzeba ponadto zauważyć, że wyjaśnienie 2.1.7.00 - nie czyni również zastrzeżeń przeciwko temu, aby drugi z zespołów stanowiących jakiś system sprzężony miał swoją listę wyrażeń pierwotnych.

Wśród sprzężonych systemów wyrażeń formalnych wyróżnimy teraz pewien węższy ich rodzaj, mianowicie systemy sformalizowane.

2.1.7.01. Wyjaśnienie. Przez „system sformalizowany” rozumiemy każdy i tylko taki sprzężony system wyrażeń formalnych, który spełnia wszystkie warunki następujące:

1) Jeżeli zespół pierwszy tego systemu sprzężonego jest systemem jednorodnym, to każde wyrażenie formalne należące do zespołu pierwszego jest tezą (a więc jakoby-zdaniem albo jakoby-funkcją zdaniową);

2) Jeżeli zespół pierwszy tego systemu sprzężonego jest niejednorodnym systemem wyrażeń formalnych, to jednym z rodzajów wyrażeń należących do zespołu pierwszego są jakoby-tezy, a ponadto dyrektywy budowania wyrażeń zespołu drugiego działają w ten sposób, że

„przepuszczają” z zespołu pierwszego do zespołu drugiego tylko jakoby-tezy;

3) Jeżeli zespół drugi tego systemu sprzężonego jest systemem wyrażeń formalnych i zawiera chociaż jedno wyrażenie pierwotne, to każde wyrażenie pierwotne zespołu drugiego jest jakoby-tezą.

2.1.7.10. Wyjaśnienie. Przez „język sformalizowany” rozumiemy pierwszy zespół wyrażeń systemu sformalizowanego.

2.1.7.11. Wyjaśnienie. Przez „teorię sformalizowaną” rozumiemy drugi zespół wyrażeń systemu sformalizowanego.

2.1.7.12. Reguła. Każdy język sformalizowany składa się wyłącznie z wyrażeń formalnych (wyjaśnienia 2.1.7.00, 2.1.7.01, 2.1.7.10).

2.1.7.13. Reguła. Każda teoria sformalizowana składa się wyłącznie z wyrażeń formalnych, mianowicie - wyłącznie z jakoby-tez (wyjaśnienia 2.1.7.00, 2.1.7.01, 2.1.7.11).

2.1.7.14. Reguła. Do żadnego języka sformalizowanego nie należy żadne wyrażenie merytoryczne (reguły 2.1.7.20 oraz 2.1.7.12).

2.1.7.15. Reguła. Do żadnej teorii sformalizowanej nie należy żadna teza prawdziwa (reguła 2.1.7.14, wyjaśnienie 2.1.7.01).

2.1.7.20. Wyjaśnienie. Przez „wyrażenie pierwotne systemu sformalizowanego” rozumiemy wyrażenie pierwotne odnośnego języka sformalizowanego.

2.1.7.21. Wyjaśnienie. Przez „wyrażenie wtórne systemu sformalizowanego” rozumiemy wyrażenie wtórne odnośnego języka sformalizowanego.

2.1.5.22. Reguła. Każdy język sformalizowany zawiera - chociaż jedno wyrażenie pierwotne (wyjaśnienia 2.1.4.00, 2.1.5.00, 2.1.5.01, 2.1.5.20).

2.1.7.23. Reguła. Każdy język sformalizowany zawiera - chociaż jedno wyrażenie wtórne (wyjaśnienia 2.1.7.00, 2.1.7.01, 2.1.7.00, 2.1.7.01, 2.1.7.21).

2.1.7.30. Wyjaśnienie. Przez „tezę pierwotną - czyli postulat, ewentualnie aksjomat, systemu sformalizowanego” rozumiemy wyrażenie pierwotne (jakoby-tezę) odnośnej teorii sformalizowanej.

2.1.7.31. Wyjaśnienie. Przez „tezę wtórną - czyli twierdzenie, systemu sformalizowanego”

rozumiemy wyrażenie wtórne, jakoby-tezę, odnośnej teorii sformalizowanej.

2.1.7.40. Wyjaśnienie. Przez „dyrektywę językową systemu sformalizowanego” rozumiemy dyrektywę budowania wyrażeń odnośnego języka sformalizowanego.

2.1.7.41. Wyjaśnienie. Przez „dyrektywę wnioskowania systemu sformalizowanego” rozumiemy dyrektywę budowania wyrażeń odnośnej teorii sformalizowanej.

Piśmiennictwo: Greniewski H. G.2.1.

2.1.8.O METAJĘZYKACH, METATEORIACH I META-SYSTEMACH

Poznaliśmy w podrozdziałach poprzednich różne rodzaje systemów wyrażeń formalnych od najprostszych aż po systemy sformalizowane. Obecnie zajmiemy się w kilku słowach metodami badania systemów zaksjomatyzowanych i systemów wyrażeń formalnych, w szczególności systemów sformalizowanych.

2.1.8.00. Wyjaśnienie. Mówimy, że dana dyrektywa jest „znaczeniotwórcza”, zamiast mówić, że dyrektywa ta ma wszystkie własności poniższe:

1) Jest to dyrektywa budowania wyrażeń;

2) Ma ona zastosowanie wyłącznie do wyrażeń merytorycznych (to jest do poszczególnych wyrażeń lub ich zespołów);

3) W wyniku zastosowania tej dyrektywy otrzymujemy zawszę wyrażenie merytoryczne.

2.1.8.01. Wyjaśnienie. Mówimy, że dana dyrektywa jest „prawdotwórcza”, zamiast mówić, że dyrektywa ta ma wszystkie własności poniższe:

1) Jest to dyrektywa budowania tez;

2) Ma ona zastosowanie wyłącznie do tez (poszczególnych tez, ewentualnie zespołów tez);

3) W wyniku zastosowania tej dyrektywy otrzymujemy zawsze tezę - następstwo tego zespołu tez, do którego dyrektywę zastosowano.

2.1.8.02. Reguła. Każda dyrektywa prawdotwórcza jest dyrektywą znaczeniotwórczą, ale nie