Friedman-reflexivity: interpreters as consistoids

TL;DR

This paper explores the concept of Friedman-reflexivity in base theories, characterizes such theories, and introduces interpreter logics that extend modal logics like S4 and L"ob's, with applications to provability and interpretability.

Contribution

It introduces the notion of Friedman-reflexivity for theories, characterizes sequential theories that are Friedman-reflexive, and develops interpreter logics satisfying L"ob conditions.

Findings

Peano Corto is Friedman-reflexive with bounded consistency statements.

A characterization theorem for Friedman-reflexive sequential theories is provided.

Conditions for extending modal logics like S4, K45, and L"ob's are established.

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 ${\sf 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\"ob Conditions. We provide conditions for when these logics extend {\sf S}4, {\sf K}45, and L\"ob's Logic. We show that, if either $U$ or $A$ is sequential, then the condition for extending L\"ob'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\"odel numbers. At the end of the paper, we briefly discuss how successful the coordinate-free approach is.