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 dziedziny informatyki, z którym można sobie poradzić dopiero wtedy, gdy weszło się w zażyłość z różnorodnymi metodami logiki. Będzie tu mowa o dwóch metodach, z których jedna jest tak pomysłowa, że potrafi zrekompensować maszynie jej notoryczny brak pomysłowości. W ten sposób naturalna ludzka inteligencja podnosi na wyżyny sztuczną.

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 nawet 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ż zdecyduje 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 sensacyjna historia zdarzyła się naprawdę przed ćwierćwieczem. Zagadnienie, na które przyniosła odpowiedź, pojawiło się przed trzema wiekami, a głowiły się nad nim przez ten czas bezskutecznie najtęższe głowy matematyczne. Kto chce poznać tę historię, niech od wszechwiedzącego Google’a zażąda wiadomości: Wielkie 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 („teraz pada tutaj śnieg”), bądź intelektualna, jak w zdaniach: „dla każdej liczby całkowitej istnieje liczba od niej większa” albo „nie jest możliwe, wydawszy ostatnie pieniądze, mieć je nadal”. Niemożliwości stanu rzeczy nie da się dostrzec zmysłami, nawet wtedy, gdy sam ten stan podpada pod zmysły (np. dotykiem poznajemy pustość kieszeni). Liczba, możliwość, konieczność 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 intelektualnej. Mają to do siebie teorie matematyczne i logiczne.

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 nazywamy 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 wykonalne, 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 Egzystencjalne).

OE: ∀_xQx → ∃_xQx

Szukając potrzebnych do dowodu przesłanek, sięgamy do logiki Davida Hilberta zawierającej aksjomaty:
A1: ∀_xQx → Qa
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 zauważyć, że można jej elementy podstawić pod zmienne w formule logiki zdań zwanej prawem sylogizmu
(Syl):

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

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

[(∀_xQx → Qa) ∧ (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. Zauważamy jednocześnie, że do tej struktury stosuje się kluczowa dla logiki reguła odrywania: jeśli prawdziwa jest implikacja i jej poprzednik, to prawdą jest też następnik. Wolno więc odłączyć go od implikacji 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 posiadanych aksjomatów udowodnić określone twierdzenie, 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 rozumowań rozwinięta, jaką jest intuicja logiczna.

Staje się ona zbędna przy takiej metodzie dowodzenia, która zwalnia od wyboru aksjomatów i korzysta z takich reguł dowodzenia, które czynią ten proces automatycznym. Jak sobie radzić bez aksjomatów, zobaczymy w #14. Owe reguły automatyzujące dowodzenie zwalniają od namysłu, którą regułę zastosować w danym miejscu: jednoznacznie o tym decyduje analiza struktury logicznej znajdującej się w tym miejscu przesłanki.

Struktura zaś całego rozumowania rządzi się prawem 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 przewrotny 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 atakować je frontalnie? Kto praktykował tę metodę, ten wie, że często szybciej i łatwiej prowadzi ona do uzyskania wyniku. Czemu tak się dzieje, zaczynamy 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 polega na rozkładaniu struktur złożonych na coraz prostsze – 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ą sprzecznych, to formuła nie‑T, skutkująca w każdym przypadku 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 przyporzą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 potrzeby 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 pochwałę, że choć na inwencję jej nie stać, to dorównuje człowiekowi w rozwiązywaniu licznych 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 dowodu 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.