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

Zapisz się do naszego newslettera

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 30 października w salonikach prasowych wielu sieci. Szczegóły zob. tutaj.

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

Aby dobrowolnie WESPRZEĆ naszą inicjatywę dowolną kwotą, kliknij „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.

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