un sistema es decidible si hay un procedimiento mec谩nico ("un procedimiento de decisi贸n") para determinar, para cada fbf del sistema, si esa fbf es un teorema, [conjunto de las verdades del sistema], o no. Ejemplos: el c谩lculo de oraciones es decidible; todo el c谩lculo de predicados (incluyendo los predicados poli谩dicos as铆 como los mon谩dicos) no lo es. Las tablas de verdad proporcionan el procedimiento de decisi贸n para el c谩lculo de oraciones; una prueba de tablas de verdad determina si una fbf es una tautolog铆a, y, por los resultados de correcci贸n y completud, todas y solamente las tautolog铆as son teoremas.
(Haack, 1978).
Cuando una f贸rmula no puede ser probada verdadera ni falsa, se dice que la f贸rmula es independiente, y que por lo tanto el sistema es no decidible. La 煤nica manera de incorporar una f贸rmula independiente a las verdades del sistema es postul谩ndola como axioma. Dos ejemplos muy importantes de f贸rmulas independientes son el axioma de elecci贸n en la teor铆a de conjuntos, y el quinto postulado de la geometr铆a euclidiana.
Decidibilidad sint谩ctica
Un sistema formal es decidible sint谩cticamente si el conjunto de todas las f贸rmulas v谩lidas en el sistema es decidible. Es decir, existe un algoritmo tal que para cada f贸rmula del sistema es capaz de decidir en un n煤mero finito de pasos si la f贸rmula es v谩lida o no en el sistema.
La l贸gica de primer orden es sint谩cticamente decidible si se limita a predicados con un solo argumento (mon谩dica). Si se incluyen predicados con dos o m谩s argumentos, no es decidible.
Toda teor铆a completa y recursivamente enumerable es decidible sint谩cticamente. Por otro lado, toda teor铆a que incluya aritm茅tica b谩sica no es decidible sint谩cticamente.
Decidibilidad sem谩ntica
Un sistema formal es decidible sem谩nticamente si existe un m茅todo l贸gico y finito para evidenciar que el axioma, proposici贸n, f贸rmula etc. es un teorema.
(Wikipedia)