La (onu)decidability de Robinson-Aritmética-sin-la Multiplicación?

Question

Tomar nuestro viejo amigo Robinson Aritmética, y lo cortan a una teoría del sucesor y la adición.

Para explicarlo (sólo para asegurarse de que estamos cantando la misma partitura), tomar el primer orden de teoría de la con $\mathsf{0}$ como la única constante, y $\mathsf{S}$ $+$ como el construido en función de los signos, con los cinco axiomas

1. $\mathsf{\forall x\ 0 \neq Sx}$
2. $\mathsf{\forall x\forall y\ Sx = Sy \to x = y}$
3. $\mathsf{\forall x(x \neq 0 \to \exists y\ x = Sy)}$
4. $\mathsf{\forall x\ (x + 0) = x}$
5. $\mathsf{\forall x\forall y\ (x + Sy) = S(x + y)}$

y cuyo sistema deductivo es su favorito de la clásica lógica de primer orden con identidad.

Desde este corte hacia abajo la teoría no se representan las funciones recursivas, no se puede utilizar la prueba usual de la undecidability aritmética. Desde este corte hacia abajo de la teoría aún no sabe que la suma es conmutativa, es decir, no se puede demostrar $\mathsf{\forall x\forall y\ x = y = y + x}$, no se puede hacer el tipo de manipulaciones dentro de la teoría involucrada en un cuantificador de la eliminación de la prueba de decidability (cf. qué sucede cuando se agrega la inducción de esta teoría para obtener la aritmética de Presburger, es decir, la Aritmética de Peano menos de multiplicación).

Ermmmm .... así .... Drat, yo debería saber cómo probar que esta corte hacia abajo de la teoría es decidable o que es indecidible. Pero me parece que han olvidado, suponiendo que yo conocía, y la búsqueda de todo no me ayudó. OK gente, yo soy más de probabilidades de tener un alto momento aquí -- tan gentil! -- pero, ¿cómo podemos mostrar que la teoría (de la onu)decidable?

Answer 1

Considere el modelo $\mathfrak{M}$ con dominio de los números naturales $\mathbb{N}$ más un objeto, decir $a$. Definir $S$ $\mathbb{N}$ normalmente y $Sa=a$. Definir $+$ $\mathbb{N}$ normalmente y $x+a=a+x=a$ todos los $x \in \mathfrak{M}$.

Entonces es muy fácil probar que $\mathfrak{M}$ es un modelo de la $5$ axiomas en los que la declaración de $\varphi$, "existe una $x$ tal que $Sx=x$" es cierto.

Por lo $\varphi$ no puede ser decidido por los axiomas ya que en el modelo estándar es falso y verdadero, de modo que la teoría es indecidible.

Answer 2

Es indecidible.

Deje $\mathcal L$ ser el primer orden de idioma con la igualdad y un predicado binario $p({-},{-})$ y no constantes o símbolos de función. Llame a un $\mathcal L$-frase de la forma $\varphi\land \exists x\exists y(x\ne y)$ "de lujo" - es bien sabido que satisfiability de sentencias de lujo es indecidible.

Considere la siguiente traducción de $\mathcal L$ en el de su aditivo Robinson aritmética:

$$\overline{\varphi\land\psi} \equiv \overline\varphi\land\overline \psi \qquad \overline{\neg\varphi} \equiv \neg\overline\varphi$$ $$\overline{\exists x.\varphi} \equiv \exists x(x=\mathsf S x \land \overline\varphi) \qquad \overline{x=y} \equiv x=y$$ $$\overline{p(x,y)} \equiv x+y=x $$

Ahora claramente si $\varphi$ es una fantasía frase y $\overline{\varphi}$ es consistente con aditivo Robinson aritmética, a continuación, $\varphi$ es válido -- es trivial para obtener un modelo de la última a partir de un modelo de la antigua; el dominio serán los elementos que son sus propios sucesores.

Por otro lado, si $\varphi$ es un conste de lujo frase, entonces no hay un modelo de aditivo Robinson aritmética que satisface $\overline\varphi$, como sigue:

Deje $(A,p)$ ser un modelo de $\varphi$; sin pérdida de generalidad tome $A$ a ser disjunta de a $\mathbb N$. Debido a $\varphi$ es de lujo $A$ tiene al menos dos elementos, así que vamos a $f:A\to A$ ser tal que $f(a)\ne a$ todos los $a\in A$. Ahora, la construcción de un modelo de aditivo Robinson aritmética con el dominio $\mathbb N\cup A$, como sigue: $$ 0 = 0 $$ $$ \mathsf S n = (n+1) \qquad \mathsf Sa = a$$ $$ n\oplus n' = (n+n') \qquad\oplus n= n\oplus a = a \qquad un\oplus una' = \begin{cases} a & \text{when }p(a,a') \\ f(a) & \text{otherwise} \end{casos}$$