Public defence of Giacomo Barlucchi’s Licentiate thesis.

Opponent Docent Sebastian Enqvist, Stockholms universitet
Examiner Docent Fredrik Engström, Göteborgs universitet

We study the computational content of fixed points in relation to two logical systems with distinct characteristics. Common to both research strands is a method for dealing with the iterative nature of fixed points. In the first part the interest is directed to a cyclic system ICA for intuitionistic arithmetic. The formal definition of the system is followed by the introduction of typed λY-calculus, whose terms represent the deductive process of cyclic proofs. A method for producing recursion schemes from instances of cyclic proofs is given. The result is a grammar whose language consists of λ-terms, capturing the computational content implicit in the initial proof. In the second part, we look at the iteration of fixed points in terms of closure ordinals of formulas in the modal μ-calculus. A method for determining an upper bound on closure ordinals is presented and applied to formulas in fragments of the Σ1 class, with results that are in line with the already existing works. Annotated structures, to track how model changes affect the ordinals, and a pumping technique for these structures are the main tools used to establish an upper bound.

A copy of Giacomo’s thesis can be obtained by sending an email to the contact person Bahareh Afshari.