Fixed IDs about Truth – Truth and Fixpoints over Intuitionistic Arithmetic

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.