Friedman-reflexivity: interpreters as consistoids

Abstract

Harvey Friedman shows that, over Peano Arithmetic, the consistency statement for a finitely axiomatised theory $A$ can be characterised as the weakest statement $C$ over Peano Arithmetic such that $\mathsf{PA}+C$ interprets $A$. We study which base theories $U$ have the property that, for any finitely axiomatised $A$, there is a weakest $C$ such that $U+C$ interprets $A$. We call such theories Friedman-reflexive. We show that a very weak theory, Peano Corto, is Friedman-reflexive. We do not get the usual consistency statements here, but bounded, cut-free or Herbrand consistency statements. We prove a characterisation theorem for Friedman-reflexive sequential theories. We provide an example of a Friedman-reflexive sequential theory that substantially differs from the paradigm cases of Peano Arithmetic and Peano Corto. The consistency-like statements provided by a Friedman-reflexive base $U$ can be used to define a provability-like notion for a finitely axiomatised $A$ that interprets $U$ via an interpretation $K$ of $U$ in $A$. We call the modal logics based on this idea \emph{interpreter logics}. These logics satisfy the Löb Conditions. We provide conditions for when these logics extend {\sf S}4, {\sf K}45, and Löb's Logic. We show that, if either $U$ or $A$ is sequential, then the condition for extending Löb's Logic is fulfilled. Moreover, if our base theory $U$ is sequential and if, in addition, its interpreters can be effectively found, we prove Solovay's Theorem. This holds even if the provability-like operator is not necessarily representable by a predicate of Gödel numbers. At the end of the paper, we briefly discuss how successful the coordinate-free approach is.

(i) some new notations were introduced to make the paper more readable, (ii) the section on interpreter logics was substantially extended, (iii) new results were added to the paper, (iv) a new both backward and forward looking last section was added

References in corpus (1)

• The theory of hereditarily bounded sets