Sildiarhiiv: tõestus

Tõestustest ja edusammudest matemaatikas

William Thurston (1994) on kirjutanud huvitava artikli teadustöö tegemisest matemaatikas. Üks tema meeldejääv mõte on, et matemaatiku ülesanne pole ainult suurimat võimalikku arvu teoreeme tõestada, vaid ka oma matemaatikavaldkonda populariseerida ja teistele selgitada.

Filosoofilisest vaatepunktist ei pea matemaatikas mitte ainult tõeseid tulemusi teadma, vaid ka nende tõestustest aru saama. Seetõttu on arvutipõhised tõestused vähem väärtuslikud, kui „käsitsi tehtud“. Thurstoni kohaselt peaks edendama inimkonna arusaamist matemaatikast, mille üks osa on uute tulemuste tõestamine, aga oluline on ka ideede selgitamine.

Isikliku kasu vaatepunktist tuleb osa uurimistöö meeldivusest teiste inimeste huvist teema vastu, nende heakskiidust tehtud tööle ja võimalusest ühist huvi pakkuval teemal arutleda. Seega peaks teadlane olema huvitatud oma valdkonna teistele selgitamisest ja teiste kaasatõmbamisest oma suuna uurimistöösse. Selle nimel on mõtet vähem uut teadustööd teha ja rohkem vana selgitada ja õpetada.

Ma ise lisaksin veel ühe iseka põhjuse, miks oma tööd teistele „müüma“ peaks – kui valdkonda lisandub teadlasi, siis tsiteeritakse varasemaid tulemusi rohkem. Need varasemad tulemused on pärit valdkonda varem sisenenud teadlastelt, kelle akadeemiline tuntus tõuseb, kui valdkond populaarsemaks muutub.

Üldisemalt on teaduse tegemise eesmärk, et ühiskond sellest mingit kasu saaks. Kasu saamiseks peavad inimesed teadust kuidagi kasutama ja kasutamiseks on vaja seda teatud määral mõista. Teaduse selgitamine teenib seega üldist eesmärki. Vahel rohkemgi, kui uue teaduse loomine.

Kuidas otsustada kuidas otsustada kuidas otsustada…

Üks majandusartikkel, mis on minu jaoks väga huvitav, aga täiesti kasutu, on Lipman 1991 How to decide how to decide how to… Modeling limited rationality. See tõestab lahenduse olemasolu järgneva otsustusprobleemi jaoks.

Olgu meil mingid alternatiivid, mille hulgast me tahame optimaalse valida. Selleks tuleb valida parim valikumeetod, aga meetodi valik on omakorda otsustusprobleem. Tuleks valida parim meetod meetodi valikuks, parim meetod meetodi valiku meetodi valikuks, meetodi valiku meetodi valiku meetodi valikuks jne. Tegemist on lõpmatu rekursiooniga.

Lipman 1991 tõestab, et lahendus sellele valikute jadale eksisteerib, aga alles pärast lõpmatust (induktsioon ordinaalarvudel, mitte naturaalarvudel). Nii et kui me läheme lõpmatusest edasi, siis jõuame kunagi lahendini. Tõestus pole konstruktiivne, näitab ainult lahendi olemasolu, nii et lahendusalgoritmi see ei anna. Seetõttu on artikkel üsna kasutu.

Kaarditarkvara teoreemide tõestamiseks

Teoreemid on nagu sõidujuhised matemaatiliste lausete ruumis – need viivad alguspunktist (eeldustest) lõpp-punkti (järeldusteni) mingite reeglite kohaselt. Teoreemitõestus on osaliselt juba automatiseeritud, kuna on olemas loogikaprogrammid, mis leiavad eelduste ja järelduste seose. Võimalik, et sõidujuhiseid arvutavast kaarditarkvarast saab ideid või elemente automaattõestamise kiiremaks ja laialdasemaks muutmiseks.

Tavalisel tõestamisel oleks abiks programm, mis erinevalt Wikipediast mõistaks matemaatiliste lausete sisu (semantilise veebi sarnaselt) ja võimaldaks esitada päringuid antud matemaatilisest lausest järelduvate lausete kohta. Samuti lausete kohta, millest antud lause järelduks, ja samaväärsete lausete kohta.

Olemasolev matemaatika kajastuks kui suunatud graaf (võrgustik), kus matemaatilised väited on tipud (sõlmed) ja teoreemid on servad (nooled). Osa matemaatikast saaks andmebaasi sisestada automaatselt, õpetades programmi Wikipedia artikleid lugema. Valemid Wikipedia lehtedel saaks nende aluseks oleva LaTeXi koodi järgi andmebaasi sisestada ja sõnu „järeldub“ või „ekvivalentne“ sisaldavad laused Wikipedia artiklites tekitaksid andmebaasis seoseid.