Shared publicly  - 
"The first thing we'll do," said the man in black, "is help Hercules defeat the Hydra." 

You're bewildered.  How will a hard drive holding a huge countable infinity of kilobytes help a hero cut off all the heads of a monster?  "Huh?  What does

ε₀ = ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^..........

have to do with that?"

"Well, each time Hercules cuts off one of the Hydra's heads, it grows new heads.  But you may not know how the battle actually works.  Look carefully at this picture here.  In stage 1, Hercules cut off a head near the upper left.  After stage 1, the Hydra grows one new copy of the part above and including the branch directly below that head."


He rolls his eyes impatiently.  "Just look at the picture until you get it."

"Hmm.  Yes, I see one new V-shaped region there."

"In stage 2, Hercules cuts off another head.  After stage 2, the Hydra grows two new copies of the part above and including the branch directly below that head."

"Wow, that was a bad move!"

"In stage 3, Hercules cuts off another head.  After stage 3, the Hydra grows three new copies of the region part and including the branch directly below that head."

"Yikes!  That's a lot of new heads!"

"Right, it looks hopeless.  And it goes on like this.  But here's the cool part.  Using the ordinary rules of arithmetic - Peano arithmetic - it's impossible to prove that Hercules will always win this battle no matter what he does."

"What's so cool about that?   It doesn't seem very likely that he will win!"

"Ah, but using mathematical induction up to

ε₀ = ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^..........

we can prove that no matter which heads Hercules cuts off, he will always eventually cut off every head of the Hydra!  That's one reason we need this hard drive."

"Wow!"  You're impressed.  But then a bunch of questions come rushing into your mind.  "What's mathematical induction up to ε₀?  And what does it have to do with this Hydra battle?  How can assuming something about a big infinite ordinal let us prove more stuff about an ordinary finite math problem?  And what if induction up to ε₀ is false? "

"Questions, questions!   Read this Wikipedia article:

and this paper, where I got the picture:

• Laurie Kirby and Jeff Paris, Accessible independence results for Peano arithmetic, Bulletin of the London Mathematical Society 14 (1982), 285–293.

If you get stuck, ask for help."
John Baez's profile photoTerence Tao's profile photoToby Bartels's profile photoRomain Brasselet's profile photo
Each time they fire one department head, they hire a bunch more. 
But "eventually" all department heads are fired...
... although at some point in the mean time, they have as many as 3·2^402653211 − 1 department heads...
... and all throughout the process, there's just you at the bottom of the organization, doing all the work.
The number of new heads added at each stage is simply the number of the stage itself.  What if instead we added a computable function of the stage number?  For example, we could use the factorial of the stage:  On stage 3 we'd add 6 new heads, stage 4 we'd add 24, etc.

We'd still fire all the department heads.  Might take longer, though.
+Joe Marshall wrote: "The number of new heads added at each stage is simply the number of the stage itself."

Not really.  Maybe someone here can find a counterexample.
I should have said "The number of new copies of the region part and including the branch directly below that head added at each stage..."  
(Just cut an edge near the root, like in stage 2).  
Okay, good.  If the Hydra always grew n heads at stage n, it would never lose.  But sometimes it grows more, and eventually it grows fewer.  In this picture the net number of heads added at stage 2 is 3: one was cut off, but the Hydra grew four new ones.

So, everybody: is Joe's more substantial claim correct? 

"What if instead we added a computable function of the stage number?  For example, we could use the factorial of the stage:  On stage 3 we'd add 6 new heads, stage 4 we'd add 24, etc.

We'd still fire all the department heads."

This is a fun topic to discuss.
One can add any finite number of new copies with each removal of a head, and it will still terminate, by mimicking the standard proof (namely, to recursively assigning an ordinal to each node of a tree (by assigning each leaf node the ordinal 0, and assigning to all other nodes being the sum (in decreasing order) of omega raised to the ordinals of the children of that node), and observing that each time one cuts off the head of a hydra, the ordinal assigned to the root node is reduced.)
Right!  In particular, there's no need for the number of heads added on to be a computable function, but +Joe Marshall's claim was on the right track.
I want to say that there will always be more heads after Hercules chops one off (except maybe at the very first stage), since we add at least n heads after he chops off only 1.  But this breaks down if our head is right next to the root; then there's no place to attach the new heads!

So I can see how Hercules can win with proper strategy: cut off the highest heads first and work your way along; the thing may sprout a lot of new stuff along the way, but you're reducing the number of each head's siblings until it has none, and then chopping it off will clear that level there.  Once the level is entirely clear, the next level will be huge, but we can keep going.

To see why he'll always win eventually, even with poor strategy, is harder.
Well, that is another way to teach recursive algorithm.
How is Russell's paradox related to this, considering the set of sets method of construction of the ordinals?
I'm not sure what that question means.  This stuff is all about theorems and non-theorems of Peano arithmetic.
I was referring to the method of construction of the ordinals using sets. Each set is a union of what comes before, therefore it does not contain itself.

0 = {}
1 = {0}
2 = {0,1}

This reminded me Russell's paradox when it is stated in the set language;

"Does the set of all sets that do not contain themselves contain itself?"

I wondered if a similar paradox would emerge at the limit of the process you are demonstrating here.
Okay, now I get you.  In the ZFC framework, which I'm implicitly using in my set-theoretic discussions here, the 'set' of all ordinals is not a set; instead it's a proper class, usually called Ord. 

Ord is a bit like 'the largest ordinal'.  However, an ordinal is required to be a set, so Ord is not really an ordinal.  And that's good: otherwise we'd get hit with the Burali-Forti paradox:
Your hydra looks like the chart of p-adic numbers - no relation I'm sure, but it looks similar.  
Mathematically they're both structures of the type known as a 'tree', which is one of the few things in math that looks exactly like it sounds.
LOL  be impressed I remembered p-adics, ok?  I'm pondering how you guys can figure out the hydra quits growing new heads after you cut enough.  That's really impressive, to me.
I'm impressed, I just don't show it.

I'll explain this hydra puzzle a bit more tomorrow!  It's an amazing thing.
I have a very naive point, but to start understanding how Hercules will win the battle, without diving deep into mathematics, first observe that the length of the longest head can only decrease as time goes by (by length, I mean the number of segments from the root to the head). More and more heads may grow, but they are all short.

Also, if Hercules cuts a head of length 1 (i.e. directly attached to the root), no head grows.

Of course, there's a huge gap between these two observations, but, as far as I understand, they somehow provide a guide to understand what the proof will be about and what will eventually happen in this epic battle.
Yes, +Romain Brasselet, that's what it boils down to.  Thanks!   I shouldn't make it sound more mysterious than it is.  The proof is fundamentally not very hard.  However, it uses a principle of reasoning that goes beyond Peano arithmetic - namely, induction on the set of all trees.  Remember that ordinary mathematical induction is equivalent to the principle of infinite descent: a sequence of natural numbers that's strictly decreasing until it hits zero must indeed hit zero.  Here we have the same sort of thing going on with trees - that is, hydras.

The deep part is showing that this reasoning can't be formalized in Peano arithmetic.
Just to understand why the set of all hydras is ε₀ = ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^ω^..........

Each node may have any ordinal number of segments (away from the root). So,
the set of all hydras of length 1 is ω,
the set of all hydras of length 2 is ω^ω,
the set of all hydras of length n is ω^ω^...^ω (n times),
and, finally, the set of all hydras of length ω is ε₀.

This is highly reminiscent of the construction of your infinite library.
Oh, and I know this is pedestrian, but I don't mind walking...
+Romain Brasselet For any* fixed height of hydra, one can prove termination in PA; for instance, PA can prove that any hydra of height at most 57 will terminate in finite time, because it is capable of induction up to omega^...^omega (with 57 omegas).  (You already indicated how to do so for height 1.)  But the proofs are non-uniform in the height; the proof for height 58 is much longer and messier than the proof for height 57, and it turns out that PA is not capable of deducing the height n+1 case from the height n case in a "one-size-fits-all" fashion that works for arbitrary n, though it can handle any* fixed value of n such as 57.

* - Actually, if one wants to be truly pedantic, PA can prove termination for any fixed standard height n, but not necessarily for a nonstandard height.  But I recommend ignoring this subtlety until one becomes expert in these matters.
+Romain Brasselet wrote in part:

>the set of all hydras of length ω is ε₀.

But that's not what we have; we have the set of all hydras of finite height.  But instead let us argue that the set of all hydras of height at most n is ω↑↑n, or better yet that the set of all hydras of height less than n (where now height counts the number of nodes in the longest chain rather than number of edges) is ω↑↑n.  Then the set of all hydras is ω↑↑ω = ϵ₀.
Add a comment...