## Busy beavers defeat Infinity

This simple fact is a striking revelation for me:

http://en.wikipedia.org/wiki/Busy_beaver#Applications

http://www.umcs.maine.edu/~chaitin/bellcom.pdf

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.

UPDATE 2:

Chaitin’s “Computing the Busy Beaver Function” is now available at this URL:

https://www.cs.auckland.ac.nz/~chaitin/bellcom.pdf

or google for pdf containing the following:

[…] Systems that have enough knowledge about certain aquatic rodents are Π1-complete (no kidding). […]

Consistency and Soundness « Drawing Blanks03/09/2011 at 6:02 am