U WAGI WSTĘPNE

2.0.1.POCHODZENIE LOGIKI

Źródeł powstania logiki należy szukać w starożytnej Grecji, gdzie między innymi powstał zbiór zasad wnioskowania – zwanych sylogizmami. Rozwój logiki helleńskiej obejmuje okres około trzystu lat, rozpoczął się około 500 roku p.n.e., a kończy się około 200 roku p.n.e. Dorobek tych trzystu lat jest w zakresie logiki niezwykle bogaty. Grecy stworzyli logikę zdań, logikę nazw oraz zaczątki tzw. logiki funktorów, formułowali i badali antynomie, a ponadto w dziedzinie metalogiki stworzyli pojęcia systemu zaksjomatyzowanego, mianowicie stoicki rachunek zdań i euklidesowy system geometrii elementarnej. Grecy zapoczątkowali też logikę indukcji.

Za ojca logiki helleńskiej uznano powszechnie Arystotelesa. Zanim jednak Arystoteles zaczął uprawiać logikę jako dość wyodrębnioną całość, powstały już zaczątki logiki w postaci przyczynków do mającej się dopiero narodzić odrębnej nauki. Warto wymienić najważniejszych twórców tego procesu formowania się logiki:

1. Pitagoras z Samos (urodzony w VI wieku p.n.e., zmarł w Metaponcie) i pitagorejczycy (uczestnicy szkoły filozoficznej założonej przez Pitagorasa, która istniała przez blisko dwieście lat) – twórcy dowodów matematycznych.

2. Eleaci (uczestnicy szkoły filozoficznej, o której w karykaturalnej nieco formie można by pokrótce powiedzieć: jeśli wynik rozumowania nie zgadza się z faktami, tym gorzej dla faktów; niemniej jednak uzyskali bardzo istotny wynik dla dalszego rozwoju logiki) – odkrywcy antynomii.

3. Sokrates (urodzony w roku 469 p.n.e. w Atenach i zmarły tamże w roku 399 p.n.e.) – twórca metody indukcji prostej oraz metody wnioskowania dialektycznego.

4. Megarejczycy (założycielem szkoły megaryjskiej był Euklides z Megary, zwany też

„Euklidesem Sokratykiem”, żyjący w latach 450-380 p.n.e., szkoła ta z zamiłowaniem poszukiwała antynomii; jedną z nich jest antynomia Kłamca) – twórcy dalszych antynomii.

5. Hipokrates (zwany „ojcem medycyny”, genialny lekarz grecki, urodził się w roku 460 p.n.e.

na wyspie Kos, zginął w roku 377 p.n.e. w Larissie. Był autorem lub współautorem zbioru pism medycznych pod nazwą Corpus Hippocrateum) – stworzył zaczątki logiki indukcji przyrodniczej.

6. Platon (zwany Ateńczykiem, urodził się w roku 427 p.n.e., zmarł w roku 347 p.n.e., był uczniem Sokratesa) – domniemany twórca metody aksjomatycznej.

7. Arystoteles (urodzony w Stagirze w roku 384 p.n.e., zmarł w Chalkis w roku 322 p.n.e. W roku 367 przybył do Aten. W Akademii platońskiej spędził dwadzieścia lat, z początku jako uczeń oraz zwolennik platonizmu, następnie jako samodzielny, oryginalny myslicie.) – twórca logiki nazw, autor pisma między innymi z dziedziny logiki. Dzieła naukowe Arystotelesa przechowały się w redakcji Andronikosa z Rodos. Otrzymały one później nazwę Organon (narzędzie) i obejmowały sześć traktatów: (1) Kategorie; (2) O wyrażeniu;

(3) Analityki wcześniejsze – traktat o dowodzie i wnioskowaniu; (4) Analityki późniejsze – również o dowodzie i wnioskowaniu; (5) Topikas – dowody prawdopodobne i sztuka prowadzenia sporów; (6) O sofizmatach – traktat o sylogizmach.

8. Tweofrast (urodzony w Eresos około roku 372 p.n.e., zmarł w Atenach około roku 287 p.n.e.) – kontynuator prac Arystotelesa, między innymi: (1) wzbogacił liczbę czterech trybów sylogizmu kategorycznego o pięć dalszych nazywanych pośrednimi; (2) Wprowadził nowe tryby sylogizmu asertorycznego; (3) Sformułował nieznane Arystotelesowi nowe twierdzenia należące do logiki zdań, takie jak przechodniość implikacji, modus ponendo-ponens i modus tollendo-tollens; (4) udoskonalił logikę wyrażeń modalnych;

(5) przeprowadził badania nad antynomią „Kłamca”.

9. Epikur (urodzony w roku 341 p.n.e., zmarł w roku 270 p.n.e.) - założył w Atenach szkołę filozoficzną zwaną „Ogrodem Epikura”. Tzw. Epikurejczycy byli współtwórcami logiki indukcji.

10. Stoicy (szkoła stoików, została założona w III wieku p.n.e. przez Zenona z Kition.

Usystematyzowanie logiki stoickiej, zawdzięczamy Chryzyp’owi urodzonemu około roku 280 p.n.e.) – pierwsi użyli terminu logika i byli twórcami rachunku zdań.

11. Euklides (żył na przełomie IV i III wieku p.n.e., studiował w Atenach na Akademii platońskiej.

Za czasów Ptomeleusza I, wykładał geometrię w Aleksandrii) – twórca pierwszego wielkiego systemu aksjomatycznego geometrii przedstawionego w pracy zatytułowanej Elementy.

Piśmiennictwo: Greniewski H. G.2.1.

2.0.2.XIX-WIECZNE PODSTAWY LOGIKI WSPÓŁCZESNEJ

Formalizacja logiki rozpoczęła się dopiero w końcu XIX wieku i została poprzedzona szeregiem bardzo istotnych również XIX wiecznych wyników. Wymienimy jedynie kilku twórców naszym zdaniem najważniejszych, podając ich nazwiska i osiągnięcia:

1. Mikołaj Łobaczewski (urodzony w 1793 roku – zmarły w 1856 roku, matematyk rosyjski - profesor Uniwersytetu w Kazaniu), Karol Fryderyk Gauss (urodzony w 1777 roku – zmarły w 1885 roku, znakomity matematyk i astronom niemiecki, profesor uniwersytetu w Getyndze), Jan Bolyai (urodzony w 1802 roku – zmarły w 1860, Węgier z zawodu oficer wojsk inżynieryjnych) i Bernard Rieman (urodzony w 1826 roku – zmarły w 1866 roku, matematyk niemiecki, wykładowca uniwersytetu w Getyndze) – niezależnych od siebie nawzajem - twórcy geometrii nieeuklidesowych.

2. Jozef Diez Geronne (urodzony w 1771 roku – zmarły w 1859 roku, matematyk i astronom francuski) – odkrywca zasady dwoistości w geometrii rzutowej.

3. George Boole (urodzony w 1815 roku – zmarły w 1864 roku, wybitny logik i matematyk brytyjski, genialny samouk - profesor uniwersytetu w Lincoln) – twórca algebry logiki (nazwanej na jego cześć Algebrą Boole’a).

4. August De Morgan (urodzony w 1806 roku – zmarły w 1871 roku, matematyk brytyjski, profesor uniwersytetu w Londynie), Płaton Porecki (urodzony w 1846 roku – zmarły w 1907 roku, logik rosyjski, profesor uniwersytetu w Kazaniu) i Erst Schr𝑜̈der (urodzony w 1841 roku – zmarły 1902 roku, logik niemiecki, profesor uniwersytetu w Karlsruhe) – kontynuatorzy algebry logiki.

5. Gottlob Frege (urodzony w 1848 roku – zmarły w 1925 roku, wybitny logik i matematyk niemiecki, profesor uniwersytetu w Jenie) – twórca pierwszego systemu sformalizowanego logiki.

Przełom, który nastąpił w logice w XX wieku, został przygotowany w dużej mierze przez początki formalizacji tradycyjnej logiki, i przez wyżej wymienionych twórców XIX wieku.

Piśmiennictwo: Greniewski H. G.2.1.

2.0.3.TEORIE LOGIKI A INFORMATYKA

Zanim zajmiemy się bliżej kilkoma teoriami logiki formalnej, zastanowimy się w jakim zakresie można mówić o przydatności logiki w formułowaniu podstaw teoretycznych informatyki.

Zacznijmy od pewnych istotnych różnic pomiędzy podejściami logiki i informatyki. Logika nie zakłada, że zbiory którymi operuje – posiadają skończone liczby elementów, wprost przeciwnie – najciekawsze wnioski, jak np. rozstrzygalność albo jej brak - dotyczy zbiorowisk poza-skończonych. Informatyka natomiast operuje zawsze zbiorami o skończonej liczbie elementów.

Wprawdzie mogą być to liczebności zboru bardzo duże, ale niemniej zawsze są skończone.

Pojemność największych pamięci jest zawsze skończona, jak również czas działania w rozumieniu informatyki, jest zawsze dyskretny – kwantowy. W teoriach logiki możemy zetknąć się zarówno z czasem ciągłym, jak i czasem dyskretnym.

W informatyce Czas Kwantowy będziemy traktować, jako zbiór elementów czasu - zwanych dalej

„chronami”. Rozmyślnie nie przesądzamy, czy chron (dowolny) jest chwilą (utożsamianą z impulsem zegarowym = punktem chronologicznym, typowa sytuacja dla urządzeń synchronicznych), czy też okresem czasu (utożsamianym z okresem czasu, jaki upływa pomiędzy dwoma kolejnymi impulsami zegarowymi = przedziałem chronologicznym, typowa sytuacja dla urządzeń asynchronicznych). Jednak przyjmujemy alternatywę rozłączną: Albo każdy chron jest chwilą, albo też każdy chron jest okresem. Ponadto przyjmujemy, że jeżeli każdy chron jest okresem, to każde dwa chrony mogą nie być równo trwałe. Ta pierwsza różnica podejścia logiki oraz informatyki - nie wydaje się być istotną. Warto zauważyć, że niedoskonałość naszego wzroku umożliwia np. obrazowanie na filmie lub wideo - ruchu z pomocą serii statycznych obrazów, wyświetlanych w odpowiednio szybko w kolejnych krótkich chronach czasu. Natomiast sprawa liczebności poza-skończonych zbiorów bardzo istotna w niektórych teoriach logiki, nie znajduje swojej odpowiedniości w informatyce. W konsekwencji predykaty logiczne: kwantyfikator istnienia „∃” oraz kwantyfikator generalizacji „∀”- są, czym innym - mimo stosowania identycznej symboliki, w rozumieniu Logiki Pierwszego Rzędu (patrz rozdział 2.7) operującej zbiorami poza skończonymi, a Notacji Z (patrz rozdział 4.4) – operująca zbiorami w rozumieniu informatyki – zawsze skończonymi. A przecież Notacja Z jest skutecznym narzędziem formułowania i analizowania wymagań na aplikacyjne systemy informatyczne, wykorzystującą metody wnioskowania zaczerpnięte z logiki. Trzeba jednak pamiętać, że zjawisko częściowej nierozstrzygalności (w rozumieniu Kurta G𝑜̈dla) – dotyczy między innymi Logiki Pierwszego Rzędu, a nie dotyczy teorii skończonych.

Odpowiedniość pomiędzy teoriami logiki a współczesną informatyki, w pewnym zakresie przypomina odpowiedniości pomiędzy płaską geometrią Euklidesa a geometrią rastrową, jaką posługuje się grafika komputerowa – celem zobrazowania graficznego krzywych i figur geometrycznych na ekranie monitora komputera. Algorytmy Bresenhama - odwzorowania odcinków i fragmentów krzywych płaskich na rastrze (patrz rozdział 4.8), prezentują odcinki prostej oraz wycinki krzywej na ekranie - jako zbiory rozłącznych odcinków odpowiednich długości (poziomych, pionowych lub dwusiecznych kąta - pomiędzy osiami współrzędnych) wyświetlanych z odpowiednim doborem kolorystyki i luminescencji. Rozłączność tych odcinków, jest widoczne na odpowiednio dużym powiększeniu, natomiast jeśli zbiór tych odcinków jest na pograniczu rozdzielczości oka ludzkiego, to wytwarza złudzenie linii ciągłej.

Piśmiennictwo: de Berg M. B.4.1., Liscov B. L.1.1., Tiuryn J. T.4.1.,Wikipedia W.2.12., W.2.13., Woodcock J.

W.7.1., Zabrodzki J. Z.1.1.

2.0.4.PROGRAM KOMPUTEROWY JAKO WYRAŻENIE LOGICZNE

Programowanie komputerów jest dzisiaj jednym z ważniejszych zastosowań logiki, ponieważ każdy program komputerowy jest formułą logiczną, podobnie jak każda formuła zdaniowa rozpatrywana w rachunku zdań. Tak jak zdanie, ze względu na kryteria rachunku zdań - może być prawdziwe lub fałszywe, tak program komputerowy, w sensie poprawności działania jego sterowania, może działać poprawnie (prawda) lub niepoprawnie (fałsz). Walidacja – to postępowanie mające na celu sprawdzenie w przypadku programu jego poprawność działania.

Walidacja programu komputerowego, jest więc niczym innym jak dowodzeniem poprawności działania danego programu. Zanim jednak przystąpimy do omawiania problematyki dowodzenia poprawności programów komputerowych zajmiemy się podstawami formalizacji.

Piśmiennictwo: Ben-Ari M. B.2.1., Hoare C.A.R. H.4.1., Holzmann G. H.3.1.