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 for intutionistic logic, but I'm not sure.



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

  • 3
    $\begingroup$ 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. $\endgroup$ Jan 9, 2016 at 0:24
  • 1
    $\begingroup$ 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. $\endgroup$ Jan 9, 2016 at 10:08
  • $\begingroup$ @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$. $\endgroup$ Jan 9, 2016 at 10:27
  • $\begingroup$ @EmilJeřábek: Thank you very much. How can I find those work? $\endgroup$ Jan 9, 2016 at 10:28
  • $\begingroup$ 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. $\endgroup$ Jan 9, 2016 at 10:49

1 Answer 1


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.