8
$\begingroup$

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 $\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)?

Improve this question
$\endgroup$
4
  • $\begingroup$ 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? $\endgroup$
    – Andrej Bauer
    Commented Jul 11, 2013 at 8:36
  • $\begingroup$ 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? $\endgroup$
    – Jason Rute
    Commented Jul 11, 2013 at 9:07
  • 1
    $\begingroup$ 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". $\endgroup$
    – Carl Mummert
    Commented Jul 11, 2013 at 16:55
  • $\begingroup$ 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. $\endgroup$
    – François G. Dorais
    Commented Jul 12, 2013 at 1:26

7 Answers 7

Reset to default
10
$\begingroup$

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.

Improve this answer
$\endgroup$
5
  • $\begingroup$ Ok, I see that choice principles are a big difference. $\endgroup$
    – Jason Rute
    Commented Jul 11, 2013 at 21:12
  • $\begingroup$ 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.) $\endgroup$
    – Jason Rute
    Commented Jul 11, 2013 at 21:15
  • $\begingroup$ 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. $\endgroup$
    – Jason Rute
    Commented Jul 11, 2013 at 22:01
  • 3
    $\begingroup$ @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. $\endgroup$
    – François G. Dorais
    Commented Jul 12, 2013 at 1:12
  • 2
    $\begingroup$ @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. $\endgroup$
    – Carl Mummert
    Commented Jul 12, 2013 at 1:43
3
$\begingroup$

Maybe it is interesting that for $CT$ (Church thesis) $BISH+CT$ is consistent, but $RCA_0\vdash \neg CT$. By $CT$ I mean axiom scheme of $CT$ for every formula.

$CT-scheme$: For every first order formula $\psi(x,y)$, $\forall x \exists y \psi(x,y)\rightarrow \exists e\forall x\exists y(\psi(x,y)\land \phi(e,x,y)$ where $\phi(e,x,y)$ is kleene predicate.

Also let $U(e,x,y)$ be a first order formula such get godel number of a formula like $\eta(x,y)$ in $e=\ulcorner \eta(x,y) \urcorner$, gets $x,y$ and simulates $\eta(x,y)$, then $CT$ can be formalized in one axiom like this: $$CT:=\forall u\exists e(\forall x\exists y U(u,x,y)\rightarrow \forall x\exists y(U(u,x,y)\land \phi(e,x,y)))$$ Define $$h(n)=\left\{\begin{matrix} 1,\exists x\phi(n,n,x)\\ 0, \forall x \neg \phi(n,n,x) \end{matrix}\right.$$ This function can represent by formula $H(n,y):=(\exists x\phi(n,n,x)\land y=1)\lor(\forall x\neg\phi(n,n,x)\land y=0)$, trivially $RCA_0\vdash \forall n \exists y H(n,y)$, therefore $RCA_0\vdash \neg CT$, but $BISH+CT\nvdash \bot$, similar arguments work if we take axiom scheme of $CT$ instead of $CT$

Improve this answer
$\endgroup$
10
  • $\begingroup$ I'm confused. Doesn't $CT$ say "every function is computable"? If so, then $\mathsf{RCA}_0$ can't prove the existence of a noncomputable function/set. Take the model $\mathsf{REC}$. Am I missing something? $\endgroup$
    – Jason Rute
    Commented Jan 20, 2016 at 21:38
  • $\begingroup$ @JasonRute: much as I know $CT$ say "every function is turing computable", therefore the function $h(n)=\left\{\begin{matrix} 1,\exists x\phi(n,n,x)\\ 0, \forall x \neg \phi(n,n,x) \end{matrix}\right.$ is not turing computable where $\phi(e,x,y)$ is kleene predicate, I think this funcion is definable and provably total in $RCA_0$ but it is not provably total in BISH, because it is consistent with $CT$, but it is possible that I miss somthing $\endgroup$
    – Erfan Khaniki
    Commented Jan 20, 2016 at 22:00
  • $\begingroup$ Again, $\mathsf{RCA}_0$ has restricted comprehension. You can't say that this function $h$ exists, or any such set or function on the natural numbers, unless the defining formula is provably equivalent to both a $\Sigma_1$ and $\Pi_1$ formula. The halting problem is certainly not of this form. $\endgroup$
    – Jason Rute
    Commented Jan 20, 2016 at 22:16
  • $\begingroup$ @JasonRute: Does $RCA_0$ has classical logic as underlying logic? $\endgroup$
    – Erfan Khaniki
    Commented Jan 20, 2016 at 22:20
  • 1
    $\begingroup$ @JasonRute: yes you are right, the $CT$ that I have in mind is scheme axiom, I mean for every formula $\psi$ we have a $CT$ axiom like :$\forall x \exists y \psi(x,y)\rightarrow \exists e \forall x \exists y (\phi(e,x,y)\land \psi(x,y))$ $\endgroup$
    – Erfan Khaniki
    Commented Jan 20, 2016 at 22:42
2
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • 7
    $\begingroup$ You should remove that last sentence, then we can edit Wikipedia to use this answer as a reference! :-) $\endgroup$
    – Asaf Karagila ♦
    Commented Jul 11, 2013 at 9:19
2
$\begingroup$

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

Improve this answer
$\endgroup$
1
  • 4
    $\begingroup$ BISH does not include FAN. See e.g. Bridges/Richman - Varieties of constructive mathematics. $\endgroup$
    – Bas Spitters
    Commented Jul 11, 2013 at 20:17
2
$\begingroup$

Wikipedia thinks RCA roughly corresponds to BISH.

Joan Moschovakis' slides give a recent overview of formal constructive reverse mathematics.

Improve this answer
$\endgroup$
1
  • 1
    $\begingroup$ That table in Wikipedia comes from Simpson's book (p 43 in second edition). The word "roughly" should not be ignored based on the above answers. $\endgroup$
    – Jason Rute
    Commented Jul 11, 2013 at 22:05
1
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • 2
    $\begingroup$ LPO can be proved in theories of second-order arithmetic much weaker than $\mathsf{RCA}_0$; LPO is a theorem of classical logic alone. $\endgroup$
    – Carl Mummert
    Commented Jul 11, 2013 at 17:03
1
$\begingroup$

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".

Improve this answer
$\endgroup$
5
  • 1
    $\begingroup$ BISH does not prove this. $\endgroup$
    – Andrej Bauer
    Commented Jul 11, 2013 at 11:20
  • $\begingroup$ ... where "this" is the intermediate value theorem, or the last sentence of my answer? $\hspace{.73 in}$ $\endgroup$
    – user5810
    Commented Jul 11, 2013 at 18:49
  • $\begingroup$ 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.) $\endgroup$
    – Jason Rute
    Commented Jul 11, 2013 at 20:04
  • $\begingroup$ Okay, I just deleted that sentence. $\:$ $\endgroup$
    – user5810
    Commented Jul 11, 2013 at 20:11
  • $\begingroup$ BISH does not prove that for all $h$ the map $f$ has a root. $\endgroup$
    – Andrej Bauer
    Commented Jul 11, 2013 at 21:26

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .