Harvey Friedman posted several manuscripts [1] proposing a program for "strict" reverse mathematics, in the sense that the base theory should be mathematically natural and coding-free.


In them he describes a number of two-sorted systems (with sorts for integers and finite sets or sequences of integers) weaker than the base theory RCA$\_0$ of reverse mathematics.


I wonder if it is known whether any of Friedman's systems are essentially equivalent to the two-sorted system called V$^0$ in Cook-Nguyen [2] (which if I understand correctly was introduced by Zambella [3]).


[1] <http://people.math.osu.edu/friedman.8/pdf/InevLogStr082907.pdf> among others


[2] Stephen Cook, Phuong Nguyen. Logical foundations of proof complexity, 2010.


[3] Domenico Zambella. Notes on polynomially bounded arithmetic, JSL, Sep. 1996.



Harvey Friedman's strict reverse mathematics vs. Cook-Nguyen's V$^0$
If I understand the notation correctly, Theorem 8.28 in [1] shows that FSTZ is a notational variant of $V^0$ (and the same holds for all the theories Friedman shows to be definitionally equivalent to FSTZ in later sections, but see below for a caveat).


Specifically, FSTZ is biinterpretable with $V^0$ as follows. (I will use Zambella’s axiomatization for simplicity.)


The natural interpretation of $V^0$ in FSTZ is given by using nonnegative integers for the number sort, and sets of nonnegative integers for the second sort (with set equality—present in Zambella’s language, but not in Friedman’s language—interpreted by extensionality). The translation of $\Sigma^b\_0$-comprehension is provable by Theorem 8.28, the axiom $A\ne\varnothing\to\exists x\in A\,(A<x+1)$ follows from the existence of the largest element of $A$ (stated in Lemma 8.1), and the other axioms are basically axioms of discretely ordered semirings, whose translation are provable in FSTZ by Theorem 8.28 and Lemma 8.1.


Conversely, we can interpret FSTZ in $V^0$ e.g. by representing nonnegative integers $n$ by $2n$, and $-n$ by $2n-1$. Proving the translation of the axioms of FSTZ in $V^0$ is then an easy exercise. The composition of the two interpretations in the $V^0\to FSTZ\to V^0$ direction is ($V^0$-provably) definably isomorphic to identity via the mapping $n\mapsto2n$, $A\mapsto\{2n:n\in A\}$. The composition in the other direction is definably isomorphic to the identity interpretation via the mappings
\begin{align\*}
f(n)&=\begin{cases}n/2,&\text{$n$ even,}\\-(n+1)/2,&\text{$n$ odd,}\end{cases}\\
F(A)&=\{f(n):n\in A\},
\end{align\*}
again provably in FSTZ (with the help of Theorem 8.28).




---


I believe Friedman’s arguments about FSTZEXP in 11.7, 11.8, and (even more so) 11.11 are erroneous. The construction in the proof of Lemma 11.7 does not work, because if $n^m$ does not exist, the set $\{\exp(n,0),\dots,\exp(n,m)\}$ is cofinal in $M$, and therefore cannot be an internal set in $M$. (And even if it were, there is no reason why the definition used in the proof should be *provable* in FSTZEXP, which would be needed to make it a definitional extension.)


Note that FSTZEXP proves the order axiom
$$n\ge2\land 0\le m<r\to\exp(n,m)<\exp(n,r)$$
of FSTZEXP' as follows: the set $A=\{\exp(n,i):0\le i\le r-1\}$ exists by axioms of FSTZEXP, and being nonempty, it has a largest element $\exp(n,i)$ by FSTZ. Since $1\in A$, $\exp(n,i)\ne0$, hence $\exp(n,i+1)=n\exp(n,i)>\exp(n,i)$. This contradicts the maximality of $\exp(n,i)$ unless $i=r-1$, in which case $\exp(n,m)\le\exp(n,r-1)<\exp(n,r)$ as $\exp(n,m)\in A$.


I *think* that Lemma 11.7 holds regardless: if we take $M$ a countable model of FSTZ, we can find an order isomorphism $f$ of (the first-order part of) $M$ and its initial segment $I$ such that $n^m$ exists for all $m\in I$ and $n\in M$ (using the fact that the order reduct of $M$ is recursively saturated), and then we can define $\exp(n,m)=n^{f(m)}$. However, this does not give an interpretation, let alone definitional equivalence.


