Wikipedia, a Trap for the Curious Mind
I lost track of a couple of hours yesterday going down Wikipedia's bunny trail.
It all started innocently enough with a self emailed post on an implementation of Conway's game of life in html 5. Reading about the rules reminded me of Stephen Wolfram's a New Kind of Science, so I explored a related page on Glider Guns, then cellular automatons, then Turing Machines, unification with Lambda calculus, and finally landed on a page that has been a splinter in my mind for the past 16 hours.
The page describes David Hilbert's proposal of Entsheidungsproblem.
The Entscheidungsproblem asks for an algorithm that will take as input a description of a formal language and a mathematical statement in the language and produce as output either "True " or "False" according to whether the statement is true or false"
Without a means of proving equivalence, I questioned how far we could take any computational model.
"Hey, I have this answer but I can't tell you that it's right". Confidence in the truth of a solution is one of my instinctual tests of algorithm utility, otherwise it's just mental masturbation.
For more specific conditions equivalence can indeed be proven.
Some first - order theories are algorithmically decidable ; examples of this include Presburger arithmetic , real closed fields and static type systems of (most ) programming languages . The general first - order theory of the natural numbers expressed in Peano's axioms cannot be decided with such an algorithm , however.