Busy beavers defeat Infinity
This simple fact is a striking revelation for me:
Basically, any decidable property of the natural numbers (a PI_1 formula) can be proved by a computer, by brute force. The program wouldn’t need to check all the numbers. If it runs longer than the busy beaver while looking for a counterexample, it will never find one.
This includes, by the way, proving consistency of formal systems: Con(F) is a PI_1 formula; we can write a program that checks each natural number for being the proof number for “1=0”.
UPDATE (6 years later):
they built an actual Turing machine that won’t halt only if ZF is consistent.
As a side benefit, machines that can prove Goldbach’s Conjecture and the Riemann Hypothesis by searching a _finite_ segment of N for counterexamples.
Chaitin’s “Computing the Busy Beaver Function” is now available at this URL:
or google for pdf containing the following: