Friedman-reflexivity: interpreters as consistoids
Abstract
Harvey Friedman shows that, over Peano Arithmetic, the consistency statement for a finitely axiomatised theory can be characterised as the weakest statement over Peano Arithmetic such that interprets . We study which base theories have the property that, for any finitely axiomatised , there is a weakest such that interprets . 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 can be used to define a provability-like notion for a finitely axiomatised that interprets via an interpretation of in . 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 or is sequential, then the condition for extending L\"ob's Logic is fulfilled. Moreover, if our base theory 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.
Keywords
Cite
@article{arxiv.2111.14413,
title = {Friedman-reflexivity: interpreters as consistoids},
author = {Albert Visser},
journal= {arXiv preprint arXiv:2111.14413},
year = {2022}
}
Comments
(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