Decidability

A logic system is decidabile if there is an algorithm that can determine whether a statement always follows from the system's axioms.

Hilbert's first concern was the completeness of mathematics: is there a way to prove all true propositions within a system of math? Hilbert's second question was about the consistency of mathematics: is there a way to prove that no contradictory statements arise in a system of math? Hilbert's third question was about decidability: is there an algorithm that can always determine whether a statement follows from the axioms?

And that leaves only the third and final big question from Hilbert: is math decidable? That is, is there an algorithm that can always determine whether a statement follows from the axioms? In 1936, Alan Turing found a way to settle this question, but to do it he had to invent the modern computer.

Last updated