Artykuł Logika

Witold Marciszewski: #13. Czy maszyna może rozumować, choć wymaga to inwencji (a maszyny na nią nie stać)?

Weźmiemy dziś na warsztat zagadnienie z dzie­dziny informatyki, z którym można sobie poradzić do­piero wtedy, gdy weszło się w zażyłość z różnorodnymi metodami logiki. Będzie tu mowa o dwóch meto­dach, z których jedna jest tak pomysłowa, że potrafi zrekompensować maszynie jej notoryczny brak po­mysłowości. W ten sposób naturalna ludzka inteligencja pod­nosi na wyżyny sztuczną.

Najnowszy numer: Esencja piękna

Zapisz się do newslettera:

---

Filozofuj z nami w social media

Najnowszy numer można nabyć od 24 stycznia w salonikach prasowych wielu sieci. Szczegóły zob. tutaj.

Numery drukowane można zamówić online > tutaj. Prenumeratę na rok 2018 można zamówić > tutaj.

Aby dobrowolnie WESPRZEĆ naszą inicjatywę dowolną kwotą, kliknij „tutaj”.

Tekst ukazał się w „Filozofuj” 2018 nr 1 (19), s. 26–27. W pełnej wersji graficznej jest dostępny w pliku  PDF.


§1. Rozumowanie, czyli poszukiwanie interesującego nas wniosku, wymaga pomysłowości, trzeba bowiem znaleźć przesłanki, z których wynikałby logicznie wniosek. Z repertuaru reguł wnioskowania należy zręcznie wybrać te, które potrzebne są, żeby przebyć drogę od przesłanek do wniosku. Zobaczymy to niżej w §2 na pewnym przykładzie rozumowania. Jest on tak łatwy, że wymaga minimum pomysłowości, ale na­wet na tym skrajnie prostym przykładzie da się dostrzec, na czym ów rys inwencyjny polega.

Przedtem jednak spróbujmy sobie wyobrazić, jak niesamowitej pomysłowości wymagałby dowód wypełniający książkę o objętości ok. 200 stron, gdy w chwili przystąpienia do pracy autor nie wie nawet tego, w jakiej teorii matematycznej da się znaleźć przesłanki. Gdy się już zde­cyduje na wybór takiej, a nie innej, droga do konkluzji będzie prowadzić przez tysiące i tysiące wierszy, a dla każdego wiersza trzeba wynaleźć przesłanki. Taka sen­sacyjna historia zdarzyła się naprawdę przed ćwierćwie­czem. Zagadnienie, na które przyniosła odpowiedź, po­jawiło się przed trzema wiekami, a głowiły się nad nim przez ten czas bezskutecznie najtęższe głowy matema­tyczne. Kto chce poznać tę historię, niech od wszechwiedzącego Google’a zażąda wiadomości: Wiel­kie Twierdzenie Fermata.

Przykład inwencyjnego sposobu rozumowania, przeciwstawnego metodzie mechanicznej, zacznijmy od refleksji nad słowem „oczywistość”. Każde bowiem uzasadnienie sprowadza się ostatecznie do powołania się na jakąś oczywistość. Ta jest bądź zmysłowa („te­raz pada tutaj śnieg”), bądź intelektualna, jak w zda­niach: „dla każdej liczby całkowitej istnieje liczba od niej większa” albo „nie jest możliwe, wydawszy ostat­nie pieniądze, mieć je nadal”. Niemożliwości stanu rze­czy nie da się dostrzec zmysłami, nawet wtedy, gdy sam ten stan podpada pod zmysły (np. dotykiem po­znajemy pustość kieszeni). Liczba, możliwość, ko­nieczność itd. to abstrakcje dostępne tylko dla rozumu.

Pojęcia oczywistości intelektualnej potrzebujemy do zdefiniowania teorii mających tę własność, że w uzasadnianiu twierdzeń nie odwołujemy się do doświadczeń zmysłowych, lecz do oczywistości intelek­tualnej. Mają to do siebie teorie matematyczne i lo­giczne.

Gdy sąd Z jest uzasadniany przez Y, zaś ten przez X itd., nie da się tego ciągnąć w nieskończoność. Żeby uzasadnić Z, trzeba wreszcie dojść do jakiegoś sądu A, który nie wymaga uzasadnienia, będąc oczywistym. Ma zaś przy tym treść na tyle bogatą, że dzięki niej da się udowodnić wiele sądów. Taki sąd podstawowy na­zywamy aksjomatem teorii. Staramy się o taki układ aksjomatów, żeby wszystkie prawdy danej teorii dały się na ich gruncie udowodnić. Nie zawsze jest to wy­konalne, ale jeśli będziemy dołączać aksjomaty, które chwytają jakieś nowe oczywistości, liczba prawd dowodliwych w danej teorii będzie rosła.

§2. Niech twierdzeniem do udowodnienia będzie formuła OE (o tym, że ze zdania Ogólnego wynika Eg­zystencjalne).

OE: ∀xQx → ∃xQx

Szukając potrzebnych do dowodu przesłanek, sięgamy do logiki Davida Hilberta zawierającej aksjomaty:
A1: ∀xQxQa
A2: Qa → ∃xQx.

Nie trzeba dużej pomysłowości, żeby na podstawie A1 i A2 udowodnić OC. Niezbędne tu minimum polega na tym, żeby połączyć A1 i A2 w koniunkcję i za­uważyć, że można jej elementy podstawić pod zmienne w formule logiki zdań zwanej prawem sylogizmu
(Syl):

[(pq) ∧ (q r)] → (p r);

Z podstawień p / ∀xQx, q / Qa, r / ∃xQx otrzymujemy implikację (Imp):

[(∀xQxQa) ∧ (Qa → ∃xQx)] → [∀xQx → ∃xQx]

 

Ostatni krok to dostrzeżenie, że poprzednik formuły Imp jest identyczny z koniunkcją aksjomatów A1 ∧ A2, zaś jej następnik z dowodzoną formułą OE. Za­uważamy jednocześnie, że do tej struktury stosuje się kluczowa dla logiki reguła odrywania: jeśli praw­dziwa jest implikacja i jej poprzednik, to prawdą jest też następnik. Wolno więc odłączyć go od implika­cji i dołączyć do teorii jako samodzielne twierdzenie. Takie odłączenie można też nazwać oderwaniem, stąd nazwa „reguła odrywania”.

Poszukując przesłanek i reguł, żeby na gruncie po­siadanych aksjomatów udowodnić określone twier­dzenie, zastanawiamy się, które aksjomaty i które reguły wybrać do tego celu. Umożliwia nam to zdolność, w swym zalążku wrodzona, a przez praktykowanie ro­zumowań rozwinięta, jaką jest intuicja logiczna.

Staje się ona zbędna przy takiej metodzie dowodze­nia, która zwalnia od wyboru aksjomatów i korzysta z takich reguł dowodzenia, które czynią ten proces au­to­ma­tycznym. Jak sobie radzić bez aksjomatów, zo­baczymy w #14. Owe reguły automatyzujące dowo­dzenie zwalniają od namysłu, którą regułę zastosować w danym miejscu: jednoznacznie o tym decyduje ana­liza struktury logicznej znajdującej się w tym miejscu przesłanki.

Struktura zaś całego rozumowania rządzi się pra­wem dowodu nie wprost. Jest mu poświęcony odcinek #12 – o sprowadzaniu do sprzeczności (zob. „Filozofuj!” 2017 nr 6, s. 26–27). Tekst ten przygotowuje do obecnych i następnych (#14) rozważań.

§3. Dowodem nie wprost nazywają logicy taki prze­wrotny sposób argumentacji, że dowód prawdziwości twierdzenia T polega na udowodnieniu fałszywości nie-T. Ponieważ fałszywość nie-T jest równoważna prawdziwości T, tą okrężną drogą dostajemy pożądany wynik. Po co tak okrążać zagadnienie zamiast ata­kować je frontalnie? Kto praktykował tę metodę, ten wie, że często szybciej i łatwiej prowadzi ona do uzyskania wyniku. Czemu tak się dzieje, zaczy­namy coraz lepiej rozumieć w miarę praktykowania tej strategii. Jej próbki w wersji przyjaznej dla ludzi i maszyn znajdą się w #14.

Tę wersję nazwiemy analitycznym dowodem nie wprost. Jest to algorytm, który analizuje strukturę kolejnych formuł, poczynając od wyjściowej, tj. od nie-T, czyli od zaprzeczenia formuły T. Analiza po­lega na rozkładaniu struktur złożonych na coraz prost­sze – aż do najprostszych, czyli formuł elementarnych.

Taka analiza posuwa się czasem jedną ścieżką, czasem rozgałęzia się na więcej. Jeśli na każdej ścieżce pojawi się para formuł elementarnych między sobą sprzecz­nych, to formuła nie-T, skutkująca w każdym przy­padku sprzecznością, nie może być prawdą. Musi więc być prawdą T – co było do dowiedzenia.

Analityczny dowód nie wprost zawdzięcza algorytmiczność temu, że każdej strukturze jest przy­porządkowana jednoznacznie reguła rozkładu na główne składniki. Wykonawca dowodu, czy to człowiek, czy maszyna, widząc tę strukturę „gołym okiem”, nie musi się zastanawiać, jaka do niej stosuje się reguła. Wyczytuje to z jej fizycznego kształtu.

Potrafi to zarówno człowiek, jak i maszyna, bez po­trzeby jakiejkolwiek inwencji. Człowiek ją ma, ale opłaca mu się dzięki takiej automatyzacji oszczędzać czas i energię. A maszyna zasługuje na po­chwałę, że choć na inwencję jej nie stać, to dorównuje człowiekowi w rozwiązywaniu licz­nych problemów, gdy się ją wyposaży w odpowiedni algorytm. W szczególności gdy jest to algorytm tak efektywny i efektowny jak metoda analitycznego do­wodu nie wprost. Więcej na jej temat w następnym odcinku naszego „serialu”.


Witold Marciszewski – Profesor dr hab. nauk humanistycznych w zakresie logiki. Wykładał na UW, w Collegium Civitas, Uniwersytecie w Salzburgu i in. Jego najbardziej znana książka to Logic from a Rhetorical Point of View (Wyd. de Gruyter). Prowadzi blog: marciszewski.eu. Ulubione zajęcie: rozmowy z żoną na wszelkie tematy.

 

Tekst jest dostępny na licencji: Uznanie autorstwa-Na tych samych warunkach 3.0 Polska.

< Powrót do spisu treści numeru.
Ilustracja: phonlamaiphoto

Dołącz do Załogi F! Pomóż nam tworzyć jedyne w Polsce czasopismo popularyzujące filozofię. Na temat obszarów współpracy można przeczytać tutaj.