The Preservativity Logic of Heyting Arithmetic
Rosalie Iemhoff

Preservativity logic is a constructive analogue of interpretability logic, to which it is classically equivalent. Like in the classical setting, provability can be expressed in terms of preservativity. Since the provability logic of Heyting Arithmetic is not contained in the provability logic of Peano Arithmetic, this also holds for preservativity logic. In this talk I will summarize the results on the provability and preservativity logic of Heyting Arithmetic that I obtained as a PhD-student. In particular, I will introduce a Kripke semantics and prove it to be sound and complete for the principles of the preservativity logic of Heyting Arithmetic known at that time.