Can Monkeys Prove Every Theorem in Mathematics?

[Kevin_Axion]

Following from this classical idea that if there were a group of monkeys typing on type-writers for an infinite amount of time they can produce a work of Shakespeare; is it possible for these monkeys to derive every theorem in mathematics or axiomatic set theory? What does Godel's Incompleteness Theorem say about this?

 

[AlephZero]

What do you mean by "derive"?

In the shakespeare example, the monkeys don't "know" they have written the complete works of shakespeare, they are just typing a "random" string of characters.

Clearly you could ask questions like "how long would it take to type the complete works of N Bourbaki compared with the complete works of shakespeare" but that has nothing to do with the monkeys creating any new math. And if they did type a new math theorem or a new proof of an old theorem, they wouldn't know they had done it.

The number of true statements (a.k.a. theorems) in any branch of math that contains integer arithmetic is infinite, so they could never all be typed by a finite process (e.g. a finite number of monkeys typing at a constant speed)

FWIW a simulation of reconstructing the works of Shakespeare this way has recently been tried and is more than 99.99% complete, but experiemnts with real monkeys were not so successful. http://www.bbc.co.uk/news/technology-15060310

 

[DaveC426913]

Yes, remember, every genuine Shakespeare play they create is in a pool of a hundred thousand versions with but a single letter wrong, which is in a pool of a billion with just two letters wrong, which is in a pool of 10^15 versions with just three letters wrong, etc.

Note that there is nothing that distinguishes a bona fide script from an error-filled one. All you have is a stack of sequences of 100,000 letters of the alphabet in every possible permutation.Same with the axoims. For every one where every letter and symbol line up, there are countless that have other permutations of symbols. Standing on a pile of all possible permutations, you are not one iota closer to having a bona fide axoim than if you had no monkeys at all.

 

[micromass]

I think I know what you're getting at

Following from this classical idea that if there were a group of monkeys typing on type-writers for an infinite amount of time they can produce a work of Shakespeare; is it possible for these monkeys to derive every theorem in mathematics or axiomatic set theory?

Yes.

What does Godel's Incompleteness Theorem say about this?

Godels theorem states that there are statements in axiomatic set theory which are not provable nor disprovable. So even if the monkeys come up with the statement, they can never come up with the proof of the statement. Neither can they come up with a counterexample.

For example, the monkeys might come up with the continuum hypothesis: there is no cardinality strictly between |\mathbb{N}| and |\mathbb{R}|. But they will never be able to write down a proof for the statement. And they can never write down a counterexample.

So the thought experiment you mention is in contradiction with Godel.

 

[Deveno]

I think I know what you're getting at



Yes.



Godels theorem states that there are statements in axiomatic set theory which are not provable nor disprovable. So even if the monkeys come up with the statement, they can never come up with the proof of the statement. Neither can they come up with a counterexample.

For example, the monkeys might come up with the continuum hypothesis: there is no cardinality strictly between |\mathbb{N}| and |\mathbb{R}|. But they will never be able to write down a proof for the statement. And they can never write down a counterexample.

So the thought experiment you mention is in contradiction with Godel.

not strictly true. there is nothing to prevent said monkeys from randomly typing the axioms of a theory outside of set theory, and proving the continuum hypothesis in that theory. for example, they might randomly construct ZFC+CH, in which a proof of CH is trivial.

of course, it is just as likely the monkeys will randomly type the axioms of a theory equivalent to ZFC+(¬CH), and disprove the continuum hypothesis.

or both.

godel's theorem only applies to proofs within a given theory. it is suspiciously silent about using a meta-theory to prove the unproveable statements in a theory. and ZFC is not the be-all and end-all of mathematics, just a very popular theory. as clint eastwood once said: "a theory's got to know its limitations".

 

[phinds]

not strictly true. there is nothing to prevent said monkeys from randomly typing the axioms of a theory outside of set theory, and proving the continuum hypothesis in that theory. for example, they might randomly construct ZFC+CH, in which a proof of CH is trivial.

of course, it is just as likely the monkeys will randomly type the axioms of a theory equivalent to ZFC+(¬CH), and disprove the continuum hypothesis.

or both.

godel's theorem only applies to proofs within a given theory. it is suspiciously silent about using a meta-theory to prove the unproveable statements in a theory. and ZFC is not the be-all and end-all of mathematics, just a very popular theory. as clint eastwood once said: "a theory's got to know its limitations".

I don't think typing random character would ever PROVE anything other than the fact that if you give monkeys enough bananas you can get them to pound on keyboards.

 

[Deveno]

it is conceivable, is it not, that some random string of characters could be as cognent and as acceptable a proof as you or i, or any other human one might care to name?

of course, i consider it very unlikely, based on the results of simulations. even simple phrases that are recognizable seem to be very rare. but...gee, infinity is a tricky thing. there's only so many symbols mankind has created in its history, and although the possible permutations of that set is a very large number indeed, it is still finite. the number of atoms in the observable universe is also a large number, but it, too, is finite. it remains to be seen whether unknown constraints on the physical world limit exactly what may happen, and to what extent.

yes, the monkey thing is a bit absurd. a high-speed computer randomly generating strings of text is not, and people are doing this, just to see what happens. there's nothing particularly sacred about mathematical proofs when seen as strings of symbols. i believe some bright people have even created a random "theorem generator" which will, for a modest fee, generate your very own unique theorem (with proof), that you can name, and so forth.

 

[disregardthat]

If you don't like the notion of monekys doing mathematics by pounding on keyboards you shouldn't accept them writing either. Surely writing letters randomly could be recognized as a word just as much as writing symbols randomly could be recognized as a formula in ZFC. But there is no reason to allow the monkeys to write any axioms. Simply by typing random strings, some of which will be formulas, some sequence of which will be a deduction, you will have the monkeys eventually writing out proofs of theorems.

i believe some bright people have even created a random "theorem generator" which will, for a modest fee, generate your very own unique theorem (with proof), that you can name, and so forth.

That's even more absurd. And kind of funny.

 

[Jamma]

Following from this classical idea that if there were a group of monkeys typing on type-writers for an infinite amount of time they can produce a work of Shakespeare; is it possible for these monkeys to derive every theorem in mathematics or axiomatic set theory?

It is obviously possible for them to derive all theorems of maths that we have so far, or all maths that we will have in the year 10,000, etc. in the analogous way to the fact that with probability 1 they will write all of Shakespeare's work. But how would we separate the proofs from the gibberish? They haven't really derived anything, they've just so happened to write something that is correct.

Since all possible theorems is an infinite set, they won't be able to produce all mathematical theorems at any point.

What does Godel's Incompleteness Theorem say about this?

Nothing. This is a very simple question. All you are asking is: "if there is a mathematical theorem that can be stated in a finite string of words, then is it likely that a group of monkeys typing randomly will eventually write it?". Of course, the answer is that they will at some point write it with probability one. The fact that these are mathematical theorems has nothing to do with anything, we could have asked "would monkeys produce all philosophical ideas if given an infinite amount of time?". This should be obvious because the monkeys aren't knowingly writing about mathematics.

 

[DaveC426913]

of course, i consider it very unlikely, based on the results of simulations. even simple phrases that are recognizable seem to be very rare. but...gee, infinity is a tricky thing.

The point is they are not phrases with meaning. They are simply one in a series of permutations of all possible letters.

Let's say the simplest Shakespearean play is comprised entirely of this: 'me'.

The monkeys start typing, and we examine their results. In fact, we even take a moment to sort them:

a b c d e f g h i j k l ... x y z aa ab ac ad ad af ... nv nx ny nz ma mb mc md me mf ... zz

Hey look, they wrote one of Shakespeare's plays! Well, they also wrote > 26^2 incorrect plays.

How about an axiom?

a=1, a=2, a=3, a=4 ... y=1, z=1, aa=1, ab=1 ... zz=26

Which of theses is a meaningful axiom? It is up to you to pick. All combinations of letters are there, including all possible meaningless or incorrect axioms.

 

[micromass]

not strictly true. there is nothing to prevent said monkeys from randomly typing the axioms of a theory outside of set theory, and proving the continuum hypothesis in that theory. for example, they might randomly construct ZFC+CH, in which a proof of CH is trivial.

of course, it is just as likely the monkeys will randomly type the axioms of a theory equivalent to ZFC+(¬CH), and disprove the continuum hypothesis.

or both.

I hardly think that typing ZF+(CH) => (CH) counts as something. When I'm talking about a "proof" of CH, then I of course mean a proof within ZFC. As this is the framework in which the question of CH was originally posed.

Can we prove (CH) in a theory outside ZFC? Undoubtly yes. But I think it's clear I was not talking about that.

 

[lavinia]

ultimately the monkeys will write Godel's proof. I think this means that the unprovable theorem would be proved in a metasystem.

 

[disregardthat]

They won't write Godels proof as they are confined to the formulas of ZFC. They might write a Gödel sentence however...

 

[Jamma]

How do you propose a way that we can write down Godel's proof without it being possible for any random string of letters to contain it?

I was thinking this topic was more fitting in the philosophy thread, but even then...

 

[Stephen Tashi]

The most entertaining treatment of this topic that I have seen is the story "The Library Of Babel" by Jorge Luis Borges.

 

[Deveno]

they might write a proof by contradiction that monkeys cannot prove anything by typing randomly.