“In 1950, while working at Los Alamos National Laboratory, the physicist Enrico Fermi had a casual conversation while walking to lunch with colleagues Emil Konopinski, Edward Teller and Herbert York.
“The men lightly discussed a recent spate of UFO reports and a cartoon facetiously blaming the disappearance of municipal trashcans on marauding aliens. They then had a more serious discussion regarding the chances of humans observing faster-than-light travel of some material object within the next ten years, which Teller put at one in a million, but Fermi put closer to one in ten.
“The conversation shifted to other subjects, until during lunch Fermi suddenly exclaimed, "Where are they?" (alternatively, "Where is everybody?"). One participant recollects that Fermi then made a series of rapid calculations using estimated figures (Fermi was known for his ability to make good estimates from first principles and minimal data). According to this account, he then concluded that Earth should have been visited long ago and many times over.”
From the excellent Wikipedia article on The Fermi Paradox which outlines most of the explanations anyone has been able to come up with. Read it by clicking here.
So here is my idea. We get an automatic theorem prover and seed it with formalised mini-theories of every conceivable type about possible alien capabilities and intentions. We add the additional proposition “we don’t see any aliens” and let the machine crank out the consequences.
What we’re looking for is a completely counter-intuitive proof which explains why they’re neither observed nor here, based on a set of premises no-one has thought of yet.
I reckon it could be done with a propositional calculus resolution theorem prover and some ‘knowledge-engineering’ to develop the mini-theories. A nice project for someone with some time and a lisp implementation.
