Que $F$ ser una fórmula válida de primer orden. Entonces el Skolemization $F$, vamos a denotar por $F_S$, es por lo menos satisfechas. Digamos que $F_S$ contiene función símbolos $f_i$ $1 \leq i \leq n$, $n\in\omega$. ¿Existe una fórmula $F$ tal que $F_S$ es cierto sólo cuando cada uno de los $f_i$ es interpretado por algunos función incomputables $\mathcal{M}^{f_i}$?
Respuestas
¿Demasiados anuncios?
BrianO
Puntos
8258
No se muy bien pero todavía no una respuesta a su pregunta acerca de la validez de las fórmulas, pero:
Esto es cierto de todos modos para que conste fórmulas, en los modelos de una teoría de la $\mathscr{T}$ tal como PA con "suficiente aritmética" para hablar acerca de la sintaxis, o, equivalentemente, máquinas de Turing. Comience con el Kleene T-predicado:
$T(e,x,y) \iff$ $e$ codifica una máquina de Turing $M$, $y$ es una terminación de cálculo de $M$ en la entrada de $x$.
T es aritmética (incluso primitiva recursiva). Una fórmula que representa la detención Problema, un completo semi-computable (r.e.) se establece, es: $$ K(e) \ffi \existe y \, T(e,0,y) \text{.} $$
El siguiente es un teorema: $$ \vdash \forall e \existe z\,((z = 1 \wedge K(e)) \vee (z = 0 \wedge \neg K(e)) \etiqueta{$S_1$} $$
En cualquier modelo de $\mathscr{T}$, cualquier función de Skolem $f(e)$ $z$ va a "resolver" la detención Problema y no es computable. Es Turing grado es $\mathbf{0'}$. Del mismo modo, mediante el uso de $K_n(e)$ en lugar de $K(e)$ donde $K_n(e)$ es una fórmula que representa un $\Sigma^0_n$-juego, una función de Skolem para la frase análoga tendrá grado $\mathbf{0^n}$.
La definición de $T$, y por lo tanto de $K$, utiliza sólo un número finito de axiomas $\mathscr{T_0}$$\mathscr{T}$, por lo que se podría formar la frase $\vdash \bigwedge \mathscr{T_0} \to S_1$. Entre los modelos no estándar de los modelos de $\mathscr{T}$ - es decir, no estándar de los modelos de PA; por un resultado de Tennenbaum, en tales modelos, incluso, $+$ $\times$ son no computables. Sin embargo, esta frase también tienen modelos que no son modelos de $\mathscr{T}$, debido a que no todos los casos de la inducción del esquema se encuentra en $\mathscr{T_0}$. En esos modelos, incluso podría no estar claro qué "computable".
Vatine
Puntos
8884
Creo que la respuesta a mi pregunta es no, no hay ningún tipo de fórmulas. La razón es algo trivial.
Si $F$ es una fórmula válida, entonces es también satisfecho en un modelo de $\mathcal{M} = (D, I)$ donde $|D| = 1$. Sólo hay una posible asignación de variable $v$ modelo: $v(x_i) = d$ donde $d$ es la única $d \in D$. Debido a esto, tanto en $\forall x \phi(x)$ $\exists x \phi(x)$ tienen el mismo valor de verdad (de acuerdo a $\mathcal{M}$) como se acaba de $\phi(x)$. Si asumimos w.l.o.g. que $F$ fue en el prefijo de forma normal, a continuación, $F$ sin cuantificadores es el mismo que $F_S$ sin cuantificadores, con la excepción de $F_S$ tener una cierta función de Skolem (sub)términos en lugar de variables. Sin embargo, cada término independientemente del contenido se interpreta como $d$, por lo que esta diferencia sintáctica no hace ninguna diferencia para la evaluación. Desde $\mathcal{M}\vDash F$, se deduce que el $\mathcal{M}\vDash F_S$. Todas las funciones son funciones de proyección, que son computables.
