Pregunta
Suponiendo que ZFC es consistente (un modelo), ¿existe un conjunto de $S$ y una relación binaria $\in_S$ $S$ que cumplir con los siguientes?
$S \subseteq \{0,1\}^*$ (esta es la estrella de Kleene, y, en particular, $S$ es contable);
$S$ es decidable, es decir, existe una máquina de Turing $C$ de manera tal que en la entrada de cualquier cadena binaria $x$, $C$ se detiene y acepta al $x \in S$ y se detiene y se rechaza en caso contrario;
$\in_S$ es decidable, es decir, existe una máquina de Turing $D$ de manera tal que en la entrada de cualquier par ordenado $(x,y) \in S \times S$, $D$ se detiene y acepta al $x \in_S y$, y se detiene y se rechaza en caso contrario;
$(S, \in_S)$ es un modelo de los axiomas de ZFC.
Detalles
Esencialmente, estoy interesada en saber si cada coherente de la teoría tiene una "computable" modelo en el anterior sentido. Por supuesto, es fácil ver que las teorías como DLOWE (denso lineal órdenes sin extremos) e incluso de primer orden de la Aritmética de Peano tienen tales modelos, simplemente deje $S$ el conjunto de los números racionales y los números enteros, respectivamente, codificado en binario en algunos canónica manera, y es un resultado estándar que $<, +, \cdots$, etc. son computables las operaciones. Así que pensé que ZFC podría ser un buen ejemplo más difícil de tratar -, pero no he sido capaz de argumentar la existencia de un modelo de la forma requerida.
Me hice esta pregunta a un amigo y se opusieron que tal vez cada contables, con cualquier operación binaria, que puede ser considerado computable en este sentido, después de todo, usted está autorizado a asignar los elementos de los contables conjunto de cadenas binarias en cualquier forma que te gusta. Sin embargo, esto no es cierto. Deje $S$ ser los vértices de un grafo dirigido que consiste de una sola dirigido ciclo para cada entero $n$, donde el ciclo tiene una longitud de busy beaver de $n$. Deje $\in_S$ ser la relación binaria correspondiente a este grafo dirigido. Luego he comprobado que $\in_S$ no es un decidable relación, no importa cómo asignar los vértices en $S$ a las cadenas. Así que es concebible que un contable modelo de la teoría de conjuntos es igualmente no computables.