1º Dado un sistema formal completo lo suficientemente potente resulta imposible demostrar cualquier verdad sobre la aritmética.
Eso no es cierto. Existen sistemas formales completos capaces de demostrar cualquier verdad aritmética. Lo que dice el primer teorema de incompletitud es que un sistema aritmético, recursivo y consistente no puede demostrar todas las verdades aritméticas, donde "sistema aritmético" significa que puede demostrar algunos hechos aritméticos básicos (basta un fragmento débil de la aritmética de Peano), "recursivo" significa que existe un criterio para distinguir qué es un axioma y qué no, y "consistente" es que no permite demostrar contradicciones.
2º Un sistema formal lo suficientemente potente siempre se puede ampliar de forma que pueda demostrar una verdad concreta sobre la aritmética.
Eso tampoco lo dicen los teoremas de incompletitud. Lo más parecido a eso que es cierto es una obviedad: si tienes un sistema aritmético consistente y hay una verdad aritmética que no es demostrable ni refutable en él, siempre puedes añadirla como axioma, y así obtienes una extensión consistente en la que dicha verdad ya es demostrable.
Entonces, si logramos un sistema formal lo suficientemente potente capaz de demostrar todas las verdades aritméticas, entonces el sistema no puede demostrar si él mismo és o no consistente.
Si eso pretende ser un enunciado del segundo teorema de incompletitud, tampoco es eso. Lo que dice el segundo teorema de incompletitud es que si un sistema aritmético recursivo es consistente, entonces una de las verdades aritméticas que no puede demostrar es la que equivale a su propia consistencia.
Si planteas el caso de un sistema formal consistente capaz de demostrar todas las verdades aritméticas, entonces el primer teorema de incompletitud implica que no es recursivo, pero en tal caso no está claro cómo hay que entender lo de que no puede probar su propia consistencia, pues si el sistema no es recursivo no está claro que se pueda expresar en su lenguaje formal su propia consistencia.
Entiendo, pues, que una de las consecuencias de ambos teoremas es que dado un sistema formal lo suficientemente potente siempre pueden ampliar sus axiomas de manera que pueda demostrar nuevas verdades.
Eso es cierto, pero no tiene nada que ver con los teoremas de incompletitud. Simplemente, a cualquier teoría axiomática consistente le puedes añadir como axioma cualquier sentencia indecidible y así pasas a tener una extensión en la que dicha sentencia es (trivialmente) demostrable, pues es un axioma.
Ahora bien, aunque introduciendo nuevos axiomas al sistema el número de verdades demostrables crecerá nunca será posible lograr un sistema completo capaz de demostrar todas las verdades posibles sobre la aritmética. Siempre habrá verdades indemostrables para cualquier sistema formal ampliado que sea completo.
Eso no tiene sentido: un sistema completo es un sistema en el que cualquier afirmación es demostrable o refutable. Si dices que en una teoría hay verdades indemostrables (y supones que no hay falsedades demostrables), entonces es necesariamente incompleta, por definición.
Existen teorías aritméticas completas, sólo que no son recursivas. Basta tomar como axiomas las sentencias del lenguaje de la aritmética de Peano que son verdaderas en el modelo natural. Ahí tienes una teoría aritmética consistente y completa, es decir, capaz de demostrar cualquier verdad aritmética, sólo que no es recursiva.
Si esto es correcto, no entiendo lo que dice Chaitin. Pues entiendo que siempre es posible crear un sistema con un número determinado de axiomas que sea capaz de demostrar si una afirmación concreta sobre la aritmética es cierto o falsa. Lo que sí será imposible es encontrar un sistema formal para el cual toda afirmación aritmética sea decidible.
Si no pones en juego la recursividad, entonces no tiene nada de imposible que un sistema formal (consistente) pueda decidir cualquier afirmación aritmética, ("decidir" en el sentido de que toda afirmación aritmética sea demostrable o refutable en él), pero no será recursivo, por lo que en realidad no decidiría nada, ya que no sabríamos qué afirmaciones aritméticas son teoremas suyos y cuáles no.
Por tanto, cabe entender que cualquier afirmación sobre la aritmética ha de ser potencialmente decidible, no?
Depende de lo que entiendas por "decidible". Si una afirmación aritmética es verdadera, siempre existe una teoría aritmética recursiva en la cual es demostrable. Basta añadirla como axioma a los axiomas de Peano si no es deducible de ellos. Pero si te refieres a que de algún modo podamos saber si es verdadera o falsa, entonces ya no es cierto. La consistencia de ZFC se puede expresar mediante una sentencia aritmética, pero no es decidible en este segundo sentido: no tenemos forma de probar si es verdadera o falsa, salvo con pruebas obvias que consistan en tomarla como axioma, o que partan de algún axioma más fuerte aún que dicha consistencia y que, por consiguiente, tampoco podemos saber si es verdadero o falso.
Otra cosa es hallar los axiomas con los que demostrar esa afirmación concreta. Pero debería de ser posible hallarlos.
Sin más precisiones que las que planteas, eso es trivial. El axioma que permite demostrar una verdad aritmética es la propia verdad aritmética.
No acabo de entender qué es lo que dices que no entiendes de Chaitin. Conjeturaba que el UTF no sería demostrable (habría que precisar en qué teoría, supongo que pensaría en ZFC o equivalente) y ha resultado ser que no. Podría haber sido que sí, pero no. Hay muchas verdades aritméticas no demostrables en ZFC y el UTF podría haber sido una de ellas, pero ahora sabemos que no lo es.