6:04 AM
@user76284 I believe it is very weak, like PA−. For comparison, PA+RCF, which I had called T in the preceding discussion, is exactly as strong as PA/ACA0, and SRA is exactly as strong as ACA. ACA0 interprets PA+RCF because you can interpret ℝ to be subsets of ℕ in ACA0 that encode a downward-closed subset of the fraction field F of ℕ that correspond to roots of odd-degree polynomials over F.

6:30 AM
I'm not sure how to prove that PA− interprets your theory, but I believe it is of that strength because you lack anything that can provide induction. You may also be interested to note that Internal Sup proves Induction over SRA minus Induction:
```First note that Internal Sup implies Internal Inf (every "≤" replaced by "≥").
Take any property Q on ℕ such that Q(0) and ∀k∈ℕ ( Q(k)⇒Q(k+1) ).
If ∃k∈ℕ ( ¬Q(k) ):
Let c∈ℕ such that ¬Q(c) and let f = ( ℕ k ↦ Q(k) ? c : k ).
Clearly f ≥ 0, so let m = inf(f).
Then m∈ℕ because m ≤ ceil(m) ≤ f.
Thus ¬Q(m) and so m > 0 since Q(0).
Thus Q(m−1) because m−1 < inf(f).
Thus Q(m) since ∀k∈ℕ ( Q(k)⇒Q(k+1) ).