Friedman-reflexivity: interpreters as consistoids

Abstract

In the present paper, we explore an idea of Harvey Friedman to obtain a coordinate-free presentation of consistency. 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 PA + C interprets A. We study the question 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 explore various implications of Friedman-reflexiveness. 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 illustrate that Peano Corto as a base theory has additional desirable properties. 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 explore what modal logics this idea gives rise to. We call such logics interpreter logics. We show that, generally, these logics satisfy the L¨ob Conditions, aka K4. We provide conditions for when these logics extend S4, K45, 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 how successful the coordinate-free approach is.