Licentiatseminarium: Dominik Wehr

Examinator: Docent Fredrik Engström, Göteborgs universitet
Opponent: Associate professor Anupam Das, University of Birmingham

Kontakta Graham Leigh via mejl om du önskar få en digital kopia av uppsatsen.

Sammanfattning

Cykliska bevissystem tillåter deriveringar vars strukturer beskrivs av ändliga grafer snarare än välgrundade träd. Vanligtvis garanteras sundheten av cykliska bevis genom att införa ytterligare sundhetskriterier utöver korrekthet m.a.p. logiska regler. Genom att införa olika sundhetskriterier till samma uppsättning av logiska regler är det möjligt att skapa olika cykliska representationer av samma logiska teori.

Denna licentiatavhandling är en sammanläggning av artiklar rörande cyklisk bevisteori som fokuserar på representationen av cykliska bevissystem. Valet av perspektiv har två motiveringar: För det första har valet av representation stor betydelse för den bevisteoretiska analysen av de cykliska bevisystemet då den direkt påverkar svårigheten att fastställa viktiga resultat. För det andra leder undersökningar som i huvudsak rör den 'cykliska' delen av cykliska bevissystem så som bevisrepresentation, snarare än specifika egenskaper hos logiken i fråga, till resultat som lättare går att överföra mellan bevissystem för olika logiska teorier.

Avhandlingen är ett bidrag till cyklisk bevisteori på flera sätt. Först formulerar vi en generell metod för att med utgångspunkt i cykliska bevissystem representerade med globala spårvillkor (global trace conditions), vilket är den i dominerande formen av cykliskt bevissystem i litteraturen, generera ekvivalenta representationer som återställningssystem (reset proof systems), en typ av representation med en nyckelroll i tidigare bevisteroretiska undersökningar. I nästa del överför vi en metod för att bevisa en ekvivalens mellan ett cykliskt och ett 'induktivt' bevissystem som först andvändes av Sprenger och Dam, till situationen då den logiska teorin i fråga är Heytings eller Peanos aritmetik. Till skillnad från tidigare bevis av en sådan ekvivalens för aritmetiska teorier som utnyttjat invecklade aritmetiska formaliseringar av metamatematiska begrepp är detta bevis formulerat i termer av representation av cykliska bevis. Slutligen kan vi genom insikter från denna bevismetod presentera en ny form av representation av cykliska bevissystem vars värde för cyklisk bevisteori är större än enbart dess användning i föregående ekvivalensbevis.