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<x$
10. $x<y \leftrightarrow (Sx<y \lor Sx=y)$
11. $x<Sy \leftrightarrow (x<y\lor x=y)$



> 
> 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<y \lor y<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](https://www.google.com/url?sa=t&rct=j&q=&esrc=s&source=web&cd=1&cad=rja&uact=8&ved=0ahUKEwixw6LikZvKAhXJuhoKHTK-CGYQFggiMAA&url=http%3A%2F%2Faleteya.cs.buap.mx%2F%7Ejlavalle%2Fpapers%2Fvan%2520Dalen%2FIntuitionistic%2520Logic.pdf&usg=AFQjCNGTB77-ykRxaWnWNCgjp8K43TEmcA&sig2=d4SvNkos7aH1KtwXhnxwMA) 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<t\in \Delta^+\_0$ 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<s \land \phi(x))\in \Delta^+\_0$ where $s$ is a term.
* if $\phi\in \Delta^+\_0$, then $\forall x(x<s \rightarrow \phi(x))\in \Delta^+\_0$ 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$.



Intutionistic Robinson Arithmetic
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.


