Á défaut, Church, Herbrand, Gödel et Turing ont tenté chacun à leur manière de déterminer si un algorithme pouvait trancher qu'on peut démontrer ou pas une assertion mathématique. “L'Entscheidungsproblem”, le problème de la décision, qui a fait tanguer les maths et, au passage, posé les bases de l'informatique.