Reducir el número de géneros en la teoría formal.

Question

En Kleene "Introducción a la Metamathematics" de 1971 en las páginas 420 muestra que si tenemos un sistema formal, que por alguna fórmula $M(x)$ se puede demostrar la declaración de $\exists x M(x)$ a continuación, puede introducir un nuevo sistema formal con uno más, el tipo de variables y las correspondientes nuevos axiomas y axioma esquemas donde la nueva ordenación intuitivamente corresponde a los objetos para los que se $M(x)$ es válido. Entonces uno puede mostrar que esta nueva especie es eliminable en el sentido de que los nuevos obtenido formal del sistema es equivalente a la anterior porque no hay una efectiva (computable) el proceso de traducción de fórmulas y ciertos provability condiciones entre las fórmulas de los diferentes sistemas de retención.

Ahora, estoy interesado en el proceso inverso. Supongamos que tenemos algunos teoría formal que tiene más de un tipo de variables. Es posible reducir el número de clases tales que el sistema formal es, en cierto sentido, equivalente a la original? Traté de buscar en los libros y en el internet, pero no pudo encontrar instrucciones precisas acerca de esto. Por ejemplo, una idea que he encontrado es que, para cada tipo que quiere ser eliminado sólo puedo añadir un nuevo predicado que intuitivamente representa la declaración "este objeto es (era) de este tipo". Pero no estoy seguro de cómo hacer que precisa, especialmente en lo que sería la definición exacta del nuevo sistema formal equivalente a la original. Sé que quiero que el nuevo sistema sea de forma intuitiva, no más fuerte y no más débiles.

Por ejemplo, en Kleene del libro, cuando decide sobre la definición de la equivalencia se impone una de las condiciones a ser que si $E$ es la fórmula en el nuevo sistema de $S_2$ e $E'$ es la correspondiente traducción oficial de sistema de $S_1$ entonces $E \iff E'$ es comprobable en $S_2$. Pero no veo cómo eso puede funcionar en la situación actual debido a que considere la posibilidad de expresión que contiene el tipo que quiero eliminar. Entonces, es una fórmula en $S_1$ pero no es una fórmula en $S_2$ (debido a que no contienen ese tipo). Así, $E \iff E'$ puede ser expresado en $S_2$. Del mismo modo, si hay una fórmula que tiene un nuevo símbolo de predicado que expresa que una variable es un miembro de una especie utilizando la nueva definición de predicado, entonces este es expresable en $S_2$ pero no es expresable en $S_1$, lo $E \iff E'$ no puede ser expresado en $S_1$ así.

Espero hice mis intenciones claras y por favor, hágamelo saber lo que piensa sobre ello. Agradecería cualquier tipo de ayuda, consejos, referencias y así sucesivamente.

Answer 1

Considerar la categoría de la teoría como un ejemplo, y el sector informal de la frase "cada objeto tiene un morfismos que va desde el objeto a sí mismo".

En un dos-versión ordenada de la categoría de la teoría de ($S_2$), el uso del lenguaje $(\mathcal{M},\mathcal{O},R,s,t)$. Aquí:

• $\mathcal{M}$ e $\mathcal{O}$ son los tipos de objetos y morfismos
• $R$ es el ternario relación con la determinación de cuando una de morfismos es la composición de los otros dos
• $s$ e $t$ son las funciones de morfismos a los objetos de la identificación de su origen y de destino.

Así, en $S_2$ escribimos la frase original como $$(**) \ \ \forall x \in \mathcal{O}\ \exists y \in \mathcal{M}\ s(y)=x \mathbin\& t(y)=x$$

En una versión ordenada de la categoría de la teoría de ($S_1$), el uso del lenguaje $(\mathcal{C},M,O,R,S,T)$. Aquí

• $\mathcal{C}$ es el conjunto de la categoría, con ambos objetos y morfismos
• $M$ e $O$ son unarios las relaciones de la identificación de objetos y morfismos
• $R$ es el ternario relación con la determinación de cuando una de morfismos es la composición de los otros dos
• $S$ es una relación binaria cierto cuando el primer argumento es una de morfismos y el segundo argumento es el de su origen
• $T$ es una relación binaria cierto cuando el primer argumento es una de morfismos y el segundo argumento es su objetivo

Así, en $S_1$ escribimos la frase original como $$(*)\ \ \forall x(O(x) \implies \exists y\ M(y) \mathbin\& S(y,x) \mathbin\& T(y,x))$$

Desde $(*)$ e $(**)$ son oraciones en diferentes sistemas formales, nunca nos prueban directamente equivalente.

En su lugar, nos muestran que tenemos un mapeo $'$ tomando fórmulas en $S_1$ a las fórmulas en $S_2$, y una asignación de $^\wedge$ tomando fórmulas en $S_2$ a las fórmulas en $S_1$. Con esas asignaciones, $(*)'$ e $(**)$ son oraciones en $S_2$ cuales son equivalentes en $S_2$. Del mismo modo, $(**)^\wedge$ e $(*)$ son oraciones en $S_1$ cuales son equivalentes en $S_1$.

En general, se puede demostrar que para todas las fórmulas en los idiomas apropiados:

$$\vdash_1 E \iff (E')^\wedge$$ $$\vdash_2 \eta \iff (\eta^\wedge)'$$ $$E \vdash_1 F \text{ iff } E' \vdash_2 F'$$ $$\eta \vdash_2 \phi \text{ iff } \eta^\wedge \vdash_1 \phi^\wedge$$

Estas son las declaraciones de puro símbolo de la manipulación, donde se $'$ e $\wedge$ e $\vdash_1$ e $\vdash_2$ están todos definidos como manipulaciones de símbolos o sus aritmética equivalentes. Así que podemos probar estas afirmaciones, en la aritmética de Peano o cualquier otro conveniente teoría de metamathematics. Y con esto se establece la equivalencia de los dos sistemas.