Om at gøre køleskabet rent

Her sidder jeg allerede med dagens første overspringshandling. Foran mig venter arbejdet med at bevise to sætninger (som egentlig kun er formodninger i skrivende stund), der er hovedresultaterne i en artikel, jeg er ved at skrive. Det er ikke overraskende resultater; de handler om det, der hedder sundhed og sikkerhed af et typesystem. For at bevise disse resultater skal jeg først etablere nogle lemmaer. I denne del af teoretisk datalogi laver jeg en masse induktive definitioner af relationer, og når jeg skal bevise egenskaber ved disse relationer, er bevisstrategien oplagt: induktionsbeviser. Hele herligheden minder om at gøre køleskabet rent og derefter manuelt afrime fryseren: jeg ved præcis, hvad jeg skal gøre, jeg ved, i hvilken rækkefølge det skal gøres og cirka hvor lang tid det vil tage og det er ikke særlig spændende, men man er nødt til det.

I sædvanlig matematik er der selvfølgelig også fyldt med kedelige beviser for kedelige sætninger, men heldigvis er der også de overrumplende – og overrumplende smukke – beviser for vigtige sætninger. Når man ser dem, ved man hvorfor ordet “elegant” har sin berettigelse også i denne verden. En interessant bog propfyldt med denne form for elegance er Proofs From The Book af Martin Aigner, Günter M. Ziegler og Karl H. Hofmann. Her er der smukke beviser for alt fra Pythagoras’ sætning til noget nyere, men stadig klassiske resultater fra bl.a. analyse, algebra og grafteori. Bogen – “The Book” – er Paul Erdös’ navn for “den store bog i himlen”, hvor alle de bedste beviser for sætningerne findes.

Mine egne køleskabsbeviser står temmelig sikkert ikke i bogen i himlen. Men én ting lærer jeg, når jeg laver dem: det store udredningsarbejde består i virkeligheden i at få tryllet definitionerne frem på en form, så beviserne falder let ud. Måske er det i virkeligheden typisk sådan, metodologien er. Og hvis det er tilfældet, er det vel et argument for den omdiskuterede matematikfilosofiske påstand, at matematiske udsagn er analytiske – dvs. at deres sandhed er selvindeholdt og derved følger af udsagnet selv.

 

(Visited 25 times, 1 visits today)
Loading Facebook Comments ...

Skriv et svar