Characterizations of interpretability in bounded arithmetic

TL;DR

This paper examines the conditions under which interpretability, conservativity, and restricted consistency are equivalent in formal arithmetical theories, focusing on the Orey-Hájek characterization and its formalization.

Contribution

It provides a detailed analysis of the Orey-Hájek characterization, identifying necessary conditions and the meta-theoretical framework for formalizing these equivalences.

Findings

Clarifies conditions for equivalence of interpretability, conservativity, and restricted consistency.

Analyzes the formalization of the Orey-Hájek characterization.

Provides insights into the meta-theoretical requirements for these formalizations.

Abstract

This paper deals with three tools to compare proof-theoretic strength of formal arithmetical theories: interpretability, $\Pi^0_1$-conservativity and proving restricted consistency. It is well known that under certain conditions these three notions are equivalent and this equivalence is often referred to as the Orey-H\'ajek characterization of interpretability. In this paper we look with detail at the Orey-H\'ajek characterization and study what conditions are needed and in what meta-theory the characterizations can be formalized.