bang! bang!
he murdered math!
{the musical!}

In 1931, a lone man murdered math with two shots from a recursive revolver. The two incompleteness theorems punctured permanent holes in our once-pristine mathematical paradise.

To this day, landmines lie lurking in the logical landscape. Who will protect our precious computers from inconsistency itself? A $1,000,000 bounty awaits the hero who thwarts the ghost of gunslingin' Gödel!

The Frontier, The Wild West, The Maths Cathedral

Good neeeeews! Two duuuudes
proved one and one makes twoooo.
True before... but now it's truer.
And only took 'em 2^ 2^ 2^ 2 words to do'er.

Colt may have made men equal, but he didn't make them even.
Men are violent, God's gone silent, there's only numbers to believe in.

But lawless numbers plague the world in eighteen-eighty-two.
You can't corral your digits in tidy little groups.

Hyperbolic! Hypothetic! Railroads turn each day to minutes.
Meanwhile, mathematicians push that calculus past its limits.

The frontiers of math surpass wilderness and Indians.
Hell, when a song's gone this wrong, you know the sarsaparilla's gone non-Euclidean.

Folks sought the rules for truth; they prayed they could be tamed.
The laws of God awed us once, but now it ain't the same.

Cantor sets up set theory, others analyze analysis,
but all are bucked by infinite infinities and self-referential paralysis.

So Frege wrote the rules on quantification, inference,
and suddenly the wilderness is filled with mathematical logicians.

Logicians are a funny folk—they care about correctness.
Historically, men, Socrates, mortality... 'til mathematics wrecked it.

Russell rustles Frege's feathers with an impish little loop:
Sets that don't contain themselves—they're bound to come unglued.

If barbers only shave non-shavers, then who's there to split the hairs?
If a logician's dog barks at strangers, it can't bark when no one's there.

This rigmarole pro'lly needs more rigor.
We've got logic in our pocket and symbols on the trigger.

Among the swamps and crocs and paradox, Hilbert yearns for terra firma:
Formal systems, rules, and axioms—let's polish all those terms up.

So Hilbert puts a bounty on all truths pure and vast,
unwielding the wilderness with a cathedral to hold the maths.

Lewis/Clark had their shot, Whitehead/Russell take the reins.
Principia Mathematica, two brains, and open planes/plains.

They bet success on sets of sets; wrangle barbers using types.
This stuff as good as it gets, bright minds to make math right.

We got two duuuuudes
to find out what's tru--

Upon Sand

Bang! Bang! Two shots from a revolving revolver will solv'er.

Every human tongue can say everything and nothing,
so we invented maths to sort the two things from the one thing.
But if math's specific, it can't say arbitrary anythings.
If it's consistent, it insists on saying something.

Thus any formal system mixes symbols, truths, and inferences.
For instance, arithmetic is consistent
but skips soft descriptions
in pursuit of precision. Listen,

Alluring, elusive, but mutually exclusive—you cannot beat this.
Gödel found Faust in all formal systems: choose consistency or completeness.

Watch yo back, in the mirror, logicians fear them when they hear them.
Kurt Gödel's two completely insane incompleteness theorems.

Too dumb to utter "What a fun introduction!"
Here comes bullet one, straight from the gun, son:

For any consistent formal system that articulates arithmetic,
one can find the numbers to encode its truths inside it.

Turnin' a Gödel number into an arithmetic operation
makes statements about other equations to the system's dismay, son.

So if formal systems talk about their paradoxes,
just say "this statement's false" to puncture logical locked boxes.

Diagonally evade direct self-reference—who, me? Correction—
any math with mirrors makes infinite reflections.

All semantic systems that are syntactically prey to this
are incomplete unless they have something to say for it.

God's gone now; ain't nobody to pray for it from a cold, cramped confession booth.
Cathedrals cannot hold the whole of maths without holes in its roof. Bullet two:

Formal systems can't prove they're consistent.
Any proof that proves so would be a contradiction.

If a system is insistent that contradictions are non-existent,
then that's a false statement and the system's inconsistent.

Good ol' Gödel's eternal hurdles is turtles on turtles—
Kurt murdered math in the bathtub, makin' logicians' blood curdle.

He ripped a page from Principia and wiped his glasses,
scrawled small proofs on stall walls, hurtin' and hurlin' from the gas.
From cradle to casket, basket cases in every math class.
Take a seat, son—you missed your last chance to pass.

Hilbert got 99 problems, but a proof ain't one.
Don't die on that hill, burnin' Good Will Huntin' in the sun.

Theorem after theorem put down without fight in 'em.
Provably unprovable purgatory ad infinitum.

The City

Well, the Wild West bested the best of us. No foundations for our fodder.
So we'll settle down and build a town for our grandsons and granddaughters.

We'll prosper! Share the gospel! Share our wealth—our hunger too.
A city of cement and steel will rise up from these ruins.

Charles Babbage dreamed of machines that could conjure some thinkin',
but it took a lady's brain to think of machines that could do some dreamin'.

Lady Lovelace listened and heard music in those digits.
It ain't a crime to paint by number once or twice, or is it?

Ada envisioned men and women aided by such precision—
no work, no war, where machines handle heavy liftin'.

Letters leap from lightning wires sparked by dots and dashes.
Ditch your horse for Morse code, son, the telegraph's in fashion.

Fast forward to the Great War, where we create great calculators
capable of storing words for warding off invaders.

Cathedrals collapse under carpet artillery, but Alonzo Church still stands,
handing man the lambda calculus, an early kernel of computer programs.

Electric contraptions get the gears turning—here's Turing—
learning machines to keep Europe from burning.

Enemies telegraph this cryptic crap behind our backs,
but we've got magic, man! That cryptography is cracked.

With ample tape and patience, computations say the same things.
No oracles, no miracles, no ways to fake the baking.

Miraculous task, Turing tasted the forbidden fruit of computing,
and in that oracular orchard, he died by an apple of his own undoing.

With the Enigma egg unscrambled, nerds tilt that Axis backwards,
extract entropy into information, and protect our precious passwords.

Eyes open, no wool pulled, shorn from the lambdas.
Punchcards pulled from the looms! The mind no longer knows what the hand does.

Soon thereafter, transistors supplant fragile vacuum tubes,
growing faster, insisting that chips can shrink by factors of two.

Damn, those busy beavers can be a lot to top,
but the halting problem never told us when to stop.

Computers continue to secure and wreck our cities,
cracking codes, building bombs, crunching heat-seeking trajectories.

Wrestling the devil with the best intentions—
the road to hell is infested with null pointer exceptions.

Integrate circuits into chips without dip, microprocessors?
Little cities built from sand? You better lay off the sauce, sir.

Good news! Grace will guide two dudes to the moon.
Soon von Neumann CPUs will fit in nanometer grooves.

When Johnny Neumann was a boy, math was but a toy to him,
but now he's a man, a maniac with an ENIAC, and still a spoiled kid.

After patching paradoxes, he slapped the axioms on algebra,
and after cracking the quantum, von Neumann caught the computer bug.

He builds the bomb, tries life, defines what games are made of.
Meanwhile, he invents the architecture for processing information.

He found that by storing instructions and data together in memory,
each machine can emulate anything without much reprogramming.

But before von Neumann got on board the train to hell,
he received a little letter from that rascal Kurt Gödel.

The Landmine

If you try to build a metropolis, you know he'll topple it!

Since every possible program fits comfortably in countably infinite space,
place 'em in sorted order and give them numerical names.

You can imagine a program that can scan and plan faster than man can,
but can that program probe programs faster than proofs expand, man?

Consider this tricky bit: if such computers can exist and go quick,
they can query the answer key in the back of the book faster than a math whiz can pull out his abacus.

Time out! Halting problem need not be heeded,
if indeed we proceed with reasonable speed and quit when needed.

These decision problems could solve oddballs within practical limits,
if checking a problem and solving it stay in limited distance.

This letter discovered, decades later, folks would find
that Kurt Gödel defined the P ≠ NP landmine ahead of his time.

To be or not to be—to P or not to P—
can non-deterministic polynomial-time programs run efficiently?

P vs NP asks if a vast rift between questions and answers exists.
It seems like solving is harder than checking, but you'll need to check with your therapist.

P vs NP posits whether taking all forks in all roads leads to Rome
or whether you'd be better off staying at home.

P vs NP asks if you can run programs backwards efficiently,
or if doing so changes big O... no complexity.

P vs NP lays cement for cryptography—
without sufficient ciphers, it sucks to be a lock and key.

P vs NP sounds simple but kills countless careers,
the naughtiest of doggone problems gone unsolved for years.

To be extra obtuse, diagonal proofs are of no use—
up Crap Creek with half a paddle and a leaky canoe.

A million-dollar bounty is out for any person with proof.
The prize of the millennium awaits you, if you can manhandle that truth.

Meanwhile, Moore's law means more and more slop:
gigahertz in our shirts and teraflops in our socks.

Computers play chess while humans play checkers against pigeons—
even Lee Sedol gets creamed by algorithms younger than infants.

If computers continue to do this, then humans are useless.
The soothsayers cry doom, the theorem provers prove ruthless.

We mined land to build a city on a landmine?
Mind blown! No diamonds. It's bound to be a bad time.

The Horizon

Math's last answers may be unattainable.
Man's last match with machines might be unsustainable.
But such is life as flesh, blessed with the best questions,
and at least a seat at the table.