Aritmética intuitiva de Robinson

Question

Por la traducción de Friedman $HA$ et $PA$ demostrar lo mismo $\Pi_2$ fórmulas. ¿Es cierto para la aritmética intuicionista de Robinson (axiomas de Robinson con lógica intuicionista) y la aritmética clásica de Robinson?

Axiomas de $Q$ son:

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. ¿Es cierto que para cada $\Pi_2$ fórmula $\phi$ , $Q\vdash_c \phi$ si $Q\vdash_i \phi$ ?

Dejemos que $$Q^e=Q\cup \{x=y \lor\neg(x=y),\neg(x=y)\leftrightarrow (x<y \lor y<x) \}$$

¿Qué ocurre con Q1 si sustituimos $Q$ por $Q^e$ ?

Q2. ¿Es cierto que para cada $\Pi_2$ fórmula $\phi$ , $Q^e\vdash_c \phi$ si $Q^e\vdash_i \phi$ ?

Creo que la segunda cuestión puede ser demostrada por la completitud fuerte de Modelo Beth para la lógica intuitiva, pero no estoy seguro.

Merci.

Editar :

Definición. El conjunto $\Delta^+_0$ es el conjunto más pequeño tal que:

• $s=t\in \Delta^+_0$ para cada término $s$ et $t$ ,
• $s<t\in \Delta^+_0$ para cada término $s$ et $t$ ,
• si $\phi,\psi\in \Delta^+_0$ entonces $\phi\circ \psi\in\Delta^+_0$ donde $\circ\in \{\lor,\land \}$ ,
• si $\phi\in \Delta^+_0$ entonces $\exists x(x<s \land \phi(x))\in \Delta^+_0$ donde $s$ es un término.
• si $\phi\in \Delta^+_0$ entonces $\forall x(x<s \rightarrow \phi(x))\in \Delta^+_0$ donde $s$ es un término.

Por $\Pi_2$ fórmula $\phi$ Es decir $\phi=\forall{\bf x}\exists{\bf y}\psi({\bf x},{\bf y})$ donde $\psi\in \Delta^+_0$ .

Answer 1

Ambas cosas son falsas. Consideremos el siguiente modelo de Kripke $M\vDash Q^e$ (de hecho, satisface la versión intuicionista de $\mathrm{PA}^-$ ): consta de dos mundos $u,v$ tal que $u$ ve $v$ la estructura de primer orden en $v$ es el semirremate $M_v$ de polinomios $f\in\mathbb Z[x]$ con coeficiente principal positivo (y $0$ ), la estructura en $u$ es la subestructura $M_u\subseteq M_v$ formado por polinomios cuyo coeficiente lineal es par. Poniendo $$\phi(x)=\exists y<x\,(y+y=x),$$ vemos que $$M,u\nvDash\phi(a)\lor\neg\phi(a)$$ para el elemento $a:=2x\in M_u$ , siendo testigo de que el intuicionismo $Q^e$ no demuestra la $\Pi_2$ sentencia $$\forall x\,(\phi(x)\lor\neg\phi(x))$$ demostrable en cualquier teoría clásica. Bajo la definición restrictiva de $\Pi_2$ como se indica en la pregunta, se puede tomar la frase equivalente $$\forall x\,(\exists y<x\,(y+y=x)\lor\forall y<x\,(y+y<x\lor y+y>x))$$ en su lugar.

Más generalmente, si la extensión clásica de una teoría intuicionista $T\supseteq Q^e$ es $\Pi_2$ -Conservador sobre $T$ entonces $T$ debe demostrar $$\tag{$ * $}\forall x\,(\phi(x)\lor\neg\phi(x))$$ por cada $\Delta_0$ fórmula $\phi$ (ejercicio: las restricciones de la pregunta no tienen, en última instancia, ninguna importancia). Un argumento de más alto nivel para que esto no sea válido para $T=Q^e$ es que $Q^e$ está incluida en la teoría IPV de Cook y Urquhart (que, confusamente, es la versión intuicionista de $S^1_2$ en lugar de PV), por lo que por el teorema del testigo para IPV, no puede demostrar $(*)$ a menos que $\phi(x)$ define un predicado poliédrico (y la teoría lo demuestra). Dado que $\Delta_0$ fórmulas definen predicados arbitrarios en la jerarquía de tiempo lineal, esto no puede ocurrir para todos $\Delta_0$ fórmulas a menos que P = NP. El argumento se relativiza a las subteorías de las versiones intuicionistas de $S^i_2$ para cualquier $i$ utilizando la no colapso de PH como suposición en lugar de P $\ne$ NP.