Interpreters as consistoids

Harvey Friedman shows that, over Peano Arithmetic as base theory, the consistency statement for a finitely axiomatised theory can be characterised as the weakest statement that, in combination with the base interprets the given theory. Thus, we have a coordinate-free characterisation of these consistency statements modulo base-theory-provable equivalence.

Let us call a base theory that, in analogy to Peano Arithmetic, has such weakest extensions: Friedman-reflexive. We call such a weakest statement the interpreter of the finite theory. Interpreters are not always consistency statements, but they are still consistency-like or ‘consistoids’.

Which theories are Friedman-reflexive and what more can we say about their consistoids and the associated provability-like notion? We will sketch some preliminary insights. (E.g., all complete theories are Friedman-reflexive.)

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 show that Peano Corto as a base theory has many additional desirable properties. In a sense, Peano Corto is, as far as current knowledge goes, the best choice for a base.

We discuss a characterisation of Friedman-reflexive sequential theories. Their interpreters generally are number-system-hopping bounded consistency statements. We have an example to show that some essential hopping may really happen.

The interpreter logic of a finitely axiomatised theory over a Friedman-reflexive sequential base contains at least Löb's logic. A fortiori, we do have an interpreter version of the second incompleteness theorem for the sequential case. (E.g., the interpreter analogue of G2 fails over finitely axiomatised, complete bases.)