proofs.
Hm, Goedel's theorem is historically deeply like Pythagoras's
discovery of irrationals, even more so than I previously
realized.
Pythagoras's assumption that all numbers are rational, that
they can be represented in a certain, finite way, corresponds
neatly to Hilbert's tacit assumption that all true statements
are 'rationally' obtainable, that is, from a finitely
describable set of axioms. But there are countably many
rationals and countably many theorems, but uncountably many
reals and uncountably many models of PA...