Comment by btilly

This is a stack overflow question that I turned into a blog post.

It covers both the limits of what can be proven in the Peano Axioms, and how one would begin bootstrapping Lisp in the Peano Axioms. All of the bad jokes are in the second section.

Corrections and follow-up questions are welcome.