Respondent:
Mattias Granberg Olsson, Department of Philosophy, Linguistics and Theory of 91̽»¨
Thesis title:
Fixed IDs about Truth:
Truth and Fixpoints over Intuitionistic Arithmetic
Examining committee:
Docent Vera Koponen, Uppsala universitet
Associate Professor Takako Nemoto, Tohoku University
Associate Professor Benno van den Berg, University of Amsterdam
Substitute if member in the committee will be missing:
Docent Fredrik Engström, Göteborgs universitet
Opponent:
Junior Associate Professor Makoto Fujiwara, Tokyo University of 91̽»¨
Chair:
Docent Susanna Radovic, Göteborgs universitet
Abstract
This dissertation concerns first-order theories of iterated positive truth and fixpoints over intuitionistic arithmetic in three respects: the strength of these theories relative to the arithmetic base theories, relationships between theories of positive fixpoints and compositional and disquotational truth for truth-positive sentences, and a comparison with the classical case.
It is known that these theories over classical Peano arithmetic (PA) are mutually interpretable and exceeds the strength of PA. Over intuitionistic Heyting arithmetic (HA), on the other hand, finite iterations of strictly positive fixpoints have been shown to be conservative.
After introducing the setting and presenting the earlier results, as well as the technical tools, the main section of the dissertation can be roughly divided into two parts. The first presents a novel proof of the conservativity result above. The proof interprets the theories into the logic of partial terms where a realizability interpretation is used to reduce the problem to fixpoints for almost negative operator forms. A diagonal argument using a hierarchy of almost negative formulae with
corresponding partial satisfaction predicates yields the result.
The second part generalises the tri-interpretation result from the second paragraph to intuitionistic theories, by proposing a new generalisation of positivity called guarded positivity with the aim to better capture the behaviour of intuitionistic implications and their interplay with transfinite iterations of truth and fixpoint predicates. As a corollary, these transfinite theories are stronger than HA.
A discussion of the results and the methods used concludes the dissertation.
