# Strength of Bishop style constructive mathematics vs $\mathsf{RCA}_0$

This question came out of this other MO question of mine. My question is

Is there a formal comparison between $\mathsf{RCA}_0$ and $\mathsf{BISH}$ (Bishop style constructive mathematics as used in constructive reverse mathematics)?

More specifically,

Is $\mathsf{BISH}$ strictly weaker than $\mathsf{RCA}_0$ (or $\mathsf{RCA_0}$ plus full induction) when formalized and restricted to second order sentences of arithmetic?

(Update: I wasn't entirely clear, I meant to ask if everything provable in provable in $\mathsf{BISH}$ is provable in $\mathsf{RCA_0}$ plus full induction. Obviously, nonconstuctive principles like LEM are provable in $\mathsf{RCA_0}$ but not in $\mathsf{BISH}$.)

I am sure people have thought of this, but I couldn't find a resource.

Also, I imagine there could be a lot of caveats. I don't know much about Bishop-style constuctivism, but I gather the community doesn't like formal theories or models, which are generally needed for such comparisons. However, I know others are interested in such things, and I believe there are formalizations of $\mathsf{BISH}$ that at least get close to the intuitive idea.

Also, this question can be answered without formal theories:

Is there a theorem known to be constructively provable (in the informal style of Bishop), that is not provable in $\mathsf{RCA}_0$ (or $\mathsf{RCA}_0$ plus full induction)?

-
One difficulty with comparing these will be that RCA wants to encode things, but BISH does not. Would you compare the encoded theorems on one side with the unencoded ones on the other? –  Andrej Bauer Jul 11 at 8:36
Andrej, would you be able to give an example? I assume the reals are still encoded as fast Cauchy seuqences of rationals. However, as you mention this, I recall functions and sets not being easily encodable by each other. Is this an example? Maybe the correct way around this is to expand the language of Second Order arithmetic to handle these objects (unencoded) on the $\mathsf{RCA}_0$ side, and then compare the results. And to be clear, I don't know the details, but I imagine someone has looked into this. Correct? –  Jason Rute Jul 11 at 9:07
To make any precise sense of claims about "provability in BISH", simply replace BISH with a formalized constructive system, such as a fragment of $\text{E-HA}^\omega$. Then it becomes straightforward to compare the strength with classical formal systems. These formal systems are common in proof theory, e.g. in proof mining, or in contexts like my paper with Jeff Hirst, "Reverse mathematics and uniformity in proofs without excluded middle". –  Carl Mummert Jul 11 at 16:55
Carl's comment is right on the spot. Since Bishop's constructivism and similarly Brouwer's intuitionism are not formal systems (by design) one can only speculate a comparison with formal systems. –  François G. Dorais Jul 12 at 1:26

BISH famously includes the full axiom of choice scheme (in the functional language of second-order arithmetic), which is utterly weak in that context but very strong when combined with the law of the excluded middle. This is precisely the context in which Bishop wrote that the axiom of choice follows from "the very meaning of existence".

Thus there are formulas of second-order arithmetic provable in BISH that are not even provable in $Z_2$, the system of clasical second-order arithmetic with full induction and comprehension.

-
Ok, I see that choice principles are a big difference. –  Jason Rute Jul 11 at 21:12
A correction: The Internet seems to say that (1) Bishop only used dependent choice, and (2) the full axiom of choice would imply (a version of) the law of excluded middle. But still, dependent choice seems to be equivalent to $\mathsf{Z}_2$ in reverse mathematics (if I am reading Simpson's book correctly). (I am not an expert on this, so feel free to correct me.) –  Jason Rute Jul 11 at 21:15
I was mistaken somewhat on my last comment. In Simpson's book, dependent choice is stronger than choice. And $\Sigma^1_\infty$ dependent choice is indeed strictly stronger than $\mathsf{Z}_2$ (I was reading a theorem in Simpson's book incorrectly). This terminology is confusing to me and and doesn't seem to agree with that in, say, kurims.kyoto-u.ac.jp/~kyodo/kokyuroku/contents/pdf/1381-10.pdf . Notice the quantifier order difference. –  Jason Rute Jul 11 at 22:01
@JasonRute: It's very difficult to sort these things out. The axiom of choice for sets implies the law of excluded middle (Diaconescu's Theorem). The scheme that Carl is referring to is for functions and is much tamer in a constructive setting. –  François G. Dorais Jul 12 at 1:12
@Jason Rute: It is very easy to get confused about Diaconescu's theorem and its relationship with constructive arithmetic, particularly when just looking at "headline" summaries of the results. The "axiom of countable choice" in Ishihara is basically of the same form as the schemes Simpson calls AC. Actually even $\Sigma^1_{\infty}\text{-AC}_0$ is unprovable in $Z_2$. The other schemes in Simpson's book take more study to work out what is going on with them compared to regular "dependent choice". One key point in comparing with Ishihara is that Simpson allows parameters in the formulas. –  Carl Mummert Jul 12 at 1:43

The intermediate value theorem seems to be provable in $RCA_0$ but is certainly not provable in the usual form in $BISH$. I am relying on Wikipedia.

-
You should remove that last sentence, then we can edit Wikipedia to use this answer as a reference! :-) –  Asaf Karagila Jul 11 at 9:19

I believe BISH includes the Fan Theorem, which, being the contrapositive of weak König's lemma, is not provable in $RCA_0$.

-
BISH does not include FAN. See e.g. Bridges/Richman - Varieties of constructive mathematics. –  Bas Spitters Jul 11 at 20:17

LPO is certainly not true in $\mathsf{BISH}$, but I believe it can be formalized and proved in $\mathsf{RCA}_0$.

I don't know if there's any agreed upon theory for formalizing $\mathsf{BISH}$ but there are formal theories used for constructive mathematics that have higher consistency strength than $\mathsf{RCA}_0$. For instance, $\mathsf{CZF}$ has the same consistency strength as $\mathsf{ID}_1$. In particular, it proves that $\mathsf{RCA}_0$ is consistent.

-
LPO can be proved in theories of second-order arithmetic much weaker than $\mathsf{RCA}_0$; LPO is a theorem of classical logic alone. –  Carl Mummert Jul 11 at 17:03

Here is a reference for "$\operatorname{RCA}_{\hspace{.01 in}0}$ proves the intermediate value theorem".

Let $\; f : \mathbb{R} \to \mathbb{R} \:$ be given by $\;\; f(x) \: = \: (2\hspace{-0.03 in}\cdot\hspace{-0.03 in}x)+|\hspace{.02 in}x\hspace{-0.03 in}-\hspace{-0.04 in}1|-(\hspace{.01 in}|\hspace{.02 in}x\hspace{-0.03 in}-\hspace{-0.04 in}1|+h) \:\:\:$,
for some real number $h$ such that $\; h \approx 0\:\:$.
$\:f(-2) \approx -1 < 0 < 1 \approx f(2) \:$, $\:$ so the intermediate value theorem applies to $\:f$.
If $\: h < 0 \:$ then all roots $z$ of $\:f$ are such that $\; z < -1\:\:$.
If $\: 0 < h \:$ then all roots $z$ of $\:f$ are such that $\; 1 < z\:\:$.
Intuitively, it follows from that one cannot prove 'constructively' that $\:f$ has a root.
However, since I know very little about $\operatorname{BISH}$, I don't know how to
convert that to "$\operatorname{BISH}$ doesn't prove the intermediate value theorem".

-
BISH does not prove this. –  Andrej Bauer Jul 11 at 11:20
... where "this" is the intermediate value theorem, or the last sentence of my answer? $\hspace{.73 in}$ –  Ricky Demer Jul 11 at 18:49
I think Carl's and Henry's answers seem to suggest that "everything that can be proved 'constructively', can be proved in $RCA_0$" is not true. (Although you left yourself wiggle room by your use of quotes.) –  Jason Rute Jul 11 at 20:04
Okay, I just deleted that sentence. $\:$ –  Ricky Demer Jul 11 at 20:11
BISH does not prove that for all $h$ the map $f$ has a root. –  Andrej Bauer Jul 11 at 21:26