DECIDIBLE: 🔎

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)

TAUTOLOGÍA: 🔎

en sentido técnico, una fbf que toma el valor "verdadero" para todas las asignaciones de valores de verdad de sus componentes atómicos, (extendido en el caso de las lógicas polivalentes a: si toma un valor designado para todas las asignaciones de sus componentes atómicos). La prueba de corrección para el calculo de oraciones muestra que solo las tautologías son teoremas; la prueba de completud muestra que todas las tautologías son teoremas.
Intuitivamente una tautología es un enunciado que dice la misma cosa dos veces y, por tanto, es trivialmente verdadero. (Haack, 1978).