Primero, para aclarar algunos términos que pueden resultar confusos: "decidible" suele ser un término aplicado a conjuntos de fórmulas, y no a fórmulas individuales en sí. En este uso, significa que existe un algoritmo para decidir si una fórmula es miembro del conjunto. Sin embargo, hay otro uso -- típicamente más antiguo -- que asumiré que estás refiriéndote en esta pregunta. Según el uso más antiguo, decimos que $A$ es decidible en un sistema lógico $\mathcal{L}$ (aproximadamente, un conjunto de axiomas) si $A$ o su negación $\lnot A$ es demostrable en $\mathcal{L}$. Asumiré este uso por el resto de la respuesta.
Con este uso en mente para decidible, aún quedan dos ambigüedades en tu pregunta. Primero,
Ahora sé lo siguiente para esta declaración en particular:
(1) ¿Lo sabes en el sentido de que tienes una prueba, o simplemente suponemos que es verdadero? Y segundo,
Si $A$ es decidible, entonces $A$ es verdadero
(2) cuando dices "$A$ es decidible" -- ¿decidible en qué sistema lógico $\mathcal{L}$?
Dependiendo de las respuestas a (1) y (2), hay algunas cosas que podemos decir. Un resultado famoso es: si la respuesta a (2) es ZFC, y la respuesta a (1) es que no solo afirmas que esto es verdadero -- ¡tienes una prueba en ZFC! -- entonces podemos concluir en realidad a partir de tu declaración ("si $A$ es decidible, entonces $A$ es verdadero") que $A$ es verdadero en sí mismo. Esto es una consecuencia del teorema de Löb, que está estrechamente relacionado con el segundo teorema de incompletitud de Gödel. El teorema de Löb establece:
- Si hay una demostración de que " "$A$ es demostrable" implica $A$, entonces hay una prueba de $A$.
Para aplicarlo a tu caso: tu declaración es que si $A$ es decidible, entonces $A$ es verdadero. Se sigue que si $A$ es demostrable, entonces $A$ es verdadero (ya que la decidibilidad significa que o bien $A$ o $\lnot A$ es demostrable). Entonces lo que establece el teorema de Löb es que la única manera de saber tu declaración (en un sistema lógico fijo) es que $A$ mismo sea conocido.
