Artykuł Logika Warsztat logiczny

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ą.

Tekst uka­zał się w „Filo­zo­fuj!” 2018 nr 1 (19), s. 26–27. W peł­nej wer­sji gra­ficz­nej jest dostęp­ny w pli­ku  PDF.


§1. Rozu­mo­wa­nie, czy­li poszu­ki­wa­nie inte­re­su­ją­ce­go nas wnio­sku, wyma­ga pomy­sło­wo­ści, trze­ba bowiem zna­leźć prze­słan­ki, z któ­rych wyni­kał­by logicz­nie wnio­sek. Z reper­tu­aru reguł wnio­sko­wa­nia nale­ży zręcz­nie wybrać te, któ­re potrzeb­ne są, żeby prze­być dro­gę od prze­sła­nek do wnio­sku. Zoba­czy­my to niżej w §2 na pew­nym przy­kła­dzie rozu­mo­wa­nia. Jest on tak łatwy, że wyma­ga mini­mum pomy­sło­wo­ści, ale na­wet na tym skraj­nie pro­stym przy­kła­dzie da się dostrzec, na czym ów rys inwen­cyj­ny polega.

Przed­tem jed­nak spró­buj­my sobie wyobra­zić, jak nie­sa­mo­wi­tej pomy­sło­wo­ści wyma­gał­by dowód wypeł­nia­ją­cy książ­kę o obję­to­ści ok. 200 stron, gdy w chwi­li przy­stą­pie­nia do pra­cy autor nie wie nawet tego, w jakiej teo­rii mate­ma­tycz­nej da się zna­leźć prze­słan­ki. Gdy się już zde­cyduje na wybór takiej, a nie innej, dro­ga do kon­klu­zji będzie pro­wa­dzić przez tysią­ce i tysią­ce wier­szy, a dla każ­de­go wier­sza trze­ba wyna­leźć prze­słan­ki. Taka sen­sacyjna histo­ria zda­rzy­ła się napraw­dę przed ćwierćwie­czem. Zagad­nie­nie, na któ­re przy­nio­sła odpo­wiedź, po­jawiło się przed trze­ma wie­ka­mi, a gło­wi­ły się nad nim przez ten czas bez­sku­tecz­nie naj­tęż­sze gło­wy matema­tyczne. Kto chce poznać tę histo­rię, niech od wszech­wie­dzą­ce­go Google’a zażą­da wia­do­mo­ści: Wiel­kie Twier­dze­nie Fermata.

Przy­kład inwen­cyj­ne­go spo­so­bu rozu­mo­wa­nia, prze­ciw­staw­ne­go meto­dzie mecha­nicz­nej, zacznij­my od reflek­sji nad sło­wem „oczy­wi­stość”. Każ­de bowiem uza­sad­nie­nie spro­wa­dza się osta­tecz­nie do powo­ła­nia się na jakąś oczy­wi­stość. Ta jest bądź zmy­sło­wa („te­raz pada tutaj śnieg”), bądź inte­lek­tu­al­na, jak w zda­niach: „dla każ­dej licz­by cał­ko­wi­tej ist­nie­je licz­ba od niej więk­sza” albo „nie jest moż­li­we, wydaw­szy ostat­nie pie­nią­dze, mieć je nadal”. Nie­moż­li­wo­ści sta­nu rze­czy nie da się dostrzec zmy­sła­mi, nawet wte­dy, gdy sam ten stan pod­pa­da pod zmy­sły (np. doty­kiem po­znajemy pustość kie­sze­ni). Licz­ba, moż­li­wość, ko­nieczność itd. to abs­trak­cje dostęp­ne tyl­ko dla rozumu.

Poję­cia oczy­wi­sto­ści inte­lek­tu­al­nej potrze­bu­je­my do zde­fi­nio­wa­nia teo­rii mają­cych tę wła­sność, że w uza­sad­nia­niu twier­dzeń nie odwo­łu­je­my się do doświad­czeń zmy­sło­wych, lecz do oczy­wi­sto­ści intelek­tualnej. Mają to do sie­bie teo­rie mate­ma­tycz­ne i logiczne.

Gdy sąd Z jest uza­sad­nia­ny przez Y, zaś ten przez X itd., nie da się tego cią­gnąć w nie­skoń­czo­ność. Żeby uza­sad­nić Z, trze­ba wresz­cie dojść do jakie­goś sądu A, któ­ry nie wyma­ga uza­sad­nie­nia, będąc oczy­wi­stym. Ma zaś przy tym treść na tyle boga­tą, że dzię­ki niej da się udo­wod­nić wie­le sądów. Taki sąd pod­sta­wo­wy na­zywamy aksjo­ma­tem teo­rii. Sta­ra­my się o taki układ aksjo­ma­tów, żeby wszyst­kie praw­dy danej teo­rii dały się na ich grun­cie udo­wod­nić. Nie zawsze jest to wy­konalne, ale jeśli będzie­my dołą­czać aksjo­ma­ty, któ­re chwy­ta­ją jakieś nowe oczy­wi­sto­ści, licz­ba prawd dowo­dli­wych w danej teo­rii będzie rosła.

§2. Niech twier­dze­niem do udo­wod­nie­nia będzie for­mu­ła OE (o tym, że ze zda­nia Ogól­ne­go wyni­ka Egzystencjalne).

OE: ∀xQx → ∃xQx

Szu­ka­jąc potrzeb­nych do dowo­du prze­sła­nek, się­ga­my do logi­ki Davi­da Hil­ber­ta zawie­ra­ją­cej aksjomaty:
A1: ∀xQxQa
A2: Qa → ∃xQx.

Nie trze­ba dużej pomy­sło­wo­ści, żeby na pod­sta­wie A1A2 udo­wod­nić OC. Nie­zbęd­ne tu mini­mum pole­ga na tym, żeby połą­czyć A1A2 w koniunk­cję i za­uważyć, że moż­na jej ele­men­ty pod­sta­wić pod zmien­ne w for­mu­le logi­ki zdań zwa­nej pra­wem sylogizmu
(Syl):

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

Z pod­sta­wień p / ∀xQx, q / Qa, r / ∃xQx otrzy­mu­je­my impli­ka­cję (Imp):

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

 

Ostat­ni krok to dostrze­że­nie, że poprzed­nik for­mu­ły Imp jest iden­tycz­ny z koniunk­cją aksjo­ma­tów A1 ∧ A2, zaś jej następ­nik z dowo­dzo­ną for­mu­łą OE. Za­uważamy jed­no­cze­śnie, że do tej struk­tu­ry sto­su­je się klu­czo­wa dla logi­ki regu­ła odry­wa­nia: jeśli praw­dziwa jest impli­ka­cja i jej poprzed­nik, to praw­dą jest też następ­nik. Wol­no więc odłą­czyć go od implika­cji i dołą­czyć do teo­rii jako samo­dziel­ne twier­dze­nie. Takie odłą­cze­nie moż­na też nazwać ode­rwa­niem, stąd nazwa „regu­ła odrywania”.

Poszu­ku­jąc prze­sła­nek i reguł, żeby na grun­cie po­siadanych aksjo­ma­tów udo­wod­nić okre­ślo­ne twier­dzenie, zasta­na­wia­my się, któ­re aksjo­ma­ty i któ­re regu­ły wybrać do tego celu. Umoż­li­wia nam to zdol­ność, w swym zaląż­ku wro­dzo­na, a przez prak­ty­ko­wa­nie ro­zumowań roz­wi­nię­ta, jaką jest intu­icja logiczna.

Sta­je się ona zbęd­na przy takiej meto­dzie dowodze­nia, któ­ra zwal­nia od wybo­ru aksjo­ma­tów i korzy­sta z takich reguł dowo­dze­nia, któ­re czy­nią ten pro­ces au­to­ma­tycznym. Jak sobie radzić bez aksjo­ma­tów, zo­baczymy w #14. Owe regu­ły auto­ma­ty­zu­ją­ce dowo­dzenie zwal­nia­ją od namy­słu, któ­rą regu­łę zasto­so­wać w danym miej­scu: jed­no­znacz­nie o tym decy­du­je ana­liza struk­tu­ry logicz­nej znaj­du­ją­cej się w tym miej­scu przesłanki.

Struk­tu­ra zaś całe­go rozu­mo­wa­nia rzą­dzi się pra­wem dowo­du nie wprost. Jest mu poświę­co­ny odci­nek #12 – o spro­wa­dza­niu do sprzecz­no­ści (zob. „Filo­zo­fuj!” 2017 nr 6, s. 26–27). Tekst ten przy­go­to­wu­je do obec­nych i następ­nych (#14) rozważań.

§3. Dowo­dem nie wprost nazy­wa­ją logi­cy taki prze­wrotny spo­sób argu­men­ta­cji, że dowód praw­dzi­wo­ści twier­dze­nia T pole­ga na udo­wod­nie­niu fał­szy­wo­ści nie‑T. Ponie­waż fał­szy­wość nie‑T jest rów­no­waż­na praw­dzi­wo­ści T, tą okręż­ną dro­gą dosta­je­my pożą­da­ny wynik. Po co tak okrą­żać zagad­nie­nie zamiast ata­kować je fron­tal­nie? Kto prak­ty­ko­wał tę meto­dę, ten wie, że czę­sto szyb­ciej i łatwiej pro­wa­dzi ona do uzy­ska­nia wyni­ku. Cze­mu tak się dzie­je, zaczy­namy coraz lepiej rozu­mieć w mia­rę prak­ty­ko­wa­nia tej stra­te­gii. Jej prób­ki w wer­sji przy­ja­znej dla ludzi i maszyn znaj­dą się w #14.

Tę wer­sję nazwie­my ana­li­tycz­nym dowo­dem nie wprost. Jest to algo­rytm, któ­ry ana­li­zu­je struk­tu­rę kolej­nych for­muł, poczy­na­jąc od wyj­ścio­wej, tj. od nie‑T, czy­li od zaprze­cze­nia for­mu­ły T. Ana­li­za po­lega na roz­kła­da­niu struk­tur zło­żo­nych na coraz prost­sze – aż do naj­prost­szych, czy­li for­muł elementarnych.

Taka ana­li­za posu­wa się cza­sem jed­ną ścież­ką, cza­sem roz­ga­łę­zia się na wię­cej. Jeśli na każ­dej ścież­ce poja­wi się para for­muł ele­men­tar­nych mię­dzy sobą sprzecz­nych, to for­mu­ła nie‑T, skut­ku­ją­ca w każ­dym przy­padku sprzecz­no­ścią, nie może być praw­dą. Musi więc być praw­dą T – co było do dowiedzenia.

Ana­li­tycz­ny dowód nie wprost zawdzię­cza algo­ryt­micz­ność temu, że każ­dej struk­tu­rze jest przy­porządkowana jed­no­znacz­nie regu­ła roz­kła­du na głów­ne skład­ni­ki. Wyko­naw­ca dowo­du, czy to czło­wiek, czy maszy­na, widząc tę struk­tu­rę „gołym okiem”, nie musi się zasta­na­wiać, jaka do niej sto­su­je się regu­ła. Wyczy­tu­je to z jej fizycz­ne­go kształtu.

Potra­fi to zarów­no czło­wiek, jak i maszy­na, bez po­trzeby jakiej­kol­wiek inwen­cji. Czło­wiek ją ma, ale opła­ca mu się dzię­ki takiej auto­ma­ty­za­cji oszczę­dzać czas i ener­gię. A maszy­na zasłu­gu­je na po­chwałę, że choć na inwen­cję jej nie stać, to dorów­nu­je czło­wie­ko­wi w roz­wią­zy­wa­niu licz­nych pro­ble­mów, gdy się ją wypo­sa­ży w odpo­wied­ni algo­rytm. W szcze­gól­no­ści gdy jest to algo­rytm tak efek­tyw­ny i efek­tow­ny jak meto­da ana­li­tycz­ne­go do­wodu nie wprost. Wię­cej na jej temat w następ­nym odcin­ku nasze­go „seria­lu”.


Witold Mar­ci­szew­ski – Pro­fe­sor dr hab. nauk huma­ni­stycz­nych w zakre­sie logi­ki. Wykła­dał na UW, w Col­le­gium Civi­tas, Uni­wer­sy­te­cie w Sal­zbur­gu i in. Jego naj­bar­dziej zna­na książ­ka to Logic from a Rhe­to­ri­cal Point of View (Wyd. de Gruy­ter). Pro­wa­dzi blog: marciszewski.eu. Ulu­bio­ne zaję­cie: roz­mo­wy z żoną na wszel­kie tematy.

 

Tekst jest dostęp­ny na licen­cji: Uzna­nie autor­stwa-Na tych samych warun­kach 3.0 Pol­ska.

< Powrót do spisu tre­ści nume­ru.
Ilu­stra­cja: phonlamaiphoto

Najnowszy numer można nabyć od 1 września w salonikach prasowych wielu sieci. Szczegóły zob. tutaj.

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

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.

Skomentuj

Kliknij, aby skomentować

55 podróży filozoficznych okładka

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