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: Jak działa język?

Zapisz się do newslettera:

---

Filozofuj z nami w social media

Najnowszy numer można nabyć od 2 października 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 „Filo­zo­fuj” 2018 nr 1 (19), s. 26–27. W pełnej wer­sji graficznej jest dostęp­ny w pliku  PDF.


§1. Rozu­mowanie, czyli poszuki­wanie intere­su­jącego nas wniosku, wyma­ga pomysłowoś­ci, trze­ba bowiem znaleźć przesłan­ki, z których wynikał­by log­icznie wniosek. Z reper­tu­aru reguł wnioskowa­nia należy zręcznie wybrać te, które potrzeb­ne są, żeby prze­być drogę od przesłanek do wniosku. Zobaczymy to niżej w §2 na pewnym przykładzie rozu­mowa­nia. Jest on tak łatwy, że wyma­ga min­i­mum pomysłowoś­ci, ale na­wet na tym skra­jnie prostym przykładzie da się dostrzec, na czym ów rys inwen­cyjny pole­ga.

Przedtem jed­nak spróbu­jmy sobie wyobraz­ić, jak niesamowitej pomysłowoś­ci wyma­gał­by dowód wypeł­ni­a­ją­cy książkę o obję­toś­ci ok. 200 stron, gdy w chwili przys­tąpi­enia do pra­cy autor nie wie nawet tego, w jakiej teorii matem­aty­cznej da się znaleźć przesłan­ki. Gdy się już zde­cyduje na wybór takiej, a nie innej, dro­ga do kon­kluzji będzie prowadz­ić przez tysiące i tysiące wier­szy, a dla każdego wier­sza trze­ba wynaleźć przesłan­ki. Taka sen­sacyjna his­to­ria zdarzyła się naprawdę przed ćwierćwie­czem. Zagad­nie­nie, na które przyniosła odpowiedź, po­jawiło się przed trze­ma wieka­mi, a głow­iły się nad nim przez ten czas bezskutecznie najtęższe głowy matema­tyczne. Kto chce poz­nać tę his­torię, niech od wszech­wiedzącego Google’a zażą­da wiado­moś­ci: Wiel­kie Twierdze­nie Fer­ma­ta.

Przykład inwen­cyjnego sposobu rozu­mowa­nia, prze­ci­w­stawnego metodzie mechan­icznej, zaczni­jmy od reflek­sji nad słowem „oczy­wis­tość”. Każde bowiem uza­sad­nie­nie sprowadza się ostate­cznie do powoła­nia się na jakąś oczy­wis­tość. Ta jest bądź zmysłowa („te­raz pada tutaj śnieg”), bądź intelek­tu­al­na, jak w zda­niach: „dla każdej licz­by całkowitej ist­nieje licz­ba od niej więk­sza” albo „nie jest możli­we, wydawszy ostat­nie pieniądze, mieć je nadal”. Niemożli­woś­ci stanu rze­czy nie da się dostrzec zmysła­mi, nawet wtedy, gdy sam ten stan pod­pa­da pod zmysły (np. dotykiem po­znajemy pus­tość kieszeni). Licz­ba, możli­wość, ko­nieczność itd. to abstrakc­je dostęp­ne tylko dla rozu­mu.

Poję­cia oczy­wis­toś­ci intelek­tu­al­nej potrze­bu­je­my do zdefin­iowa­nia teorii mają­cych tę włas­ność, że w uza­sad­ni­a­n­iu twierdzeń nie odwołu­je­my się do doświad­czeń zmysłowych, lecz do oczy­wis­toś­ci intelek­tualnej. Mają to do siebie teorie matem­aty­czne i lo­giczne.

Gdy sąd Z jest uza­sad­ni­any przez Y, zaś ten przez X itd., nie da się tego ciągnąć w nieskońc­zoność. Żeby uza­sad­nić Z, trze­ba wresz­cie dojść do jakiegoś sądu A, który nie wyma­ga uza­sad­nienia, będąc oczy­wistym. Ma zaś przy tym treść na tyle bogatą, że dzię­ki niej da się udowod­nić wiele sądów. Taki sąd pod­sta­wowy na­zywamy aksjo­matem teorii. Staramy się o taki układ aksjo­matów, żeby wszys­tkie prawdy danej teorii dały się na ich grun­cie udowod­nić. Nie zawsze jest to wy­konalne, ale jeśli będziemy dołączać aksjo­maty, które chwyta­ją jakieś nowe oczy­wis­toś­ci, licz­ba prawd dowodli­wych w danej teorii będzie rosła.

§2. Niech twierdze­niem do udowod­nienia będzie for­muła OE (o tym, że ze zda­nia Ogól­nego wyni­ka Eg­zystencjalne).

OE: ∀xQx → ∃xQx

Szuka­jąc potrzeb­nych do dowodu przesłanek, sięgamy do logi­ki Davi­da Hilber­ta zaw­ier­a­jącej aksjo­maty:
A1: ∀xQxQa
A2: Qa → ∃xQx.

Nie trze­ba dużej pomysłowoś­ci, żeby na pod­staw­ie A1 i A2 udowod­nić OC. Niezbędne tu min­i­mum pole­ga na tym, żeby połączyć A1 i A2 w koni­unkcję i za­uważyć, że moż­na jej ele­men­ty pod­staw­ić pod zmi­enne w for­mule logi­ki zdań zwanej prawem sylo­giz­mu
(Syl):

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

Z pod­staw­ień p / ∀xQx, q / Qa, r / ∃xQx otrzy­mu­je­my imp­likację (Imp):

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

 

Ostat­ni krok to dostrzeże­nie, że poprzed­nik for­muły Imp jest iden­ty­czny z koni­unkcją aksjo­matów A1 ∧ A2, zaś jej następ­nik z dowod­zoną for­mułą OE. Za­uważamy jed­nocześnie, że do tej struk­tu­ry sto­su­je się kluc­zowa dla logi­ki reguła odry­wa­nia: jeśli praw­dziwa jest imp­likac­ja i jej poprzed­nik, to prawdą jest też następ­nik. Wol­no więc odłączyć go od implika­cji i dołączyć do teorii jako samodzielne twierdze­nie. Takie odłącze­nie moż­na też nazwać oder­waniem, stąd nazwa „reguła odry­wa­nia”.

Poszuku­jąc przesłanek i reguł, żeby na grun­cie po­siadanych aksjo­matów udowod­nić określone twier­dzenie, zas­tanaw­iamy się, które aksjo­maty i które reguły wybrać do tego celu. Umożli­wia nam to zdol­ność, w swym zalążku wrod­zona, a przez prak­tykowanie ro­zumowań rozwinię­ta, jaką jest intu­ic­ja log­icz­na.

Sta­je się ona zbęd­na przy takiej metodzie dowodze­nia, która zwal­nia od wyboru aksjo­matów i korzys­ta z takich reguł dowodzenia, które czynią ten pro­ces au­to­ma­tycznym. Jak sobie radz­ić bez aksjo­matów, zo­baczymy w #14. Owe reguły automatyzu­jące dowo­dzenie zwal­ni­a­ją od namysłu, którą regułę zas­tosować w danym miejs­cu: jed­noz­nacznie o tym decy­du­je ana­liza struk­tu­ry log­icznej zna­j­du­jącej się w tym miejs­cu przesłan­ki.

Struk­tu­ra zaś całego rozu­mowa­nia rządzi się pra­wem dowodu nie wprost. Jest mu poświę­cony odcinek #12 – o sprowadza­niu do sprzecznoś­ci (zob. „Filo­zo­fuj!” 2017 nr 6, s. 26–27). Tekst ten przy­go­towu­je do obec­nych i następ­nych (#14) rozważań.

§3. Dowo­dem nie wprost nazy­wa­ją log­i­cy taki prze­wrotny sposób argu­men­tacji, że dowód prawdzi­woś­ci twierdzenia T pole­ga na udowod­nie­niu fałszy­woś­ci nie-T. Ponieważ fałszy­wość nie-T jest równoważ­na prawdzi­woś­ci T, tą okrężną drogą dosta­je­my pożą­dany wynik. Po co tak okrążać zagad­nie­nie zami­ast ata­kować je frontal­nie? Kto prak­tykował tę metodę, ten wie, że częs­to szy­b­ciej i łatwiej prowadzi ona do uzyska­nia wyniku. Czemu tak się dzieje, zaczy­namy coraz lep­iej rozu­mieć w miarę prak­tykowa­nia tej strate­gii. Jej prób­ki w wer­sji przy­jaznej dla ludzi i maszyn zna­jdą się w #14.

Tę wer­sję nazwiemy anal­i­ty­cznym dowo­dem nie wprost. Jest to algo­rytm, który anal­izu­je struk­turę kole­jnych for­muł, poczy­na­jąc od wyjś­ciowej, tj. od nie-T, czyli od zaprzeczenia for­muły T. Anal­iza po­lega na rozkłada­niu struk­tur złożonych na coraz prost­sze – aż do najprost­szych, czyli for­muł ele­men­tarnych.

Taka anal­iza posuwa się cza­sem jed­ną ścieżką, cza­sem roz­gałęzia się na więcej. Jeśli na każdej ścieżce pojawi się para for­muł ele­men­tarnych między sobą sprzecz­nych, to for­muła nie-T, skutku­ją­ca w każdym przy­padku sprzecznoś­cią, nie może być prawdą. Musi więc być prawdą T – co było do dowiedzenia.

Anal­i­ty­czny dowód nie wprost zawdz­ięcza algo­ryt­miczność temu, że każdej struk­turze jest przy­porządkowana jed­noz­nacznie reguła rozkładu na główne skład­ni­ki. Wykon­aw­ca dowodu, czy to człowiek, czy maszy­na, widząc tę struk­turę „gołym okiem”, nie musi się zas­tanaw­iać, jaka do niej sto­su­je się reguła. Wyczy­tu­je to z jej fizy­cznego ksz­tał­tu.

Potrafi to zarówno człowiek, jak i maszy­na, bez po­trzeby jakiejkol­wiek inwencji. Człowiek ją ma, ale opła­ca mu się dzię­ki takiej automatyza­cji oszczędzać czas i energię. A maszy­na zasługu­je na po­chwałę, że choć na inwencję jej nie stać, to dorównu­je człowiekowi w rozwiązy­wa­niu licz­nych prob­lemów, gdy się ją wyposaży w odpowied­ni algo­rytm. W szczegól­noś­ci gdy jest to algo­rytm tak efek­ty­wny i efek­towny jak meto­da anal­i­ty­cznego do­wodu nie wprost. Więcej na jej tem­at w następ­nym odcinku naszego „seri­alu”.


Witold Mar­ciszews­ki – Pro­fe­sor dr hab. nauk human­isty­cznych w zakre­sie logi­ki. Wykładał na UW, w Col­legium Civ­i­tas, Uni­w­er­syte­cie w Salzbur­gu i in. Jego najbardziej znana książ­ka to Log­ic from a Rhetor­i­cal Point of View (Wyd. de Gruyter). Prowadzi blog: marciszewski.eu. Ulu­bione zaję­cie: roz­mowy z żoną na wszelkie tem­aty.

 

Tekst jest dostęp­ny na licencji: Uznanie autorstwa-Na tych samych warunk­ach 3.0 Pol­s­ka.

< Powrót do spisu treś­ci numeru.
Ilus­trac­ja: phon­la­maipho­to

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.

Wesprzyj „Filozofuj!” finansowo

Jeśli chcesz wesprzeć tę inicjatywę dowolną kwotą (1 zł, 2 zł lub inną), przejdź do zakładki „WSPARCIE” na naszej stronie, klikając poniższy link. Klik: Chcę wesprzeć „Filozofuj!”

Polecamy