En el tema de Información se habló de las preguntas más simples que permiten buscar un dato. Preguntas binarias, cuya respuesta sólo puede ser sí o no. Éste es el problema más simple que puede formularse: saber si algo ocurre o no, si es o no es, si es falso o verdadero. Y se explicó ahí que da lugar a la noción de bit. Un problema está definido por un conjunto de entradas, y para cada una, las salidas que deben ser producidas por un algoritmo que lo resuelve. A los problemas que tienen sólo dos salidas posibles se les llama problemas de decisión.
El matemático David Hilbert propuso el Entscheidungsproblem (problema de decidibilidad en alemán) en 1928. Éste consiste esencialmente en diseñar un algoritmo para resolver un problema de decisión en un sistema formal. De especial interés es el sistema formal de la aritmética. Es decir, diseñar un algoritmo que tome como entrada un enunciado matemático acerca de los números enteros, y conteste sí o no, según si el enunciado es verdadero o falso. Por ejemplo, la Conjetura de Goldbach dice "cualquier número entero par mayor a 2 puede ser escrito como la suma de dos números primos": 4 = 2 + 2, 6 = 3 + 3, 8 = 3 + 5, etc. Con la ayuda de computadoras se ha logrado verificar que el enunciado es cierto para números enormes, hasta de 17 cifras, pero aún no se ha podido responder si este enunciado es cierto o no en general. La pregunta de Hilbert se remonta a Leibniz, quien en el siglo XVII soñaba con diseñar tal algoritmo, al construir exitosamente una máquina mecánica de cálculo, que pudiera manipular símbolos para determinar si una frase en matemáticas es un teorema. Tanto los resultados de Turing que se han mencionado como simultáneamente los de Alonzo Church en 1936, de manera independiente, demostraron que no existe tal algoritmo.
La geometría plana que se vio en la sección anterior es otro ejemplo de un sistema formal, y ahí un enunciado podría ser, por ejemplo, que dados dos puntos por ellos pasa una y sólo una recta. En general, se puede definir un sistema formal mediante un conjunto de postulados que se asumen ciertos, llamados axiomas, y a partir de ellos se deducen nuevos enunciados verdaderos en el sistema: se les suele llamar teoremas; los axiomas junto con todos los teoremas que se pueden deducir a partir de ellos constituyen lo que se denomina un sistema formal. En términos generales el problema de decidibilidad consiste en lo siguiente: dados un conjunto de axiomas y una proposición, diseñar un algoritmo que responda si la proposición es verdadera o no en el sistema formal. O sea decidir si la proposición es o no un teorema del sistema formal.
Las máquinas de Turing son justamente una formalización de la noción de algoritmo, y el Teorema de Church-Turing (no confundir con la Tesis de Church-Turing) dice que existen proposiciones de aritmética que ninguna máquina de Turing puede decidir. No se puede saber si son verdaderas o no, mecánicamente. Existen sistemas en los que, en efecto, toda proposición es decidible, pero son más simples que la aritmética. Church y Turing demostraron que el Entscheidungsproblem en general no tiene solución.
