Esto surgió en una pregunta en los foros de xkcd. ¿Es posible tener una metaprueba no constructiva, es decir, una prueba de que existe una prueba en algún sistema formal que no construye dicha prueba? ¿Hay algún ejemplo conocido, preferiblemente con algún sistema formal conocido como PA?
A la inversa, ¿es posible demostrar un metateorema que diga que cualquier metaprueba puede utilizarse para encontrar una prueba?
En teoría, la respuesta de David es correcta. Sin embargo, en la práctica es perfectamente posible demostrar la existencia de una prueba de forma no constructiva (como por ejemplo manipulando modelos y luego apelando al teorema de completitud) cuando nadie tiene ni idea de cómo encontrar realmente la prueba.
Un ejemplo que me viene a la mente es el teorema de Jacobson: si $R$ es un anillo tal que para cada $a\in R$ existe un número entero $n > 1$ tal que $a=a^n$ entonces $R$ es conmutativo. Por completitud de la lógica ecuacional, esto implica que para cualquier $n > 1$ existe una derivación ecuacional de $xy=yx$ a partir de los axiomas de los anillos y $x^n=x$ . Ya se ha encontrado dicha derivación para $n=3$ es un ejercicio no trivial; se conocen derivaciones explícitas para algunos $n$ pero no en general.
Si el sistema de pruebas es recursivamente axiomatizable, esta situación no puede darse.
Si existe una prueba de $\Theta$ existe un algoritmo para encontrar esa prueba. Es decir, busca en el conjunto recursivamente enumerable de deducciones hasta encontrar una prueba de $\Theta$ . Esto debe terminar, ya que hemos demostrado que $\Theta$ es demostrable.
Si el sistema de pruebas NO es recursivo, entonces esto puede ser posible. Considere el siguiente conjunto de axiomas $\Sigma$ en la firma de la aritmética. Sea $A$ sea un conjunto infinito que no contenga ningún conjunto infinito r.e. Definir $$ \Sigma = \{ (\bar k = \bar k) \wedge \sigma \mid k \in A, k > \ulcorner \sigma \urcorner, \mathfrak N \models \sigma \} $$
Ahora bien, nótese que cualquier sentencia demostrable en $Th(\cal N)$ es demostrable es en $\Sigma$ . Sin embargo, no existe ningún algoritmo para transformar producir tales pruebas a partir de $\Sigma$ . Para ello sería necesario enumerar elementos arbitrariamente grandes de $A$ , lo cual es imposible
¿Qué hay de los ejemplos de análisis no estándar? Por el principio de transferencia, dada una prueba de $\phi$ en el análisis no estándar, sabemos que existe una prueba de $\phi$ usando sólo técnicas estándar; pero en general no hay una forma agradable de extraer la prueba estándar de la prueba no estándar, y si recuerdo correctamente hay teoremas que tienen una prueba no estándar conocida sin una prueba estándar conocida. ¿Contará esto como una metaprueba no constructiva?
I-Ciencias es una comunidad de estudiantes y amantes de la ciencia en la que puedes resolver tus problemas y dudas.
Puedes consultar las preguntas de otros usuarios, hacer tus propias preguntas o resolver las de los demás.
