La única manera de incorporar una fórmula independiente a las verdades del sistema es postulándola como axioma.
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).
Por otro lado, toda teoría que incluya aritmética básica no es decidible sintácticamente.
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.