Drawing Blanks

Premature Optimization is a Prerequisite for Success

Busy beavers defeat Infinity

with one comment

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):

The 8000th Busy Beaver number eludes ZF set theory: new paper by Adam Yedidia and me

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:

Gregory J. Chaitin COMPUTING THE BUSY BEAVER FUNCTION
In T. M. Cover and B. Gopinath, Open Problems in Communication and Computation, Springer, 1987

 

 

 

 

Advertisements

Written by bbzippo

09/09/2010 at 2:01 am

Posted in math, programming

One Response

Subscribe to comments with RSS.

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


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

%d bloggers like this: