Forskningsprojekt Cirkulära resonemang: en undersökning om icke-välgrundade bevis
Det traditionella synsättet är att en giltig slutledning består av en serie härledningssteg, som ska följa vissa sanningsbevarande regler. Slutledningen börjar med premisser, som antas vara sanna, och leder fram till den slutsats som ska bevisas. Projektet ansluter till en väl etablerad forskningslinje som studerar cirkulära och icke-välgrundade bevis.
Detta projekt befinner sig inom området logik, som kan beskrivas som vetenskapen om korrekta slutledningar. Det traditionella synsättet är att en giltig slutledning består av en serie härledningssteg, som ska följa vissa sanningsbevarande regler. Slutledningen börjar med en eller ett flertal premisser, som antas vara sanna, och leder stegvis fram till den slutsats som skall bevisas. Läran om formella regelsystem för härledning kallas bevisteori, och är en av grundpelarna inom modern formell logik.
Implicit i den bild av korrekta logiska slutledningar som ges av traditionell bevisteori ligger att korrekta resonemang ska vara välgrundade, alltså cirkulära resonemang eller oändliga kedjor av slutledningssteg skall avvisas som felaktiga. Projektet ansluter Trots till en väl etablerad forskningslinje inom modern bevisteori som studerar just cirkulära och icke-välgrundade bevis.
Projektbeskrivning
Detta projekt befinner sig inom området logik, som kan beskrivas som vetenskapen om korrekta slutledningar. Det traditionella synsättet är att en giltig slutledning består av en serie härledningssteg, som ska följa vissa sanningsbevarande regler. Slutledningen börjar med en eller ett flertal premisser, som antas vara sanna, och leder stegvis fram till den slutsats som skall bevisas. Läran om formella regelsystem för härledning kallas bevisteori, och är en av grundpelarna inom modern formell logik.
Implicit i den bild av korrekta logiska slutledningar som ges av traditionell bevisteori ligger att korrekta resonemang ska vara välgrundade, alltså cirkulära resonemang eller oändliga kedjor av slutledningssteg skall avvisas som felaktiga. En korrekt logisk slutledning skall ytterst grunda sig i antaganden (axiom) som antas vara sanna, och som därmed inte behöver motiveras ytterligare. Detta kan tyckas vara ett självklart villkor på korrekta bevis, och synen på cirkularitet som något problematiskt har varit central inom logikens och filosofins historia. Från Aristoteles argument för en första orsak med motivationen att undvika en oändlig regress, till Russells förespråkande av "predikativitet" inom matematikens grundvalar, har misstänksamheten mot icke-välgrundade resonemang en lång historia inom filosofin. Trots detta finns det en väl etablerad forskningslinje inom modern bevisteori som studerar just cirkulära och icke-välgrundade bevis. Under vissa villkor kan sådana bevis vara helt sunda, och dessutom väldigt användbara. Det handlar framförallt om fall som behandlar självreferens i någon form, det vill säga begrepp som definieras på ett sådant sätt att det som skall definieras utgör en del av själva definitionen. Den som har studerat matematik eller datavetenskap känner säkert till rekursiva definitioner, som t.ex. följande definition av funktionen fakultet:
0! = 1,
1!= 1,
(n + 1)! = n*(n!)
Denna funktion multiplicerar ett givet positivt heltal tal med alla mindre positiva heltal. Den rekursiva definitionen ges av två stycken basfall, motsvarande n = 0 och n = 1, och sedan en rekursiv klausul som gör att funktionen blir definierad för alla positiva heltal. Vi ser här att definitionen av rekursionssteget refererar till själva funktionen som skall definieras. När denna teknik lärs ut hörs ofta förklaringar som försäkrar oss att medan definitionen kanske ser cirkulär ut, så är den giltig eftersom varje upprepning av rekursionssteget för oss ett steg närmre basfallen, så ytterst grundas definitionen i dessa. Vi ser likheten med traditionell bevisteori här: ett bevis får inte lov att fortsätta i all oändlighet, utan måste till sist grundas i vissa antaganden. Precis som det finns forskning inom bevisteorin som bryter mot detta antagande, så finns en väletablerad matematisk teori om självrefererande definitioner som faktiskt är icke-välgrundade, alltså där det inte finns några basfall. Sådana definitioner kallas för co-rekursiva definitioner, och spelar en viktig roll inom vissa delar av datavetenskapen. Co-rekursiva definitioner kan tillåtas under sådana villkor där man kan visa att definitionen har en unik "lösning", alltså det finns ett unikt objekt som uppfyller definitionens ekvationer. Inom logiken behandlas rekursivt och corekursivt definierade begrepp av så kallade fixpunkt-operatorer, och det är alltså med avseende på logiska system som innefattar sådana fixpunktoperatorer som icke-välgrundade bevis framförallt varit av intresse.
I det här projektet kommer jag studera icke-välgrundade bevis från både en teknisk och en filosofisk sida. Den tekniska sidan av projektet kommer bland annat handla om att utveckla nya icke-välgrundade bevissystem och använda dem för att studera kända logiska system. Den filosofiska sidan av projektet är tänkt att omvärdera invanda synsätt på cirkularitet inom logiken och matematikens grundvalar, med den befintliga forskningen om ickevälgrundade bevis och co-rekursion som utgångspunkt.
Projektmedlemmar
Projektansvariga
Sebastian Enqvist
Universitetslektor
