Licentiatseminarium i logik. Titeln på licentiatuppsatsen är "Computational Content of Fixed Points".
Seminarium
Datum
20 dec 2022
Tid
09:15 - 11:00
Plats
Sal J309, Renströmsgatan 6, Humanisten
Arrangör
Institutionen för filosofi, lingvistik och vetenskapsteori
Examinator: Docent Fredrik Engström, Göteborgs universitet Opponent: Docent Sebastian Enqvist, Stockholms universitet
En kopia av licentiatuppsatsen kan fås genom att mejla Bahareh Afshari och be om en sådan.
Sammanfattning:
Vi studerar det beräkningsmässiga innehållet hos fixpunkter i förhållande till två logiska system med olika egenskaper. Gemensamt för båda studierna är en metod för att hantera fixpunkternas iterativa karaktär. I den första delen riktas intresset mot ett cykliskt system ICA för intuitionistisk aritmetik. Den formella definitionen av systemet följs av införandet av en typad λY-kalkyl, vars termer representerar den deduktiva processen för cykliska bevis. Här ges en metod för att producera rekursionsscheman från instanser av cykliska bevis. Resultatet är en grammatik vars språk består av λ-termer, som fångar det beräkningsmässiga innehållet som finns i det ursprungliga beviset. I den andra delen tittar vi på iteration av fixpunkter i termer av tillslutningsordinaltal för formler i den modala μ-kalkylen.
Här presenteras en metod för att bestämma en övre gräns för tillslutningsordinaltal och den tillämpas på formler i fragment av Σ1-klassen, där resultaten ligger i linje med redan existerande arbeten. De viktigaste verktygen för att fastställa en övre gräns är kommenterade strukturer, för att spåra hur modelländringar påverkar ordinaltalen, och en pumpteknik för dessa strukturer.
