Si no entendido mal lo que dice Carlos es que para todo sistema formal coherente y lo suficientemente potente para incluir la aritmética, siempre habrá afirmaciones sobre el sistema que el propio sistema no puede demostrar,
Eso es el primer teorema de incompletitud.
y luego pone como ejemplo que el sistema formal ZFC no puede demostrar de forma no trivial su propia consistencia.
Si ZFC es consistente, no puede probar su consistencia, ni de forma no trivial, ni de forma trivial. Eso es lo que dice el segundo teorema de incompletitud (aplicado a ZFC).
En otras palabras, el sistema ZFC no puede demostrar si la afirmación "el sistema ZFC es consistente" es cierta.
Si es consistente, no puede demostrarlo. Si es contradictorio, sí.
Luego, lo que yo pregunto es que, una afirmación como "el sistema ZFC es consistente", si bien el propio sistema no puede demostrar si es cierta de forma no trivial (sin usarla como axioma de una expansión del sistema),
Si añades un axioma a ZFC, lo que te sale ya no es ZFC, es otra teoría más fuerte. Si ZFC es consistente, entonces ZFC (sin más axiomas) no puede demostrar su consistencia ni trivial ni no trivialmente.
acaso no sería posible desarrollar otro sistema diferente que demostrara si es cierta de forma no trivial.
Claro que es posible. Por ejemplo, si a ZFC le añades como axioma que la medida de Lebesgue tiene una extensión a todos los subconjuntos de \( \mathbb R \), a partir de ahí puedes demostrar que ZFC es consistente, y la demostración no es trivial en absoluto, pero que no sea trivial no significa para nada que sea convincente. Nadie va a decir: Ah, vale, con este argumento ya podemos estar seguros de que ZFC es consistente. Perfectamente podría ocurrir que ZFC fuera contradictorio y que tal demostración no trivial fuera papel mojado.
Hay muchas demostraciones no triviales de la consistencia de ZFC, pero en extensiones de ZFC que son aún más sospechas que el propio ZFC de ser contradictorias, con lo que no aportan nada a la hora de saber si ZFC es consistente o no.
Lo que decía que es imposible es encontrar un argumento "convincente" de que ZFC es consistente, no en el sentido de que sea plausible admitir que lo es. Si a mí me ofrecieran una paga de \( 50\,000 \) euros al mes durante toda mi vida a cambio de que si, en algún momento, alguien encuentra una contradicción en ZFC reconocida como tal por la comunidad matemática, me cortarían la cabeza, yo aceptaría sin dudar. Pero eso es una cosa y otra muy distinta tener un argumento matemáticamente irrefutable de que ZFC no puede ser contradictorio. Eso no existe, porque cualquier argumento "convincente" se puede formalizar en ZFC. ZFC no pone trabas a cualquier argumento que emplee funciones arbitrarias, relaciones arbitrarias, ... lo que uno quiera. Es cierto que hay argumentos que no se pueden formalizar en ZFC, debido a que requieren hechos sobre clases propias que ZFC sólo puede probar sobre conjuntos, pero una demostración de ZFC que no sea formalizable en ZFC porque se base en el trato diferente que ZFC da a las clases propias frente a los conjuntos estaría suponiendo (aunque fuera informalmente) la consistencia de una teoría tan compleja o más que ZFC (de, hecho, estrictamente más compleja, por el segundo teorema de incompletitud), luego el argumento estaría dando por supuesto tácitamente lo que pretendería demostrar.
