Faculty Opponent: Associate Professor Michal Skrzypczak, University of Warsaw, Poland

Examining committee: 

  • Professor Martin Lange, University of Kassel, Germany
  • Associate Professor lsabel Oitavem, NOVA University of Lisbon, Portugal
  • Associate Professor Paulo Oliva, Queen Mary University of London, UK
  • Professor Eleni Gregoromichelaki, Göteborgs universitet (substitute)

Abstract A fixed point of a function can be described as a special mathematical object, with several powerful applications. This thesis studies fixed points in the context of two distinct frameworks. Common to both research strands is a method for dealing with the iterative nature of fixed points. The first part of the thesis looks at the computation of least fixed points in terms of closure ordinals of formulas in the modal 𝜇𝜇 ­calculus. Using annotated structures, a new framework is defined to describe how the iterations of a fixed point formula evolve in a transition system. Applying a pumping technique allows us to establish an upper bound for countable closure ordinals. The method is tailored to the lower levels of the alternation hierarchy, but the fragment covered is broad enough to allow for considerations on the effects of fixed point alternation. In the second part, fixed points are considered in the context of a cyclic proof system for intuitionistic arithmetic. Cyclic proofs internalise induction in their structure, suggesting a natural fitting with quantifiers defined in terms of fixed points. Using higher order recursion schemes generated from instances of cyclic proofs, we investigate the computational content implicit in the initial proof.