Harvey Friedman's strict reverse mathematics vs. Cook-Nguyen's V$^0$

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]).

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

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

-
The "strictness" that Friedman proposes is less about logical strength of the base system and more about the relevance of the base system, so the first sentence is not quite correct. For example, $\mathsf{RCA}_0$ includes $\Sigma^0_1$-induction which is relatively meaningless to an everyday mathematician in the sense that you can't expect an everyday mathematician to tell whether their use of induction is $\Sigma^0_1$ or not. Friedman proposes systems where restrictions on induction (and similar schemes) are such that every mathematician could check them and ....... – François G. Dorais Jan 5 '14 at 23:28
...... the distinction between such instances and others feels natural in everyday mathematics. Note that this makes sense for systems that can be much stronger than $\mathsf{V}^0$ or $\mathsf{RCA}_0$ or whatnot. In that sense, $\mathsf{V}^0$ is just as arcane as $\mathsf{RCA}_0$ and therefore does not fit well into Friedman's goals. On the other hand, it would be nice (as you asked) to compare Friedman's "strict" systems with $\mathsf{V}^0$ and other very weak systems proposed by Cook and Nguyen. – François G. Dorais Jan 5 '14 at 23:30
Thanks, @françois... I see what you are saying. I rephrased my question to avoid propagating this confusion. – Kevin Watkins Feb 2 '14 at 19:18

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.

-
Completely off-topic, but sentences like this "because if $n^m$ does not exist,..." strike me as particularly ultrafinitist. – David Roberts Feb 2 '14 at 23:43
@DavidRoberts: These $n$ and $m$ are not usual integers, but elements of a nonstandard model where exponentiation is not necessarily total. The way I wrote it is a common jargon, but more properly it should read $M\models\neg\exists x\,\phi(n,m,x)$ where $\phi$ is a $\Delta_0$-definition of the graph of exponentiation in $I\Delta_0$. – Emil Jeřábek Feb 3 '14 at 12:22
I mean, in FSTZ. – Emil Jeřábek Feb 3 '14 at 12:24