12
$\begingroup$

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.

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

$\endgroup$
  • 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$ – François G. Dorais Jan 9 '16 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$ – Emil Jeřábek Jan 9 '16 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$ – Erfan Khaniki Jan 9 '16 at 10:27
  • $\begingroup$ @EmilJeřábek: Thank you very much. How can I find those work? $\endgroup$ – Erfan Khaniki Jan 9 '16 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$ – Emil Jeřábek Jan 9 '16 at 10:49
7
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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