(The proof complexity theme song)

By Jan Johannsen and Antonina Kolokolova
(based on earlier work by Lennon et. al. [LM68])

You say you work on resolution
Well, you know, we all want a lower bound
You tell me you'd add substitution
Well, you know, first you gotta prove it sound

But if a random restriction doesn't preserve your proofs
All I can tell you is Brother you're going to lose

You say you can prove Pigeonhole
Well, you know, hard examples are hard to find
Though bounds for circuits play a role
Well, you know, this connection isn't well-defined

And with assumptions weaker than that "pigs can fly"
You'll have to wait for a proof by Ajtai

You talk of cut-elimination
Well, you know, not all systems are cut-free
You claim a smaller derivation
Well, you know, I have to ask for the degree

But if what you work on is arithmetical
Even you admit it's too theoretical

But if your work is based on Cook-Reckhow
You ain't gonna get tenure anywhere anyhow...


[LM68] J. Lennon and P. McCartney, "Revolution", The White Album, 1968