# Intutionistic Robinson Arithmetic

By Friedman translation $$HA$$ and $$PA$$ prove the same $$\Pi_2$$ formulas. Is it true for Intutionistic Robinson arithmetic(Robinson axioms with intutionistic logic) and classic Robinson arithmetic?

Axioms of $$Q$$ are:

1. $$\neg(Sx=0)$$
2. $$Sx=Sy\rightarrow x=y$$
3. $$y=0 \lor \exists x(Sx=y)$$
4. $$x+0=x$$
5. $$x+Sy=S(x+y)$$
6. $$x\cdot 0=0$$
7. $$x\cdot Sy=(x\cdot y)+x$$
8. $$\neg(x<0)$$
9. $$0=x\lor 0
10. $$x
11. $$x

Q1. Is it true that for every $$\Pi_2$$ formula $$\phi$$, $$Q\vdash_c \phi$$ iff $$Q\vdash_i \phi$$?

Let $$Q^e=Q\cup \{x=y \lor\neg(x=y),\neg(x=y)\leftrightarrow (x

What happens to Q1 if we replace $$Q$$ by $$Q^e$$?

Q2. Is it true that for every $$\Pi_2$$ formula $$\phi$$, $$Q^e\vdash_c \phi$$ iff $$Q^e\vdash_i \phi$$?

I think the second question can be proved by strong completeness of Beth model for intutionistic logic, but I'm not sure.

Thanks.

Edit:

Definition. The set $$\Delta^+_0$$ formula is the smallest set such that:

• $$s=t\in \Delta^+_0$$ for every term $$s$$ and $$t$$,
• $$s for every term $$s$$ and $$t$$,
• if $$\phi,\psi\in \Delta^+_0$$, then $$\phi\circ \psi\in\Delta^+_0$$ where $$\circ\in \{\lor,\land \}$$,
• if $$\phi\in \Delta^+_0$$, then $$\exists x(x where $$s$$ is a term.
• if $$\phi\in \Delta^+_0$$, then $$\forall x(x where $$s$$ is a term.

By $$\Pi_2$$ formula $$\phi$$ I mean $$\phi=\forall{\bf x}\exists{\bf y}\psi({\bf x},{\bf y})$$ where $$\psi\in \Delta^+_0$$.

• Since the "usual" $Q$ hardly proves any $\Pi_2$ facts and you're interested in a nontrivial extension of $Q$, it might be better to state all the axioms to avoid confusion. Jan 9, 2016 at 0:24
• Michal Dančák is studying intuitionistic $Q$, some of it jointly with Albert Visser. I don't think anything is published, yet. There are subtleties concerning the choice of axioms. Jan 9, 2016 at 10:08
• @FrançoisG.Dorais: Thank you for you answer. As you said "usual" $Q$ hardly proves any $\Pi_2$ formula, but for example for every $\Delta_0$ formula $\phi$,$Q\vdash_c \phi \lor \neg \phi$. Jan 9, 2016 at 10:27
• @EmilJeřábek: Thank you very much. How can I find those work? Jan 9, 2016 at 10:28
• You may try sending an email to Michal or Albert. But you just answered your own question negatively: neither $Q$ nor $Q^e$ should prove decidability of $\Delta_0$ formulas. Jan 9, 2016 at 10:49

Both are false. Consider the following Kripke model $M\vDash Q^e$ (in fact, it satisfies the intuitionistic version of $\mathrm{PA}^-$): it consists of two worlds $u,v$ such that $u$ sees $v$; the first-order structure at $v$ is the semiring $M_v$ of polynomials $f\in\mathbb Z[x]$ with positive leading coefficient (and $0$), the structure at $u$ is the substructure $M_u\subseteq M_v$ consisting of polynomials whose linear coefficient is even. Putting $$\phi(x)=\exists y<x\,(y+y=x),$$ we see that $$M,u\nvDash\phi(a)\lor\neg\phi(a)$$ for the element $a:=2x\in M_u$, witnessing that intuitionistic $Q^e$ does not prove the $\Pi_2$ sentence $$\forall x\,(\phi(x)\lor\neg\phi(x))$$ provable in any classical theory. Under the restrictive definition of $\Pi_2$ as given in the question, one can take the equivalent sentence $$\forall x\,(\exists y<x\,(y+y=x)\lor\forall y<x\,(y+y<x\lor y+y>x))$$ instead.
More generally, if the classical extension of an intuitionistic theory $T\supseteq Q^e$ is $\Pi_2$-conservative over $T$, then $T$ must prove $$\tag{*}\forall x\,(\phi(x)\lor\neg\phi(x))$$ for every $\Delta_0$ formula $\phi$ (exercise: the restrictions in the question are ultimately of no consequence). A higher-level argument that this shouldn’t hold for $T=Q^e$ is that $Q^e$ is included in Cook and Urquhart’s theory IPV (which, confusingly, is the intuitionistic version of $S^1_2$ rather than PV), thus by the witnessing theorem for IPV, it cannot prove $(*)$ unless $\phi(x)$ defines a poly-time predicate (and the theory proves this). Since $\Delta_0$ formulas define arbitrary predicates in the linear-time hierarchy, this cannot happen for all $\Delta_0$ formulas unless P = NP. The argument relativizes to subtheories of intuitionistic versions of $S^i_2$ for any $i$, using non-collapse of PH as an assumption in place of P $\ne$ NP.