La equivalencia de distintas consistencia frases

Question

Tomar cualquier sistema formal $S$ que tiene una prueba del comprobador de programa e interpreta CT o PA$^-$. $ \def\imp{\Rightarrow} \def\con{\text{Con}} $

A continuación, los teoremas de incompletitud muestran que $S$ no demuestran $\con_1(S)$, donde el subíndice indica que se basa en una codificación particular de una determinada prueba verificador de $S$ en $S$. $S$ también no prueban $\con_2(S)$, por la otra, la elección de la prueba del comprobador y la codificación. Pero...

Qué $S$ siempre resultan $( \con_1(S) \imp \con_2(S) )$ (independientemente de las dos opciones)?

Creo que la respuesta es no, porque me parece necesario $S$ a apoyo de inducción para establecer ese tipo de prueba, es decir, me parece que necesite $S$ a interpretar ni PA o de CT+I (donde I es un esquema de inducción). Así que...

Si mi suposición es incorrecta, ¿cómo podemos mostrar que $S$ demuestra la equivalencia?

Si mi suposición es correcta, ¿cuáles son las dos opciones de $\con_1$ $\con_2$ que los testigos?

Answer 1

Esto es complicado. Es equivalente a la pregunta de si el estándar de Gödel frases para $S$ producido por dos diferentes codificaciones será seguramente equivalente en $S$.

Supongamos que definimos una sentencia de Gödel a un punto fijo de un "no-comprobable-en-$S$" predicado, a continuación, elija una de codificación que determina los detalles de la no-comprobable predicado. A continuación, los puntos fijos de este no-comprobable predicado será interderivable. Eso es elemental, bien conocido, y en muchos de los libros de texto.

Pero eso no ayuda con su pregunta, que viene: si hacemos variar el no-comprobable predicado por la variación de la codificación, se fija ponts como variar el predicado todavía estancia interderivable? Presumbably que habrá algunas restricciones en lo que cuenta como un método aceptable de codificación: pero yo no sé lo que las restricciones son. Ni la costumbre (o no tan habitual) los libros de texto nos dicen, de nuevo como lo que yo sé. Cual es la razón por la que me hicieron una pregunta similar en mathoverflow: la respuesta fue "no creo que hay ningún útil conocer criterios que se garanticen los comprobable equivalencia de dos a prueba de predicados que no iba a pedir la cuestión."

Yo también estaría encantada de saber si podemos hacer algo mejor que eso!